---

Step * of Lemma reg_seq_mul-regular

∀[x,y:ℝ].
  ∀B:ℕ+
    B-regular-seq(reg_seq_mul(x;y)) supposing ∀n,m:ℕ+.  ((2 * ((m * |x n|) + (n * |y m|))) ≤ ((n * m) * ((4 * B) - 1)))
BY
{ (Auto
   THEN (InstLemma `reg_seq_mul-regular-eventually` [⌜x⌝;⌜y⌝;⌜B⌝;⌜1⌝]⋅ THENA Auto)
   THEN UnfoldTopAb 0
   THEN RepeatFor 2 (ParallelLast)) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].
    \mforall{}B:\mBbbN{}\msupplus{}
        B-regular-seq(reg\_seq\_mul(x;y)) 
        supposing  \mforall{}n,m:\mBbbN{}\msupplus{}.    ((2  *  ((m  *  |x  n|)  +  (n  *  |y  m|)))  \mleq{}  ((n  *  m)  *  ((4  *  B)  -  1)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `reg\_seq\_mul-regular-eventually`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  UnfoldTopAb  0
  THEN  RepeatFor  2  (ParallelLast))

---

Home Index