Nuprl Lemma : IVT-deriv-seq-test

∀a:ℝ. ∀b:{b:ℝ| a < b} . ∀f:[a, b] ⟶ℝ.
  ∀c:ℝ
    ((f(a) ≤ c)
    ⇒ (c ≤ f(b))
    ⇒ (∀u,v:{v:ℝ| v ∈ [a, b]} .
          ((u < v)
          ⇒ (∃k:ℕ
               ∃F:ℕk + 1 ⟶ [a, b] ⟶ℝ
                (finite-deriv-seq([a, b];k;i,x.F[i;x])
                ∧ (∀x:{x:ℝ| x ∈ [a, b]} . (F[0;x] = (f(x) - c)))
                ∧ (∃z:{z:ℝ| z ∈ [u, v]} . (r0 < Σ{|F[i;z]| | 0≤i≤k}))))))
    ⇒ (∃x:ℝ [((x ∈ [a, b]) ∧ (f(x) = c))])) 
  supposing ∀x,y:{x:ℝ| x ∈ [a, b]} .  ((x = y) ⇒ (f[x] = f[y]))


Proof



Definitions occuring in Statement :  finite-deriv-seq: finite-deriv-seq(I;k;i,x.F[i; x]),  r-ap: f(x),  rfun: I ⟶ℝ,  rccint: [l, u],  i-member: r ∈ I,  rsum: Σ{x[k] | n≤k≤m},  rleq: x ≤ y,  rless: x < y,  rabs: |x|,  rsub: x - y,  req: x = y,  int-to-real: r(n),  real: ℝ,  int_seg: {i..j-},  nat: ℕ,  uimplies: b supposing a,  so_apply: x[s1;s2],  so_apply: x[s],  all: ∀x:A. B[x],  sq_exists: ∃x:A [B[x]],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q,  set: {x:A| B[x]} ,  function: x:A ⟶ B[x],  add: n + m,  natural_number: $n
Definitions unfolded in proof :  all: ∀x:A. B[x],  uimplies: b supposing a,  member: t ∈ T,  implies: P ⇒ Q,  uall: ∀[x:A]. B[x],  so_apply: x[s],  rfun: I ⟶ℝ,  prop: ℙ,  exists: ∃x:A. B[x],  nat: ℕ,  and: P ∧ Q,  so_lambda: λ2x y.t[x; y],  label: ...$L... t,  so_apply: x[s1;s2],  subtype_rel: A ⊆r B,  int_seg: {i..j-},  rless: x < y,  sq_exists: ∃x:A [B[x]],  nat_plus: ℕ+,  ge: i ≥ j ,  lelt: i ≤ j < k,  decidable: Dec(P),  or: P ∨ Q,  not: ¬A,  satisfiable_int_formula: satisfiable_int_formula(fmla),  top: Top,  false: False,  i-member: r ∈ I,  rccint: [l, u],  sq_stable: SqStable(P),  squash: ↓T,  so_lambda: λ2x.t[x],  cand: A c∧ B,  guard: {T}
Lemmas referenced :  req_witness,  IVT-locally-non-constant,  locally-non-constant-deriv-seq-test,  i-member_wf,  rccint_wf,  rless_wf,  istype-nat,  int_seg_wf,  finite-deriv-seq_wf,  subtype_rel_self,  real_wf,  req_wf,  nat_properties,  nat_plus_properties,  decidable__le,  full-omega-unsat,  intformnot_wf,  intformle_wf,  itermConstant_wf,  istype-int,  int_formula_prop_not_lemma,  istype-void,  int_formula_prop_le_lemma,  int_term_value_constant_lemma,  int_formula_prop_wf,  decidable__lt,  intformand_wf,  intformless_wf,  itermAdd_wf,  itermVar_wf,  int_formula_prop_and_lemma,  int_formula_prop_less_lemma,  int_term_value_add_lemma,  int_term_value_var_lemma,  istype-le,  istype-less_than,  rsub_wf,  r-ap_wf,  member_rccint_lemma,  sq_stable__rleq,  int-to-real_wf,  rsum_wf,  rabs_wf,  rleq_transitivity,  rleq_wf,  rleq_weakening_rless,  rleq_weakening_equal,  rfun_wf
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  lambdaFormation_alt,  isect_memberFormation_alt,  cut,  introduction,  sqequalRule,  sqequalHypSubstitution,  lambdaEquality_alt,  dependent_functionElimination,  thin,  hypothesisEquality,  extract_by_obid,  isectElimination,  applyEquality,  because_Cache,  independent_functionElimination,  hypothesis,  functionIsTypeImplies,  inhabitedIsType,  rename,  independent_isectElimination,  functionIsType,  setIsType,  universeIsType,  setElimination,  productIsType,  natural_numberEquality,  addEquality,  functionEquality,  setEquality,  dependent_set_memberEquality_alt,  independent_pairFormation,  unionElimination,  approximateComputation,  dependent_pairFormation_alt,  isect_memberEquality_alt,  voidElimination,  int_eqEquality,  productElimination,  imageMemberEquality,  baseClosed,  imageElimination
Latex:
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  <  b\}  .  \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.
    \mforall{}c:\mBbbR{}
        ((f(a)  \mleq{}  c)
        {}\mRightarrow{}  (c  \mleq{}  f(b))
        {}\mRightarrow{}  (\mforall{}u,v:\{v:\mBbbR{}|  v  \mmember{}  [a,  b]\}  .
                    ((u  <  v)
                    {}\mRightarrow{}  (\mexists{}k:\mBbbN{}
                              \mexists{}F:\mBbbN{}k  +  1  {}\mrightarrow{}  [a,  b]  {}\mrightarrow{}\mBbbR{}
                                (finite-deriv-seq([a,  b];k;i,x.F[i;x])
                                \mwedge{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  (F[0;x]  =  (f(x)  -  c)))
                                \mwedge{}  (\mexists{}z:\{z:\mBbbR{}|  z  \mmember{}  [u,  v]\}  .  (r0  <  \mSigma{}\{|F[i;z]|  |  0\mleq{}i\mleq{}k\}))))))
        {}\mRightarrow{}  (\mexists{}x:\mBbbR{}  [((x  \mmember{}  [a,  b])  \mwedge{}  (f(x)  =  c))])) 
    supposing  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))


Date html generated: 2019_10_30-AM-09_12_42
Last ObjectModification: 2019_04_03-PM-08_35_58

Theory : reals


Home Index