Metamath Proof Explorer

Theorem logtaylsum

Description: The Taylor series for -u log ( 1 - A ) , as an infinite sum. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion logtaylsum 
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> sum_ k e. NN ( ( A ^ k ) / k ) = -u ( log ` ( 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 id 
 |-  ( n = k -> n = k )
5 3 4 oveq12d 
 |-  ( n = k -> ( ( A ^ n ) / n ) = ( ( A ^ k ) / k ) )
6 eqid 
 |-  ( n e. NN |-> ( ( A ^ n ) / n ) ) = ( n e. NN |-> ( ( A ^ n ) / n ) )
7 ovex 
 |-  ( ( A ^ k ) / k ) e. _V
8 5 6 7 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( ( A ^ n ) / n ) ) ` k ) = ( ( A ^ k ) / k ) )
9 8 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( A ^ n ) / n ) ) ` k ) = ( ( A ^ k ) / k ) )
10 simpl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. CC )
11 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
12 expcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
13 10 11 12 syl2an 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( A ^ k ) e. CC )
14 nncn 
 |-  ( k e. NN -> k e. CC )
15 14 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> k e. CC )
16 nnne0 
 |-  ( k e. NN -> k =/= 0 )
17 16 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> k =/= 0 )
18 13 15 17 divcld 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( ( A ^ k ) / k ) e. CC )
19 logtayl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( n e. NN |-> ( ( A ^ n ) / n ) ) ) ~~> -u ( log ` ( 1 - A ) ) )
20 1 2 9 18 19 isumclim 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> sum_ k e. NN ( ( A ^ k ) / k ) = -u ( log ` ( 1 - A ) ) )