---

Step * 1 of Lemma sum_of_geometric_prog_q

.....assertion..... 
∀[a:ℚ]. ∀[n:ℕ].  (((1 + -(a)) * Σ0 ≤ i < n. q-rng-nexp(a;i)) = (1 + -(q-rng-nexp(a;n))) ∈ ℚ)
BY
{ (Unfolds ``q-rng-nexp qsum`` 0 THEN (ProveSpecializedLemmaWReduce sum_of_geometric_prog) 0 [⌜parm{i}⌝;⌜<ℚ+*>⌝]⋅) }

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}[a:\mBbbQ{}].  \mforall{}[n:\mBbbN{}].    (((1  +  -(a))  *  \mSigma{}0  \mleq{}  i  <  n.  q-rng-nexp(a;i))  =  (1  +  -(q-rng-nexp(a;n))))


By

---

Latex:
(Unfolds  ``q-rng-nexp  qsum``  0
  THEN  (ProveSpecializedLemmaWReduce  sum\_of\_geometric\_prog)  0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}<\mBbbQ{}+*>\mkleeneclose{}]\mcdot{}
  )

---

Home Index