---

Step * 1 of Lemma reg-seq-mul-regular


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))
BY
{ (((Assert |x n| ≤ (n * k) BY BackThruSomeHyp) THEN (Mul ⌜m⌝ (-1) ⋅ THENA Auto))
   THEN (Assert |y m| ≤ (m * k) BY
               BackThruSomeHyp)
   THEN (Mul ⌜n⌝ (-1) ⋅ THENA Auto)
   THEN (RWO "-3 -1" 0 THENA Auto)
   THEN (Assert (4 * k) ≤ ((4 * (k + 1)) - 2) BY
               Auto)
   THEN RWO "-1<" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  k  :  \mBbbN{}\msupplus{}
4.  \mforall{}n:\mBbbN{}\msupplus{}.  ((|x  n|  \mleq{}  (n  *  k))  \mwedge{}  (|y  n|  \mleq{}  (n  *  k)))
5.  n  :  \{1...\}
6.  m  :  \{1...\}
\mvdash{}  (2  *  ((m  *  |x  n|)  +  (n  *  |y  m|)))  \mleq{}  ((n  *  m)  *  ((4  *  (k  +  1))  -  2))


By

---

Latex:
(((Assert  |x  n|  \mleq{}  (n  *  k)  BY  BackThruSomeHyp)  THEN  (Mul  \mkleeneopen{}m\mkleeneclose{}  (-1)  \mcdot{}  THENA  Auto))
  THEN  (Assert  |y  m|  \mleq{}  (m  *  k)  BY
                          BackThruSomeHyp)
  THEN  (Mul  \mkleeneopen{}n\mkleeneclose{}  (-1)  \mcdot{}  THENA  Auto)
  THEN  (RWO  "-3  -1"  0  THENA  Auto)
  THEN  (Assert  (4  *  k)  \mleq{}  ((4  *  (k  +  1))  -  2)  BY
                          Auto)
  THEN  RWO  "-1<"  0
  THEN  Auto)

---

Home Index