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=1ballabs1
Assertion logtayl2 ASseq1+k1k1kA1klogA

Proof

Step Hyp Ref Expression
1 logtayl2.s S=1ballabs1
2 nnuz =1
3 1zzd AS1
4 neg1cn 1
5 4 a1i AS1
6 ax-1cn 1
7 1 eleq2i ASA1ballabs1
8 cnxmet abs∞Met
9 1xr 1*
10 elbl abs∞Met11*A1ballabs1A1absA<1
11 8 6 9 10 mp3an A1ballabs1A1absA<1
12 7 11 bitri ASA1absA<1
13 12 simplbi ASA
14 subcl 1A1A
15 6 13 14 sylancr AS1A
16 eqid abs=abs
17 16 cnmetdval 1A1absA=1A
18 6 13 17 sylancr AS1absA=1A
19 12 simprbi AS1absA<1
20 18 19 eqbrtrrd AS1A<1
21 logtayl 1A1A<1seq1+k1Akklog11A
22 15 20 21 syl2anc ASseq1+k1Akklog11A
23 nncan 1A11A=A
24 6 13 23 sylancr AS11A=A
25 24 fveq2d ASlog11A=logA
26 25 negeqd ASlog11A=logA
27 22 26 breqtrd ASseq1+k1AkklogA
28 oveq2 k=n1Ak=1An
29 id k=nk=n
30 28 29 oveq12d k=n1Akk=1Ann
31 eqid k1Akk=k1Akk
32 ovex 1AnnV
33 30 31 32 fvmpt nk1Akkn=1Ann
34 33 adantl ASnk1Akkn=1Ann
35 nnnn0 nn0
36 expcl 1An01An
37 15 35 36 syl2an ASn1An
38 nncn nn
39 38 adantl ASnn
40 nnne0 nn0
41 40 adantl ASnn0
42 37 39 41 divcld ASn1Ann
43 34 42 eqeltrd ASnk1Akkn
44 37 39 41 divnegd ASn1Ann=1Ann
45 42 mulm1d ASn-11Ann=1Ann
46 35 adantl ASnn0
47 expcl 1n01n
48 4 46 47 sylancr ASn1n
49 subcl A1A1
50 13 6 49 sylancl ASA1
51 expcl A1n0A1n
52 50 35 51 syl2an ASnA1n
53 48 52 mulneg1d ASn1nA1n=1nA1n
54 4 a1i ASn1
55 neg1ne0 10
56 55 a1i ASn10
57 nnz nn
58 57 adantl ASnn
59 54 56 58 expm1d ASn1n1=1n1
60 6 a1i ASn1
61 ax-1ne0 10
62 61 a1i ASn10
63 48 60 62 divneg2d ASn1n1=1n1
64 48 div1d ASn1n1=1n
65 64 negeqd ASn1n1=1n
66 59 63 65 3eqtr2d ASn1n1=1n
67 66 oveq1d ASn1n1A1n=1nA1n
68 50 mulm1d AS-1A1=A1
69 negsubdi2 A1A1=1A
70 13 6 69 sylancl ASA1=1A
71 68 70 eqtr2d AS1A=-1A1
72 71 oveq1d AS1An=-1A1n
73 72 adantr ASn1An=-1A1n
74 mulexp 1A1n0-1A1n=1nA1n
75 4 50 35 74 mp3an3an ASn-1A1n=1nA1n
76 73 75 eqtrd ASn1An=1nA1n
77 76 negeqd ASn1An=1nA1n
78 53 67 77 3eqtr4d ASn1n1A1n=1An
79 78 oveq1d ASn1n1A1nn=1Ann
80 44 45 79 3eqtr4d ASn-11Ann=1n1A1nn
81 nnm1nn0 nn10
82 81 adantl ASnn10
83 expcl 1n101n1
84 4 82 83 sylancr ASn1n1
85 84 52 39 41 div23d ASn1n1A1nn=1n1nA1n
86 80 85 eqtr2d ASn1n1nA1n=-11Ann
87 oveq1 k=nk1=n1
88 87 oveq2d k=n1k1=1n1
89 88 29 oveq12d k=n1k1k=1n1n
90 oveq2 k=nA1k=A1n
91 89 90 oveq12d k=n1k1kA1k=1n1nA1n
92 eqid k1k1kA1k=k1k1kA1k
93 ovex 1n1nA1nV
94 91 92 93 fvmpt nk1k1kA1kn=1n1nA1n
95 94 adantl ASnk1k1kA1kn=1n1nA1n
96 34 oveq2d ASn-1k1Akkn=-11Ann
97 86 95 96 3eqtr4d ASnk1k1kA1kn=-1k1Akkn
98 2 3 5 27 43 97 isermulc2 ASseq1+k1k1kA1k-1logA
99 1 dvlog2lem S−∞0
100 99 sseli ASA−∞0
101 eqid −∞0=−∞0
102 101 logdmn0 A−∞0A0
103 100 102 syl ASA0
104 13 103 logcld ASlogA
105 104 negcld ASlogA
106 105 mulm1d AS-1logA=logA
107 104 negnegd ASlogA=logA
108 106 107 eqtrd AS-1logA=logA
109 98 108 breqtrd ASseq1+k1k1kA1klogA