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 
|- ( ph -> A e. CC )
georeclim.2 
|- ( ph -> 1 < ( abs ` A ) )
georeclim.3 
|- ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( ( 1 / A ) ^ k ) )
Assertion georeclim 
|- ( ph -> seq 0 ( + , F ) ~~> ( A / ( A - 1 ) ) )

Proof

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