Metamath Proof Explorer


Theorem georeclim

Description: The limit of a geometric series of reciprocals. (Contributed by Paul Chapman, 28-Dec-2007) (Revised by Mario Carneiro, 26-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 georeclim.1 φ A
2 georeclim.2 φ 1 < A
3 georeclim.3 φ k 0 F k = 1 A k
4 0le1 0 1
5 0re 0
6 1re 1
7 5 6 lenlti 0 1 ¬ 1 < 0
8 4 7 mpbi ¬ 1 < 0
9 fveq2 A = 0 A = 0
10 abs0 0 = 0
11 9 10 syl6eq A = 0 A = 0
12 11 breq2d A = 0 1 < A 1 < 0
13 8 12 mtbiri A = 0 ¬ 1 < A
14 13 necon2ai 1 < A A 0
15 2 14 syl φ A 0
16 1 15 reccld φ 1 A
17 1cnd φ 1
18 17 1 15 absdivd φ 1 A = 1 A
19 abs1 1 = 1
20 19 oveq1i 1 A = 1 A
21 18 20 syl6eq φ 1 A = 1 A
22 1 15 absrpcld φ A +
23 22 recgt1d φ 1 < A 1 A < 1
24 2 23 mpbid φ 1 A < 1
25 21 24 eqbrtrd φ 1 A < 1
26 16 25 3 geolim φ seq 0 + F 1 1 1 A
27 1 17 1 15 divsubdird φ A 1 A = A A 1 A
28 1 15 dividd φ A A = 1
29 28 oveq1d φ A A 1 A = 1 1 A
30 27 29 eqtrd φ A 1 A = 1 1 A
31 30 oveq2d φ 1 A 1 A = 1 1 1 A
32 ax-1cn 1
33 subcl A 1 A 1
34 1 32 33 sylancl φ A 1
35 6 ltnri ¬ 1 < 1
36 fveq2 A = 1 A = 1
37 36 19 syl6eq A = 1 A = 1
38 37 breq2d A = 1 1 < A 1 < 1
39 35 38 mtbiri A = 1 ¬ 1 < A
40 39 necon2ai 1 < A A 1
41 2 40 syl φ A 1
42 subeq0 A 1 A 1 = 0 A = 1
43 1 32 42 sylancl φ A 1 = 0 A = 1
44 43 necon3bid φ A 1 0 A 1
45 41 44 mpbird φ A 1 0
46 34 1 45 15 recdivd φ 1 A 1 A = A A 1
47 31 46 eqtr3d φ 1 1 1 A = A A 1
48 26 47 breqtrd φ seq 0 + F A A 1