Nuprl Lemma : rroot-exists1
∀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 :
all: ∀x:A. B[x],
member: t ∈ T,
exists: ∃x:A. B[x],
and: P ∧ Q,
cand: A c∧ B,
or: P ∨ Q,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
prop: ℙ,
so_apply: x[s],
implies: P ⇒ Q,
int_upper: {i...},
subtype_rel: A ⊆r B,
nat: ℕ,
le: A ≤ B,
less_than': less_than'(a;b),
false: False,
not: ¬A
Lemmas referenced :
rroot-exists-part1,
all_wf,
nat_wf,
or_wf,
rleq_wf,
int-to-real_wf,
assert_wf,
isEven_wf,
converges-to_wf,
rnexp_wf,
int_upper_subtype_nat,
false_wf,
le_wf,
real_wf,
int_upper_wf
Rules used in proof :
cut,
lemma_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
productElimination,
dependent_pairFormation,
sqequalRule,
independent_pairFormation,
dependent_set_memberEquality,
productEquality,
isectElimination,
lambdaEquality,
because_Cache,
natural_numberEquality,
applyEquality,
functionEquality,
setElimination,
rename,
setEquality
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:
2016_05_18-AM-09_33_08
Last ObjectModification:
2015_12_27-PM-11_18_47
Theory : reals
Home
Index