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

Metamath Proof Explorer

Theorem geoisum1

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

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

Proof

Step Hyp Ref Expression
1 nnuz 
 |-  NN = ( ZZ>= ` 1 )
2 1zzd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 1 e. ZZ )
3 oveq2 
 |-  ( n = k -> ( A ^ n ) = ( A ^ k ) )
4 eqid 
 |-  ( n e. NN |-> ( A ^ n ) ) = ( n e. NN |-> ( A ^ n ) )
5 ovex 
 |-  ( A ^ k ) e. _V
6 3 4 5 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
7 6 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( ( n e. NN |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
8 simpl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. CC )
9 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
10 expcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
11 8 9 10 syl2an 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( A ^ k ) e. CC )
12 simpr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) < 1 )
13 1nn0 
 |-  1 e. NN0
14 13 a1i 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 1 e. NN0 )
15 elnnuz 
 |-  ( k e. NN <-> k e. ( ZZ>= ` 1 ) )
16 15 7 sylan2br 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. ( ZZ>= ` 1 ) ) -> ( ( n e. NN |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
17 8 12 14 16 geolim2 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( n e. NN |-> ( A ^ n ) ) ) ~~> ( ( A ^ 1 ) / ( 1 - A ) ) )
18 1 2 7 11 17 isumclim 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> sum_ k e. NN ( A ^ k ) = ( ( A ^ 1 ) / ( 1 - A ) ) )
19 exp1 
 |-  ( A e. CC -> ( A ^ 1 ) = A )
20 19 adantr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ^ 1 ) = A )
21 20 oveq1d 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( A ^ 1 ) / ( 1 - A ) ) = ( A / ( 1 - A ) ) )
22 18 21 eqtrd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> sum_ k e. NN ( A ^ k ) = ( A / ( 1 - A ) ) )