Metamath Proof Explorer

Theorem logtayl2

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

Ref Expression
Hypothesis logtayl2.s ⊒ 𝑆 = ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 )
Assertion logtayl2 ( 𝐴 ∈ 𝑆 β†’ seq 1 ( + , ( π‘˜ ∈ β„• ↦ ( ( ( - 1 ↑ ( π‘˜ βˆ’ 1 ) ) / π‘˜ ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ π‘˜ ) ) ) ) ⇝ ( log β€˜ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 logtayl2.s ⊒ 𝑆 = ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 )
2 nnuz ⊒ β„• = ( β„€β‰₯ β€˜ 1 )
3 1zzd ⊒ ( 𝐴 ∈ 𝑆 β†’ 1 ∈ β„€ )
4 neg1cn ⊒ - 1 ∈ β„‚
5 4 a1i ⊒ ( 𝐴 ∈ 𝑆 β†’ - 1 ∈ β„‚ )
6 ax-1cn ⊒ 1 ∈ β„‚
7 1 eleq2i ⊒ ( 𝐴 ∈ 𝑆 ↔ 𝐴 ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) )
8 cnxmet ⊒ ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ )
9 1xr ⊒ 1 ∈ ℝ*
10 elbl ⊒ ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 1 ∈ β„‚ ∧ 1 ∈ ℝ* ) β†’ ( 𝐴 ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↔ ( 𝐴 ∈ β„‚ ∧ ( 1 ( abs ∘ βˆ’ ) 𝐴 ) < 1 ) ) )
11 8 6 9 10 mp3an ⊒ ( 𝐴 ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↔ ( 𝐴 ∈ β„‚ ∧ ( 1 ( abs ∘ βˆ’ ) 𝐴 ) < 1 ) )
12 7 11 bitri ⊒ ( 𝐴 ∈ 𝑆 ↔ ( 𝐴 ∈ β„‚ ∧ ( 1 ( abs ∘ βˆ’ ) 𝐴 ) < 1 ) )
13 12 simplbi ⊒ ( 𝐴 ∈ 𝑆 β†’ 𝐴 ∈ β„‚ )
14 subcl ⊒ ( ( 1 ∈ β„‚ ∧ 𝐴 ∈ β„‚ ) β†’ ( 1 βˆ’ 𝐴 ) ∈ β„‚ )
15 6 13 14 sylancr ⊒ ( 𝐴 ∈ 𝑆 β†’ ( 1 βˆ’ 𝐴 ) ∈ β„‚ )
16 eqid ⊒ ( abs ∘ βˆ’ ) = ( abs ∘ βˆ’ )
17 16 cnmetdval ⊒ ( ( 1 ∈ β„‚ ∧ 𝐴 ∈ β„‚ ) β†’ ( 1 ( abs ∘ βˆ’ ) 𝐴 ) = ( abs β€˜ ( 1 βˆ’ 𝐴 ) ) )
18 6 13 17 sylancr ⊒ ( 𝐴 ∈ 𝑆 β†’ ( 1 ( abs ∘ βˆ’ ) 𝐴 ) = ( abs β€˜ ( 1 βˆ’ 𝐴 ) ) )
19 12 simprbi ⊒ ( 𝐴 ∈ 𝑆 β†’ ( 1 ( abs ∘ βˆ’ ) 𝐴 ) < 1 )
20 18 19 eqbrtrrd ⊒ ( 𝐴 ∈ 𝑆 β†’ ( abs β€˜ ( 1 βˆ’ 𝐴 ) ) < 1 )
21 logtayl ⊒ ( ( ( 1 βˆ’ 𝐴 ) ∈ β„‚ ∧ ( abs β€˜ ( 1 βˆ’ 𝐴 ) ) < 1 ) β†’ seq 1 ( + , ( π‘˜ ∈ β„• ↦ ( ( ( 1 βˆ’ 𝐴 ) ↑ π‘˜ ) / π‘˜ ) ) ) ⇝ - ( log β€˜ ( 1 βˆ’ ( 1 βˆ’ 𝐴 ) ) ) )
22 15 20 21 syl2anc ⊒ ( 𝐴 ∈ 𝑆 β†’ seq 1 ( + , ( π‘˜ ∈ β„• ↦ ( ( ( 1 βˆ’ 𝐴 ) ↑ π‘˜ ) / π‘˜ ) ) ) ⇝ - ( log β€˜ ( 1 βˆ’ ( 1 βˆ’ 𝐴 ) ) ) )
23 nncan ⊒ ( ( 1 ∈ β„‚ ∧ 𝐴 ∈ β„‚ ) β†’ ( 1 βˆ’ ( 1 βˆ’ 𝐴 ) ) = 𝐴 )
24 6 13 23 sylancr ⊒ ( 𝐴 ∈ 𝑆 β†’ ( 1 βˆ’ ( 1 βˆ’ 𝐴 ) ) = 𝐴 )
25 24 fveq2d ⊒ ( 𝐴 ∈ 𝑆 β†’ ( log β€˜ ( 1 βˆ’ ( 1 βˆ’ 𝐴 ) ) ) = ( log β€˜ 𝐴 ) )
26 25 negeqd ⊒ ( 𝐴 ∈ 𝑆 β†’ - ( log β€˜ ( 1 βˆ’ ( 1 βˆ’ 𝐴 ) ) ) = - ( log β€˜ 𝐴 ) )
27 22 26 breqtrd ⊒ ( 𝐴 ∈ 𝑆 β†’ seq 1 ( + , ( π‘˜ ∈ β„• ↦ ( ( ( 1 βˆ’ 𝐴 ) ↑ π‘˜ ) / π‘˜ ) ) ) ⇝ - ( log β€˜ 𝐴 ) )
28 oveq2 ⊒ ( π‘˜ = 𝑛 β†’ ( ( 1 βˆ’ 𝐴 ) ↑ π‘˜ ) = ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) )
29 id ⊒ ( π‘˜ = 𝑛 β†’ π‘˜ = 𝑛 )
30 28 29 oveq12d ⊒ ( π‘˜ = 𝑛 β†’ ( ( ( 1 βˆ’ 𝐴 ) ↑ π‘˜ ) / π‘˜ ) = ( ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) / 𝑛 ) )
31 eqid ⊒ ( π‘˜ ∈ β„• ↦ ( ( ( 1 βˆ’ 𝐴 ) ↑ π‘˜ ) / π‘˜ ) ) = ( π‘˜ ∈ β„• ↦ ( ( ( 1 βˆ’ 𝐴 ) ↑ π‘˜ ) / π‘˜ ) )
32 ovex ⊒ ( ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ∈ V
33 30 31 32 fvmpt ⊒ ( 𝑛 ∈ β„• β†’ ( ( π‘˜ ∈ β„• ↦ ( ( ( 1 βˆ’ 𝐴 ) ↑ π‘˜ ) / π‘˜ ) ) β€˜ 𝑛 ) = ( ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) / 𝑛 ) )
34 33 adantl ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( ( π‘˜ ∈ β„• ↦ ( ( ( 1 βˆ’ 𝐴 ) ↑ π‘˜ ) / π‘˜ ) ) β€˜ 𝑛 ) = ( ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) / 𝑛 ) )
35 nnnn0 ⊒ ( 𝑛 ∈ β„• β†’ 𝑛 ∈ β„•0 )
36 expcl ⊒ ( ( ( 1 βˆ’ 𝐴 ) ∈ β„‚ ∧ 𝑛 ∈ β„•0 ) β†’ ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) ∈ β„‚ )
37 15 35 36 syl2an ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) ∈ β„‚ )
38 nncn ⊒ ( 𝑛 ∈ β„• β†’ 𝑛 ∈ β„‚ )
39 38 adantl ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ 𝑛 ∈ β„‚ )
40 nnne0 ⊒ ( 𝑛 ∈ β„• β†’ 𝑛 β‰  0 )
41 40 adantl ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ 𝑛 β‰  0 )
42 37 39 41 divcld ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ∈ β„‚ )
43 34 42 eqeltrd ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( ( π‘˜ ∈ β„• ↦ ( ( ( 1 βˆ’ 𝐴 ) ↑ π‘˜ ) / π‘˜ ) ) β€˜ 𝑛 ) ∈ β„‚ )
44 37 39 41 divnegd ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ - ( ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) / 𝑛 ) = ( - ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) / 𝑛 ) )
45 42 mulm1d ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( - 1 Β· ( ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) = - ( ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) / 𝑛 ) )
46 35 adantl ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ 𝑛 ∈ β„•0 )
47 expcl ⊒ ( ( - 1 ∈ β„‚ ∧ 𝑛 ∈ β„•0 ) β†’ ( - 1 ↑ 𝑛 ) ∈ β„‚ )
48 4 46 47 sylancr ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( - 1 ↑ 𝑛 ) ∈ β„‚ )
49 subcl ⊒ ( ( 𝐴 ∈ β„‚ ∧ 1 ∈ β„‚ ) β†’ ( 𝐴 βˆ’ 1 ) ∈ β„‚ )
50 13 6 49 sylancl ⊒ ( 𝐴 ∈ 𝑆 β†’ ( 𝐴 βˆ’ 1 ) ∈ β„‚ )
51 expcl ⊒ ( ( ( 𝐴 βˆ’ 1 ) ∈ β„‚ ∧ 𝑛 ∈ β„•0 ) β†’ ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ∈ β„‚ )
52 50 35 51 syl2an ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ∈ β„‚ )
53 48 52 mulneg1d ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( - ( - 1 ↑ 𝑛 ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) = - ( ( - 1 ↑ 𝑛 ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) )
54 4 a1i ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ - 1 ∈ β„‚ )
55 neg1ne0 ⊒ - 1 β‰  0
56 55 a1i ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ - 1 β‰  0 )
57 nnz ⊒ ( 𝑛 ∈ β„• β†’ 𝑛 ∈ β„€ )
58 57 adantl ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ 𝑛 ∈ β„€ )
59 54 56 58 expm1d ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) = ( ( - 1 ↑ 𝑛 ) / - 1 ) )
60 6 a1i ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ 1 ∈ β„‚ )
61 ax-1ne0 ⊒ 1 β‰  0
62 61 a1i ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ 1 β‰  0 )
63 48 60 62 divneg2d ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ - ( ( - 1 ↑ 𝑛 ) / 1 ) = ( ( - 1 ↑ 𝑛 ) / - 1 ) )
64 48 div1d ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( ( - 1 ↑ 𝑛 ) / 1 ) = ( - 1 ↑ 𝑛 ) )
65 64 negeqd ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ - ( ( - 1 ↑ 𝑛 ) / 1 ) = - ( - 1 ↑ 𝑛 ) )
66 59 63 65 3eqtr2d ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) = - ( - 1 ↑ 𝑛 ) )
67 66 oveq1d ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) = ( - ( - 1 ↑ 𝑛 ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) )
68 50 mulm1d ⊒ ( 𝐴 ∈ 𝑆 β†’ ( - 1 Β· ( 𝐴 βˆ’ 1 ) ) = - ( 𝐴 βˆ’ 1 ) )
69 negsubdi2 ⊒ ( ( 𝐴 ∈ β„‚ ∧ 1 ∈ β„‚ ) β†’ - ( 𝐴 βˆ’ 1 ) = ( 1 βˆ’ 𝐴 ) )
70 13 6 69 sylancl ⊒ ( 𝐴 ∈ 𝑆 β†’ - ( 𝐴 βˆ’ 1 ) = ( 1 βˆ’ 𝐴 ) )
71 68 70 eqtr2d ⊒ ( 𝐴 ∈ 𝑆 β†’ ( 1 βˆ’ 𝐴 ) = ( - 1 Β· ( 𝐴 βˆ’ 1 ) ) )
72 71 oveq1d ⊒ ( 𝐴 ∈ 𝑆 β†’ ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) = ( ( - 1 Β· ( 𝐴 βˆ’ 1 ) ) ↑ 𝑛 ) )
73 72 adantr ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) = ( ( - 1 Β· ( 𝐴 βˆ’ 1 ) ) ↑ 𝑛 ) )
74 mulexp ⊒ ( ( - 1 ∈ β„‚ ∧ ( 𝐴 βˆ’ 1 ) ∈ β„‚ ∧ 𝑛 ∈ β„•0 ) β†’ ( ( - 1 Β· ( 𝐴 βˆ’ 1 ) ) ↑ 𝑛 ) = ( ( - 1 ↑ 𝑛 ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) )
75 4 50 35 74 mp3an3an ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( ( - 1 Β· ( 𝐴 βˆ’ 1 ) ) ↑ 𝑛 ) = ( ( - 1 ↑ 𝑛 ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) )
76 73 75 eqtrd ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) = ( ( - 1 ↑ 𝑛 ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) )
77 76 negeqd ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ - ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) = - ( ( - 1 ↑ 𝑛 ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) )
78 53 67 77 3eqtr4d ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) = - ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) )
79 78 oveq1d ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( ( ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) / 𝑛 ) = ( - ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) / 𝑛 ) )
80 44 45 79 3eqtr4d ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( - 1 Β· ( ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) = ( ( ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) / 𝑛 ) )
81 nnm1nn0 ⊒ ( 𝑛 ∈ β„• β†’ ( 𝑛 βˆ’ 1 ) ∈ β„•0 )
82 81 adantl ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( 𝑛 βˆ’ 1 ) ∈ β„•0 )
83 expcl ⊒ ( ( - 1 ∈ β„‚ ∧ ( 𝑛 βˆ’ 1 ) ∈ β„•0 ) β†’ ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) ∈ β„‚ )
84 4 82 83 sylancr ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) ∈ β„‚ )
85 84 52 39 41 div23d ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( ( ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) / 𝑛 ) = ( ( ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) / 𝑛 ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) )
86 80 85 eqtr2d ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( ( ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) / 𝑛 ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) = ( - 1 Β· ( ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) )
87 oveq1 ⊒ ( π‘˜ = 𝑛 β†’ ( π‘˜ βˆ’ 1 ) = ( 𝑛 βˆ’ 1 ) )
88 87 oveq2d ⊒ ( π‘˜ = 𝑛 β†’ ( - 1 ↑ ( π‘˜ βˆ’ 1 ) ) = ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) )
89 88 29 oveq12d ⊒ ( π‘˜ = 𝑛 β†’ ( ( - 1 ↑ ( π‘˜ βˆ’ 1 ) ) / π‘˜ ) = ( ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) / 𝑛 ) )
90 oveq2 ⊒ ( π‘˜ = 𝑛 β†’ ( ( 𝐴 βˆ’ 1 ) ↑ π‘˜ ) = ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) )
91 89 90 oveq12d ⊒ ( π‘˜ = 𝑛 β†’ ( ( ( - 1 ↑ ( π‘˜ βˆ’ 1 ) ) / π‘˜ ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ π‘˜ ) ) = ( ( ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) / 𝑛 ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) )
92 eqid ⊒ ( π‘˜ ∈ β„• ↦ ( ( ( - 1 ↑ ( π‘˜ βˆ’ 1 ) ) / π‘˜ ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ π‘˜ ) ) ) = ( π‘˜ ∈ β„• ↦ ( ( ( - 1 ↑ ( π‘˜ βˆ’ 1 ) ) / π‘˜ ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ π‘˜ ) ) )
93 ovex ⊒ ( ( ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) / 𝑛 ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) ∈ V
94 91 92 93 fvmpt ⊒ ( 𝑛 ∈ β„• β†’ ( ( π‘˜ ∈ β„• ↦ ( ( ( - 1 ↑ ( π‘˜ βˆ’ 1 ) ) / π‘˜ ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ π‘˜ ) ) ) β€˜ 𝑛 ) = ( ( ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) / 𝑛 ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) )
95 94 adantl ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( ( π‘˜ ∈ β„• ↦ ( ( ( - 1 ↑ ( π‘˜ βˆ’ 1 ) ) / π‘˜ ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ π‘˜ ) ) ) β€˜ 𝑛 ) = ( ( ( - 1 ↑ ( 𝑛 βˆ’ 1 ) ) / 𝑛 ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ 𝑛 ) ) )
96 34 oveq2d ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( - 1 Β· ( ( π‘˜ ∈ β„• ↦ ( ( ( 1 βˆ’ 𝐴 ) ↑ π‘˜ ) / π‘˜ ) ) β€˜ 𝑛 ) ) = ( - 1 Β· ( ( ( 1 βˆ’ 𝐴 ) ↑ 𝑛 ) / 𝑛 ) ) )
97 86 95 96 3eqtr4d ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝑛 ∈ β„• ) β†’ ( ( π‘˜ ∈ β„• ↦ ( ( ( - 1 ↑ ( π‘˜ βˆ’ 1 ) ) / π‘˜ ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ π‘˜ ) ) ) β€˜ 𝑛 ) = ( - 1 Β· ( ( π‘˜ ∈ β„• ↦ ( ( ( 1 βˆ’ 𝐴 ) ↑ π‘˜ ) / π‘˜ ) ) β€˜ 𝑛 ) ) )
98 2 3 5 27 43 97 isermulc2 ⊒ ( 𝐴 ∈ 𝑆 β†’ seq 1 ( + , ( π‘˜ ∈ β„• ↦ ( ( ( - 1 ↑ ( π‘˜ βˆ’ 1 ) ) / π‘˜ ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ π‘˜ ) ) ) ) ⇝ ( - 1 Β· - ( log β€˜ 𝐴 ) ) )
99 1 dvlog2lem ⊒ 𝑆 βŠ† ( β„‚ βˆ– ( -∞ (,] 0 ) )
100 99 sseli ⊒ ( 𝐴 ∈ 𝑆 β†’ 𝐴 ∈ ( β„‚ βˆ– ( -∞ (,] 0 ) ) )
101 eqid ⊒ ( β„‚ βˆ– ( -∞ (,] 0 ) ) = ( β„‚ βˆ– ( -∞ (,] 0 ) )
102 101 logdmn0 ⊒ ( 𝐴 ∈ ( β„‚ βˆ– ( -∞ (,] 0 ) ) β†’ 𝐴 β‰  0 )
103 100 102 syl ⊒ ( 𝐴 ∈ 𝑆 β†’ 𝐴 β‰  0 )
104 13 103 logcld ⊒ ( 𝐴 ∈ 𝑆 β†’ ( log β€˜ 𝐴 ) ∈ β„‚ )
105 104 negcld ⊒ ( 𝐴 ∈ 𝑆 β†’ - ( log β€˜ 𝐴 ) ∈ β„‚ )
106 105 mulm1d ⊒ ( 𝐴 ∈ 𝑆 β†’ ( - 1 Β· - ( log β€˜ 𝐴 ) ) = - - ( log β€˜ 𝐴 ) )
107 104 negnegd ⊒ ( 𝐴 ∈ 𝑆 β†’ - - ( log β€˜ 𝐴 ) = ( log β€˜ 𝐴 ) )
108 106 107 eqtrd ⊒ ( 𝐴 ∈ 𝑆 β†’ ( - 1 Β· - ( log β€˜ 𝐴 ) ) = ( log β€˜ 𝐴 ) )
109 98 108 breqtrd ⊒ ( 𝐴 ∈ 𝑆 β†’ seq 1 ( + , ( π‘˜ ∈ β„• ↦ ( ( ( - 1 ↑ ( π‘˜ βˆ’ 1 ) ) / π‘˜ ) Β· ( ( 𝐴 βˆ’ 1 ) ↑ π‘˜ ) ) ) ) ⇝ ( log β€˜ 𝐴 ) )