PrintForm Definitions exponent Sections AutomataTheory Doc

At: geom series wf


q,n:. (qn)

By:
UnivCD
THEN
NatInd 2
THEN
RecCaseSplit `geom_series`


Generated subgoals:

11. q:
2. 0 = 0
0
21. q:
2. 0 = 0
(q-1)+(q-1)
31. q:
2. n:
3. 0 < n
4. (qn-1)
5. n = 0
0
41. q:
2. n:
3. 0 < n
4. (qn-1)
5. n = 0
(qn-1)+(qn-1)


About:
allmembernatural_numberaddminussubtract