### Nuprl Lemma : Rolles-theorem

`∀a,b:ℝ.`
`  ((a < b)`
`  `` (∀f,f':[a, b] ⟶ℝ.`
`        (f'[x] continuous for x ∈ [a, b]`
`        `` d(f[x])/dx = λx.f'[x] on [a, b]`
`        `` (f[a] = f[b])`
`        `` (∀e:ℝ. ((r0 < e) `` (∃x:ℝ. ((x ∈ [a, b]) ∧ (|f'[x]| ≤ e))))))))`

Proof

Definitions occuring in Statement :  derivative: `d(f[x])/dx = λz.g[z] on I` continuous: `f[x] continuous for x ∈ I` rfun: `I ⟶ℝ` rccint: `[l, u]` i-member: `r ∈ I` rleq: `x ≤ y` rless: `x < y` rabs: `|x|` req: `x = y` int-to-real: `r(n)` real: `ℝ` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` rfun: `I ⟶ℝ` so_apply: `x[s]` prop: `ℙ` top: `Top` and: `P ∧ Q` cand: `A c∧ B` uimplies: `b supposing a` guard: `{T}` label: `...\$L... t` iff: `P `⇐⇒` Q` not: `¬A` exists: `∃x:A. B[x]` inf: `inf(A) = b` lower-bound: `lower-bound(A;b)` rrange: `f[x](x∈I)` rset-member: `x ∈ A` i-member: `r ∈ I` rccint: `[l, u]` nat_plus: `ℕ+` rneq: `x ≠ y` or: `P ∨ Q` rev_implies: `P `` Q` rless: `x < y` sq_exists: `∃x:{A| B[x]}` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` derivative: `d(f[x])/dx = λz.g[z] on I` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` i-approx: `i-approx(I;n)` iproper: `iproper(I)` int_upper: `{i...}` subtype_rel: `A ⊆r B` real: `ℝ` sq_stable: `SqStable(P)` int_seg: `{i..j-}` uiff: `uiff(P;Q)` lelt: `i ≤ j < k` subtract: `n - m` le: `A ≤ B` rev_uimplies: `rev_uimplies(P;Q)` itermConstant: `"const"` req_int_terms: `t1 ≡ t2` real_term_value: `real_term_value(f;t)` int_term_ind: int_term_ind itermSubtract: `left (-) right` itermVar: `vvar` pointwise-req: `x[k] = y[k] for k ∈ [n,m]` pointwise-rleq: `x[k] ≤ y[k] for k ∈ [n,m]` rleq: `x ≤ y` rnonneg: `rnonneg(x)` rge: `x ≥ y` rsub: `x - y` rdiv: `(x/y)`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis sqequalRule lambdaEquality applyEquality setElimination rename dependent_set_memberEquality setEquality independent_functionElimination natural_numberEquality because_Cache dependent_functionElimination isect_memberEquality voidElimination voidEquality independent_isectElimination independent_pairFormation productEquality productElimination dependent_pairFormation inrFormation unionElimination int_eqEquality intEquality computeAll functionEquality imageMemberEquality baseClosed addEquality imageElimination functionExtensionality addLevel hyp_replacement equalitySymmetry equalityTransitivity applyLambdaEquality levelHypothesis multiplyEquality minusEquality independent_pairEquality axiomEquality universeEquality inlFormation isect_memberFormation orFunctionality promote_hyp comment orLevelFunctionality

Latex:
\mforall{}a,b:\mBbbR{}.
((a  <  b)
{}\mRightarrow{}  (\mforall{}f,f':[a,  b]  {}\mrightarrow{}\mBbbR{}.
(f'[x]  continuous  for  x  \mmember{}  [a,  b]
{}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  [a,  b]
{}\mRightarrow{}  (f[a]  =  f[b])
{}\mRightarrow{}  (\mforall{}e:\mBbbR{}.  ((r0  <  e)  {}\mRightarrow{}  (\mexists{}x:\mBbbR{}.  ((x  \mmember{}  [a,  b])  \mwedge{}  (|f'[x]|  \mleq{}  e))))))))

Date html generated: 2017_10_03-PM-00_20_46
Last ObjectModification: 2017_07_28-AM-08_39_54

Theory : reals

Home Index