Step * of Lemma rnonneg-iff

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

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

2
1. : ℝ
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