### Nuprl Lemma : differentiable-continuous

`∀I:Interval. ∀f,g:I ⟶ℝ.`
`  ((∀x,y:{x:ℝ| x ∈ I} .  ((x = y) `` (g[x] = g[y]))) `` d(f[x])/dx = λx.g[x] on I `` f[x] (proper)continuous for x ∈ I)`

Proof

Definitions occuring in Statement :  derivative: `d(f[x])/dx = λz.g[z] on I` proper-continuous: `f[x] (proper)continuous for x ∈ I` rfun: `I ⟶ℝ` i-member: `r ∈ I` interval: `Interval` req: `x = y` real: `ℝ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} `
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` so_lambda: `λ2x.t[x]` rfun: `I ⟶ℝ` so_apply: `x[s]` uall: `∀[x:A]. B[x]` prop: `ℙ` label: `...\$L... t` proper-continuous: `f[x] (proper)continuous for x ∈ I` nat_plus: `ℕ+` and: `P ∧ Q` subtype_rel: `A ⊆r B` uimplies: `b supposing a` subinterval: `I ⊆ J ` sq_stable: `SqStable(P)` squash: `↓T` r-ap: `f(x)` exists: `∃x:A. B[x]` sup: `sup(A) = b` rev_uimplies: `rev_uimplies(P;Q)` nat: `ℕ` le: `A ≤ B` rge: `x ≥ y` guard: `{T}` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` not: `¬A` rev_implies: `P `` Q` false: `False` uiff: `uiff(P;Q)` cand: `A c∧ B` subtract: `n - m` top: `Top` less_than': `less_than'(a;b)` true: `True` ge: `i ≥ j ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` upper-bound: `A ≤ b` derivative: `d(f[x])/dx = λz.g[z] on I` less_than: `a < b` sq_exists: `∃x:A [B[x]]` rleq: `x ≤ y` rnonneg: `rnonneg(x)` rneq: `x ≠ y` rdiv: `(x/y)` req_int_terms: `t1 ≡ t2` rless: `x < y` nequal: `a ≠ b ∈ T `
Lemmas referenced :  function-proper-continuous i-member_wf real_wf derivative_wf all_wf req_wf rfun_wf interval_wf i-approx-is-subinterval less_than_wf sup-range i-approx_wf icompact_wf rabs_wf subtype_rel_sets continuous-abs subtype_rel_dep_function subtype_rel_self set_wf proper-continuous-implies sq_stable__icompact sq_stable__iproper r-archimedean upper-bound_functionality rrange_wf int-to-real_wf upper-bound_wf nat_plus_wf iproper_wf decidable__lt false_wf not-lt-2 condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel rleq-int nat_properties nat_plus_properties sq_stable__and decidable__le full-omega-unsat intformnot_wf intformle_wf itermVar_wf itermAdd_wf itermConstant_wf int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_wf rset-member-rrange rmul_wf rsub_wf zero-rleq-rabs rleq_wf rleq_weakening_equal rleq_functionality rabs-rmul req_weakening rleq_functionality_wrt_implies rmul_functionality_wrt_rleq2 r-triangle-inequality less_than'_wf radd_wf rdiv_wf rless-int rless_wf equal_wf itermSubtract_wf req-iff-rsub-is-0 rinv_wf2 itermMultiply_wf rleq_weakening radd_functionality_wrt_rleq rmul_functionality rabs-difference-symmetry rabs_functionality req_transitivity radd_functionality rinv1 rmul-identity1 real_polynomial_null real_term_value_sub_lemma real_term_value_add_lemma real_term_value_var_lemma real_term_value_const_lemma real_term_value_mul_lemma req_inversion radd-int rmul-distrib2 rmin_wf mul_bounds_1b less-iff-le rmin_strict_ub rless-int-fractions2 mul_nat_plus intformless_wf int_formula_prop_less_lemma int_term_value_mul_lemma intformand_wf int_formula_prop_and_lemma rmin_ub rneq_functionality rmul-int rneq-int int_entire_a intformeq_wf int_formula_prop_eq_lemma equal-wf-base int_subtype_base equal-wf-T-base rdiv_functionality squash_wf true_wf iff_weakening_equal rmul-neq-zero rleq-implies-rleq rmul_preserves_rleq2 rleq_weakening_rless rmul-one rinv-of-rmul rmul-rinv rinv-as-rdiv
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality sqequalRule lambdaEquality applyEquality setElimination rename dependent_set_memberEquality hypothesis isectElimination setEquality independent_functionElimination because_Cache functionEquality natural_numberEquality productElimination independent_isectElimination imageMemberEquality baseClosed imageElimination dependent_pairFormation productEquality addEquality unionElimination independent_pairFormation voidElimination isect_memberEquality voidEquality intEquality minusEquality approximateComputation int_eqEquality inlFormation equalityTransitivity equalitySymmetry independent_pairEquality axiomEquality inrFormation dependent_set_memberFormation multiplyEquality baseApply closedConclusion universeEquality

Latex:
\mforall{}I:Interval.  \mforall{}f,g:I  {}\mrightarrow{}\mBbbR{}.
((\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (g[x]  =  g[y])))
{}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.g[x]  on  I
{}\mRightarrow{}  f[x]  (proper)continuous  for  x  \mmember{}  I)

Date html generated: 2018_05_22-PM-02_44_44
Last ObjectModification: 2017_10_21-PM-07_20_16

Theory : reals

Home Index