| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nnuz 12922 | . . 3
⊢ ℕ =
(ℤ≥‘1) | 
| 2 |  | 1zzd 12650 | . . 3
⊢ (𝐴 ∈ 𝑆 → 1 ∈ ℤ) | 
| 3 |  | neg1cn 12381 | . . . 4
⊢ -1 ∈
ℂ | 
| 4 | 3 | a1i 11 | . . 3
⊢ (𝐴 ∈ 𝑆 → -1 ∈ ℂ) | 
| 5 |  | ax-1cn 11214 | . . . . . 6
⊢ 1 ∈
ℂ | 
| 6 |  | logtayl2.s | . . . . . . . . 9
⊢ 𝑆 = (1(ball‘(abs ∘
− ))1) | 
| 7 | 6 | eleq2i 2832 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑆 ↔ 𝐴 ∈ (1(ball‘(abs ∘ −
))1)) | 
| 8 |  | cnxmet 24794 | . . . . . . . . 9
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) | 
| 9 |  | 1xr 11321 | . . . . . . . . 9
⊢ 1 ∈
ℝ* | 
| 10 |  | elbl 24399 | . . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℂ
∧ 1 ∈ ℝ*) → (𝐴 ∈ (1(ball‘(abs ∘ −
))1) ↔ (𝐴 ∈
ℂ ∧ (1(abs ∘ − )𝐴) < 1))) | 
| 11 | 8, 5, 9, 10 | mp3an 1462 | . . . . . . . 8
⊢ (𝐴 ∈ (1(ball‘(abs
∘ − ))1) ↔ (𝐴 ∈ ℂ ∧ (1(abs ∘ −
)𝐴) <
1)) | 
| 12 | 7, 11 | bitri 275 | . . . . . . 7
⊢ (𝐴 ∈ 𝑆 ↔ (𝐴 ∈ ℂ ∧ (1(abs ∘ −
)𝐴) <
1)) | 
| 13 | 12 | simplbi 497 | . . . . . 6
⊢ (𝐴 ∈ 𝑆 → 𝐴 ∈ ℂ) | 
| 14 |  | subcl 11508 | . . . . . 6
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 − 𝐴) ∈ ℂ) | 
| 15 | 5, 13, 14 | sylancr 587 | . . . . 5
⊢ (𝐴 ∈ 𝑆 → (1 − 𝐴) ∈ ℂ) | 
| 16 |  | eqid 2736 | . . . . . . . 8
⊢ (abs
∘ − ) = (abs ∘ − ) | 
| 17 | 16 | cnmetdval 24792 | . . . . . . 7
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1(abs ∘ − )𝐴) = (abs‘(1 − 𝐴))) | 
| 18 | 5, 13, 17 | sylancr 587 | . . . . . 6
⊢ (𝐴 ∈ 𝑆 → (1(abs ∘ − )𝐴) = (abs‘(1 − 𝐴))) | 
| 19 | 12 | simprbi 496 | . . . . . 6
⊢ (𝐴 ∈ 𝑆 → (1(abs ∘ − )𝐴) < 1) | 
| 20 | 18, 19 | eqbrtrrd 5166 | . . . . 5
⊢ (𝐴 ∈ 𝑆 → (abs‘(1 − 𝐴)) < 1) | 
| 21 |  | logtayl 26703 | . . . . 5
⊢ (((1
− 𝐴) ∈ ℂ
∧ (abs‘(1 − 𝐴)) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ (((1
− 𝐴)↑𝑘) / 𝑘))) ⇝ -(log‘(1 − (1 −
𝐴)))) | 
| 22 | 15, 20, 21 | syl2anc 584 | . . . 4
⊢ (𝐴 ∈ 𝑆 → seq1( + , (𝑘 ∈ ℕ ↦ (((1 − 𝐴)↑𝑘) / 𝑘))) ⇝ -(log‘(1 − (1 −
𝐴)))) | 
| 23 |  | nncan 11539 | . . . . . . 7
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 − (1 − 𝐴)) = 𝐴) | 
| 24 | 5, 13, 23 | sylancr 587 | . . . . . 6
⊢ (𝐴 ∈ 𝑆 → (1 − (1 − 𝐴)) = 𝐴) | 
| 25 | 24 | fveq2d 6909 | . . . . 5
⊢ (𝐴 ∈ 𝑆 → (log‘(1 − (1 −
𝐴))) = (log‘𝐴)) | 
| 26 | 25 | negeqd 11503 | . . . 4
⊢ (𝐴 ∈ 𝑆 → -(log‘(1 − (1 −
𝐴))) = -(log‘𝐴)) | 
| 27 | 22, 26 | breqtrd 5168 | . . 3
⊢ (𝐴 ∈ 𝑆 → seq1( + , (𝑘 ∈ ℕ ↦ (((1 − 𝐴)↑𝑘) / 𝑘))) ⇝ -(log‘𝐴)) | 
| 28 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑘 = 𝑛 → ((1 − 𝐴)↑𝑘) = ((1 − 𝐴)↑𝑛)) | 
| 29 |  | id 22 | . . . . . . 7
⊢ (𝑘 = 𝑛 → 𝑘 = 𝑛) | 
| 30 | 28, 29 | oveq12d 7450 | . . . . . 6
⊢ (𝑘 = 𝑛 → (((1 − 𝐴)↑𝑘) / 𝑘) = (((1 − 𝐴)↑𝑛) / 𝑛)) | 
| 31 |  | eqid 2736 | . . . . . 6
⊢ (𝑘 ∈ ℕ ↦ (((1
− 𝐴)↑𝑘) / 𝑘)) = (𝑘 ∈ ℕ ↦ (((1 − 𝐴)↑𝑘) / 𝑘)) | 
| 32 |  | ovex 7465 | . . . . . 6
⊢ (((1
− 𝐴)↑𝑛) / 𝑛) ∈ V | 
| 33 | 30, 31, 32 | fvmpt 7015 | . . . . 5
⊢ (𝑛 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((1
− 𝐴)↑𝑘) / 𝑘))‘𝑛) = (((1 − 𝐴)↑𝑛) / 𝑛)) | 
| 34 | 33 | adantl 481 | . . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (((1 − 𝐴)↑𝑘) / 𝑘))‘𝑛) = (((1 − 𝐴)↑𝑛) / 𝑛)) | 
| 35 |  | nnnn0 12535 | . . . . . 6
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) | 
| 36 |  | expcl 14121 | . . . . . 6
⊢ (((1
− 𝐴) ∈ ℂ
∧ 𝑛 ∈
ℕ0) → ((1 − 𝐴)↑𝑛) ∈ ℂ) | 
| 37 | 15, 35, 36 | syl2an 596 | . . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((1 − 𝐴)↑𝑛) ∈ ℂ) | 
| 38 |  | nncn 12275 | . . . . . 6
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) | 
| 39 | 38 | adantl 481 | . . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) | 
| 40 |  | nnne0 12301 | . . . . . 6
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) | 
| 41 | 40 | adantl 481 | . . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0) | 
| 42 | 37, 39, 41 | divcld 12044 | . . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (((1 − 𝐴)↑𝑛) / 𝑛) ∈ ℂ) | 
| 43 | 34, 42 | eqeltrd 2840 | . . 3
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (((1 − 𝐴)↑𝑘) / 𝑘))‘𝑛) ∈ ℂ) | 
| 44 | 37, 39, 41 | divnegd 12057 | . . . . . 6
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → -(((1 − 𝐴)↑𝑛) / 𝑛) = (-((1 − 𝐴)↑𝑛) / 𝑛)) | 
| 45 | 42 | mulm1d 11716 | . . . . . 6
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (-1 · (((1
− 𝐴)↑𝑛) / 𝑛)) = -(((1 − 𝐴)↑𝑛) / 𝑛)) | 
| 46 | 35 | adantl 481 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0) | 
| 47 |  | expcl 14121 | . . . . . . . . . 10
⊢ ((-1
∈ ℂ ∧ 𝑛
∈ ℕ0) → (-1↑𝑛) ∈ ℂ) | 
| 48 | 3, 46, 47 | sylancr 587 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (-1↑𝑛) ∈
ℂ) | 
| 49 |  | subcl 11508 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 −
1) ∈ ℂ) | 
| 50 | 13, 5, 49 | sylancl 586 | . . . . . . . . . 10
⊢ (𝐴 ∈ 𝑆 → (𝐴 − 1) ∈ ℂ) | 
| 51 |  | expcl 14121 | . . . . . . . . . 10
⊢ (((𝐴 − 1) ∈ ℂ ∧
𝑛 ∈
ℕ0) → ((𝐴 − 1)↑𝑛) ∈ ℂ) | 
| 52 | 50, 35, 51 | syl2an 596 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((𝐴 − 1)↑𝑛) ∈ ℂ) | 
| 53 | 48, 52 | mulneg1d 11717 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (-(-1↑𝑛) · ((𝐴 − 1)↑𝑛)) = -((-1↑𝑛) · ((𝐴 − 1)↑𝑛))) | 
| 54 | 3 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → -1 ∈
ℂ) | 
| 55 |  | neg1ne0 12383 | . . . . . . . . . . . 12
⊢ -1 ≠
0 | 
| 56 | 55 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → -1 ≠
0) | 
| 57 |  | nnz 12636 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) | 
| 58 | 57 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ) | 
| 59 | 54, 56, 58 | expm1d 14197 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (-1↑(𝑛 − 1)) = ((-1↑𝑛) / -1)) | 
| 60 | 5 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → 1 ∈
ℂ) | 
| 61 |  | ax-1ne0 11225 | . . . . . . . . . . . 12
⊢ 1 ≠
0 | 
| 62 | 61 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → 1 ≠
0) | 
| 63 | 48, 60, 62 | divneg2d 12058 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → -((-1↑𝑛) / 1) = ((-1↑𝑛) / -1)) | 
| 64 | 48 | div1d 12036 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((-1↑𝑛) / 1) = (-1↑𝑛)) | 
| 65 | 64 | negeqd 11503 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → -((-1↑𝑛) / 1) = -(-1↑𝑛)) | 
| 66 | 59, 63, 65 | 3eqtr2d 2782 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (-1↑(𝑛 − 1)) = -(-1↑𝑛)) | 
| 67 | 66 | oveq1d 7447 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((-1↑(𝑛 − 1)) · ((𝐴 − 1)↑𝑛)) = (-(-1↑𝑛) · ((𝐴 − 1)↑𝑛))) | 
| 68 | 50 | mulm1d 11716 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑆 → (-1 · (𝐴 − 1)) = -(𝐴 − 1)) | 
| 69 |  | negsubdi2 11569 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → -(𝐴 −
1) = (1 − 𝐴)) | 
| 70 | 13, 5, 69 | sylancl 586 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑆 → -(𝐴 − 1) = (1 − 𝐴)) | 
| 71 | 68, 70 | eqtr2d 2777 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑆 → (1 − 𝐴) = (-1 · (𝐴 − 1))) | 
| 72 | 71 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑆 → ((1 − 𝐴)↑𝑛) = ((-1 · (𝐴 − 1))↑𝑛)) | 
| 73 | 72 | adantr 480 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((1 − 𝐴)↑𝑛) = ((-1 · (𝐴 − 1))↑𝑛)) | 
| 74 |  | mulexp 14143 | . . . . . . . . . . 11
⊢ ((-1
∈ ℂ ∧ (𝐴
− 1) ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((-1
· (𝐴 −
1))↑𝑛) =
((-1↑𝑛) ·
((𝐴 − 1)↑𝑛))) | 
| 75 | 3, 50, 35, 74 | mp3an3an 1468 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((-1 · (𝐴 − 1))↑𝑛) = ((-1↑𝑛) · ((𝐴 − 1)↑𝑛))) | 
| 76 | 73, 75 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((1 − 𝐴)↑𝑛) = ((-1↑𝑛) · ((𝐴 − 1)↑𝑛))) | 
| 77 | 76 | negeqd 11503 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → -((1 − 𝐴)↑𝑛) = -((-1↑𝑛) · ((𝐴 − 1)↑𝑛))) | 
| 78 | 53, 67, 77 | 3eqtr4d 2786 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((-1↑(𝑛 − 1)) · ((𝐴 − 1)↑𝑛)) = -((1 − 𝐴)↑𝑛)) | 
| 79 | 78 | oveq1d 7447 | . . . . . 6
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (((-1↑(𝑛 − 1)) · ((𝐴 − 1)↑𝑛)) / 𝑛) = (-((1 − 𝐴)↑𝑛) / 𝑛)) | 
| 80 | 44, 45, 79 | 3eqtr4d 2786 | . . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (-1 · (((1
− 𝐴)↑𝑛) / 𝑛)) = (((-1↑(𝑛 − 1)) · ((𝐴 − 1)↑𝑛)) / 𝑛)) | 
| 81 |  | nnm1nn0 12569 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) | 
| 82 | 81 | adantl 481 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (𝑛 − 1) ∈
ℕ0) | 
| 83 |  | expcl 14121 | . . . . . . 7
⊢ ((-1
∈ ℂ ∧ (𝑛
− 1) ∈ ℕ0) → (-1↑(𝑛 − 1)) ∈ ℂ) | 
| 84 | 3, 82, 83 | sylancr 587 | . . . . . 6
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (-1↑(𝑛 − 1)) ∈
ℂ) | 
| 85 | 84, 52, 39, 41 | div23d 12081 | . . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (((-1↑(𝑛 − 1)) · ((𝐴 − 1)↑𝑛)) / 𝑛) = (((-1↑(𝑛 − 1)) / 𝑛) · ((𝐴 − 1)↑𝑛))) | 
| 86 | 80, 85 | eqtr2d 2777 | . . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (((-1↑(𝑛 − 1)) / 𝑛) · ((𝐴 − 1)↑𝑛)) = (-1 · (((1 − 𝐴)↑𝑛) / 𝑛))) | 
| 87 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑘 = 𝑛 → (𝑘 − 1) = (𝑛 − 1)) | 
| 88 | 87 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑘 = 𝑛 → (-1↑(𝑘 − 1)) = (-1↑(𝑛 − 1))) | 
| 89 | 88, 29 | oveq12d 7450 | . . . . . . 7
⊢ (𝑘 = 𝑛 → ((-1↑(𝑘 − 1)) / 𝑘) = ((-1↑(𝑛 − 1)) / 𝑛)) | 
| 90 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑘 = 𝑛 → ((𝐴 − 1)↑𝑘) = ((𝐴 − 1)↑𝑛)) | 
| 91 | 89, 90 | oveq12d 7450 | . . . . . 6
⊢ (𝑘 = 𝑛 → (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘)) = (((-1↑(𝑛 − 1)) / 𝑛) · ((𝐴 − 1)↑𝑛))) | 
| 92 |  | eqid 2736 | . . . . . 6
⊢ (𝑘 ∈ ℕ ↦
(((-1↑(𝑘 − 1)) /
𝑘) · ((𝐴 − 1)↑𝑘))) = (𝑘 ∈ ℕ ↦ (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘))) | 
| 93 |  | ovex 7465 | . . . . . 6
⊢
(((-1↑(𝑛
− 1)) / 𝑛) ·
((𝐴 − 1)↑𝑛)) ∈ V | 
| 94 | 91, 92, 93 | fvmpt 7015 | . . . . 5
⊢ (𝑛 ∈ ℕ → ((𝑘 ∈ ℕ ↦
(((-1↑(𝑘 − 1)) /
𝑘) · ((𝐴 − 1)↑𝑘)))‘𝑛) = (((-1↑(𝑛 − 1)) / 𝑛) · ((𝐴 − 1)↑𝑛))) | 
| 95 | 94 | adantl 481 | . . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘)))‘𝑛) = (((-1↑(𝑛 − 1)) / 𝑛) · ((𝐴 − 1)↑𝑛))) | 
| 96 | 34 | oveq2d 7448 | . . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (-1 · ((𝑘 ∈ ℕ ↦ (((1
− 𝐴)↑𝑘) / 𝑘))‘𝑛)) = (-1 · (((1 − 𝐴)↑𝑛) / 𝑛))) | 
| 97 | 86, 95, 96 | 3eqtr4d 2786 | . . 3
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘)))‘𝑛) = (-1 · ((𝑘 ∈ ℕ ↦ (((1 − 𝐴)↑𝑘) / 𝑘))‘𝑛))) | 
| 98 | 1, 2, 4, 27, 43, 97 | isermulc2 15695 | . 2
⊢ (𝐴 ∈ 𝑆 → seq1( + , (𝑘 ∈ ℕ ↦ (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘)))) ⇝ (-1 · -(log‘𝐴))) | 
| 99 | 6 | dvlog2lem 26695 | . . . . . . . 8
⊢ 𝑆 ⊆ (ℂ ∖
(-∞(,]0)) | 
| 100 | 99 | sseli 3978 | . . . . . . 7
⊢ (𝐴 ∈ 𝑆 → 𝐴 ∈ (ℂ ∖
(-∞(,]0))) | 
| 101 |  | eqid 2736 | . . . . . . . 8
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) | 
| 102 | 101 | logdmn0 26683 | . . . . . . 7
⊢ (𝐴 ∈ (ℂ ∖
(-∞(,]0)) → 𝐴
≠ 0) | 
| 103 | 100, 102 | syl 17 | . . . . . 6
⊢ (𝐴 ∈ 𝑆 → 𝐴 ≠ 0) | 
| 104 | 13, 103 | logcld 26613 | . . . . 5
⊢ (𝐴 ∈ 𝑆 → (log‘𝐴) ∈ ℂ) | 
| 105 | 104 | negcld 11608 | . . . 4
⊢ (𝐴 ∈ 𝑆 → -(log‘𝐴) ∈ ℂ) | 
| 106 | 105 | mulm1d 11716 | . . 3
⊢ (𝐴 ∈ 𝑆 → (-1 · -(log‘𝐴)) = --(log‘𝐴)) | 
| 107 | 104 | negnegd 11612 | . . 3
⊢ (𝐴 ∈ 𝑆 → --(log‘𝐴) = (log‘𝐴)) | 
| 108 | 106, 107 | eqtrd 2776 | . 2
⊢ (𝐴 ∈ 𝑆 → (-1 · -(log‘𝐴)) = (log‘𝐴)) | 
| 109 | 98, 108 | breqtrd 5168 | 1
⊢ (𝐴 ∈ 𝑆 → seq1( + , (𝑘 ∈ ℕ ↦ (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘)))) ⇝ (log‘𝐴)) |