Nuprl Lemma : derivative-implies-decreasing

I:Interval
  (iproper(I)
   (∀f,f':I ⟶ℝ.
        (d(f[x])/dx = λx.f'[x] on I
         f'[x] continuous for x ∈ I
         (∀x:{x:ℝx ∈ I} (f'[x] ≤ r0))
         f[x] decreasing for x ∈ I)))


Proof




Definitions occuring in Statement :  decreasing-on-interval: f[x] decreasing for x ∈ I derivative: d(f[x])/dx = λz.g[z] on I continuous: f[x] continuous for x ∈ I rfun: I ⟶ℝ i-member: r ∈ I iproper: iproper(I) interval: Interval rleq: x ≤ y int-to-real: r(n) real: so_apply: x[s] all: x:A. B[x] implies:  Q set: {x:A| B[x]}  natural_number: $n
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q decreasing-on-interval: f[x] decreasing for x ∈ I member: t ∈ T iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q cand: c∧ B sq_stable: SqStable(P) squash: T prop: uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s] rfun: I ⟶ℝ label: ...$L... t guard: {T} uiff: uiff(P;Q) uimplies: supposing a exists: x:A. B[x] continuous: f[x] continuous for x ∈ I i-approx: i-approx(I;n) rccint: [l, u] nat_plus: + less_than: a < b less_than': less_than'(a;b) true: True sq_exists: x:{A| B[x]} rneq: x ≠ y or: P ∨ Q rless: x < y decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) false: False not: ¬A top: Top rleq: x ≤ y rnonneg: rnonneg(x) le: A ≤ B subtype_rel: A ⊆B i-member: r ∈ I subinterval: I ⊆  rsub: y real: rev_uimplies: rev_uimplies(P;Q) rge: x ≥ y
Lemmas referenced :  rcc-subinterval sq_stable__i-member rleq_wf continuous_functionality_wrt_subinterval rccint_wf set_wf real_wf i-member_wf all_wf int-to-real_wf continuous_wf derivative_wf rfun_wf iproper_wf interval_wf differentiable-continuous req_wf continuous-implies-functional proper-continuous-is-continuous rleq-iff-all-rless small-reciprocal-real rless_wf less_than_wf rccint-icompact icompact_wf sq_stable__and i-approx_wf rabs_wf rsub_wf rdiv_wf rless-int nat_plus_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf sq_stable__rless sq_stable__all sq_stable__rleq less_than'_wf nat_plus_wf squash_wf member_rccint_lemma rleq_weakening_equal rless-cases radd_wf trivial-rless-radd mean-value-theorem rfun_subtype derivative_functionality_wrt_subinterval not-rless radd-preserves-rless rminus_wf rless_functionality radd-zero-both req_weakening radd-rminus-assoc radd_comm radd_functionality rmul_preserves_rless equal_wf rmul_wf rmul-one-both rmul-zero-both rmul_functionality radd-int req_transitivity rminus-as-rmul req_inversion rmul-identity1 rmul-distrib2 rmul-rdiv-cancel2 rmul-int rmul_comm rmul_preserves_rleq2 rleq_weakening_rless uiff_transitivity rleq_functionality rabs-of-nonneg radd-preserves-rleq rless_transitivity2 rminus_functionality rleq_functionality_wrt_implies radd_functionality_wrt_rleq rless_transitivity1 rless_irreflexivity radd-assoc rabs-difference-bound-rleq radd-ac trivial-rleq-radd radd-rminus-both
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality setElimination rename hypothesis productElimination independent_functionElimination sqequalRule imageMemberEquality baseClosed imageElimination independent_pairFormation isectElimination because_Cache lambdaEquality setEquality applyEquality dependent_set_memberEquality natural_numberEquality independent_isectElimination isect_memberEquality functionEquality inrFormation unionElimination dependent_pairFormation int_eqEquality intEquality voidElimination voidEquality computeAll independent_pairEquality minusEquality axiomEquality equalityTransitivity equalitySymmetry promote_hyp addLevel levelHypothesis productEquality multiplyEquality addEquality isect_memberFormation

Latex:
\mforall{}I:Interval
    (iproper(I)
    {}\mRightarrow{}  (\mforall{}f,f':I  {}\mrightarrow{}\mBbbR{}.
                (d(f[x])/dx  =  \mlambda{}x.f'[x]  on  I
                {}\mRightarrow{}  f'[x]  continuous  for  x  \mmember{}  I
                {}\mRightarrow{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (f'[x]  \mleq{}  r0))
                {}\mRightarrow{}  f[x]  decreasing  for  x  \mmember{}  I)))



Date html generated: 2017_10_03-PM-00_28_14
Last ObjectModification: 2017_07_28-AM-08_42_26

Theory : reals


Home Index