This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem geoisumr

Description: The infinite sum of reciprocals 1 + ( 1 / A ) ^ 1 + ( 1 / A ) ^ 2 ... is A / ( A - 1 ) . (Contributed by rpenner, 3-Nov-2007) (Revised by Mario Carneiro, 26-Apr-2014)

Ref Expression
Assertion geoisumr 
|- ( ( A e. CC /\ 1 < ( abs ` A ) ) -> sum_ k e. NN0 ( ( 1 / A ) ^ k ) = ( A / ( A - 1 ) ) )

Proof

Step Hyp Ref Expression
1 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
2 0zd 
 |-  ( ( A e. CC /\ 1 < ( abs ` A ) ) -> 0 e. ZZ )
3 oveq2 
 |-  ( n = k -> ( ( 1 / A ) ^ n ) = ( ( 1 / A ) ^ k ) )
4 eqid 
 |-  ( n e. NN0 |-> ( ( 1 / A ) ^ n ) ) = ( n e. NN0 |-> ( ( 1 / A ) ^ n ) )
5 ovex 
 |-  ( ( 1 / A ) ^ k ) e. _V
6 3 4 5 fvmpt 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( ( 1 / A ) ^ n ) ) ` k ) = ( ( 1 / A ) ^ k ) )
7 6 adantl 
 |-  ( ( ( A e. CC /\ 1 < ( abs ` A ) ) /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( 1 / A ) ^ n ) ) ` k ) = ( ( 1 / A ) ^ k ) )
8 0le1 
 |-  0 <_ 1
9 0re 
 |-  0 e. RR
10 1re 
 |-  1 e. RR
11 9 10 lenlti 
 |-  ( 0 <_ 1 <-> -. 1 < 0 )
12 8 11 mpbi 
 |-  -. 1 < 0
13 fveq2 
 |-  ( A = 0 -> ( abs ` A ) = ( abs ` 0 ) )
14 abs0 
 |-  ( abs ` 0 ) = 0
15 13 14 eqtrdi 
 |-  ( A = 0 -> ( abs ` A ) = 0 )
16 15 breq2d 
 |-  ( A = 0 -> ( 1 < ( abs ` A ) <-> 1 < 0 ) )
17 12 16 mtbiri 
 |-  ( A = 0 -> -. 1 < ( abs ` A ) )
18 17 necon2ai 
 |-  ( 1 < ( abs ` A ) -> A =/= 0 )
19 reccl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) e. CC )
20 18 19 sylan2 
 |-  ( ( A e. CC /\ 1 < ( abs ` A ) ) -> ( 1 / A ) e. CC )
21 expcl 
 |-  ( ( ( 1 / A ) e. CC /\ k e. NN0 ) -> ( ( 1 / A ) ^ k ) e. CC )
22 20 21 sylan 
 |-  ( ( ( A e. CC /\ 1 < ( abs ` A ) ) /\ k e. NN0 ) -> ( ( 1 / A ) ^ k ) e. CC )
23 simpl 
 |-  ( ( A e. CC /\ 1 < ( abs ` A ) ) -> A e. CC )
24 simpr 
 |-  ( ( A e. CC /\ 1 < ( abs ` A ) ) -> 1 < ( abs ` A ) )
25 23 24 7 georeclim 
 |-  ( ( A e. CC /\ 1 < ( abs ` A ) ) -> seq 0 ( + , ( n e. NN0 |-> ( ( 1 / A ) ^ n ) ) ) ~~> ( A / ( A - 1 ) ) )
26 1 2 7 22 25 isumclim 
 |-  ( ( A e. CC /\ 1 < ( abs ` A ) ) -> sum_ k e. NN0 ( ( 1 / A ) ^ k ) = ( A / ( A - 1 ) ) )