---

Step * of Lemma reg-seq-mul-regular

∀[x,y:ℝ].  ∀k:ℕ+. k + 1-regular-seq(reg-seq-mul(x;y)) supposing ∀n:ℕ+. ((|x n| ≤ (n * k)) ∧ (|y n| ≤ (n * k)))
BY
{ (Auto
   THEN (InstLemma `reg-seq-mul-regular-eventually` [⌜x⌝;⌜y⌝;⌜k + 1⌝;⌜1⌝]⋅
   THENM (UnfoldTopAb 0 THEN RepeatFor 2 (ParallelLast))
   )
   THEN Auto) }

1
1. x : ℝ
2. y : ℝ
3. k : ℕ+
4. ∀n:ℕ+. ((|x n| ≤ (n * k)) ∧ (|y n| ≤ (n * k)))
5. n : {1...}
6. m : {1...}
⊢ (2 * ((m * |x n|) + (n * |y m|))) ≤ ((n * m) * ((4 * (k + 1)) - 2))

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].
    \mforall{}k:\mBbbN{}\msupplus{}
        k  +  1-regular-seq(reg-seq-mul(x;y))  supposing  \mforall{}n:\mBbbN{}\msupplus{}.  ((|x  n|  \mleq{}  (n  *  k))  \mwedge{}  (|y  n|  \mleq{}  (n  *  k)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `reg-seq-mul-regular-eventually`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}k  +  1\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}
  THENM  (UnfoldTopAb  0  THEN  RepeatFor  2  (ParallelLast))
  )
  THEN  Auto)

---

Home Index