---

Step * 2 of Lemma rnonneg-iff


1. x : ℝ
2. ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * (x m)))@i
⊢ rnonneg(x)
BY
{ ((Skolemize 2 `N'⋅ THENA Auto)
   THEN (Assert ∀n:ℕ+. ∀m:{N n...}. ∀k:ℕ+.  (((-2) * n * m) ≤ (((n * m) * (x k)) + ((2 * k) * (n + m)))) BY
               (RepeatFor 2 (ParallelLast')
                THEN Auto
                THEN D 1
                THEN (Unhide THENA Auto)
                THEN Unfold `regular-int-seq` 2
                THEN (InstHyp [⌜k⌝;⌜m⌝] 2⋅ THENA Auto)
                THEN ((RWO "absval_ubound" (-1) THENM D -1) THENA Auto)
                THEN (Using [`n',⌜n⌝] (FLemma `mul_preserves_le` [-2])⋅ THENA Auto)
                THEN (RW IntNormC (-1) THENA Auto)
                THEN (RW IntNormC 0 THENA Auto)
                THEN Using [`n',⌜k⌝] (FLemma `mul_preserves_le` [-5])⋅
                THEN Auto'))
   ) }

1
1. x : ℝ
2. ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * (x m)))
3. N : n:ℕ+ ⟶ ℕ+
4. ∀n:ℕ+. ∀m:{N n...}.  (((-2) * m) ≤ (n * (x m)))
5. ∀n:ℕ+. ∀m:{N n...}. ∀k:ℕ+.  (((-2) * n * m) ≤ (((n * m) * (x k)) + ((2 * k) * (n + m))))
⊢ rnonneg(x)

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  \mforall{}n:\mBbbN{}\msupplus{}.  \mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}m:\{N...\}.  (((-2)  *  m)  \mleq{}  (n  *  (x  m)))@i
\mvdash{}  rnonneg(x)


By

---

Latex:
((Skolemize  2  `N'\mcdot{}  THENA  Auto)
  THEN  (Assert  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}m:\{N  n...\}.  \mforall{}k:\mBbbN{}\msupplus{}.
                                (((-2)  *  n  *  m)  \mleq{}  (((n  *  m)  *  (x  k))  +  ((2  *  k)  *  (n  +  m))))  BY
                          (RepeatFor  2  (ParallelLast')
                            THEN  Auto
                            THEN  D  1
                            THEN  (Unhide  THENA  Auto)
                            THEN  Unfold  `regular-int-seq`  2
                            THEN  (InstHyp  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]  2\mcdot{}  THENA  Auto)
                            THEN  ((RWO  "absval\_ubound"  (-1)  THENM  D  -1)  THENA  Auto)
                            THEN  (Using  [`n',\mkleeneopen{}n\mkleeneclose{}]  (FLemma  `mul\_preserves\_le`  [-2])\mcdot{}  THENA  Auto)
                            THEN  (RW  IntNormC  (-1)  THENA  Auto)
                            THEN  (RW  IntNormC  0  THENA  Auto)
                            THEN  Using  [`n',\mkleeneopen{}k\mkleeneclose{}]  (FLemma  `mul\_preserves\_le`  [-5])\mcdot{}
                            THEN  Auto'))
  )

---

Home Index