### 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