---

Step * of Lemma reg-seq-mul_wf2

∀[x,y:ℝ].  (reg-seq-mul(x;y) ∈ {f:ℕ+ ⟶ ℤ| imax(|x 1|;|y 1|) + 4-regular-seq(f)} )
BY
{ (Auto THEN MemTypeCD THEN Auto THEN Subst' imax(|x 1|;|y 1|) + 4 ~ imax(canon-bnd(x);canon-bnd(y)) + 1 0) }

1
.....equality..... 
1. x : ℝ
2. y : ℝ
⊢ imax(|x 1|;|y 1|) + 4 ~ imax(canon-bnd(x);canon-bnd(y)) + 1

2
1. x : ℝ
2. y : ℝ
⊢ imax(canon-bnd(x);canon-bnd(y)) + 1-regular-seq(reg-seq-mul(x;y))

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    (reg-seq-mul(x;y)  \mmember{}  \{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  imax(|x  1|;|y  1|)  +  4-regular-seq(f)\}  )


By

---

Latex:
(Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  Subst'  imax(|x  1|;|y  1|)  +  4  \msim{}  imax(canon-bnd(x);canon-bnd(y))  +  1  0)

---

Home Index