---

Step * of Lemma rpositive-iff

∀[x:ℝ]. (rpositive(x) ⇐⇒ rpositive2(x))
BY
{ (Unfold `rpositive2` 0 THEN Auto THEN ExRepD) }

1
1. [x] : ℝ
2. rpositive(x)
⊢ ∃n:ℕ+. ∀m:ℕ+. ((n ≤ m) ⇒ (m ≤ (n * (x m))))

2
1. [x] : ℝ
2. n : ℕ+
3. ∀m:ℕ+. ((n ≤ m) ⇒ (m ≤ (n * (x m))))
⊢ rpositive(x)

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (rpositive(x)  \mLeftarrow{}{}\mRightarrow{}  rpositive2(x))


By

---

Latex:
(Unfold  `rpositive2`  0  THEN  Auto  THEN  ExRepD)

---

Home Index