---

Step * of Lemma sum_plus_q

No Annotations
∀[a,b:ℤ].  ∀[E,F:{a..b-} ⟶ ℚ].  (Σa ≤ i < b. E[i] + F[i] = (Σa ≤ i < b. E[i] + Σa ≤ i < b. F[i]) ∈ ℚ) supposing a ≤ b
BY
{ ((ProveSpecializedLemmaWReduce rng_sum_plus) 0 [⌜parm{i}⌝;⌜<ℚ+*>⌝]⋅ THEN Fold `qsum` (-1) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a,b:\mBbbZ{}].
    \mforall{}[E,F:\{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}].    (\mSigma{}a  \mleq{}  i  <  b.  E[i]  +  F[i]  =  (\mSigma{}a  \mleq{}  i  <  b.  E[i]  +  \mSigma{}a  \mleq{}  i  <  b.  F[i])) 
    supposing  a  \mleq{}  b


By

---

Latex:
((ProveSpecializedLemmaWReduce  rng\_sum\_plus)  0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}<\mBbbQ{}+*>\mkleeneclose{}]\mcdot{}  THEN  Fold  `qsum`  (-1)  THEN  Auto)

---

Home Index