---

Step * of Lemma rnonneg-iff

∀[x:ℝ]. (rnonneg(x) ⇐⇒ rnonneg2(x))
BY
{ (Unfold `rnonneg2` 0 THEN Auto) }

1
1. [x] : ℝ
2. rnonneg(x)@i
3. n : ℕ+@i
⊢ ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * (x m)))

2
1. x : ℝ
2. ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * (x m)))@i
⊢ rnonneg(x)

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (rnonneg(x)  \mLeftarrow{}{}\mRightarrow{}  rnonneg2(x))


By

---

Latex:
(Unfold  `rnonneg2`  0  THEN  Auto)

---

Home Index