---

Step * of Lemma sum_of_geometric_prog_q

No Annotations
∀[a:ℚ]. ∀[n:ℕ].  (((1 + -(a)) * Σ0 ≤ i < n. a ↑ i) = (1 + -(a ↑ n)) ∈ ℚ)
BY
{ TACTIC:Assert ⌜∀[a:ℚ]. ∀[n:ℕ].  (((1 + -(a)) * Σ0 ≤ i < n. q-rng-nexp(a;i)) = (1 + -(q-rng-nexp(a;n))) ∈ ℚ)⌝⋅ }

1
.....assertion..... 
∀[a:ℚ]. ∀[n:ℕ].  (((1 + -(a)) * Σ0 ≤ i < n. q-rng-nexp(a;i)) = (1 + -(q-rng-nexp(a;n))) ∈ ℚ)

2
1. ∀[a:ℚ]. ∀[n:ℕ].  (((1 + -(a)) * Σ0 ≤ i < n. q-rng-nexp(a;i)) = (1 + -(q-rng-nexp(a;n))) ∈ ℚ)
⊢ ∀[a:ℚ]. ∀[n:ℕ].  (((1 + -(a)) * Σ0 ≤ i < n. a ↑ i) = (1 + -(a ↑ n)) ∈ ℚ)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a:\mBbbQ{}].  \mforall{}[n:\mBbbN{}].    (((1  +  -(a))  *  \mSigma{}0  \mleq{}  i  <  n.  a  \muparrow{}  i)  =  (1  +  -(a  \muparrow{}  n)))


By

---

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

---

Home Index