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