Metamath Proof Explorer

Theorem geoisum

Description: The infinite sum of 1 + A ^ 1 + A ^ 2 ... is ( 1 / ( 1 - A ) ) . (Contributed by NM, 15-May-2006) (Revised by Mario Carneiro, 26-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
2 0zd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 0 e. ZZ )
3 oveq2 
 |-  ( n = k -> ( A ^ n ) = ( A ^ k ) )
4 eqid 
 |-  ( n e. NN0 |-> ( A ^ n ) ) = ( n e. NN0 |-> ( A ^ n ) )
5 ovex 
 |-  ( A ^ k ) e. _V
6 3 4 5 fvmpt 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
7 6 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
8 expcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
9 8 adantlr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( A ^ k ) e. CC )
10 simpl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. CC )
11 simpr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) < 1 )
12 10 11 7 geolim 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) ~~> ( 1 / ( 1 - A ) ) )
13 1 2 7 9 12 isumclim 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> sum_ k e. NN0 ( A ^ k ) = ( 1 / ( 1 - A ) ) )