---

Step * of Lemma q-geometric-series

No Annotations
∀[a:ℚ]. ∀[n:ℕ].  (Σ0 ≤ i < n. a ↑ i = if qeq(a;1) then n else (1 - a ↑ n/1 - a) fi  ∈ ℚ)
BY
{ (Auto THEN (InstLemma `sum_of_geometric_prog_q` [⌜a⌝;⌜n⌝]⋅ THENA Auto) THEN SplitOnConclITE THEN Auto) }

1
.....truecase..... 
1. a : ℚ
2. n : ℕ
3. ((1 + -(a)) * Σ0 ≤ i < n. a ↑ i) = (1 + -(a ↑ n)) ∈ ℚ
4. a = 1 ∈ ℚ
⊢ Σ0 ≤ i < n. a ↑ i = n ∈ ℚ

2
.....falsecase..... 
1. a : ℚ
2. n : ℕ
3. ((1 + -(a)) * Σ0 ≤ i < n. a ↑ i) = (1 + -(a ↑ n)) ∈ ℚ
4. ¬(a = 1 ∈ ℚ)
⊢ Σ0 ≤ i < n. a ↑ i = (1 - a ↑ n/1 - a) ∈ ℚ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a:\mBbbQ{}].  \mforall{}[n:\mBbbN{}].    (\mSigma{}0  \mleq{}  i  <  n.  a  \muparrow{}  i  =  if  qeq(a;1)  then  n  else  (1  -  a  \muparrow{}  n/1  -  a)  fi  )


By

---

Latex:
(Auto
  THEN  (InstLemma  `sum\_of\_geometric\_prog\_q`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SplitOnConclITE
  THEN  Auto)

---

Home Index