---

Step * 1 of Lemma qsum_product


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] ∈ ℚ
BY
{ ((RWO "qsum-linearity1<" 0 THEN Auto)⋅ THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  c  :  \mBbbZ{}
4.  d  :  \mBbbZ{}
5.  x  :  \{a..b  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}
6.  y  :  \{c..d  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}
\mvdash{}  (\mSigma{}c  \mleq{}  j  <  d.  y[j]  *  \mSigma{}a  \mleq{}  i  <  b.  x[i])  =  \mSigma{}a  \mleq{}  i  <  b.  \mSigma{}c  \mleq{}  j  <  d.  x[i]  *  y[j]


By

---

Latex:
((RWO  "qsum-linearity1<"  0  THEN  Auto)\mcdot{}  THEN  EqCD  THEN  Auto)

---

Home Index