---

Step * of Lemma rational-inner-approx-property

No Annotations
∀x:ℝ. ∀n:ℕ+.  ((|rational-inner-approx(x;n)| ≤ |x|) ∧ (|x - rational-inner-approx(x;n)| ≤ (r(2)/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-inner-approx` 0
   THEN (CallByValueReduce  0⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜(x (2 * n)) = a ∈ ℤ⌝⋅ THENA Auto)
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN (D 0 THENA Auto)
   THEN (Decide ⌜4 < a⌝⋅ THENA Auto)
   THEN (OReduce 0 THENA Auto)) }

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

2
1. x : ℝ
2. n : ℕ+
3. a : ℤ
4. (x (2 * n)) = a ∈ ℤ
5. |x - (r(a))/2 * 2 * n| ≤ (r1/r(2 * n))
6. ¬4 < a
⊢ (|(r(if a <z -4 then a + 2 else 0 fi ))/2 * 2 * n| ≤ |x|)
∧ (|x - (r(if a <z -4 then a + 2 else 0 fi ))/2 * 2 * n| ≤ (r(2)/r(n)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.
    ((|rational-inner-approx(x;n)|  \mleq{}  |x|)  \mwedge{}  (|x  -  rational-inner-approx(x;n)|  \mleq{}  (r(2)/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-inner-approx`  0
  THEN  (CallByValueReduce    0\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}(x  (2  *  n))  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  (Decide  \mkleeneopen{}4  <  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (OReduce  0  THENA  Auto))

---

Home Index