---

Step * of Lemma radd*_functionality_wrt_infinitesmal

∀x,y:ℝ*.  (is-infinitesmal(x) ⇒ is-infinitesmal(y) ⇒ is-infinitesmal(x + y))
BY
{ ((RWO "infinitesmal-iff" 0 THEN Auto)
   THEN (Assert (r/r(2)) ∈ {r:ℝ| r0 < r}  BY
               (DVar `r' THEN MemTypeCD THEN Auto THEN nRMul ⌜r(2)⌝ 0⋅ THEN Auto))
   THEN RepeatFor 2 ((D 3 With ⌜(r/r(2))⌝  THENA Auto))) }

1
1. x : ℝ*
2. y : ℝ*
3. r : {r:ℝ| r0 < r} 
4. (r/r(2)) ∈ {r:ℝ| r0 < r} 
5. |x| < ((r/r(2)))*
6. |y| < ((r/r(2)))*
⊢ |x + y| < (r)*

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}*.    (is-infinitesmal(x)  {}\mRightarrow{}  is-infinitesmal(y)  {}\mRightarrow{}  is-infinitesmal(x  +  y))


By

---

Latex:
((RWO  "infinitesmal-iff"  0  THEN  Auto)
  THEN  (Assert  (r/r(2))  \mmember{}  \{r:\mBbbR{}|  r0  <  r\}    BY
                          (DVar  `r'  THEN  MemTypeCD  THEN  Auto  THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  RepeatFor  2  ((D  3  With  \mkleeneopen{}(r/r(2))\mkleeneclose{}    THENA  Auto)))

---

Home Index