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 ‘ 𝐴 ) )