---

Step * of Lemma rational-lower-approx-property

∀x:ℝ. ∀n:ℕ+.  (((below x within 1/n) ≤ x) ∧ (x ≤ ((below x within 1/n) + (r1/r(n)))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (InstLemma `rational-approx-property` [⌜x⌝;⌜2 * n⌝]⋅ THENA Auto)
   THEN Unfold `rational-approx` -1
   THEN Unfold `rational-lower-approx` 0
   THEN (CallByValueReduce  0⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜(x (2 * n)) = a ∈ ℤ⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Assert ⌜(r(a - 2))/2 * 2 * n = ((r(a))/2 * 2 * n - (r1/r(2 * n)))⌝⋅) }

1
.....assertion..... 
1. x : ℝ
2. n : ℕ+
3. a : ℤ
4. (x (2 * n)) = a ∈ ℤ
⊢ (r(a - 2))/2 * 2 * n = ((r(a))/2 * 2 * n - (r1/r(2 * n)))

2
1. x : ℝ
2. n : ℕ+
3. a : ℤ
4. (x (2 * n)) = a ∈ ℤ
5. (r(a - 2))/2 * 2 * n = ((r(a))/2 * 2 * n - (r1/r(2 * n)))
⊢ (|x - (r(a))/2 * 2 * n| ≤ (r1/r(2 * n))) ⇒ (((r(a - 2))/2 * 2 * n ≤ x) ∧ (x ≤ ((r(a - 2))/2 * 2 * n + (r1/r(n)))))

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    (((below  x  within  1/n)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  ((below  x  within  1/n)  +  (r1/r(n)))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (InstLemma  `rational-approx-property`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}2  *  n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `rational-approx`  -1
  THEN  Unfold  `rational-lower-approx`  0
  THEN  (CallByValueReduce    0\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}(x  (2  *  n))  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Assert  \mkleeneopen{}(r(a  -  2))/2  *  2  *  n  =  ((r(a))/2  *  2  *  n  -  (r1/r(2  *  n)))\mkleeneclose{}\mcdot{})

---

Home Index