---

Step * of Lemma qsum_product

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

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RW  (AddrC  [2]  (LemmaC  `qmul\_com`))  0  THEN  Auto)

---

Home Index