---

Step * 2 1 1 of Lemma reg-seq-mul_wf2


1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. canon-bnd(x) ≤ imax(canon-bnd(x);canon-bnd(y))
5. (n * canon-bnd(x)) ≤ (n * imax(canon-bnd(x);canon-bnd(y)))
⊢ |x n| ≤ (n * canon-bnd(x))
BY
{ (GenConclTerm ⌜canon-bnd(x)⌝⋅ THEN Auto THEN D -2 THEN Unhide THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  n  :  \mBbbN{}\msupplus{}
4.  canon-bnd(x)  \mleq{}  imax(canon-bnd(x);canon-bnd(y))
5.  (n  *  canon-bnd(x))  \mleq{}  (n  *  imax(canon-bnd(x);canon-bnd(y)))
\mvdash{}  |x  n|  \mleq{}  (n  *  canon-bnd(x))


By

---

Latex:
(GenConclTerm  \mkleeneopen{}canon-bnd(x)\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  D  -2  THEN  Unhide  THEN  Auto)

---

Home Index