Metamath Proof Explorer

Theorem geoisum1c

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

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> A e. CC )
2 simp2 
 |-  ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> R e. CC )
3 ax-1cn 
 |-  1 e. CC
4 subcl 
 |-  ( ( 1 e. CC /\ R e. CC ) -> ( 1 - R ) e. CC )
5 3 2 4 sylancr 
 |-  ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> ( 1 - R ) e. CC )
6 simp3 
 |-  ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> ( abs ` R ) < 1 )
7 1re 
 |-  1 e. RR
8 7 ltnri 
 |-  -. 1 < 1
9 abs1 
 |-  ( abs ` 1 ) = 1
10 fveq2 
 |-  ( 1 = R -> ( abs ` 1 ) = ( abs ` R ) )
11 9 10 eqtr3id 
 |-  ( 1 = R -> 1 = ( abs ` R ) )
12 11 breq1d 
 |-  ( 1 = R -> ( 1 < 1 <-> ( abs ` R ) < 1 ) )
13 8 12 mtbii 
 |-  ( 1 = R -> -. ( abs ` R ) < 1 )
14 13 necon2ai 
 |-  ( ( abs ` R ) < 1 -> 1 =/= R )
15 6 14 syl 
 |-  ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> 1 =/= R )
16 subeq0 
 |-  ( ( 1 e. CC /\ R e. CC ) -> ( ( 1 - R ) = 0 <-> 1 = R ) )
17 16 necon3bid 
 |-  ( ( 1 e. CC /\ R e. CC ) -> ( ( 1 - R ) =/= 0 <-> 1 =/= R ) )
18 3 2 17 sylancr 
 |-  ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> ( ( 1 - R ) =/= 0 <-> 1 =/= R ) )
19 15 18 mpbird 
 |-  ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> ( 1 - R ) =/= 0 )
20 1 2 5 19 divassd 
 |-  ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> ( ( A x. R ) / ( 1 - R ) ) = ( A x. ( R / ( 1 - R ) ) ) )
21 geoisum1 
 |-  ( ( R e. CC /\ ( abs ` R ) < 1 ) -> sum_ k e. NN ( R ^ k ) = ( R / ( 1 - R ) ) )
22 21 3adant1 
 |-  ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> sum_ k e. NN ( R ^ k ) = ( R / ( 1 - R ) ) )
23 22 oveq2d 
 |-  ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> ( A x. sum_ k e. NN ( R ^ k ) ) = ( A x. ( R / ( 1 - R ) ) ) )
24 nnuz 
 |-  NN = ( ZZ>= ` 1 )
25 1zzd 
 |-  ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> 1 e. ZZ )
26 oveq2 
 |-  ( n = k -> ( R ^ n ) = ( R ^ k ) )
27 eqid 
 |-  ( n e. NN |-> ( R ^ n ) ) = ( n e. NN |-> ( R ^ n ) )
28 ovex 
 |-  ( R ^ k ) e. _V
29 26 27 28 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( R ^ n ) ) ` k ) = ( R ^ k ) )
30 29 adantl 
 |-  ( ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) /\ k e. NN ) -> ( ( n e. NN |-> ( R ^ n ) ) ` k ) = ( R ^ k ) )
31 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
32 expcl 
 |-  ( ( R e. CC /\ k e. NN0 ) -> ( R ^ k ) e. CC )
33 2 31 32 syl2an 
 |-  ( ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) /\ k e. NN ) -> ( R ^ k ) e. CC )
34 1nn0 
 |-  1 e. NN0
35 34 a1i 
 |-  ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> 1 e. NN0 )
36 elnnuz 
 |-  ( k e. NN <-> k e. ( ZZ>= ` 1 ) )
37 36 30 sylan2br 
 |-  ( ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) /\ k e. ( ZZ>= ` 1 ) ) -> ( ( n e. NN |-> ( R ^ n ) ) ` k ) = ( R ^ k ) )
38 2 6 35 37 geolim2 
 |-  ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> seq 1 ( + , ( n e. NN |-> ( R ^ n ) ) ) ~~> ( ( R ^ 1 ) / ( 1 - R ) ) )
39 seqex 
 |-  seq 1 ( + , ( n e. NN |-> ( R ^ n ) ) ) e. _V
40 ovex 
 |-  ( ( R ^ 1 ) / ( 1 - R ) ) e. _V
41 39 40 breldm 
 |-  ( seq 1 ( + , ( n e. NN |-> ( R ^ n ) ) ) ~~> ( ( R ^ 1 ) / ( 1 - R ) ) -> seq 1 ( + , ( n e. NN |-> ( R ^ n ) ) ) e. dom ~~> )
42 38 41 syl 
 |-  ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> seq 1 ( + , ( n e. NN |-> ( R ^ n ) ) ) e. dom ~~> )
43 24 25 30 33 42 1 isummulc2 
 |-  ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> ( A x. sum_ k e. NN ( R ^ k ) ) = sum_ k e. NN ( A x. ( R ^ k ) ) )
44 20 23 43 3eqtr2rd 
 |-  ( ( A e. CC /\ R e. CC /\ ( abs ` R ) < 1 ) -> sum_ k e. NN ( A x. ( R ^ k ) ) = ( ( A x. R ) / ( 1 - R ) ) )