Nuprl Lemma : rless-implies-rleq
∀x,y:ℝ. ((x < y) ⇒ (∃m:ℕ+. (x ≤ (y - (r1/r(m))))))
Proof
Definitions occuring in Statement :
rdiv: (x/y),
rleq: x ≤ y,
rless: x < y,
rsub: x - y,
int-to-real: r(n),
real: ℝ,
nat_plus: ℕ+,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
iff: P ⇐⇒ Q,
and: P ∧ Q
Lemmas referenced :
rless-iff-rleq,
real_wf
Rules used in proof :
cut,
lemma_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
productElimination
Latex:
\mforall{}x,y:\mBbbR{}. ((x < y) {}\mRightarrow{} (\mexists{}m:\mBbbN{}\msupplus{}. (x \mleq{} (y - (r1/r(m))))))
Date html generated:
2016_05_18-AM-07_53_38
Last ObjectModification:
2015_12_28-AM-01_07_12
Theory : reals
Home
Index