Metamath Proof Explorer


Theorem geolim

Description: The partial sums in the infinite series 1 + A ^ 1 + A ^ 2 ... converge to ( 1 / ( 1 - A ) ) . (Contributed by NM, 15-May-2006)

Ref Expression
Hypotheses geolim.1 φ A
geolim.2 φ A < 1
geolim.3 φ k 0 F k = A k
Assertion geolim φ seq 0 + F 1 1 A

Proof

Step Hyp Ref Expression
1 geolim.1 φ A
2 geolim.2 φ A < 1
3 geolim.3 φ k 0 F k = A k
4 nn0uz 0 = 0
5 0zd φ 0
6 1 2 expcnv φ n 0 A n 0
7 ax-1cn 1
8 subcl 1 A 1 A
9 7 1 8 sylancr φ 1 A
10 1re 1
11 10 ltnri ¬ 1 < 1
12 fveq2 A = 1 A = 1
13 abs1 1 = 1
14 12 13 syl6eq A = 1 A = 1
15 14 breq1d A = 1 A < 1 1 < 1
16 11 15 mtbiri A = 1 ¬ A < 1
17 16 necon2ai A < 1 A 1
18 2 17 syl φ A 1
19 18 necomd φ 1 A
20 subeq0 1 A 1 A = 0 1 = A
21 7 1 20 sylancr φ 1 A = 0 1 = A
22 21 necon3bid φ 1 A 0 1 A
23 19 22 mpbird φ 1 A 0
24 1 9 23 divcld φ A 1 A
25 nn0ex 0 V
26 25 mptex n 0 A n + 1 1 A V
27 26 a1i φ n 0 A n + 1 1 A V
28 oveq2 n = j A n = A j
29 eqid n 0 A n = n 0 A n
30 ovex A j V
31 28 29 30 fvmpt j 0 n 0 A n j = A j
32 31 adantl φ j 0 n 0 A n j = A j
33 expcl A j 0 A j
34 1 33 sylan φ j 0 A j
35 32 34 eqeltrd φ j 0 n 0 A n j
36 expp1 A j 0 A j + 1 = A j A
37 1 36 sylan φ j 0 A j + 1 = A j A
38 1 adantr φ j 0 A
39 34 38 mulcomd φ j 0 A j A = A A j
40 37 39 eqtrd φ j 0 A j + 1 = A A j
41 40 oveq1d φ j 0 A j + 1 1 A = A A j 1 A
42 9 adantr φ j 0 1 A
43 23 adantr φ j 0 1 A 0
44 38 34 42 43 div23d φ j 0 A A j 1 A = A 1 A A j
45 41 44 eqtrd φ j 0 A j + 1 1 A = A 1 A A j
46 oveq1 n = j n + 1 = j + 1
47 46 oveq2d n = j A n + 1 = A j + 1
48 47 oveq1d n = j A n + 1 1 A = A j + 1 1 A
49 eqid n 0 A n + 1 1 A = n 0 A n + 1 1 A
50 ovex A j + 1 1 A V
51 48 49 50 fvmpt j 0 n 0 A n + 1 1 A j = A j + 1 1 A
52 51 adantl φ j 0 n 0 A n + 1 1 A j = A j + 1 1 A
53 32 oveq2d φ j 0 A 1 A n 0 A n j = A 1 A A j
54 45 52 53 3eqtr4d φ j 0 n 0 A n + 1 1 A j = A 1 A n 0 A n j
55 4 5 6 24 27 35 54 climmulc2 φ n 0 A n + 1 1 A A 1 A 0
56 24 mul01d φ A 1 A 0 = 0
57 55 56 breqtrd φ n 0 A n + 1 1 A 0
58 9 23 reccld φ 1 1 A
59 seqex seq 0 + F V
60 59 a1i φ seq 0 + F V
61 peano2nn0 j 0 j + 1 0
62 expcl A j + 1 0 A j + 1
63 1 61 62 syl2an φ j 0 A j + 1
64 63 42 43 divcld φ j 0 A j + 1 1 A
65 52 64 eqeltrd φ j 0 n 0 A n + 1 1 A j
66 nn0cn j 0 j
67 66 adantl φ j 0 j
68 pncan j 1 j + 1 - 1 = j
69 67 7 68 sylancl φ j 0 j + 1 - 1 = j
70 69 oveq2d φ j 0 0 j + 1 - 1 = 0 j
71 70 sumeq1d φ j 0 k = 0 j + 1 - 1 A k = k = 0 j A k
72 7 a1i φ j 0 1
73 72 63 42 43 divsubdird φ j 0 1 A j + 1 1 A = 1 1 A A j + 1 1 A
74 18 adantr φ j 0 A 1
75 61 adantl φ j 0 j + 1 0
76 38 74 75 geoser φ j 0 k = 0 j + 1 - 1 A k = 1 A j + 1 1 A
77 52 oveq2d φ j 0 1 1 A n 0 A n + 1 1 A j = 1 1 A A j + 1 1 A
78 73 76 77 3eqtr4d φ j 0 k = 0 j + 1 - 1 A k = 1 1 A n 0 A n + 1 1 A j
79 simpll φ j 0 k 0 j φ
80 elfznn0 k 0 j k 0
81 80 adantl φ j 0 k 0 j k 0
82 79 81 3 syl2anc φ j 0 k 0 j F k = A k
83 simpr φ j 0 j 0
84 83 4 eleqtrdi φ j 0 j 0
85 79 1 syl φ j 0 k 0 j A
86 85 81 expcld φ j 0 k 0 j A k
87 82 84 86 fsumser φ j 0 k = 0 j A k = seq 0 + F j
88 71 78 87 3eqtr3rd φ j 0 seq 0 + F j = 1 1 A n 0 A n + 1 1 A j
89 4 5 57 58 60 65 88 climsubc2 φ seq 0 + F 1 1 A 0
90 58 subid1d φ 1 1 A 0 = 1 1 A
91 89 90 breqtrd φ seq 0 + F 1 1 A