### Nuprl Lemma : rroot-exists-part2

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

Proof

Definitions occuring in Statement :  cauchy: `cauchy(n.x[n])` 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]` 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]` implies: `P `` Q` converges-to: `lim n→∞.x[n] = y` exists: `∃x:A. B[x]` cauchy: `cauchy(n.x[n])` member: `t ∈ T` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` nat_plus: `ℕ+` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` and: `P ∧ Q` prop: `ℙ` so_lambda: `λ2x.t[x]` nat: `ℕ` le: `A ≤ B` false: `False` not: `¬A` so_apply: `x[s]` or: `P ∨ Q` int_upper: `{i...}` sq_exists: `∃x:{A| B[x]}` uimplies: `b supposing a` rneq: `x ≠ y` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` ge: `i ≥ j ` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` sq_stable: `SqStable(P)` rleq: `x ≤ y` rnonneg: `rnonneg(x)` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)` rge: `x ≥ y` rless: `x < y` real: `ℝ`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution cut hypothesis promote_hyp thin productElimination introduction extract_by_obid isectElimination hypothesisEquality applyEquality because_Cache sqequalRule dependent_set_memberEquality natural_numberEquality independent_pairFormation imageMemberEquality baseClosed equalityTransitivity equalitySymmetry lambdaEquality setElimination rename functionEquality productEquality functionExtensionality independent_isectElimination inrFormation dependent_functionElimination independent_functionElimination unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll minusEquality independent_pairEquality axiomEquality imageElimination applyLambdaEquality dependent_set_memberFormation multiplyEquality addEquality universeEquality

Latex:
\mforall{}i:\{2...\}.  \mforall{}x:\{x:\mBbbR{}|  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  x)\}  .  \mforall{}q:\{q:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}|
(\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))))\}  .
(lim  n\mrightarrow{}\minfty{}.q  n\^{}i  =  x  {}\mRightarrow{}  cauchy(n.q  n))

Date html generated: 2017_10_03-AM-10_39_01
Last ObjectModification: 2017_07_28-AM-08_15_31

Theory : reals

Home Index