---

Step * of Lemma rnonzero-lemma1

∀[x:ℝ]. ∀[n:ℕ+].  ∀m:ℕ+. ((n ≤ m) ⇒ (m ≤ (n * |x m|))) supposing 5 ≤ |x n|
BY
{ (Auto
   THEN D 1
   THEN (Unhide THENA Auto)
   THEN (With ⌜n⌝ (D 2)⋅ THENA Auto)
   THEN (InstHyp [⌜m⌝] (-1)⋅ THENA Auto)
   THEN Thin (-2)
   THEN (Assert |(n * (x m)) + ((m * (x n)) - n * (x m))| ≤ (|n * (x m)| + |(m * (x n)) - n * (x m)|) BY
               (BLemma `int-triangle-inequality` THENA Auto))
   THEN (RWO "-2" (-1) THENA Auto)
   THEN (RW IntNormC (-1) THENA Auto)) }

1
1. x : ℕ+ ⟶ ℤ
2. n : ℕ+
3. 5 ≤ |x n|
4. m : ℕ+
5. n ≤ m
6. |(m * (x n)) - n * (x m)| ≤ ((2 * 1) * (n + m))
7. |m * (x n)| ≤ ((2 * m) + (2 * n) + |n * (x m)|)
⊢ m ≤ (n * |x m|)

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  \mforall{}[n:\mBbbN{}\msupplus{}].    \mforall{}m:\mBbbN{}\msupplus{}.  ((n  \mleq{}  m)  {}\mRightarrow{}  (m  \mleq{}  (n  *  |x  m|)))  supposing  5  \mleq{}  |x  n|


By

---

Latex:
(Auto
  THEN  D  1
  THEN  (Unhide  THENA  Auto)
  THEN  (With  \mkleeneopen{}n\mkleeneclose{}  (D  2)\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}m\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Thin  (-2)
  THEN  (Assert  |(n  *  (x  m))  +  ((m  *  (x  n))  -  n  *  (x  m))|  \mleq{}  (|n  *  (x  m)|
                            +  |(m  *  (x  n))  -  n  *  (x  m)|)  BY
                          (BLemma  `int-triangle-inequality`  THENA  Auto))
  THEN  (RWO  "-2"  (-1)  THENA  Auto)
  THEN  (RW  IntNormC  (-1)  THENA  Auto))

---

Home Index