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: P ⇒ Q,  set: {x:A| B[x]} ,  natural_number: $n
Definitions unfolded in proof :  all: ∀x:A. B[x],  implies: P ⇒ Q,  decreasing-on-interval: f[x] decreasing for x ∈ I,  member: t ∈ T,  iff: P ⇐⇒ Q,  and: P ∧ Q,  rev_implies: P ⇐ Q,  cand: A 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: b 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 ⊆r B,  i-member: r ∈ I,  subinterval: I ⊆ J ,  rsub: x - 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