---

Step * of Lemma ireal-approx-radd

∀[x,y:ℝ]. ∀[j,i:ℕ]. ∀[M:ℕ+]. ∀[a,b:ℤ].  (j-approx(x;M;a) ⇒ i-approx(y;M;b) ⇒ j + i-approx(x + y;M;a + b))
BY
{ (Auto
   THEN All (Unfold  `ireal-approx`)
   THEN (Assert ((x + y) - (r(a + b)/r(2 * M))) = ((x - (r(a)/r(2 * M))) + (y - (r(b)/r(2 * M)))) BY
               (RWO "radd-int<" 0 THEN Auto THEN nRMul ⌜r(2 * M)⌝ 0⋅ THEN Auto))
   THEN RWW "-1 r-triangle-inequality -2 -3 radd-rdiv radd-int" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].  \mforall{}[j,i:\mBbbN{}].  \mforall{}[M:\mBbbN{}\msupplus{}].  \mforall{}[a,b:\mBbbZ{}].
    (j-approx(x;M;a)  {}\mRightarrow{}  i-approx(y;M;b)  {}\mRightarrow{}  j  +  i-approx(x  +  y;M;a  +  b))


By

---

Latex:
(Auto
  THEN  All  (Unfold    `ireal-approx`)
  THEN  (Assert  ((x  +  y)  -  (r(a  +  b)/r(2  *  M)))  =  ((x  -  (r(a)/r(2  *  M)))  +  (y  -  (r(b)/r(2  *  M))))  BY
                          (RWO  "radd-int<"  0  THEN  Auto  THEN  nRMul  \mkleeneopen{}r(2  *  M)\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  RWW  "-1  r-triangle-inequality  -2  -3  radd-rdiv  radd-int"  0
  THEN  Auto)

---

Home Index