Theorem georeclim 7183

Description: The limit of a geometric series of reciprocals. (Contributed by Paul Chapman, 28-Dec-2007.)

Hypothesis

Ref	Expression
georeclim.1	|- F = {<.j, y>. | (j e. NN0 /\ y = ((1 / A)^j))}

Assertion

Ref	Expression
georeclim	|- ((A e. CC /\ 1 < (abs` A)) -> ( + seq0 F) ~~> (A / (A - 1)))

Distinct variable group:   A,j,y

Proof of Theorem georeclim

Step	Hyp	Ref	Expression
1		georeclim.1	. . . 4 |- F = {<.j, y>. | (j e. NN0 /\ y = ((1 / A)^j))}
2	1	geolim 7180	. . 3 |- (((1 / A) e. CC /\ (abs` (1 / A)) < 1) -> ( + seq0 F) ~~> (1 / (1 - (1 / A))))
3		gt0ne0t 5600	. . . . . 6 |- (((abs` A) e. RR /\ 0 < (abs` A)) -> (abs` A) =/= 0)
4		absclt 6776	. . . . . . 7 |- (A e. CC -> (abs` A) e. RR)
5	4	adantr 389	. . . . . 6 |- ((A e. CC /\ 1 < (abs` A)) -> (abs` A) e. RR)
6		lt01 5661	. . . . . . . 8 |- 0 < 1
7		0re 5420	. . . . . . . . . 10 |- 0 e. RR
8		1re 5415	. . . . . . . . . 10 |- 1 e. RR
9		axlttrn 5484	. . . . . . . . . 10 |- ((0 e. RR /\ 1 e. RR /\ (abs` A) e. RR) -> ((0 < 1 /\ 1 < (abs` A)) -> 0 < (abs` A)))
10	7, 8, 9	mp3an12 904	. . . . . . . . 9 |- ((abs` A) e. RR -> ((0 < 1 /\ 1 < (abs` A)) -> 0 < (abs` A)))
11	4, 10	syl 10	. . . . . . . 8 |- (A e. CC -> ((0 < 1 /\ 1 < (abs` A)) -> 0 < (abs` A)))
12	6, 11	mpani 697	. . . . . . 7 |- (A e. CC -> (1 < (abs` A) -> 0 < (abs` A)))
13	12	imp 350	. . . . . 6 |- ((A e. CC /\ 1 < (abs` A)) -> 0 < (abs` A))
14	3, 5, 13	sylanc 471	. . . . 5 |- ((A e. CC /\ 1 < (abs` A)) -> (abs` A) =/= 0)
15		abs00t 6796	. . . . . . 7 |- (A e. CC -> ((abs` A) = 0 <-> A = 0))
16	15	necon3bid 1598	. . . . . 6 |- (A e. CC -> ((abs` A) =/= 0 <-> A =/= 0))
17	16	adantr 389	. . . . 5 |- ((A e. CC /\ 1 < (abs` A)) -> ((abs` A) =/= 0 <-> A =/= 0))
18	14, 17	mpbid 195	. . . 4 |- ((A e. CC /\ 1 < (abs` A)) -> A =/= 0)
19		recclt 5692	. . . 4 |- ((A e. CC /\ A =/= 0) -> (1 / A) e. CC)
20	18, 19	syldan 467	. . 3 |- ((A e. CC /\ 1 < (abs` A)) -> (1 / A) e. CC)
21		ax1cn 5249	. . . . . . 7 |- 1 e. CC
22		absdivt 6803	. . . . . . 7 |- ((1 e. CC /\ A e. CC /\ A =/= 0) -> (abs` (1 / A)) = ((abs` 1) / (abs` A)))
23	21, 22	mp3an1 901	. . . . . 6 |- ((A e. CC /\ A =/= 0) -> (abs` (1 / A)) = ((abs` 1) / (abs` A)))
24	18, 23	syldan 467	. . . . 5 |- ((A e. CC /\ 1 < (abs` A)) -> (abs` (1 / A)) = ((abs` 1) / (abs` A)))
25	7, 8, 6	ltlei 5562	. . . . . . 7 |- 0 <_ 1
26		absidt 6805	. . . . . . 7 |- ((1 e. RR /\ 0 <_ 1) -> (abs` 1) = 1)
27	8, 25, 26	mp2an 696	. . . . . 6 |- (abs` 1) = 1
28	27	opreq1i 3962	. . . . 5 |- ((abs` 1) / (abs` A)) = (1 / (abs` A))
29	24, 28	syl6eq 1520	. . . 4 |- ((A e. CC /\ 1 < (abs` A)) -> (abs` (1 / A)) = (1 / (abs` A)))
30		recgt1t 5855	. . . . . . . . 9 |- (((abs` A) e. RR /\ 0 < (abs` A)) -> (1 < (abs` A) <-> (1 / (abs` A)) < 1))
31	30, 5, 13	sylanc 471	. . . . . . . 8 |- ((A e. CC /\ 1 < (abs` A)) -> (1 < (abs` A) <-> (1 / (abs` A)) < 1))
32	31	biimpd 153	. . . . . . 7 |- ((A e. CC /\ 1 < (abs` A)) -> (1 < (abs` A) -> (1 / (abs` A)) < 1))
33	32	ex 373	. . . . . 6 |- (A e. CC -> (1 < (abs` A) -> (1 < (abs` A) -> (1 / (abs` A)) < 1)))
34	33	pm2.43d 65	. . . . 5 |- (A e. CC -> (1 < (abs` A) -> (1 / (abs` A)) < 1))
35	34	imp 350	. . . 4 |- ((A e. CC /\ 1 < (abs` A)) -> (1 / (abs` A)) < 1)
36	29, 35	eqbrtrd 2630	. . 3 |- ((A e. CC /\ 1 < (abs` A)) -> (abs` (1 / A)) < 1)
37	2, 20, 36	sylanc 471	. 2 |- ((A e. CC /\ 1 < (abs` A)) -> ( + seq0 F) ~~> (1 / (1 - (1 / A))))
38		dividt 5730	. . . . . 6 |- ((A e. CC /\ A =/= 0) -> (A / A) = 1)
39	18, 38	syldan 467	. . . . 5 |- ((A e. CC /\ 1 < (abs` A)) -> (A / A) = 1)
40	39	opreq2d 3967	. . . 4 |- ((A e. CC /\ 1 < (abs` A)) -> ((1 / (1 - (1 / A))) / (A / A)) = ((1 / (1 - (1 / A))) / 1))
41		divdivdivt 5749	. . . . 5 |- ((((1 e. CC /\ (1 - (1 / A)) e. CC) /\ (A e. CC /\ A e. CC)) /\ ((1 - (1 / A)) =/= 0 /\ A =/= 0 /\ A =/= 0)) -> ((1 / (1 - (1 / A))) / (A / A)) = ((1 x. A) / ((1 - (1 / A)) x. A)))
42		subclt 5347	. . . . . . . 8 |- ((1 e. CC /\ (1 / A) e. CC) -> (1 - (1 / A)) e. CC)
43	21	a1i 8	. . . . . . . 8 |- ((A e. CC /\ 1 < (abs` A)) -> 1 e. CC)
44	42, 43, 20	sylanc 471	. . . . . . 7 |- ((A e. CC /\ 1 < (abs` A)) -> (1 - (1 / A)) e. CC)
45	44, 21	jctil 292	. . . . . 6 |- ((A e. CC /\ 1 < (abs` A)) -> (1 e. CC /\ (1 - (1 / A)) e. CC))
46		pm3.26 319	. . . . . . 7 |- ((A e. CC /\ 1 < (abs` A)) -> A e. CC)
47	46, 46	jca 288	. . . . . 6 |- ((A e. CC /\ 1 < (abs` A)) -> (A e. CC /\ A e. CC))
48	45, 47	jca 288	. . . . 5 |- ((A e. CC /\ 1 < (abs` A)) -> ((1 e. CC /\ (1 - (1 / A)) e. CC) /\ (A e. CC /\ A e. CC)))
49		abssubne0t 6828	. . . . . . . 8 |- (((1 / A) e. CC /\ 1 e. RR /\ (abs` (1 / A)) < 1) -> (1 - (1 / A)) =/= 0)
50	8, 49	mp3an2 902	. . . . . . 7 |- (((1 / A) e. CC /\ (abs` (1 / A)) < 1) -> (1 - (1 / A)) =/= 0)
51	50, 20, 36	sylanc 471	. . . . . 6 |- ((A e. CC /\ 1 < (abs` A)) -> (1 - (1 / A)) =/= 0)
52	51, 18, 18	3jca 818	. . . . 5 |- ((A e. CC /\ 1 < (abs` A)) -> ((1 - (1 / A)) =/= 0 /\ A =/= 0 /\ A =/= 0))
53	41, 48, 52	sylanc 471	. . . 4 |- ((A e. CC /\ 1 < (abs` A)) -> ((1 / (1 - (1 / A))) / (A / A)) = ((1 x. A) / ((1 - (1 / A)) x. A)))
54		recclt 5692	. . . . . 6 |- (((1 - (1 / A)) e. CC /\ (1 - (1 / A)) =/= 0) -> (1 / (1 - (1 / A))) e. CC)
55	54, 44, 51	sylanc 471	. . . . 5 |- ((A e. CC /\ 1 < (abs` A)) -> (1 / (1 - (1 / A))) e. CC)
56		div1t 5737	. . . . 5 |- ((1 / (1 - (1 / A))) e. CC -> ((1 / (1 - (1 / A))) / 1) = (1 / (1 - (1 / A))))
57	55, 56	syl 10	. . . 4 |- ((A e. CC /\ 1 < (abs` A)) -> ((1 / (1 - (1 / A))) / 1) = (1 / (1 - (1 / A))))
58	40, 53, 57	3eqtr3rd 1513	. . 3 |- ((A e. CC /\ 1 < (abs` A)) -> (1 / (1 - (1 / A))) = ((1 x. A) / ((1 - (1 / A)) x. A)))
59		mulid2t 5397	. . . . 5 |- (A e. CC -> (1 x. A) = A)
60	59	adantr 389	. . . 4 |- ((A e. CC /\ 1 < (abs` A)) -> (1 x. A) = A)
61		subdirt 5408	. . . . . 6 |- ((1 e. CC /\ (1 / A) e. CC /\ A e. CC) -> ((1 - (1 / A)) x. A) = ((1 x. A) - ((1 / A) x. A)))
62	61, 43, 20, 46	syl3anc 857	. . . . 5 |- ((A e. CC /\ 1 < (abs` A)) -> ((1 - (1 / A)) x. A) = ((1 x. A) - ((1 / A) x. A)))
63		recid2t 5707	. . . . . . 7 |- ((A e. CC /\ A =/= 0) -> ((1 /