Step | Hyp | Ref
| Expression |
1 | | nnuz 11599 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11285 |
. . 3
⊢ (𝐴 ∈ 𝑆 → 1 ∈ ℤ) |
3 | | neg1cn 11001 |
. . . 4
⊢ -1 ∈
ℂ |
4 | 3 | a1i 11 |
. . 3
⊢ (𝐴 ∈ 𝑆 → -1 ∈ ℂ) |
5 | | ax-1cn 9873 |
. . . . . 6
⊢ 1 ∈
ℂ |
6 | | logtayl2.s |
. . . . . . . . 9
⊢ 𝑆 = (1(ball‘(abs ∘
− ))1) |
7 | 6 | eleq2i 2680 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑆 ↔ 𝐴 ∈ (1(ball‘(abs ∘ −
))1)) |
8 | | cnxmet 22386 |
. . . . . . . . 9
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
9 | | 1rp 11712 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ+ |
10 | | rpxr 11716 |
. . . . . . . . . 10
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . 9
⊢ 1 ∈
ℝ* |
12 | | elbl 22003 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℂ
∧ 1 ∈ ℝ*) → (𝐴 ∈ (1(ball‘(abs ∘ −
))1) ↔ (𝐴 ∈
ℂ ∧ (1(abs ∘ − )𝐴) < 1))) |
13 | 8, 5, 11, 12 | mp3an 1416 |
. . . . . . . 8
⊢ (𝐴 ∈ (1(ball‘(abs
∘ − ))1) ↔ (𝐴 ∈ ℂ ∧ (1(abs ∘ −
)𝐴) <
1)) |
14 | 7, 13 | bitri 263 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑆 ↔ (𝐴 ∈ ℂ ∧ (1(abs ∘ −
)𝐴) <
1)) |
15 | 14 | simplbi 475 |
. . . . . 6
⊢ (𝐴 ∈ 𝑆 → 𝐴 ∈ ℂ) |
16 | | subcl 10159 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 − 𝐴) ∈ ℂ) |
17 | 5, 15, 16 | sylancr 694 |
. . . . 5
⊢ (𝐴 ∈ 𝑆 → (1 − 𝐴) ∈ ℂ) |
18 | | eqid 2610 |
. . . . . . . 8
⊢ (abs
∘ − ) = (abs ∘ − ) |
19 | 18 | cnmetdval 22384 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1(abs ∘ − )𝐴) = (abs‘(1 − 𝐴))) |
20 | 5, 15, 19 | sylancr 694 |
. . . . . 6
⊢ (𝐴 ∈ 𝑆 → (1(abs ∘ − )𝐴) = (abs‘(1 − 𝐴))) |
21 | 14 | simprbi 479 |
. . . . . 6
⊢ (𝐴 ∈ 𝑆 → (1(abs ∘ − )𝐴) < 1) |
22 | 20, 21 | eqbrtrrd 4607 |
. . . . 5
⊢ (𝐴 ∈ 𝑆 → (abs‘(1 − 𝐴)) < 1) |
23 | | logtayl 24206 |
. . . . 5
⊢ (((1
− 𝐴) ∈ ℂ
∧ (abs‘(1 − 𝐴)) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ (((1
− 𝐴)↑𝑘) / 𝑘))) ⇝ -(log‘(1 − (1 −
𝐴)))) |
24 | 17, 22, 23 | syl2anc 691 |
. . . 4
⊢ (𝐴 ∈ 𝑆 → seq1( + , (𝑘 ∈ ℕ ↦ (((1 − 𝐴)↑𝑘) / 𝑘))) ⇝ -(log‘(1 − (1 −
𝐴)))) |
25 | | nncan 10189 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 − (1 − 𝐴)) = 𝐴) |
26 | 5, 15, 25 | sylancr 694 |
. . . . . 6
⊢ (𝐴 ∈ 𝑆 → (1 − (1 − 𝐴)) = 𝐴) |
27 | 26 | fveq2d 6107 |
. . . . 5
⊢ (𝐴 ∈ 𝑆 → (log‘(1 − (1 −
𝐴))) = (log‘𝐴)) |
28 | 27 | negeqd 10154 |
. . . 4
⊢ (𝐴 ∈ 𝑆 → -(log‘(1 − (1 −
𝐴))) = -(log‘𝐴)) |
29 | 24, 28 | breqtrd 4609 |
. . 3
⊢ (𝐴 ∈ 𝑆 → seq1( + , (𝑘 ∈ ℕ ↦ (((1 − 𝐴)↑𝑘) / 𝑘))) ⇝ -(log‘𝐴)) |
30 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → ((1 − 𝐴)↑𝑘) = ((1 − 𝐴)↑𝑛)) |
31 | | id 22 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → 𝑘 = 𝑛) |
32 | 30, 31 | oveq12d 6567 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (((1 − 𝐴)↑𝑘) / 𝑘) = (((1 − 𝐴)↑𝑛) / 𝑛)) |
33 | | eqid 2610 |
. . . . . 6
⊢ (𝑘 ∈ ℕ ↦ (((1
− 𝐴)↑𝑘) / 𝑘)) = (𝑘 ∈ ℕ ↦ (((1 − 𝐴)↑𝑘) / 𝑘)) |
34 | | ovex 6577 |
. . . . . 6
⊢ (((1
− 𝐴)↑𝑛) / 𝑛) ∈ V |
35 | 32, 33, 34 | fvmpt 6191 |
. . . . 5
⊢ (𝑛 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((1
− 𝐴)↑𝑘) / 𝑘))‘𝑛) = (((1 − 𝐴)↑𝑛) / 𝑛)) |
36 | 35 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (((1 − 𝐴)↑𝑘) / 𝑘))‘𝑛) = (((1 − 𝐴)↑𝑛) / 𝑛)) |
37 | | nnnn0 11176 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
38 | | expcl 12740 |
. . . . . 6
⊢ (((1
− 𝐴) ∈ ℂ
∧ 𝑛 ∈
ℕ0) → ((1 − 𝐴)↑𝑛) ∈ ℂ) |
39 | 17, 37, 38 | syl2an 493 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((1 − 𝐴)↑𝑛) ∈ ℂ) |
40 | | nncn 10905 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
41 | 40 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) |
42 | | nnne0 10930 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) |
43 | 42 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0) |
44 | 39, 41, 43 | divcld 10680 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (((1 − 𝐴)↑𝑛) / 𝑛) ∈ ℂ) |
45 | 36, 44 | eqeltrd 2688 |
. . 3
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (((1 − 𝐴)↑𝑘) / 𝑘))‘𝑛) ∈ ℂ) |
46 | 39, 41, 43 | divnegd 10693 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → -(((1 − 𝐴)↑𝑛) / 𝑛) = (-((1 − 𝐴)↑𝑛) / 𝑛)) |
47 | 44 | mulm1d 10361 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (-1 · (((1
− 𝐴)↑𝑛) / 𝑛)) = -(((1 − 𝐴)↑𝑛) / 𝑛)) |
48 | 37 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0) |
49 | | expcl 12740 |
. . . . . . . . . 10
⊢ ((-1
∈ ℂ ∧ 𝑛
∈ ℕ0) → (-1↑𝑛) ∈ ℂ) |
50 | 3, 48, 49 | sylancr 694 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (-1↑𝑛) ∈
ℂ) |
51 | | subcl 10159 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 −
1) ∈ ℂ) |
52 | 15, 5, 51 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑆 → (𝐴 − 1) ∈ ℂ) |
53 | | expcl 12740 |
. . . . . . . . . 10
⊢ (((𝐴 − 1) ∈ ℂ ∧
𝑛 ∈
ℕ0) → ((𝐴 − 1)↑𝑛) ∈ ℂ) |
54 | 52, 37, 53 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((𝐴 − 1)↑𝑛) ∈ ℂ) |
55 | 50, 54 | mulneg1d 10362 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (-(-1↑𝑛) · ((𝐴 − 1)↑𝑛)) = -((-1↑𝑛) · ((𝐴 − 1)↑𝑛))) |
56 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → -1 ∈
ℂ) |
57 | | neg1ne0 11003 |
. . . . . . . . . . . 12
⊢ -1 ≠
0 |
58 | 57 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → -1 ≠
0) |
59 | | nnz 11276 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
60 | 59 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ) |
61 | 56, 58, 60 | expm1d 12880 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (-1↑(𝑛 − 1)) = ((-1↑𝑛) / -1)) |
62 | 5 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → 1 ∈
ℂ) |
63 | | ax-1ne0 9884 |
. . . . . . . . . . . 12
⊢ 1 ≠
0 |
64 | 63 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → 1 ≠
0) |
65 | 50, 62, 64 | divneg2d 10694 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → -((-1↑𝑛) / 1) = ((-1↑𝑛) / -1)) |
66 | 50 | div1d 10672 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((-1↑𝑛) / 1) = (-1↑𝑛)) |
67 | 66 | negeqd 10154 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → -((-1↑𝑛) / 1) = -(-1↑𝑛)) |
68 | 61, 65, 67 | 3eqtr2d 2650 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (-1↑(𝑛 − 1)) = -(-1↑𝑛)) |
69 | 68 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((-1↑(𝑛 − 1)) · ((𝐴 − 1)↑𝑛)) = (-(-1↑𝑛) · ((𝐴 − 1)↑𝑛))) |
70 | 52 | mulm1d 10361 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑆 → (-1 · (𝐴 − 1)) = -(𝐴 − 1)) |
71 | | negsubdi2 10219 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → -(𝐴 −
1) = (1 − 𝐴)) |
72 | 15, 5, 71 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑆 → -(𝐴 − 1) = (1 − 𝐴)) |
73 | 70, 72 | eqtr2d 2645 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑆 → (1 − 𝐴) = (-1 · (𝐴 − 1))) |
74 | 73 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑆 → ((1 − 𝐴)↑𝑛) = ((-1 · (𝐴 − 1))↑𝑛)) |
75 | 74 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((1 − 𝐴)↑𝑛) = ((-1 · (𝐴 − 1))↑𝑛)) |
76 | | mulexp 12761 |
. . . . . . . . . . . 12
⊢ ((-1
∈ ℂ ∧ (𝐴
− 1) ∈ ℂ ∧ 𝑛 ∈ ℕ0) → ((-1
· (𝐴 −
1))↑𝑛) =
((-1↑𝑛) ·
((𝐴 − 1)↑𝑛))) |
77 | 3, 76 | mp3an1 1403 |
. . . . . . . . . . 11
⊢ (((𝐴 − 1) ∈ ℂ ∧
𝑛 ∈
ℕ0) → ((-1 · (𝐴 − 1))↑𝑛) = ((-1↑𝑛) · ((𝐴 − 1)↑𝑛))) |
78 | 52, 37, 77 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((-1 · (𝐴 − 1))↑𝑛) = ((-1↑𝑛) · ((𝐴 − 1)↑𝑛))) |
79 | 75, 78 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((1 − 𝐴)↑𝑛) = ((-1↑𝑛) · ((𝐴 − 1)↑𝑛))) |
80 | 79 | negeqd 10154 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → -((1 − 𝐴)↑𝑛) = -((-1↑𝑛) · ((𝐴 − 1)↑𝑛))) |
81 | 55, 69, 80 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((-1↑(𝑛 − 1)) · ((𝐴 − 1)↑𝑛)) = -((1 − 𝐴)↑𝑛)) |
82 | 81 | oveq1d 6564 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (((-1↑(𝑛 − 1)) · ((𝐴 − 1)↑𝑛)) / 𝑛) = (-((1 − 𝐴)↑𝑛) / 𝑛)) |
83 | 46, 47, 82 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (-1 · (((1
− 𝐴)↑𝑛) / 𝑛)) = (((-1↑(𝑛 − 1)) · ((𝐴 − 1)↑𝑛)) / 𝑛)) |
84 | | nnm1nn0 11211 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
85 | 84 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (𝑛 − 1) ∈
ℕ0) |
86 | | expcl 12740 |
. . . . . . 7
⊢ ((-1
∈ ℂ ∧ (𝑛
− 1) ∈ ℕ0) → (-1↑(𝑛 − 1)) ∈ ℂ) |
87 | 3, 85, 86 | sylancr 694 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (-1↑(𝑛 − 1)) ∈
ℂ) |
88 | 87, 54, 41, 43 | div23d 10717 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (((-1↑(𝑛 − 1)) · ((𝐴 − 1)↑𝑛)) / 𝑛) = (((-1↑(𝑛 − 1)) / 𝑛) · ((𝐴 − 1)↑𝑛))) |
89 | 83, 88 | eqtr2d 2645 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (((-1↑(𝑛 − 1)) / 𝑛) · ((𝐴 − 1)↑𝑛)) = (-1 · (((1 − 𝐴)↑𝑛) / 𝑛))) |
90 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (𝑘 − 1) = (𝑛 − 1)) |
91 | 90 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → (-1↑(𝑘 − 1)) = (-1↑(𝑛 − 1))) |
92 | 91, 31 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → ((-1↑(𝑘 − 1)) / 𝑘) = ((-1↑(𝑛 − 1)) / 𝑛)) |
93 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → ((𝐴 − 1)↑𝑘) = ((𝐴 − 1)↑𝑛)) |
94 | 92, 93 | oveq12d 6567 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘)) = (((-1↑(𝑛 − 1)) / 𝑛) · ((𝐴 − 1)↑𝑛))) |
95 | | eqid 2610 |
. . . . . 6
⊢ (𝑘 ∈ ℕ ↦
(((-1↑(𝑘 − 1)) /
𝑘) · ((𝐴 − 1)↑𝑘))) = (𝑘 ∈ ℕ ↦ (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘))) |
96 | | ovex 6577 |
. . . . . 6
⊢
(((-1↑(𝑛
− 1)) / 𝑛) ·
((𝐴 − 1)↑𝑛)) ∈ V |
97 | 94, 95, 96 | fvmpt 6191 |
. . . . 5
⊢ (𝑛 ∈ ℕ → ((𝑘 ∈ ℕ ↦
(((-1↑(𝑘 − 1)) /
𝑘) · ((𝐴 − 1)↑𝑘)))‘𝑛) = (((-1↑(𝑛 − 1)) / 𝑛) · ((𝐴 − 1)↑𝑛))) |
98 | 97 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘)))‘𝑛) = (((-1↑(𝑛 − 1)) / 𝑛) · ((𝐴 − 1)↑𝑛))) |
99 | 36 | oveq2d 6565 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → (-1 · ((𝑘 ∈ ℕ ↦ (((1
− 𝐴)↑𝑘) / 𝑘))‘𝑛)) = (-1 · (((1 − 𝐴)↑𝑛) / 𝑛))) |
100 | 89, 98, 99 | 3eqtr4d 2654 |
. . 3
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘)))‘𝑛) = (-1 · ((𝑘 ∈ ℕ ↦ (((1 − 𝐴)↑𝑘) / 𝑘))‘𝑛))) |
101 | 1, 2, 4, 29, 45, 100 | isermulc2 14236 |
. 2
⊢ (𝐴 ∈ 𝑆 → seq1( + , (𝑘 ∈ ℕ ↦ (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘)))) ⇝ (-1 · -(log‘𝐴))) |
102 | 6 | dvlog2lem 24198 |
. . . . . . . 8
⊢ 𝑆 ⊆ (ℂ ∖
(-∞(,]0)) |
103 | 102 | sseli 3564 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑆 → 𝐴 ∈ (ℂ ∖
(-∞(,]0))) |
104 | | eqid 2610 |
. . . . . . . 8
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
105 | 104 | logdmn0 24186 |
. . . . . . 7
⊢ (𝐴 ∈ (ℂ ∖
(-∞(,]0)) → 𝐴
≠ 0) |
106 | 103, 105 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ 𝑆 → 𝐴 ≠ 0) |
107 | 15, 106 | logcld 24121 |
. . . . 5
⊢ (𝐴 ∈ 𝑆 → (log‘𝐴) ∈ ℂ) |
108 | 107 | negcld 10258 |
. . . 4
⊢ (𝐴 ∈ 𝑆 → -(log‘𝐴) ∈ ℂ) |
109 | 108 | mulm1d 10361 |
. . 3
⊢ (𝐴 ∈ 𝑆 → (-1 · -(log‘𝐴)) = --(log‘𝐴)) |
110 | 107 | negnegd 10262 |
. . 3
⊢ (𝐴 ∈ 𝑆 → --(log‘𝐴) = (log‘𝐴)) |
111 | 109, 110 | eqtrd 2644 |
. 2
⊢ (𝐴 ∈ 𝑆 → (-1 · -(log‘𝐴)) = (log‘𝐴)) |
112 | 101, 111 | breqtrd 4609 |
1
⊢ (𝐴 ∈ 𝑆 → seq1( + , (𝑘 ∈ ℕ ↦ (((-1↑(𝑘 − 1)) / 𝑘) · ((𝐴 − 1)↑𝑘)))) ⇝ (log‘𝐴)) |