---

Step * of Lemma rsum_product

No Annotations
∀[a,b,c,d:ℤ]. ∀[x:{a..b + 1-} ⟶ ℝ]. ∀[y:{c..d + 1-} ⟶ ℝ].
  ((Σ{x[i] | a≤i≤b} * Σ{y[j] | c≤j≤d}) = Σ{Σ{x[i] * y[j] | c≤j≤d} | a≤i≤b})
BY
{ (Auto THEN RW (AddrC [1] (LemmaC `rmul_comm`)) 0 THEN Auto) }

1
1. a : ℤ
2. b : ℤ
3. c : ℤ
4. d : ℤ
5. x : {a..b + 1-} ⟶ ℝ
6. y : {c..d + 1-} ⟶ ℝ
⊢ (Σ{y[j] | c≤j≤d} * Σ{x[i] | a≤i≤b}) = Σ{Σ{x[i] * y[j] | c≤j≤d} | a≤i≤b}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a,b,c,d:\mBbbZ{}].  \mforall{}[x:\{a..b  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[y:\{c..d  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}].
    ((\mSigma{}\{x[i]  |  a\mleq{}i\mleq{}b\}  *  \mSigma{}\{y[j]  |  c\mleq{}j\mleq{}d\})  =  \mSigma{}\{\mSigma{}\{x[i]  *  y[j]  |  c\mleq{}j\mleq{}d\}  |  a\mleq{}i\mleq{}b\})


By

---

Latex:
(Auto  THEN  RW  (AddrC  [1]  (LemmaC  `rmul\_comm`))  0  THEN  Auto)

---

Home Index