Nuprl Lemma : rroot-exists1-ext
∀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
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 :
member: t ∈ T,
int-to-real: r(n),
rdiv: (x/y),
rmul: a * b,
rinv: rinv(x),
lt_int: i <z j,
btrue: tt,
it: ⋅,
bfalse: ff,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
accelerate: accelerate(k;f),
reg-seq-inv: reg-seq-inv(x),
reg-seq-adjust: reg-seq-adjust(n;x),
imax: imax(a;b),
le_int: i ≤z j,
bnot: ¬bb,
reg-seq-mul: reg-seq-mul(x;y),
int-rdiv: (a)/k1,
rsub: x - y,
radd: a + b,
reg-seq-list-add: reg-seq-list-add(L),
cbv_list_accum: cbv_list_accum(x,a.f[x; a];y;L),
bottom: ⊥,
cons: [a / b],
rminus: -(x),
nil: [],
experimental: experimental{impliesFunctionality}(possibleextract),
pi1: fst(t),
subtract: n - m,
rroot-exists1,
rroot-exists-part1,
decidable__or,
decidable__rless-int-fractions,
rleq_functionality_wrt_implies,
any: any x,
rabs-difference-bound-rleq,
iff_weakening_equal,
rleq_functionality,
rless_transitivity1,
rless-implies-rless,
rless_transitivity2,
rless_functionality,
radd-preserves-rless,
decidable__lt,
decidable__equal_int,
rmul_preserves_rless,
rless-int,
rmul_preserves_req,
req_functionality,
req_weakening,
rleq_weakening_rless,
rleq_weakening,
rleq_weakening_equal,
decidable_functionality,
rless-int-fractions,
rless-iff4,
rless-iff-large-diff,
sq_stable__rless,
radd_functionality_wrt_rless1,
decidable__int_equal,
decidable__squash,
decidable__and,
decidable__less_than',
rmul_functionality_wrt_rless,
rinv-positive,
iff_preserves_decidability,
regular-less-iff,
decidable__le,
rless-iff-rpositive,
rpositive_functionality,
rpositive-radd2,
squash_elim,
sq_stable_from_decidable,
rpositive-iff,
rpositive2_functionality,
bdd-diff_inversion,
accelerate-bdd-diff,
rnonneg-iff,
imax_lb,
sq_stable__from_stable,
stable__from_decidable,
bdd-diff-equiv,
le_functionality,
uall: ∀[x:A]. B[x],
so_lambda: so_lambda4,
so_apply: x[s1;s2;s3;s4],
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
uimplies: b supposing a,
so_lambda: λ2x.t[x],
so_apply: x[s]
Latex:
\mforall{}i:\{2...\}. \mforall{}x:\{x:\mBbbR{}| (\muparrow{}isEven(i)) {}\mRightarrow{} (r0 \mleq{} x)\} .
\mexists{}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
Date html generated:
2020_05_20-PM-00_29_42
Last ObjectModification:
2020_03_19-PM-02_23_57
Theory : reals
Home
Index