---

Step * of Lemma infinitesmal-zero

∀[x:ℝ]. uiff(x = r0;∀[k:ℕ+]. (|x| ≤ (r1/r(k))))
BY
{ (Auto THEN Try ((BLemma `rneq-int` THEN Auto))) }

1
1. x : ℝ
2. x = r0
3. k : ℕ+
⊢ |x| ≤ (r1/r(k))

2
1. x : ℝ
2. ∀[k:ℕ+]. (|x| ≤ (r1/r(k)))
⊢ x = r0

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  uiff(x  =  r0;\mforall{}[k:\mBbbN{}\msupplus{}].  (|x|  \mleq{}  (r1/r(k))))


By

---

Latex:
(Auto  THEN  Try  ((BLemma  `rneq-int`  THEN  Auto)))

---

Home Index