Nuprl Lemma : regular-iff
∀x:ℕ+ ⟶ ℤ
(regular-seq(x)
⇐⇒ ∀n,m:ℕ+.
∃z:ℝ
((((r((x n) - 2)/r(2 * n)) ≤ z) ∧ (z ≤ (r((x n) + 2)/r(2 * n))))
∧ ((r((x m) - 2)/r(2 * m)) ≤ z)
∧ (z ≤ (r((x m) + 2)/r(2 * m)))))
Proof
Definitions occuring in Statement :
rdiv: (x/y),
rleq: x ≤ y,
int-to-real: r(n),
real: ℝ,
regular-int-seq: k-regular-seq(f),
nat_plus: ℕ+,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
multiply: n * m,
subtract: n - m,
add: n + m,
natural_number: $n,
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
nat_plus: ℕ+,
less_than: a < b,
squash: ↓T,
less_than': less_than'(a;b),
true: True,
and: P ∧ Q,
uall: ∀[x:A]. B[x],
prop: ℙ,
iff: P ⇐⇒ Q
Lemmas referenced :
regular-int-seq-iff,
less_than_wf,
mul-one,
nat_plus_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
dependent_functionElimination,
thin,
dependent_set_memberEquality,
natural_numberEquality,
sqequalRule,
independent_pairFormation,
imageMemberEquality,
hypothesisEquality,
baseClosed,
hypothesis,
isectElimination,
lambdaFormation,
productElimination,
functionEquality,
intEquality
Latex:
\mforall{}x:\mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}
(regular-seq(x)
\mLeftarrow{}{}\mRightarrow{} \mforall{}n,m:\mBbbN{}\msupplus{}.
\mexists{}z:\mBbbR{}
((((r((x n) - 2)/r(2 * n)) \mleq{} z) \mwedge{} (z \mleq{} (r((x n) + 2)/r(2 * n))))
\mwedge{} ((r((x m) - 2)/r(2 * m)) \mleq{} z)
\mwedge{} (z \mleq{} (r((x m) + 2)/r(2 * m)))))
Date html generated:
2017_10_03-AM-08_45_05
Last ObjectModification:
2017_09_11-PM-01_36_29
Theory : reals
Home
Index