Step
*
of Lemma
rational-lower-approx-as-rat2real
No Annotations
∀x:ℝ. ∀n:ℕ+. ∃q:ℚ. ((below x within 1/n) = rat2real(q))
BY
{ (Auto
THEN RepUR ``rational-lower-approx`` 0
THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
THEN D 0 With ⌜((x (2 * n)) - 2/2 * 2 * n)⌝
THEN Auto
THEN (RWO "rat2real-qdiv int-rdiv-req" 0 THENM BLemma `rdiv_functionality`)
THEN Auto
THEN (GenConclTerm ⌜(x (2 * n)) - 2⌝⋅ THENA Auto)
THEN RepUR ``rat2real`` 0
THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}x:\mBbbR{}. \mforall{}n:\mBbbN{}\msupplus{}. \mexists{}q:\mBbbQ{}. ((below x within 1/n) = rat2real(q))
By
Latex:
(Auto
THEN RepUR ``rational-lower-approx`` 0
THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
THEN D 0 With \mkleeneopen{}((x (2 * n)) - 2/2 * 2 * n)\mkleeneclose{}
THEN Auto
THEN (RWO "rat2real-qdiv int-rdiv-req" 0 THENM BLemma `rdiv\_functionality`)
THEN Auto
THEN (GenConclTerm \mkleeneopen{}(x (2 * n)) - 2\mkleeneclose{}\mcdot{} THENA Auto)
THEN RepUR ``rat2real`` 0
THEN Auto)
Home
Index