---

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


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index