Nuprl Lemma : rationals-dense-ext
∀x:ℝ. ∀y:{y:ℝ| x < y} . ∃n:ℕ+. ∃m:ℤ. ((x < (r(m)/r(n))) ∧ ((r(m)/r(n)) < y))
Proof
Definitions occuring in Statement :
rdiv: (x/y),
rless: x < y,
int-to-real: r(n),
real: ℝ,
nat_plus: ℕ+,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
int: ℤ
Definitions unfolded in proof :
sq_stable__rless,
sq_stable__and,
rationals-dense,
member: t ∈ T
Lemmas referenced :
rationals-dense,
sq_stable__rless,
sq_stable__and
Rules used in proof :
equalitySymmetry,
equalityTransitivity,
sqequalHypSubstitution,
thin,
sqequalRule,
hypothesis,
extract_by_obid,
instantiate,
cut,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
introduction
Latex:
\mforall{}x:\mBbbR{}. \mforall{}y:\{y:\mBbbR{}| x < y\} . \mexists{}n:\mBbbN{}\msupplus{}. \mexists{}m:\mBbbZ{}. ((x < (r(m)/r(n))) \mwedge{} ((r(m)/r(n)) < y))
Date html generated:
2018_05_22-PM-01_50_11
Last ObjectModification:
2018_05_21-AM-00_08_33
Theory : reals
Home
Index