Metamath Proof Explorer

Theorem logtayl2

Description: Power series expression for the logarithm. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Hypothesis logtayl2.s 
|- S = ( 1 ( ball ` ( abs o. - ) ) 1 )
Assertion logtayl2 
|- ( A e. S -> seq 1 ( + , ( k e. NN |-> ( ( ( -u 1 ^ ( k - 1 ) ) / k ) x. ( ( A - 1 ) ^ k ) ) ) ) ~~> ( log ` A ) )

Proof

Step Hyp Ref Expression
1 logtayl2.s 
 |-  S = ( 1 ( ball ` ( abs o. - ) ) 1 )
2 nnuz 
 |-  NN = ( ZZ>= ` 1 )
3 1zzd 
 |-  ( A e. S -> 1 e. ZZ )
4 neg1cn 
 |-  -u 1 e. CC
5 4 a1i 
 |-  ( A e. S -> -u 1 e. CC )
6 ax-1cn 
 |-  1 e. CC
7 1 eleq2i 
 |-  ( A e. S <-> A e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
8 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
9 1xr 
 |-  1 e. RR*
10 elbl 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 1 e. CC /\ 1 e. RR* ) -> ( A e. ( 1 ( ball ` ( abs o. - ) ) 1 ) <-> ( A e. CC /\ ( 1 ( abs o. - ) A ) < 1 ) ) )
11 8 6 9 10 mp3an 
 |-  ( A e. ( 1 ( ball ` ( abs o. - ) ) 1 ) <-> ( A e. CC /\ ( 1 ( abs o. - ) A ) < 1 ) )
12 7 11 bitri 
 |-  ( A e. S <-> ( A e. CC /\ ( 1 ( abs o. - ) A ) < 1 ) )
13 12 simplbi 
 |-  ( A e. S -> A e. CC )
14 subcl 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( 1 - A ) e. CC )
15 6 13 14 sylancr 
 |-  ( A e. S -> ( 1 - A ) e. CC )
16 eqid 
 |-  ( abs o. - ) = ( abs o. - )
17 16 cnmetdval 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( 1 ( abs o. - ) A ) = ( abs ` ( 1 - A ) ) )
18 6 13 17 sylancr 
 |-  ( A e. S -> ( 1 ( abs o. - ) A ) = ( abs ` ( 1 - A ) ) )
19 12 simprbi 
 |-  ( A e. S -> ( 1 ( abs o. - ) A ) < 1 )
20 18 19 eqbrtrrd 
 |-  ( A e. S -> ( abs ` ( 1 - A ) ) < 1 )
21 logtayl 
 |-  ( ( ( 1 - A ) e. CC /\ ( abs ` ( 1 - A ) ) < 1 ) -> seq 1 ( + , ( k e. NN |-> ( ( ( 1 - A ) ^ k ) / k ) ) ) ~~> -u ( log ` ( 1 - ( 1 - A ) ) ) )
22 15 20 21 syl2anc 
 |-  ( A e. S -> seq 1 ( + , ( k e. NN |-> ( ( ( 1 - A ) ^ k ) / k ) ) ) ~~> -u ( log ` ( 1 - ( 1 - A ) ) ) )
23 nncan 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( 1 - ( 1 - A ) ) = A )
24 6 13 23 sylancr 
 |-  ( A e. S -> ( 1 - ( 1 - A ) ) = A )
25 24 fveq2d 
 |-  ( A e. S -> ( log ` ( 1 - ( 1 - A ) ) ) = ( log ` A ) )
26 25 negeqd 
 |-  ( A e. S -> -u ( log ` ( 1 - ( 1 - A ) ) ) = -u ( log ` A ) )
27 22 26 breqtrd 
 |-  ( A e. S -> seq 1 ( + , ( k e. NN |-> ( ( ( 1 - A ) ^ k ) / k ) ) ) ~~> -u ( log ` A ) )
28 oveq2 
 |-  ( k = n -> ( ( 1 - A ) ^ k ) = ( ( 1 - A ) ^ n ) )
29 id 
 |-  ( k = n -> k = n )
30 28 29 oveq12d 
 |-  ( k = n -> ( ( ( 1 - A ) ^ k ) / k ) = ( ( ( 1 - A ) ^ n ) / n ) )
31 eqid 
 |-  ( k e. NN |-> ( ( ( 1 - A ) ^ k ) / k ) ) = ( k e. NN |-> ( ( ( 1 - A ) ^ k ) / k ) )
32 ovex 
 |-  ( ( ( 1 - A ) ^ n ) / n ) e. _V
33 30 31 32 fvmpt 
 |-  ( n e. NN -> ( ( k e. NN |-> ( ( ( 1 - A ) ^ k ) / k ) ) ` n ) = ( ( ( 1 - A ) ^ n ) / n ) )
34 33 adantl 
 |-  ( ( A e. S /\ n e. NN ) -> ( ( k e. NN |-> ( ( ( 1 - A ) ^ k ) / k ) ) ` n ) = ( ( ( 1 - A ) ^ n ) / n ) )
35 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
36 expcl 
 |-  ( ( ( 1 - A ) e. CC /\ n e. NN0 ) -> ( ( 1 - A ) ^ n ) e. CC )
37 15 35 36 syl2an 
 |-  ( ( A e. S /\ n e. NN ) -> ( ( 1 - A ) ^ n ) e. CC )
38 nncn 
 |-  ( n e. NN -> n e. CC )
39 38 adantl 
 |-  ( ( A e. S /\ n e. NN ) -> n e. CC )
40 nnne0 
 |-  ( n e. NN -> n =/= 0 )
41 40 adantl 
 |-  ( ( A e. S /\ n e. NN ) -> n =/= 0 )
42 37 39 41 divcld 
 |-  ( ( A e. S /\ n e. NN ) -> ( ( ( 1 - A ) ^ n ) / n ) e. CC )
43 34 42 eqeltrd 
 |-  ( ( A e. S /\ n e. NN ) -> ( ( k e. NN |-> ( ( ( 1 - A ) ^ k ) / k ) ) ` n ) e. CC )
44 37 39 41 divnegd 
 |-  ( ( A e. S /\ n e. NN ) -> -u ( ( ( 1 - A ) ^ n ) / n ) = ( -u ( ( 1 - A ) ^ n ) / n ) )
45 42 mulm1d 
 |-  ( ( A e. S /\ n e. NN ) -> ( -u 1 x. ( ( ( 1 - A ) ^ n ) / n ) ) = -u ( ( ( 1 - A ) ^ n ) / n ) )
46 35 adantl 
 |-  ( ( A e. S /\ n e. NN ) -> n e. NN0 )
47 expcl 
 |-  ( ( -u 1 e. CC /\ n e. NN0 ) -> ( -u 1 ^ n ) e. CC )
48 4 46 47 sylancr 
 |-  ( ( A e. S /\ n e. NN ) -> ( -u 1 ^ n ) e. CC )
49 subcl 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( A - 1 ) e. CC )
50 13 6 49 sylancl 
 |-  ( A e. S -> ( A - 1 ) e. CC )
51 expcl 
 |-  ( ( ( A - 1 ) e. CC /\ n e. NN0 ) -> ( ( A - 1 ) ^ n ) e. CC )
52 50 35 51 syl2an 
 |-  ( ( A e. S /\ n e. NN ) -> ( ( A - 1 ) ^ n ) e. CC )
53 48 52 mulneg1d 
 |-  ( ( A e. S /\ n e. NN ) -> ( -u ( -u 1 ^ n ) x. ( ( A - 1 ) ^ n ) ) = -u ( ( -u 1 ^ n ) x. ( ( A - 1 ) ^ n ) ) )
54 4 a1i 
 |-  ( ( A e. S /\ n e. NN ) -> -u 1 e. CC )
55 neg1ne0 
 |-  -u 1 =/= 0
56 55 a1i 
 |-  ( ( A e. S /\ n e. NN ) -> -u 1 =/= 0 )
57 nnz 
 |-  ( n e. NN -> n e. ZZ )
58 57 adantl 
 |-  ( ( A e. S /\ n e. NN ) -> n e. ZZ )
59 54 56 58 expm1d 
 |-  ( ( A e. S /\ n e. NN ) -> ( -u 1 ^ ( n - 1 ) ) = ( ( -u 1 ^ n ) / -u 1 ) )
60 6 a1i 
 |-  ( ( A e. S /\ n e. NN ) -> 1 e. CC )
61 ax-1ne0 
 |-  1 =/= 0
62 61 a1i 
 |-  ( ( A e. S /\ n e. NN ) -> 1 =/= 0 )
63 48 60 62 divneg2d 
 |-  ( ( A e. S /\ n e. NN ) -> -u ( ( -u 1 ^ n ) / 1 ) = ( ( -u 1 ^ n ) / -u 1 ) )
64 48 div1d 
 |-  ( ( A e. S /\ n e. NN ) -> ( ( -u 1 ^ n ) / 1 ) = ( -u 1 ^ n ) )
65 64 negeqd 
 |-  ( ( A e. S /\ n e. NN ) -> -u ( ( -u 1 ^ n ) / 1 ) = -u ( -u 1 ^ n ) )
66 59 63 65 3eqtr2d 
 |-  ( ( A e. S /\ n e. NN ) -> ( -u 1 ^ ( n - 1 ) ) = -u ( -u 1 ^ n ) )
67 66 oveq1d 
 |-  ( ( A e. S /\ n e. NN ) -> ( ( -u 1 ^ ( n - 1 ) ) x. ( ( A - 1 ) ^ n ) ) = ( -u ( -u 1 ^ n ) x. ( ( A - 1 ) ^ n ) ) )
68 50 mulm1d 
 |-  ( A e. S -> ( -u 1 x. ( A - 1 ) ) = -u ( A - 1 ) )
69 negsubdi2 
 |-  ( ( A e. CC /\ 1 e. CC ) -> -u ( A - 1 ) = ( 1 - A ) )
70 13 6 69 sylancl 
 |-  ( A e. S -> -u ( A - 1 ) = ( 1 - A ) )
71 68 70 eqtr2d 
 |-  ( A e. S -> ( 1 - A ) = ( -u 1 x. ( A - 1 ) ) )
72 71 oveq1d 
 |-  ( A e. S -> ( ( 1 - A ) ^ n ) = ( ( -u 1 x. ( A - 1 ) ) ^ n ) )
73 72 adantr 
 |-  ( ( A e. S /\ n e. NN ) -> ( ( 1 - A ) ^ n ) = ( ( -u 1 x. ( A - 1 ) ) ^ n ) )
74 mulexp 
 |-  ( ( -u 1 e. CC /\ ( A - 1 ) e. CC /\ n e. NN0 ) -> ( ( -u 1 x. ( A - 1 ) ) ^ n ) = ( ( -u 1 ^ n ) x. ( ( A - 1 ) ^ n ) ) )
75 4 50 35 74 mp3an3an 
 |-  ( ( A e. S /\ n e. NN ) -> ( ( -u 1 x. ( A - 1 ) ) ^ n ) = ( ( -u 1 ^ n ) x. ( ( A - 1 ) ^ n ) ) )
76 73 75 eqtrd 
 |-  ( ( A e. S /\ n e. NN ) -> ( ( 1 - A ) ^ n ) = ( ( -u 1 ^ n ) x. ( ( A - 1 ) ^ n ) ) )
77 76 negeqd 
 |-  ( ( A e. S /\ n e. NN ) -> -u ( ( 1 - A ) ^ n ) = -u ( ( -u 1 ^ n ) x. ( ( A - 1 ) ^ n ) ) )
78 53 67 77 3eqtr4d 
 |-  ( ( A e. S /\ n e. NN ) -> ( ( -u 1 ^ ( n - 1 ) ) x. ( ( A - 1 ) ^ n ) ) = -u ( ( 1 - A ) ^ n ) )
79 78 oveq1d 
 |-  ( ( A e. S /\ n e. NN ) -> ( ( ( -u 1 ^ ( n - 1 ) ) x. ( ( A - 1 ) ^ n ) ) / n ) = ( -u ( ( 1 - A ) ^ n ) / n ) )
80 44 45 79 3eqtr4d 
 |-  ( ( A e. S /\ n e. NN ) -> ( -u 1 x. ( ( ( 1 - A ) ^ n ) / n ) ) = ( ( ( -u 1 ^ ( n - 1 ) ) x. ( ( A - 1 ) ^ n ) ) / n ) )
81 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
82 81 adantl 
 |-  ( ( A e. S /\ n e. NN ) -> ( n - 1 ) e. NN0 )
83 expcl 
 |-  ( ( -u 1 e. CC /\ ( n - 1 ) e. NN0 ) -> ( -u 1 ^ ( n - 1 ) ) e. CC )
84 4 82 83 sylancr 
 |-  ( ( A e. S /\ n e. NN ) -> ( -u 1 ^ ( n - 1 ) ) e. CC )
85 84 52 39 41 div23d 
 |-  ( ( A e. S /\ n e. NN ) -> ( ( ( -u 1 ^ ( n - 1 ) ) x. ( ( A - 1 ) ^ n ) ) / n ) = ( ( ( -u 1 ^ ( n - 1 ) ) / n ) x. ( ( A - 1 ) ^ n ) ) )
86 80 85 eqtr2d 
 |-  ( ( A e. S /\ n e. NN ) -> ( ( ( -u 1 ^ ( n - 1 ) ) / n ) x. ( ( A - 1 ) ^ n ) ) = ( -u 1 x. ( ( ( 1 - A ) ^ n ) / n ) ) )
87 oveq1 
 |-  ( k = n -> ( k - 1 ) = ( n - 1 ) )
88 87 oveq2d 
 |-  ( k = n -> ( -u 1 ^ ( k - 1 ) ) = ( -u 1 ^ ( n - 1 ) ) )
89 88 29 oveq12d 
 |-  ( k = n -> ( ( -u 1 ^ ( k - 1 ) ) / k ) = ( ( -u 1 ^ ( n - 1 ) ) / n ) )
90 oveq2 
 |-  ( k = n -> ( ( A - 1 ) ^ k ) = ( ( A - 1 ) ^ n ) )
91 89 90 oveq12d 
 |-  ( k = n -> ( ( ( -u 1 ^ ( k - 1 ) ) / k ) x. ( ( A - 1 ) ^ k ) ) = ( ( ( -u 1 ^ ( n - 1 ) ) / n ) x. ( ( A - 1 ) ^ n ) ) )
92 eqid 
 |-  ( k e. NN |-> ( ( ( -u 1 ^ ( k - 1 ) ) / k ) x. ( ( A - 1 ) ^ k ) ) ) = ( k e. NN |-> ( ( ( -u 1 ^ ( k - 1 ) ) / k ) x. ( ( A - 1 ) ^ k ) ) )
93 ovex 
 |-  ( ( ( -u 1 ^ ( n - 1 ) ) / n ) x. ( ( A - 1 ) ^ n ) ) e. _V
94 91 92 93 fvmpt 
 |-  ( n e. NN -> ( ( k e. NN |-> ( ( ( -u 1 ^ ( k - 1 ) ) / k ) x. ( ( A - 1 ) ^ k ) ) ) ` n ) = ( ( ( -u 1 ^ ( n - 1 ) ) / n ) x. ( ( A - 1 ) ^ n ) ) )
95 94 adantl 
 |-  ( ( A e. S /\ n e. NN ) -> ( ( k e. NN |-> ( ( ( -u 1 ^ ( k - 1 ) ) / k ) x. ( ( A - 1 ) ^ k ) ) ) ` n ) = ( ( ( -u 1 ^ ( n - 1 ) ) / n ) x. ( ( A - 1 ) ^ n ) ) )
96 34 oveq2d 
 |-  ( ( A e. S /\ n e. NN ) -> ( -u 1 x. ( ( k e. NN |-> ( ( ( 1 - A ) ^ k ) / k ) ) ` n ) ) = ( -u 1 x. ( ( ( 1 - A ) ^ n ) / n ) ) )
97 86 95 96 3eqtr4d 
 |-  ( ( A e. S /\ n e. NN ) -> ( ( k e. NN |-> ( ( ( -u 1 ^ ( k - 1 ) ) / k ) x. ( ( A - 1 ) ^ k ) ) ) ` n ) = ( -u 1 x. ( ( k e. NN |-> ( ( ( 1 - A ) ^ k ) / k ) ) ` n ) ) )
98 2 3 5 27 43 97 isermulc2 
 |-  ( A e. S -> seq 1 ( + , ( k e. NN |-> ( ( ( -u 1 ^ ( k - 1 ) ) / k ) x. ( ( A - 1 ) ^ k ) ) ) ) ~~> ( -u 1 x. -u ( log ` A ) ) )
99 1 dvlog2lem 
 |-  S C_ ( CC \ ( -oo (,] 0 ) )
100 99 sseli 
 |-  ( A e. S -> A e. ( CC \ ( -oo (,] 0 ) ) )
101 eqid 
 |-  ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
102 101 logdmn0 
 |-  ( A e. ( CC \ ( -oo (,] 0 ) ) -> A =/= 0 )
103 100 102 syl 
 |-  ( A e. S -> A =/= 0 )
104 13 103 logcld 
 |-  ( A e. S -> ( log ` A ) e. CC )
105 104 negcld 
 |-  ( A e. S -> -u ( log ` A ) e. CC )
106 105 mulm1d 
 |-  ( A e. S -> ( -u 1 x. -u ( log ` A ) ) = -u -u ( log ` A ) )
107 104 negnegd 
 |-  ( A e. S -> -u -u ( log ` A ) = ( log ` A ) )
108 106 107 eqtrd 
 |-  ( A e. S -> ( -u 1 x. -u ( log ` A ) ) = ( log ` A ) )
109 98 108 breqtrd 
 |-  ( A e. S -> seq 1 ( + , ( k e. NN |-> ( ( ( -u 1 ^ ( k - 1 ) ) / k ) x. ( ( A - 1 ) ^ k ) ) ) ) ~~> ( log ` A ) )