Nuprl Lemma : rroot-exists-ext
∀i:{2...}. ∀x:{x:ℝ| (↑isEven(i)) ⇒ (r0 ≤ x)} . (∃y:ℝ [(((↑isEven(i)) ⇒ (r0 ≤ y)) ∧ (y^i = x))])
Proof
Definitions occuring in Statement :
rleq: x ≤ y,
rnexp: x^k1,
req: x = y,
int-to-real: r(n),
real: ℝ,
isEven: isEven(n),
int_upper: {i...},
assert: ↑b,
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
natural_number: $n
Definitions unfolded in proof :
member: t ∈ T,
subtract: n - m,
so_lambda: λ2x.t[x],
so_apply: x[s],
accelerate: accelerate(k;f),
rroot-exists,
rroot-exists1-ext,
converges-iff-cauchy,
rroot-exists-part2,
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
Latex:
\mforall{}i:\{2...\}. \mforall{}x:\{x:\mBbbR{}| (\muparrow{}isEven(i)) {}\mRightarrow{} (r0 \mleq{} x)\} . (\mexists{}y:\mBbbR{} [(((\muparrow{}isEven(i)) {}\mRightarrow{} (r0 \mleq{} y)) \mwedge{} (y\^{}i = x))])
Date html generated:
2020_05_20-PM-00_30_06
Last ObjectModification:
2020_03_17-PM-02_58_33
Theory : reals
Home
Index