Nuprl Lemma : derivative-rinv

`∀I:Interval. ∀f,g:I ⟶ℝ.`
`  ((∀x,y:{t:ℝ| t ∈ I} .  ((x = y) `` (g[x] = g[y])))`
`  `` f[x]≠r0 for x ∈ I`
`  `` d(f[x])/dx = λx.g[x] on I`
`  `` d((r1/f[x]))/dx = λx.(-(g[x])/f[x] * f[x]) on I)`

Proof

Definitions occuring in Statement :  derivative: `d(f[x])/dx = λz.g[z] on I` nonzero-on: `f[x]≠r0 for x ∈ I` rfun: `I ⟶ℝ` i-member: `r ∈ I` interval: `Interval` rdiv: `(x/y)` req: `x = y` rmul: `a * b` rminus: `-(x)` int-to-real: `r(n)` real: `ℝ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} ` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` derivative: `d(f[x])/dx = λz.g[z] on I` member: `t ∈ T` nat_plus: `ℕ+` uall: `∀[x:A]. B[x]` nonzero-on: `f[x]≠r0 for x ∈ I` and: `P ∧ Q` prop: `ℙ` subtype_rel: `A ⊆r B` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` rfun: `I ⟶ℝ` so_apply: `x[s]` sq_stable: `SqStable(P)` squash: `↓T` subinterval: `I ⊆ J ` rneq: `x ≠ y` label: `...\$L... t` guard: `{T}` exists: `∃x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` top: `Top` cand: `A c∧ B` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)` rge: `x ≥ y` less_than: `a < b` less_than': `less_than'(a;b)` true: `True` sq_exists: `∃x:A [B[x]]` continuous: `f[x] continuous for x ∈ I` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` rless: `x < y` int_nzero: `ℤ-o` nequal: `a ≠ b ∈ T ` sq_type: `SQType(T)` req_int_terms: `t1 ≡ t2` rdiv: `(x/y)`
Lemmas referenced :  i-approx-is-subinterval istype-less_than nonzero-on-implies icompact_wf i-approx_wf continuous-implies-functional rfun_subtype proper-continuous-implies differentiable-continuous sq_stable__icompact sq_stable__iproper function-is-continuous rdiv_wf int-to-real_wf subtype_rel_sets_simple real_wf i-member_wf sq_stable__i-member req_wf i-member-approx iproper_wf nat_plus_wf derivative_wf nonzero-on_wf rfun_wf interval_wf req_weakening rdiv_functionality Inorm-bound Inorm_wf rleq_wf rabs_wf imax_wf r-bound_wf imax_nat_plus nat_plus_properties decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf intformeq_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_wf rmax_wf rmax_ub rleq_functionality req_inversion rmax-int r-bound-property rleq_functionality_wrt_implies rleq_weakening_equal mul_nat_plus i-approx-approx rmin_wf rsub_wf rless_wf rmul_wf rminus_wf rless-int rmin_strict_ub rmin-rleq implies_weakening_uimplies rneq-int int_entire_a mul_nzero subtype_base_sq int_subtype_base nequal_wf rneq_wf rmul_reverses_rless rmul_preserves_rless squash_wf true_wf rabs-rminus subtype_rel_self iff_weakening_equal itermSubtract_wf itermMultiply_wf radd_wf rinv_wf2 itermMinus_wf itermAdd_wf rless_functionality req-iff-rsub-is-0 real_polynomial_null real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_const_lemma real_term_value_var_lemma uiff_transitivity req_functionality rmul_functionality rabs-rmul req_transitivity rabs_functionality rminus_functionality rsub_functionality rinv-of-rmul radd_functionality rinv-mul-as-rdiv rinv-as-rdiv rmul-rinv3 rmul-rinv real_term_value_minus_lemma real_term_value_add_lemma rmul-nonneg-case1 zero-rleq-rabs rmul_functionality_wrt_rleq2 rleq-int decidable__le intformle_wf int_formula_prop_le_lemma rmul_preserves_rleq2 rmul-identity1 rmul-int uimplies_transitivity rleq_transitivity r-triangle-inequality rleq_weakening multiply_nat_plus int_term_value_mul_lemma radd_functionality_wrt_rleq rabs-difference-symmetry rabs-rmul-rleq rleq-int-fractions rmul-int-rdiv mul_bounds_1a nat_plus_subtype_nat rneq_functionality set_subtype_base less_than_wf rinv_functionality2 rmul_preserves_rleq square-nonzero
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin because_Cache dependent_set_memberEquality_alt setElimination rename hypothesisEquality hypothesis isectElimination natural_numberEquality independent_functionElimination productElimination universeIsType applyEquality independent_isectElimination sqequalRule lambdaEquality_alt imageMemberEquality baseClosed imageElimination closedConclusion setIsType promote_hyp inhabitedIsType productIsType functionIsType dependent_pairFormation_alt equalityTransitivity equalitySymmetry isectIsType applyLambdaEquality unionElimination approximateComputation int_eqEquality isect_memberEquality_alt voidElimination independent_pairFormation equalityIsType1 inlFormation_alt inrFormation_alt dependent_set_memberFormation_alt multiplyEquality instantiate cumulativity intEquality equalityIsType4 universeEquality baseApply

Latex:
\mforall{}I:Interval.  \mforall{}f,g:I  {}\mrightarrow{}\mBbbR{}.
((\mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (g[x]  =  g[y])))
{}\mRightarrow{}  f[x]\mneq{}r0  for  x  \mmember{}  I
{}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.g[x]  on  I
{}\mRightarrow{}  d((r1/f[x]))/dx  =  \mlambda{}x.(-(g[x])/f[x]  *  f[x])  on  I)

Date html generated: 2019_10_30-AM-09_02_57
Last ObjectModification: 2018_11_12-AM-11_59_54

Theory : reals

Home Index