---

Step * 2 of Lemma reg-seq-mul_wf2


1. x : ℝ
2. y : ℝ
⊢ imax(canon-bnd(x);canon-bnd(y)) + 1-regular-seq(reg-seq-mul(x;y))
BY
{ (BLemma `reg-seq-mul-regular` THEN Auto) }

1
1. x : ℝ
2. y : ℝ
3. n : ℕ+
⊢ |x n| ≤ (n * imax(canon-bnd(x);canon-bnd(y)))

2
1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. |x n| ≤ (n * imax(canon-bnd(x);canon-bnd(y)))
⊢ |y n| ≤ (n * imax(canon-bnd(x);canon-bnd(y)))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
\mvdash{}  imax(canon-bnd(x);canon-bnd(y))  +  1-regular-seq(reg-seq-mul(x;y))


By

---

Latex:
(BLemma  `reg-seq-mul-regular`  THEN  Auto)

---

Home Index