Theorem geoser 7169

Description: The value of the finite geometric series 1 + A^1 + A^2 +... + A^N.

Hypotheses

Ref	Expression
geoser.1	|- F = {<.k, y>. | (k e. NN0 /\ y = (A^k))}
geoser.2	|- A e. CC

Assertion

Ref	Expression
geoser	|- ((N e. NN0 /\ A =/= 1) -> (( + seq0 F)` N) = ((1 - (A^(N + 1))) / (1 - A)))

Distinct variable group:   y,k,A

Proof of Theorem geoser

Step	Hyp	Ref	Expression
1		ax1cn 5241	. . . . 5 |- 1 e. CC
2		geoser.2	. . . . 5 |- A e. CC
3	1, 2	subcl 5338	. . . 4 |- (1 - A) e. CC
4		divcan4t 5719	. . . 4 |- (((1 - A) e. CC /\ (( + seq0 F)` N) e. CC /\ (1 - A) =/= 0) -> (((( + seq0 F)` N) x. (1 - A)) / (1 - A)) = (( + seq0 F)` N))
5	3, 4	mp3an1 900	. . 3 |- (((( + seq0 F)` N) e. CC /\ (1 - A) =/= 0) -> (((( + seq0 F)` N) x. (1 - A)) / (1 - A)) = (( + seq0 F)` N))
6		geoser.1	. . . . 5 |- F = {<.k, y>. | (k e. NN0 /\ y = (A^k))}
7		expclt 6513	. . . . . 6 |- ((A e. CC /\ k e. NN0) -> (A^k) e. CC)
8	2, 7	mpan 693	. . . . 5 |- (k e. NN0 -> (A^k) e. CC)
9	6, 8	fopab 3812	. . . 4 |- F:NN0-->CC
10	9	ser0cl1 6496	. . 3 |- (N e. NN0 -> (( + seq0 F)` N) e. CC)
11	2	subid 5363	. . . . . . 7 |- (A - A) = 0
12	11	eqeq1i 1474	. . . . . 6 |- ((A - A) = (1 - A) <-> 0 = (1 - A))
13	2, 1, 2	subcan2 5386	. . . . . 6 |- ((A - A) = (1 - A) <-> A = 1)
14		eqcom 1469	. . . . . 6 |- (0 = (1 - A) <-> (1 - A) = 0)
15	12, 13, 14	3bitr3 181	. . . . 5 |- (A = 1 <-> (1 - A) = 0)
16	15	necon3bii 1590	. . . 4 |- (A =/= 1 <-> (1 - A) =/= 0)
17	16	biimp 151	. . 3 |- (A =/= 1 -> (1 - A) =/= 0)
18	5, 10, 17	syl2an 454	. 2 |- ((N e. NN0 /\ A =/= 1) -> (((( + seq0 F)` N) x. (1 - A)) / (1 - A)) = (( + seq0 F)` N))
19		oprex 3968	. . . . . . . . . . 11 |- (A^(m + 1)) e. V
20		opreq2 3954	. . . . . . . . . . 11 |- (k = (m + 1) -> (A^k) = (A^(m + 1)))
21	6, 19, 20	ser0p1 6499	. . . . . . . . . 10 |- (m e. NN0 -> (( + seq0 F)` (m + 1)) = ((( + seq0 F)` m) + (A^(m + 1))))
22	21	opreq1d 3960	. . . . . . . . 9 |- (m e. NN0 -> ((( + seq0 F)` (m + 1)) x. (1 - A)) = (((( + seq0 F)` m) + (A^(m + 1))) x. (1 - A)))
23		adddirt 5291	. . . . . . . . . . 11 |- (((( + seq0 F)` m) e. CC /\ (A^(m + 1)) e. CC /\ (1 - A) e. CC) -> (((( + seq0 F)` m) + (A^(m + 1))) x. (1 - A)) = (((( + seq0 F)` m) x. (1 - A)) + ((A^(m + 1)) x. (1 - A))))
24	3, 23	mp3an3 902	. . . . . . . . . 10 |- (((( + seq0 F)` m) e. CC /\ (A^(m + 1)) e. CC) -> (((( + seq0 F)` m) + (A^(m + 1))) x. (1 - A)) = (((( + seq0 F)` m) x. (1 - A)) + ((A^(m + 1)) x. (1 - A))))
25	9	ser0cl1 6496	. . . . . . . . . 10 |- (m e. NN0 -> (( + seq0 F)` m) e. CC)
26		peano2nn0 6071	. . . . . . . . . . 11 |- (m e. NN0 -> (m + 1) e. NN0)
27		expclt 6513	. . . . . . . . . . . 12 |- ((A e. CC /\ (m + 1) e. NN0) -> (A^(m + 1)) e. CC)
28	2, 27	mpan 693	. . . . . . . . . . 11 |- ((m + 1) e. NN0 -> (A^(m + 1)) e. CC)
29	26, 28	syl 10	. . . . . . . . . 10 |- (m e. NN0 -> (A^(m + 1)) e. CC)
30	24, 25, 29	sylanc 471	. . . . . . . . 9 |- (m e. NN0 -> (((( + seq0 F)` m) + (A^(m + 1))) x. (1 - A)) = (((( + seq0 F)` m) x. (1 - A)) + ((A^(m + 1)) x. (1 - A))))
31	22, 30	eqtrd 1499	. . . . . . . 8 |- (m e. NN0 -> ((( + seq0 F)` (m + 1)) x. (1 - A)) = (((( + seq0 F)` m) x. (1 - A)) + ((A^(m + 1)) x. (1 - A))))
32	31	adantr 389	. . . . . . 7 |- ((m e. NN0 /\ ((( + seq0 F)` m) x. (1 - A)) = (1 - (A^(m + 1)))) -> ((( + seq0 F)` (m + 1)) x. (1 - A)) = (((( + seq0 F)` m) x. (1 - A)) + ((A^(m + 1)) x. (1 - A))))
33		opreq1 3953	. . . . . . . 8 |- (((( + seq0 F)` m) x. (1 - A)) = (1 - (A^(m + 1))) -> (((( + seq0 F)` m) x. (1 - A)) + ((A^(m + 1)) x. (1 - A))) = ((1 - (A^(m + 1))) + ((A^(m + 1)) x. (1 - A))))
34		expp1t 6506	. . . . . . . . . . . 12 |- ((A e. CC /\ (m + 1) e. NN0) -> (A^((m + 1) + 1)) = ((A^(m + 1)) x. A))
35	2, 34	mpan 693	. . . . . . . . . . 11 |- ((m + 1) e. NN0 -> (A^((m + 1) + 1)) = ((A^(m + 1)) x. A))
36	26, 35	syl 10	. . . . . . . . . 10 |- (m e. NN0 -> (A^((m + 1) + 1)) = ((A^(m + 1)) x. A))
37	36	opreq2d 3961	. . . . . . . . 9 |- (m e. NN0 -> (1 - (A^((m + 1) + 1))) = (1 - ((A^(m + 1)) x. A)))
38		ax1id 5254	. . . . . . . . . . . . 13 |- ((A^(m + 1)) e. CC -> ((A^(m + 1)) x. 1) = (A^(m + 1)))
39	29, 38	syl 10	. . . . . . . . . . . 12 |- (m e. NN0 -> ((A^(m + 1)) x. 1) = (A^(m + 1)))
40	39	opreq1d 3960	. . . . . . . . . . 11 |- (m e. NN0 -> (((A^(m + 1)) x. 1) - ((A^(m + 1)) x. (1 - A))) = ((A^(m + 1)) - ((A^(m + 1)) x. (1 - A))))
41		subdit 5399	. . . . . . . . . . . . . 14 |- (((A^(m + 1)) e. CC /\ 1 e. CC /\ (1 - A) e. CC) -> ((A^(m + 1)) x. (1 - (1 - A))) = (((A^(m + 1)) x. 1) - ((A^(m + 1)) x. (1 - A))))
42	1, 3, 41	mp3an23 905	. . . . . . . . . . . . 13 |- ((A^(m + 1)) e. CC -> ((A^(m + 1)) x. (1 - (1 - A))) = (((A^(m + 1)) x. 1) - ((A^(m + 1)) x. (1 - A))))
43	29, 42	syl 10	. . . . . . . . . . . 12 |- (m e. NN0 -> ((A^(m + 1)) x. (1 - (1 - A))) = (((A^(m + 1)) x. 1) - ((A^(m + 1)) x. (1 - A))))
44		nncant 5441	. . . . . . . . . . . . . 14 |- ((1 e. CC /\ A e. CC) -> (1 - (1 - A)) = A)
45	1, 2, 44	mp2an 695	. . . . . . . . . . . . 13 |- (1 - (1 - A)) = A
46	45	opreq2i 3957	. . . . . . . . . . . 12 |- ((A^(m + 1)) x. (1 - (1 - A))) = ((A^(m + 1)) x. A)
47	43, 46	syl5reqr 1514	. . . . . . . . . . 11 |- (m e. NN0 -> (((A^(m + 1)) x. 1) - ((A^(m + 1)) x. (1 - A))) = ((A^(m + 1)) x. A))
48	40, 47	eqtr3d 1501	. . . . . . . . . 10 |- (m e. NN0 -> ((A^(m + 1)) - ((A^(m + 1)) x. (1 - A))) = ((A^(m + 1)) x. A))
49	48	opreq2d 3961	. . . . . . . . 9 |- (m e. NN0 -> (1 - ((A^(m + 1)) - ((A^(m + 1)) x. (1 - A)))) = (1 - ((A^(m + 1)) x. A)))
50		subsubt 5434	. . . . . . . . . . 11 |- ((1 e. CC /\ (A^(m + 1)) e. CC /\ ((A^(m + 1)) x. (1 - A)) e. CC) -> (1 - ((A^(m + 1)) - ((A^(m + 1)) x. (1 - A)))) =