### Nuprl Lemma : rroot-exists-part1

`∀i:{2...}. ∀x:{x:ℝ| (↑isEven(i)) `` (r0 ≤ x)} .`
`  ∃q:ℕ ⟶ ℝ`
`   (lim n→∞.q n^i = x`
`   ∧ (∀n,m:ℕ.  (((r0 ≤ (q n)) ∧ (r0 ≤ (q m))) ∨ (((q n) ≤ r0) ∧ ((q m) ≤ r0))))`
`   ∧ ((↑isEven(i)) `` (∀m:ℕ. (r0 ≤ (q m)))))`

Proof

Definitions occuring in Statement :  converges-to: `lim n→∞.x[n] = y` rleq: `x ≤ y` rnexp: `x^k1` int-to-real: `r(n)` real: `ℝ` isEven: `isEven(n)` int_upper: `{i...}` nat: `ℕ` assert: `↑b` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` implies: `P `` Q` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` int_upper: `{i...}` real: `ℝ` exists: `∃x:A. B[x]` nat_plus: `ℕ+` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` and: `P ∧ Q` subtype_rel: `A ⊆r B` le: `A ≤ B` false: `False` not: `¬A` or: `P ∨ Q` rational-approx: `(x within 1/n)` top: `Top` int_nzero: `ℤ-o` nequal: `a ≠ b ∈ T ` guard: `{T}` satisfiable_int_formula: `satisfiable_int_formula(fmla)` rneq: `x ≠ y` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` decidable: `Dec(P)` uiff: `uiff(P;Q)` nat: `ℕ` rless: `x < y` sq_exists: `∃x:A [B[x]]` rdiv: `(x/y)` req_int_terms: `t1 ≡ t2` rev_uimplies: `rev_uimplies(P;Q)` rge: `x ≥ y` sq_stable: `SqStable(P)` cand: `A c∧ B` subtract: `n - m` pi1: `fst(t)` converges-to: `lim n→∞.x[n] = y` ge: `i ≥ j `
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut because_Cache hypothesisEquality cutEval introduction dependent_set_memberEquality extract_by_obid sqequalHypSubstitution isectElimination thin sqequalRule hypothesis lambdaEquality independent_isectElimination functionEquality setElimination rename natural_numberEquality intEquality dependent_pairFormation independent_pairFormation imageMemberEquality baseClosed equalitySymmetry hyp_replacement applyLambdaEquality productEquality applyEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality multiplyEquality approximateComputation independent_functionElimination int_eqEquality baseApply closedConclusion inrFormation productElimination unionElimination equalityTransitivity minusEquality imageElimination instantiate universeEquality inlFormation setEquality promote_hyp addEquality addLevel functionExtensionality dependent_set_memberFormation

Latex:
\mforall{}i:\{2...\}.  \mforall{}x:\{x:\mBbbR{}|  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  x)\}  .
\mexists{}q:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}
(lim  n\mrightarrow{}\minfty{}.q  n\^{}i  =  x
\mwedge{}  (\mforall{}n,m:\mBbbN{}.    (((r0  \mleq{}  (q  n))  \mwedge{}  (r0  \mleq{}  (q  m)))  \mvee{}  (((q  n)  \mleq{}  r0)  \mwedge{}  ((q  m)  \mleq{}  r0))))
\mwedge{}  ((\muparrow{}isEven(i))  {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  (r0  \mleq{}  (q  m)))))

Date html generated: 2019_10_30-AM-07_54_15
Last ObjectModification: 2018_08_27-PM-11_52_17

Theory : reals

Home Index