Step | Hyp | Ref
| Expression |
1 | | nn0uz 11598 |
. . . 4
⊢
ℕ0 = (ℤ≥‘0) |
2 | | 0zd 11266 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 0 ∈ ℤ) |
3 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → (𝑘 = 0 ↔ 𝑛 = 0)) |
4 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → (1 / 𝑘) = (1 / 𝑛)) |
5 | 3, 4 | ifbieq2d 4061 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → if(𝑘 = 0, 0, (1 / 𝑘)) = if(𝑛 = 0, 0, (1 / 𝑛))) |
6 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (𝐴↑𝑘) = (𝐴↑𝑛)) |
7 | 5, 6 | oveq12d 6567 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛))) |
8 | | eqid 2610 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
↦ (if(𝑘 = 0, 0, (1 /
𝑘)) · (𝐴↑𝑘))) = (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘))) |
9 | | ovex 6577 |
. . . . . 6
⊢ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)) ∈ V |
10 | 7, 8, 9 | fvmpt 6191 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛))) |
11 | 10 | adantl 481 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛))) |
12 | | 0cnd 9912 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) ∧ 𝑛 = 0) → 0 ∈
ℂ) |
13 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → 𝑛 ∈ ℕ0) |
14 | | elnn0 11171 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
↔ (𝑛 ∈ ℕ
∨ 𝑛 =
0)) |
15 | 13, 14 | sylib 207 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (𝑛 ∈ ℕ ∨ 𝑛 = 0)) |
16 | 15 | ord 391 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (¬ 𝑛 ∈ ℕ → 𝑛 = 0)) |
17 | 16 | con1d 138 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (¬ 𝑛 = 0 → 𝑛 ∈ ℕ)) |
18 | 17 | imp 444 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) ∧ ¬ 𝑛 = 0) → 𝑛 ∈ ℕ) |
19 | 18 | nnrecred 10943 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℝ) |
20 | 19 | recnd 9947 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) ∧ ¬ 𝑛 = 0) → (1 / 𝑛) ∈ ℂ) |
21 | 12, 20 | ifclda 4070 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → if(𝑛 = 0, 0, (1 / 𝑛)) ∈ ℂ) |
22 | | expcl 12740 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑛 ∈ ℕ0)
→ (𝐴↑𝑛) ∈
ℂ) |
23 | 22 | adantlr 747 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (𝐴↑𝑛) ∈ ℂ) |
24 | 21, 23 | mulcld 9939 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)) ∈ ℂ) |
25 | | logtayllem 24205 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , (𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))) ∈ dom ⇝ ) |
26 | 1, 2, 11, 24, 25 | isumclim2 14331 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , (𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))) ⇝ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛))) |
27 | | simpl 472 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 𝐴 ∈
ℂ) |
28 | | 0cn 9911 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
29 | | eqid 2610 |
. . . . . . . . 9
⊢ (abs
∘ − ) = (abs ∘ − ) |
30 | 29 | cnmetdval 22384 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 ∈
ℂ) → (𝐴(abs
∘ − )0) = (abs‘(𝐴 − 0))) |
31 | 27, 28, 30 | sylancl 693 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (𝐴(abs ∘
− )0) = (abs‘(𝐴
− 0))) |
32 | | subid1 10180 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴) |
33 | 32 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (𝐴 − 0) =
𝐴) |
34 | 33 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘(𝐴
− 0)) = (abs‘𝐴)) |
35 | 31, 34 | eqtrd 2644 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (𝐴(abs ∘
− )0) = (abs‘𝐴)) |
36 | | simpr 476 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) <
1) |
37 | 35, 36 | eqbrtrd 4605 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (𝐴(abs ∘
− )0) < 1) |
38 | | cnxmet 22386 |
. . . . . . 7
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
39 | | 1rp 11712 |
. . . . . . . 8
⊢ 1 ∈
ℝ+ |
40 | | rpxr 11716 |
. . . . . . . 8
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) |
41 | 39, 40 | ax-mp 5 |
. . . . . . 7
⊢ 1 ∈
ℝ* |
42 | | elbl3 22007 |
. . . . . . 7
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (0 ∈ ℂ ∧ 𝐴 ∈ ℂ)) → (𝐴 ∈ (0(ball‘(abs ∘ −
))1) ↔ (𝐴(abs ∘
− )0) < 1)) |
43 | 38, 41, 42 | mpanl12 714 |
. . . . . 6
⊢ ((0
∈ ℂ ∧ 𝐴
∈ ℂ) → (𝐴
∈ (0(ball‘(abs ∘ − ))1) ↔ (𝐴(abs ∘ − )0) <
1)) |
44 | 28, 27, 43 | sylancr 694 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (𝐴 ∈
(0(ball‘(abs ∘ − ))1) ↔ (𝐴(abs ∘ − )0) <
1)) |
45 | 37, 44 | mpbird 246 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 𝐴 ∈
(0(ball‘(abs ∘ − ))1)) |
46 | | tru 1479 |
. . . . . 6
⊢
⊤ |
47 | | eqid 2610 |
. . . . . . . 8
⊢
(0(ball‘(abs ∘ − ))1) = (0(ball‘(abs ∘
− ))1) |
48 | | 0cnd 9912 |
. . . . . . . 8
⊢ (⊤
→ 0 ∈ ℂ) |
49 | 41 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 1 ∈ ℝ*) |
50 | | ax-1cn 9873 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
51 | | blssm 22033 |
. . . . . . . . . . . . . . 15
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 1 ∈ ℝ*) → (0(ball‘(abs ∘ −
))1) ⊆ ℂ) |
52 | 38, 28, 41, 51 | mp3an 1416 |
. . . . . . . . . . . . . 14
⊢
(0(ball‘(abs ∘ − ))1) ⊆ ℂ |
53 | 52 | sseli 3564 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → 𝑦 ∈ ℂ) |
54 | | subcl 10159 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ 𝑦
∈ ℂ) → (1 − 𝑦) ∈ ℂ) |
55 | 50, 53, 54 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (1 − 𝑦) ∈ ℂ) |
56 | 53 | abscld 14023 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (abs‘𝑦) ∈ ℝ) |
57 | 29 | cnmetdval 22384 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℂ ∧ 0 ∈
ℂ) → (𝑦(abs
∘ − )0) = (abs‘(𝑦 − 0))) |
58 | 53, 28, 57 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (𝑦(abs ∘ − )0) = (abs‘(𝑦 − 0))) |
59 | 53 | subid1d 10260 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (𝑦 − 0) = 𝑦) |
60 | 59 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (abs‘(𝑦 − 0)) = (abs‘𝑦)) |
61 | 58, 60 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (𝑦(abs ∘ − )0) = (abs‘𝑦)) |
62 | | elbl3 22007 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (0 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↔ (𝑦(abs ∘
− )0) < 1)) |
63 | 38, 41, 62 | mpanl12 714 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℂ ∧ 𝑦
∈ ℂ) → (𝑦
∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑦(abs ∘ − )0) <
1)) |
64 | 28, 53, 63 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↔ (𝑦(abs ∘
− )0) < 1)) |
65 | 64 | ibi 255 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (𝑦(abs ∘ − )0) <
1) |
66 | 61, 65 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (abs‘𝑦) < 1) |
67 | 56, 66 | gtned 10051 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → 1 ≠ (abs‘𝑦)) |
68 | | abs1 13885 |
. . . . . . . . . . . . . . . 16
⊢
(abs‘1) = 1 |
69 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (1 =
𝑦 → (abs‘1) =
(abs‘𝑦)) |
70 | 68, 69 | syl5eqr 2658 |
. . . . . . . . . . . . . . 15
⊢ (1 =
𝑦 → 1 =
(abs‘𝑦)) |
71 | 70 | necon3i 2814 |
. . . . . . . . . . . . . 14
⊢ (1 ≠
(abs‘𝑦) → 1 ≠
𝑦) |
72 | 67, 71 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → 1 ≠ 𝑦) |
73 | | subeq0 10186 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℂ ∧ 𝑦
∈ ℂ) → ((1 − 𝑦) = 0 ↔ 1 = 𝑦)) |
74 | 73 | necon3bid 2826 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℂ ∧ 𝑦
∈ ℂ) → ((1 − 𝑦) ≠ 0 ↔ 1 ≠ 𝑦)) |
75 | 50, 53, 74 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → ((1 − 𝑦) ≠ 0 ↔ 1 ≠ 𝑦)) |
76 | 72, 75 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (1 − 𝑦) ≠ 0) |
77 | 55, 76 | logcld 24121 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (log‘(1 − 𝑦)) ∈ ℂ) |
78 | 77 | negcld 10258 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → -(log‘(1 − 𝑦)) ∈ ℂ) |
79 | 78 | adantl 481 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ (0(ball‘(abs ∘ − ))1)) → -(log‘(1 −
𝑦)) ∈
ℂ) |
80 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) ↦ -(log‘(1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ -(log‘(1 − 𝑦))) |
81 | 79, 80 | fmptd 6292 |
. . . . . . . 8
⊢ (⊤
→ (𝑦 ∈
(0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))):(0(ball‘(abs ∘
− ))1)⟶ℂ) |
82 | 53 | absge0d 14031 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → 0 ≤ (abs‘𝑦)) |
83 | 56 | rexrd 9968 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (abs‘𝑦) ∈
ℝ*) |
84 | | peano2re 10088 |
. . . . . . . . . . . . . . . 16
⊢
((abs‘𝑦)
∈ ℝ → ((abs‘𝑦) + 1) ∈ ℝ) |
85 | 56, 84 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → ((abs‘𝑦) + 1) ∈ ℝ) |
86 | 85 | rehalfcld 11156 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℝ) |
87 | 86 | rexrd 9968 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈
ℝ*) |
88 | | iccssxr 12127 |
. . . . . . . . . . . . . . 15
⊢
(0[,]+∞) ⊆ ℝ* |
89 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑗 → (𝑚 = 0 ↔ 𝑗 = 0)) |
90 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑗 → (1 / 𝑚) = (1 / 𝑗)) |
91 | 89, 90 | ifbieq2d 4061 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑗 → if(𝑚 = 0, 0, (1 / 𝑚)) = if(𝑗 = 0, 0, (1 / 𝑗))) |
92 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ ℕ0
↦ if(𝑚 = 0, 0, (1 /
𝑚))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚))) |
93 | | c0ex 9913 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
V |
94 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 /
𝑗) ∈
V |
95 | 93, 94 | ifex 4106 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ if(𝑗 = 0, 0, (1 / 𝑗)) ∈ V |
96 | 91, 92, 95 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ0
→ ((𝑚 ∈
ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) = if(𝑗 = 0, 0, (1 / 𝑗))) |
97 | 96 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ0
→ if(𝑗 = 0, 0, (1 /
𝑗)) = ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗)) |
98 | 97 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ0
→ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑥↑𝑗)) = (((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑗) · (𝑥↑𝑗))) |
99 | 98 | mpteq2ia 4668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑥↑𝑗))) = (𝑗 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0
↦ if(𝑚 = 0, 0, (1 /
𝑚)))‘𝑗) · (𝑥↑𝑗))) |
100 | 99 | mpteq2i 4669 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑥↑𝑗)))) = (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0
↦ if(𝑚 = 0, 0, (1 /
𝑚)))‘𝑗) · (𝑥↑𝑗)))) |
101 | | 0cnd 9912 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑚
∈ ℕ0) ∧ 𝑚 = 0) → 0 ∈
ℂ) |
102 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℂ) |
103 | 102 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑚
∈ ℕ0) → 𝑚 ∈ ℂ) |
104 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ≠ 0 ↔ ¬ 𝑚 = 0) |
105 | 104 | biimpri 217 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑚 = 0 → 𝑚 ≠ 0) |
106 | | reccl 10571 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ ℂ ∧ 𝑚 ≠ 0) → (1 / 𝑚) ∈
ℂ) |
107 | 103, 105,
106 | syl2an 493 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑚
∈ ℕ0) ∧ ¬ 𝑚 = 0) → (1 / 𝑚) ∈ ℂ) |
108 | 101, 107 | ifclda 4070 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑚
∈ ℕ0) → if(𝑚 = 0, 0, (1 / 𝑚)) ∈ ℂ) |
109 | 108, 92 | fmptd 6292 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ (𝑚 ∈
ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚))):ℕ0⟶ℂ) |
110 | | recn 9905 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑟 ∈ ℝ → 𝑟 ∈
ℂ) |
111 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑟 → (𝑥↑𝑗) = (𝑟↑𝑗)) |
112 | 111 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑟 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗))) |
113 | 112 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑟 → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) |
114 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑥↑𝑗)))) = (𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗)))) |
115 | | nn0ex 11175 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
ℕ0 ∈ V |
116 | 115 | mptex 6390 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗))) ∈ V |
117 | 113, 114,
116 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑟 ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑥↑𝑗))))‘𝑟) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) |
118 | 110, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 ∈ ℝ → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑥↑𝑗))))‘𝑟) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) |
119 | 118 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 ∈ ℝ → (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗))) = ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗))))‘𝑟)) |
120 | 119 | seqeq3d 12671 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ ℝ → seq0( + ,
(𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) = seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗))))‘𝑟))) |
121 | 120 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ ℝ → (seq0( +
, (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ ↔ seq0( + ,
((𝑥 ∈ ℂ ↦
(𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗))))‘𝑟)) ∈ dom ⇝ )) |
122 | 121 | rabbiia 3161 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ } = {𝑟 ∈ ℝ ∣ seq0( +
, ((𝑥 ∈ ℂ
↦ (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗))))‘𝑟)) ∈ dom ⇝ } |
123 | 122 | supeq1i 8236 |
. . . . . . . . . . . . . . . 16
⊢
sup({𝑟 ∈
ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ) = sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑥↑𝑗))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
124 | 100, 109,
123 | radcnvcl 23975 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ sup({𝑟 ∈
ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ) ∈ (0[,]+∞)) |
125 | 88, 124 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ sup({𝑟 ∈
ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ) ∈ ℝ*) |
126 | 46, 125 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ) ∈ ℝ*) |
127 | | 1re 9918 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
128 | | avglt1 11147 |
. . . . . . . . . . . . . . 15
⊢
(((abs‘𝑦)
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑦) < 1 ↔ (abs‘𝑦) < (((abs‘𝑦) + 1) / 2))) |
129 | 56, 127, 128 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → ((abs‘𝑦) < 1 ↔ (abs‘𝑦) < (((abs‘𝑦) + 1) / 2))) |
130 | 66, 129 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (abs‘𝑦) < (((abs‘𝑦) + 1) / 2)) |
131 | | 0red 9920 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → 0 ∈ ℝ) |
132 | 131, 56, 86, 82, 130 | lelttrd 10074 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → 0 < (((abs‘𝑦) + 1) / 2)) |
133 | 131, 86, 132 | ltled 10064 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → 0 ≤ (((abs‘𝑦) + 1) / 2)) |
134 | 86, 133 | absidd 14009 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (abs‘(((abs‘𝑦) + 1) / 2)) = (((abs‘𝑦) + 1) / 2)) |
135 | 46, 109 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚))):ℕ0⟶ℂ) |
136 | 86 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (((abs‘𝑦) + 1) / 2) ∈ ℂ) |
137 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = (((abs‘𝑦) + 1) / 2) → (𝑥↑𝑗) = ((((abs‘𝑦) + 1) / 2)↑𝑗)) |
138 | 137 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (((abs‘𝑦) + 1) / 2) → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗))) |
139 | 138 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (((abs‘𝑦) + 1) / 2) → (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑥↑𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))) |
140 | 115 | mptex 6390 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) ·
((((abs‘𝑦) + 1) /
2)↑𝑗))) ∈
V |
141 | 139, 114,
140 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . 18
⊢
((((abs‘𝑦) +
1) / 2) ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗))))‘(((abs‘𝑦) + 1) / 2)) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))) |
142 | 136, 141 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗))))‘(((abs‘𝑦) + 1) / 2)) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))) |
143 | 142 | seqeq3d 12671 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗))))‘(((abs‘𝑦) + 1) / 2))) = seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗))))) |
144 | | avglt2 11148 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((abs‘𝑦)
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑦) < 1 ↔ (((abs‘𝑦) + 1) / 2) <
1)) |
145 | 56, 127, 144 | sylancl 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → ((abs‘𝑦) < 1 ↔ (((abs‘𝑦) + 1) / 2) <
1)) |
146 | 66, 145 | mpbid 221 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (((abs‘𝑦) + 1) / 2) < 1) |
147 | 134, 146 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (abs‘(((abs‘𝑦) + 1) / 2)) < 1) |
148 | | logtayllem 24205 |
. . . . . . . . . . . . . . . . 17
⊢
(((((abs‘𝑦) +
1) / 2) ∈ ℂ ∧ (abs‘(((abs‘𝑦) + 1) / 2)) < 1) → seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) ·
((((abs‘𝑦) + 1) /
2)↑𝑗)))) ∈ dom
⇝ ) |
149 | 136, 147,
148 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · ((((abs‘𝑦) + 1) / 2)↑𝑗)))) ∈ dom ⇝ ) |
150 | 143, 149 | eqeltrd 2688 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → seq0( + , ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗))))‘(((abs‘𝑦) + 1) / 2))) ∈ dom ⇝
) |
151 | 100, 135,
123, 136, 150 | radcnvle 23978 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (abs‘(((abs‘𝑦) + 1) / 2)) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )) |
152 | 134, 151 | eqbrtrrd 4607 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (((abs‘𝑦) + 1) / 2) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )) |
153 | 83, 87, 126, 130, 152 | xrltletrd 11868 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (abs‘𝑦) < sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )) |
154 | | 0re 9919 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
155 | | elico2 12108 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ sup({𝑟
∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ) ∈ ℝ*) →
((abs‘𝑦) ∈
(0[,)sup({𝑟 ∈ ℝ
∣ seq0( + , (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )) ↔ ((abs‘𝑦) ∈ ℝ ∧ 0 ≤
(abs‘𝑦) ∧
(abs‘𝑦) <
sup({𝑟 ∈ ℝ
∣ seq0( + , (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )))) |
156 | 154, 126,
155 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → ((abs‘𝑦) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )) ↔ ((abs‘𝑦) ∈ ℝ ∧ 0 ≤
(abs‘𝑦) ∧
(abs‘𝑦) <
sup({𝑟 ∈ ℝ
∣ seq0( + , (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )))) |
157 | 56, 82, 153, 156 | mpbir3and 1238 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (abs‘𝑦) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) |
158 | | absf 13925 |
. . . . . . . . . . . 12
⊢
abs:ℂ⟶ℝ |
159 | | ffn 5958 |
. . . . . . . . . . . 12
⊢
(abs:ℂ⟶ℝ → abs Fn ℂ) |
160 | | elpreima 6245 |
. . . . . . . . . . . 12
⊢ (abs Fn
ℂ → (𝑦 ∈
(◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( +
, (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ↔ (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( +
, (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))))) |
161 | 158, 159,
160 | mp2b 10 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ↔ (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( +
, (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )))) |
162 | 53, 157, 161 | sylanbrc 695 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → 𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )))) |
163 | | cnvimass 5404 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ⊆ dom abs |
164 | 158 | fdmi 5965 |
. . . . . . . . . . . . . . . . . 18
⊢ dom abs =
ℂ |
165 | 163, 164 | sseqtri 3600 |
. . . . . . . . . . . . . . . . 17
⊢ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ⊆ ℂ |
166 | 165 | sseli 3564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) → 𝑦 ∈ ℂ) |
167 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑦 → (𝑥↑𝑗) = (𝑦↑𝑗)) |
168 | 167 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑦 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗)) = (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦↑𝑗))) |
169 | 168 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦↑𝑗)))) |
170 | 115 | mptex 6390 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑦↑𝑗))) ∈ V |
171 | 169, 114,
170 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℂ → ((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑥↑𝑗))))‘𝑦) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦↑𝑗)))) |
172 | 171 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0)
→ ((𝑥 ∈ ℂ
↦ (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗))))‘𝑦) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦↑𝑗)))) |
173 | 172 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0)
→ (((𝑥 ∈ ℂ
↦ (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗))))‘𝑦)‘𝑛) = ((𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦↑𝑗)))‘𝑛)) |
174 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑛 → (𝑗 = 0 ↔ 𝑛 = 0)) |
175 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑛 → (1 / 𝑗) = (1 / 𝑛)) |
176 | 174, 175 | ifbieq2d 4061 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑛 → if(𝑗 = 0, 0, (1 / 𝑗)) = if(𝑛 = 0, 0, (1 / 𝑛))) |
177 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑛 → (𝑦↑𝑗) = (𝑦↑𝑛)) |
178 | 176, 177 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑛 → (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦↑𝑗)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))) |
179 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑦↑𝑗))) = (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦↑𝑗))) |
180 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)) ∈ V |
181 | 178, 179,
180 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ0
→ ((𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦↑𝑗)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))) |
182 | 181 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0)
→ ((𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑦↑𝑗)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))) |
183 | 173, 182 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℂ ∧ 𝑛 ∈ ℕ0)
→ (if(𝑛 = 0, 0, (1 /
𝑛)) · (𝑦↑𝑛)) = (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗))))‘𝑦)‘𝑛)) |
184 | 183 | sumeq2dv 14281 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℂ →
Σ𝑛 ∈
ℕ0 (if(𝑛 =
0, 0, (1 / 𝑛)) ·
(𝑦↑𝑛)) = Σ𝑛 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑥↑𝑗))))‘𝑦)‘𝑛)) |
185 | 166, 184 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)) = Σ𝑛 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑥↑𝑗))))‘𝑦)‘𝑛)) |
186 | 185 | mpteq2ia 4668 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))) = (𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑥↑𝑗))))‘𝑦)‘𝑛)) |
187 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) = (◡abs
“ (0[,)sup({𝑟 ∈
ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) |
188 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
if(sup({𝑟 ∈
ℝ ∣ seq0( + , (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ) ∈ ℝ, (((abs‘𝑧) + sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )) / 2), ((abs‘𝑧) + 1)) = if(sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ) ∈ ℝ, (((abs‘𝑧) + sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )) / 2), ((abs‘𝑧) + 1)) |
189 | 100, 186,
109, 123, 187, 188 | psercn 23984 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))) ∈ ((◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )))–cn→ℂ)) |
190 | | cncff 22504 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))) ∈ ((◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )))–cn→ℂ) → (𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))):(◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )))⟶ℂ) |
191 | 189, 190 | syl 17 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))):(◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )))⟶ℂ) |
192 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))) = (𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))) |
193 | 192 | fmpt 6289 |
. . . . . . . . . . . 12
⊢
(∀𝑦 ∈
(◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( +
, (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )))Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)) ∈ ℂ ↔ (𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))):(◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )))⟶ℂ) |
194 | 191, 193 | sylibr 223 |
. . . . . . . . . . 11
⊢ (⊤
→ ∀𝑦 ∈
(◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( +
, (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )))Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)) ∈ ℂ) |
195 | 194 | r19.21bi 2916 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( +
, (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )))) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)) ∈ ℂ) |
196 | 162, 195 | sylan2 490 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ (0(ball‘(abs ∘ − ))1)) → Σ𝑛 ∈ ℕ0
(if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)) ∈ ℂ) |
197 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))) = (𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ Σ𝑛
∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))) |
198 | 196, 197 | fmptd 6292 |
. . . . . . . 8
⊢ (⊤
→ (𝑦 ∈
(0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))):(0(ball‘(abs ∘ −
))1)⟶ℂ) |
199 | | cnelprrecn 9908 |
. . . . . . . . . . . . 13
⊢ ℂ
∈ {ℝ, ℂ} |
200 | 199 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
201 | 77 | adantl 481 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑦
∈ (0(ball‘(abs ∘ − ))1)) → (log‘(1 −
𝑦)) ∈
ℂ) |
202 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ ((1 / (1
− 𝑦)) · -1)
∈ V |
203 | 202 | a1i 11 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑦
∈ (0(ball‘(abs ∘ − ))1)) → ((1 / (1 − 𝑦)) · -1) ∈
V) |
204 | 29 | cnmetdval 22384 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℂ ∧ (1 − 𝑦) ∈ ℂ) → (1(abs ∘
− )(1 − 𝑦)) =
(abs‘(1 − (1 − 𝑦)))) |
205 | 50, 55, 204 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) = (abs‘(1 − (1
− 𝑦)))) |
206 | | nncan 10189 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℂ ∧ 𝑦
∈ ℂ) → (1 − (1 − 𝑦)) = 𝑦) |
207 | 50, 53, 206 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (1 − (1 − 𝑦)) = 𝑦) |
208 | 207 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (abs‘(1 − (1 − 𝑦))) = (abs‘𝑦)) |
209 | 205, 208 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) = (abs‘𝑦)) |
210 | 209, 66 | eqbrtrd 4605 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (1(abs ∘ − )(1 − 𝑦)) < 1) |
211 | | elbl 22003 |
. . . . . . . . . . . . . . . 16
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℂ
∧ 1 ∈ ℝ*) → ((1 − 𝑦) ∈ (1(ball‘(abs ∘ −
))1) ↔ ((1 − 𝑦)
∈ ℂ ∧ (1(abs ∘ − )(1 − 𝑦)) < 1))) |
212 | 38, 50, 41, 211 | mp3an 1416 |
. . . . . . . . . . . . . . 15
⊢ ((1
− 𝑦) ∈
(1(ball‘(abs ∘ − ))1) ↔ ((1 − 𝑦) ∈ ℂ ∧ (1(abs ∘ −
)(1 − 𝑦)) <
1)) |
213 | 55, 210, 212 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (1 − 𝑦) ∈ (1(ball‘(abs ∘ −
))1)) |
214 | 213 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑦
∈ (0(ball‘(abs ∘ − ))1)) → (1 − 𝑦) ∈ (1(ball‘(abs
∘ − ))1)) |
215 | | neg1cn 11001 |
. . . . . . . . . . . . . 14
⊢ -1 ∈
ℂ |
216 | 215 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑦
∈ (0(ball‘(abs ∘ − ))1)) → -1 ∈
ℂ) |
217 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘
− ))1) |
218 | 217 | dvlog2lem 24198 |
. . . . . . . . . . . . . . . . 17
⊢
(1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖
(-∞(,]0)) |
219 | 218 | sseli 3564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1(ball‘(abs
∘ − ))1) → 𝑥 ∈ (ℂ ∖
(-∞(,]0))) |
220 | 219 | eldifad 3552 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1(ball‘(abs
∘ − ))1) → 𝑥 ∈ ℂ) |
221 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
222 | 221 | logdmn0 24186 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (ℂ ∖
(-∞(,]0)) → 𝑥
≠ 0) |
223 | 219, 222 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1(ball‘(abs
∘ − ))1) → 𝑥 ≠ 0) |
224 | 220, 223 | logcld 24121 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1(ball‘(abs
∘ − ))1) → (log‘𝑥) ∈ ℂ) |
225 | 224 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(ball‘(abs ∘ − ))1)) → (log‘𝑥) ∈
ℂ) |
226 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ (1 /
𝑥) ∈
V |
227 | 226 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(ball‘(abs ∘ − ))1)) → (1 / 𝑥) ∈ V) |
228 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑦
∈ ℂ) → 𝑦
∈ ℂ) |
229 | 50, 228, 54 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑦
∈ ℂ) → (1 − 𝑦) ∈ ℂ) |
230 | 215 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑦
∈ ℂ) → -1 ∈ ℂ) |
231 | | 1cnd 9935 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑦
∈ ℂ) → 1 ∈ ℂ) |
232 | | 0cnd 9912 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑦
∈ ℂ) → 0 ∈ ℂ) |
233 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ 1 ∈ ℂ) |
234 | 200, 233 | dvmptc 23527 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ 1)) = (𝑦
∈ ℂ ↦ 0)) |
235 | 200 | dvmptid 23526 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ 𝑦)) =
(𝑦 ∈ ℂ ↦
1)) |
236 | 200, 231,
232, 234, 228, 231, 235 | dvmptsub 23536 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ (1 − 𝑦))) = (𝑦 ∈ ℂ ↦ (0 −
1))) |
237 | | df-neg 10148 |
. . . . . . . . . . . . . . . 16
⊢ -1 = (0
− 1) |
238 | 237 | mpteq2i 4669 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℂ ↦ -1) =
(𝑦 ∈ ℂ ↦
(0 − 1)) |
239 | 236, 238 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (ℂ D (𝑦 ∈
ℂ ↦ (1 − 𝑦))) = (𝑦 ∈ ℂ ↦ -1)) |
240 | 52 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (0(ball‘(abs ∘ − ))1) ⊆
ℂ) |
241 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
242 | 241 | cnfldtop 22397 |
. . . . . . . . . . . . . . . 16
⊢
(TopOpen‘ℂfld) ∈ Top |
243 | 241 | cnfldtopon 22396 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
244 | 243 | toponunii 20547 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
245 | 244 | restid 15917 |
. . . . . . . . . . . . . . . 16
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
246 | 242, 245 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
247 | 246 | eqcomi 2619 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
248 | 241 | cnfldtopn 22395 |
. . . . . . . . . . . . . . . . 17
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
249 | 248 | blopn 22115 |
. . . . . . . . . . . . . . . 16
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 1 ∈ ℝ*) → (0(ball‘(abs ∘ −
))1) ∈ (TopOpen‘ℂfld)) |
250 | 38, 28, 41, 249 | mp3an 1416 |
. . . . . . . . . . . . . . 15
⊢
(0(ball‘(abs ∘ − ))1) ∈
(TopOpen‘ℂfld) |
251 | 250 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (0(ball‘(abs ∘ − ))1) ∈
(TopOpen‘ℂfld)) |
252 | 200, 229,
230, 239, 240, 247, 241, 251 | dvmptres 23532 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑦 ∈
(0(ball‘(abs ∘ − ))1) ↦ (1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ -1)) |
253 | 217 | dvlog2 24199 |
. . . . . . . . . . . . . 14
⊢ (ℂ
D (log ↾ (1(ball‘(abs ∘ − ))1))) = (𝑥 ∈ (1(ball‘(abs ∘ −
))1) ↦ (1 / 𝑥)) |
254 | | logf1o 24115 |
. . . . . . . . . . . . . . . . . . . 20
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
255 | | f1of 6050 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})⟶ran log) |
256 | 254, 255 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
log:(ℂ ∖ {0})⟶ran log |
257 | 221 | logdmss 24188 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℂ
∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}) |
258 | 218, 257 | sstri 3577 |
. . . . . . . . . . . . . . . . . . 19
⊢
(1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖
{0}) |
259 | | fssres 5983 |
. . . . . . . . . . . . . . . . . . 19
⊢
((log:(ℂ ∖ {0})⟶ran log ∧ (1(ball‘(abs
∘ − ))1) ⊆ (ℂ ∖ {0})) → (log ↾
(1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ −
))1)⟶ran log) |
260 | 256, 258,
259 | mp2an 704 |
. . . . . . . . . . . . . . . . . 18
⊢ (log
↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘
− ))1)⟶ran log |
261 | 260 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ (log ↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs
∘ − ))1)⟶ran log) |
262 | 261 | feqmptd 6159 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ (log ↾ (1(ball‘(abs ∘ − ))1)) = (𝑥 ∈ (1(ball‘(abs
∘ − ))1) ↦ ((log ↾ (1(ball‘(abs ∘ −
))1))‘𝑥))) |
263 | | fvres 6117 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1(ball‘(abs
∘ − ))1) → ((log ↾ (1(ball‘(abs ∘ −
))1))‘𝑥) =
(log‘𝑥)) |
264 | 263 | mpteq2ia 4668 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1(ball‘(abs
∘ − ))1) ↦ ((log ↾ (1(ball‘(abs ∘ −
))1))‘𝑥)) = (𝑥 ∈ (1(ball‘(abs
∘ − ))1) ↦ (log‘𝑥)) |
265 | 262, 264 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ (log ↾ (1(ball‘(abs ∘ − ))1)) = (𝑥 ∈ (1(ball‘(abs
∘ − ))1) ↦ (log‘𝑥))) |
266 | 265 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (ℂ D (log ↾ (1(ball‘(abs ∘ − ))1))) =
(ℂ D (𝑥 ∈
(1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥)))) |
267 | 253, 266 | syl5reqr 2659 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑥 ∈
(1(ball‘(abs ∘ − ))1) ↦ (log‘𝑥))) = (𝑥 ∈ (1(ball‘(abs ∘ −
))1) ↦ (1 / 𝑥))) |
268 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1 − 𝑦) → (log‘𝑥) = (log‘(1 − 𝑦))) |
269 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1 − 𝑦) → (1 / 𝑥) = (1 / (1 − 𝑦))) |
270 | 200, 200,
214, 216, 225, 227, 252, 267, 268, 269 | dvmptco 23541 |
. . . . . . . . . . . 12
⊢ (⊤
→ (ℂ D (𝑦 ∈
(0(ball‘(abs ∘ − ))1) ↦ (log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ ((1 / (1 − 𝑦)) · -1))) |
271 | 200, 201,
203, 270 | dvmptneg 23535 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑦 ∈
(0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ -((1 / (1 − 𝑦)) · -1))) |
272 | 55, 76 | reccld 10673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (1 / (1 − 𝑦)) ∈ ℂ) |
273 | | mulcom 9901 |
. . . . . . . . . . . . . . . 16
⊢ (((1 / (1
− 𝑦)) ∈ ℂ
∧ -1 ∈ ℂ) → ((1 / (1 − 𝑦)) · -1) = (-1 · (1 / (1
− 𝑦)))) |
274 | 272, 215,
273 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → ((1 / (1 − 𝑦)) · -1) = (-1 · (1 / (1
− 𝑦)))) |
275 | 272 | mulm1d 10361 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (-1 · (1 / (1 − 𝑦))) = -(1 / (1 − 𝑦))) |
276 | 274, 275 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → ((1 / (1 − 𝑦)) · -1) = -(1 / (1 − 𝑦))) |
277 | 276 | negeqd 10154 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → -((1 / (1 − 𝑦)) · -1) = --(1 / (1 − 𝑦))) |
278 | 272 | negnegd 10262 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → --(1 / (1 − 𝑦)) = (1 / (1 − 𝑦))) |
279 | 277, 278 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → -((1 / (1 − 𝑦)) · -1) = (1 / (1 − 𝑦))) |
280 | 279 | mpteq2ia 4668 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) ↦ -((1 / (1 − 𝑦)) · -1)) = (𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ (1 / (1 − 𝑦))) |
281 | 271, 280 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (⊤
→ (ℂ D (𝑦 ∈
(0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ (1 / (1 − 𝑦)))) |
282 | 281 | dmeqd 5248 |
. . . . . . . . 9
⊢ (⊤
→ dom (ℂ D (𝑦
∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 −
𝑦)))) = dom (𝑦 ∈ (0(ball‘(abs
∘ − ))1) ↦ (1 / (1 − 𝑦)))) |
283 | | dmmptg 5549 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
(0(ball‘(abs ∘ − ))1)(1 / (1 − 𝑦)) ∈ V → dom (𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ (1 / (1 − 𝑦))) = (0(ball‘(abs ∘ −
))1)) |
284 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (1 / (1
− 𝑦)) ∈
V |
285 | 284 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → (1 / (1 − 𝑦)) ∈ V) |
286 | 283, 285 | mprg 2910 |
. . . . . . . . 9
⊢ dom
(𝑦 ∈
(0(ball‘(abs ∘ − ))1) ↦ (1 / (1 − 𝑦))) = (0(ball‘(abs ∘
− ))1) |
287 | 282, 286 | syl6eq 2660 |
. . . . . . . 8
⊢ (⊤
→ dom (ℂ D (𝑦
∈ (0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 −
𝑦)))) = (0(ball‘(abs
∘ − ))1)) |
288 | | sumex 14266 |
. . . . . . . . . . . 12
⊢
Σ𝑛 ∈
ℕ ((𝑛 ·
((𝑚 ∈
ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) ∈ V |
289 | 288 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑦
∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( +
, (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )))) → Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) ∈ V) |
290 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑘 → (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗))))‘𝑦)‘𝑛) = (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗))))‘𝑦)‘𝑘)) |
291 | 290 | cbvsumv 14274 |
. . . . . . . . . . . . . 14
⊢
Σ𝑛 ∈
ℕ0 (((𝑥
∈ ℂ ↦ (𝑗
∈ ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑥↑𝑗))))‘𝑦)‘𝑛) = Σ𝑘 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑥↑𝑗))))‘𝑦)‘𝑘) |
292 | 185, 291 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)) = Σ𝑘 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑥↑𝑗))))‘𝑦)‘𝑘)) |
293 | 292 | mpteq2ia 4668 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))) = (𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ↦ Σ𝑘 ∈ ℕ0 (((𝑥 ∈ ℂ ↦ (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑥↑𝑗))))‘𝑦)‘𝑘)) |
294 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(0(ball‘(abs ∘ − ))(((abs‘𝑧) + if(sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ) ∈ ℝ, (((abs‘𝑧) + sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )) / 2), ((abs‘𝑧) + 1))) / 2)) = (0(ball‘(abs ∘
− ))(((abs‘𝑧) +
if(sup({𝑟 ∈ ℝ
∣ seq0( + , (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ) ∈ ℝ, (((abs‘𝑧) + sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )) / 2), ((abs‘𝑧) + 1))) / 2)) |
295 | 100, 293,
109, 123, 187, 188, 294 | pserdv2 23988 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑦 ∈
(◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( +
, (𝑗 ∈
ℕ0 ↦ (if(𝑗 = 0, 0, (1 / 𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)))) = (𝑦 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))))) |
296 | 162 | ssriv 3572 |
. . . . . . . . . . . 12
⊢
(0(ball‘(abs ∘ − ))1) ⊆ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < ))) |
297 | 296 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ (0(ball‘(abs ∘ − ))1) ⊆ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑗 ∈ ℕ0
↦ (if(𝑗 = 0, 0, (1 /
𝑗)) · (𝑟↑𝑗)))) ∈ dom ⇝ },
ℝ*, < )))) |
298 | 200, 195,
289, 295, 297, 247, 241, 251 | dvmptres 23532 |
. . . . . . . . . 10
⊢ (⊤
→ (ℂ D (𝑦 ∈
(0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)))) = (𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ Σ𝑛
∈ ℕ ((𝑛 ·
((𝑚 ∈
ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))))) |
299 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
300 | 299 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ (0(ball‘(abs
∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0) |
301 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → (𝑚 = 0 ↔ 𝑛 = 0)) |
302 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛)) |
303 | 301, 302 | ifbieq2d 4061 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → if(𝑚 = 0, 0, (1 / 𝑚)) = if(𝑛 = 0, 0, (1 / 𝑛))) |
304 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 /
𝑛) ∈
V |
305 | 93, 304 | ifex 4106 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(𝑛 = 0, 0, (1 / 𝑛)) ∈ V |
306 | 303, 92, 305 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ0
→ ((𝑚 ∈
ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛) = if(𝑛 = 0, 0, (1 / 𝑛))) |
307 | 300, 306 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (0(ball‘(abs
∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛) = if(𝑛 = 0, 0, (1 / 𝑛))) |
308 | | nnne0 10930 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) |
309 | 308 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ (0(ball‘(abs
∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0) |
310 | 309 | neneqd 2787 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ (0(ball‘(abs
∘ − ))1) ∧ 𝑛 ∈ ℕ) → ¬ 𝑛 = 0) |
311 | 310 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (0(ball‘(abs
∘ − ))1) ∧ 𝑛 ∈ ℕ) → if(𝑛 = 0, 0, (1 / 𝑛)) = (1 / 𝑛)) |
312 | 307, 311 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ (0(ball‘(abs
∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛) = (1 / 𝑛)) |
313 | 312 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ (0(ball‘(abs
∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) = (𝑛 · (1 / 𝑛))) |
314 | | nncn 10905 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
315 | 314 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ (0(ball‘(abs
∘ − ))1) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) |
316 | 315, 309 | recidd 10675 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ (0(ball‘(abs
∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · (1 / 𝑛)) = 1) |
317 | 313, 316 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ (0(ball‘(abs
∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) = 1) |
318 | 317 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ (0(ball‘(abs
∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (1 · (𝑦↑(𝑛 − 1)))) |
319 | | nnm1nn0 11211 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
320 | | expcl 12740 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℂ ∧ (𝑛 − 1) ∈
ℕ0) → (𝑦↑(𝑛 − 1)) ∈ ℂ) |
321 | 53, 319, 320 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ (0(ball‘(abs
∘ − ))1) ∧ 𝑛 ∈ ℕ) → (𝑦↑(𝑛 − 1)) ∈ ℂ) |
322 | 321 | mulid2d 9937 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ (0(ball‘(abs
∘ − ))1) ∧ 𝑛 ∈ ℕ) → (1 · (𝑦↑(𝑛 − 1))) = (𝑦↑(𝑛 − 1))) |
323 | 318, 322 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ (0(ball‘(abs
∘ − ))1) ∧ 𝑛 ∈ ℕ) → ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (𝑦↑(𝑛 − 1))) |
324 | 323 | sumeq2dv 14281 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1))) |
325 | | nnuz 11599 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘1) |
326 | | 1e0p1 11428 |
. . . . . . . . . . . . . . . 16
⊢ 1 = (0 +
1) |
327 | 326 | fveq2i 6106 |
. . . . . . . . . . . . . . 15
⊢
(ℤ≥‘1) = (ℤ≥‘(0 +
1)) |
328 | 325, 327 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘(0 + 1)) |
329 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (1 + 𝑚) → (𝑛 − 1) = ((1 + 𝑚) − 1)) |
330 | 329 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (1 + 𝑚) → (𝑦↑(𝑛 − 1)) = (𝑦↑((1 + 𝑚) − 1))) |
331 | | 1zzd 11285 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → 1 ∈ ℤ) |
332 | | 0zd 11266 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → 0 ∈ ℤ) |
333 | 1, 328, 330, 331, 332, 321 | isumshft 14410 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)) = Σ𝑚 ∈ ℕ0 (𝑦↑((1 + 𝑚) − 1))) |
334 | | pncan2 10167 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ 𝑚
∈ ℂ) → ((1 + 𝑚) − 1) = 𝑚) |
335 | 50, 102, 334 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ0
→ ((1 + 𝑚) − 1)
= 𝑚) |
336 | 335 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ0
→ (𝑦↑((1 + 𝑚) − 1)) = (𝑦↑𝑚)) |
337 | 336 | sumeq2i 14277 |
. . . . . . . . . . . . 13
⊢
Σ𝑚 ∈
ℕ0 (𝑦↑((1 + 𝑚) − 1)) = Σ𝑚 ∈ ℕ0 (𝑦↑𝑚) |
338 | 333, 337 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → Σ𝑛 ∈ ℕ (𝑦↑(𝑛 − 1)) = Σ𝑚 ∈ ℕ0 (𝑦↑𝑚)) |
339 | | geoisum 14447 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℂ ∧
(abs‘𝑦) < 1)
→ Σ𝑚 ∈
ℕ0 (𝑦↑𝑚) = (1 / (1 − 𝑦))) |
340 | 53, 66, 339 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → Σ𝑚 ∈ ℕ0 (𝑦↑𝑚) = (1 / (1 − 𝑦))) |
341 | 324, 338,
340 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) → Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1))) = (1 / (1 − 𝑦))) |
342 | 341 | mpteq2ia 4668 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (0(ball‘(abs
∘ − ))1) ↦ Σ𝑛 ∈ ℕ ((𝑛 · ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 0, (1 / 𝑚)))‘𝑛)) · (𝑦↑(𝑛 − 1)))) = (𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ (1 / (1 − 𝑦))) |
343 | 298, 342 | syl6eq 2660 |
. . . . . . . . 9
⊢ (⊤
→ (ℂ D (𝑦 ∈
(0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)))) = (𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ (1 / (1 − 𝑦)))) |
344 | 281, 343 | eqtr4d 2647 |
. . . . . . . 8
⊢ (⊤
→ (ℂ D (𝑦 ∈
(0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))) = (ℂ D (𝑦 ∈ (0(ball‘(abs
∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))))) |
345 | | blcntr 22028 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 1 ∈ ℝ+) → 0 ∈ (0(ball‘(abs ∘
− ))1)) |
346 | 38, 28, 39, 345 | mp3an 1416 |
. . . . . . . . 9
⊢ 0 ∈
(0(ball‘(abs ∘ − ))1) |
347 | 346 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 0 ∈ (0(ball‘(abs ∘ − ))1)) |
348 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 0 → (1 − 𝑦) = (1 −
0)) |
349 | | 1m0e1 11008 |
. . . . . . . . . . . . . . . 16
⊢ (1
− 0) = 1 |
350 | 348, 349 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 0 → (1 − 𝑦) = 1) |
351 | 350 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 0 → (log‘(1
− 𝑦)) =
(log‘1)) |
352 | | log1 24136 |
. . . . . . . . . . . . . 14
⊢
(log‘1) = 0 |
353 | 351, 352 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 0 → (log‘(1
− 𝑦)) =
0) |
354 | 353 | negeqd 10154 |
. . . . . . . . . . . 12
⊢ (𝑦 = 0 → -(log‘(1
− 𝑦)) =
-0) |
355 | | neg0 10206 |
. . . . . . . . . . . 12
⊢ -0 =
0 |
356 | 354, 355 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑦 = 0 → -(log‘(1
− 𝑦)) =
0) |
357 | 356, 80, 93 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (0 ∈
(0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ -(log‘(1 − 𝑦)))‘0) = 0) |
358 | 346, 357 | mp1i 13 |
. . . . . . . . 9
⊢ (⊤
→ ((𝑦 ∈
(0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘0) =
0) |
359 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (0 =
if(𝑛 = 0, 0, (1 / 𝑛)) → (0 · (𝑦↑𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))) |
360 | 359 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (0 =
if(𝑛 = 0, 0, (1 / 𝑛)) → ((0 · (𝑦↑𝑛)) = 0 ↔ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)) = 0)) |
361 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ ((1 /
𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)) → ((1 / 𝑛) · (𝑦↑𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛))) |
362 | 361 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ ((1 /
𝑛) = if(𝑛 = 0, 0, (1 / 𝑛)) → (((1 / 𝑛) · (𝑦↑𝑛)) = 0 ↔ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)) = 0)) |
363 | | simpll 786 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑦 = 0) |
364 | 363, 28 | syl6eqel 2696 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑦 ∈ ℂ) |
365 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → 𝑛 ∈ ℕ0) |
366 | 364, 365 | expcld 12870 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → (𝑦↑𝑛) ∈ ℂ) |
367 | 366 | mul02d 10113 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → (0 · (𝑦↑𝑛)) = 0) |
368 | | simpll 786 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) → 𝑦 = 0) |
369 | 368 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) → (𝑦↑𝑛) = (0↑𝑛)) |
370 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
371 | 370, 14 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (𝑛 ∈ ℕ ∨ 𝑛 = 0)) |
372 | 371 | ord 391 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (¬
𝑛 ∈ ℕ →
𝑛 = 0)) |
373 | 372 | con1d 138 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (¬
𝑛 = 0 → 𝑛 ∈
ℕ)) |
374 | 373 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) → 𝑛 ∈
ℕ) |
375 | 374 | 0expd 12886 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) → (0↑𝑛) = 0) |
376 | 369, 375 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) → (𝑦↑𝑛) = 0) |
377 | 376 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) → ((1 / 𝑛) · (𝑦↑𝑛)) = ((1 / 𝑛) · 0)) |
378 | 374 | nnrecred 10943 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) → (1 / 𝑛) ∈
ℝ) |
379 | 378 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) → (1 / 𝑛) ∈
ℂ) |
380 | 379 | mul01d 10114 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) → ((1 / 𝑛) · 0) =
0) |
381 | 377, 380 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑛 = 0) → ((1 / 𝑛) · (𝑦↑𝑛)) = 0) |
382 | 360, 362,
367, 381 | ifbothda 4073 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 0 ∧ 𝑛 ∈ ℕ0) → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)) = 0) |
383 | 382 | sumeq2dv 14281 |
. . . . . . . . . . . 12
⊢ (𝑦 = 0 → Σ𝑛 ∈ ℕ0
(if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)) = Σ𝑛 ∈ ℕ0
0) |
384 | 1 | eqimssi 3622 |
. . . . . . . . . . . . . 14
⊢
ℕ0 ⊆
(ℤ≥‘0) |
385 | 384 | orci 404 |
. . . . . . . . . . . . 13
⊢
(ℕ0 ⊆ (ℤ≥‘0) ∨
ℕ0 ∈ Fin) |
386 | | sumz 14300 |
. . . . . . . . . . . . 13
⊢
((ℕ0 ⊆ (ℤ≥‘0) ∨
ℕ0 ∈ Fin) → Σ𝑛 ∈ ℕ0 0 =
0) |
387 | 385, 386 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
Σ𝑛 ∈
ℕ0 0 = 0 |
388 | 383, 387 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑦 = 0 → Σ𝑛 ∈ ℕ0
(if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)) = 0) |
389 | 388, 197,
93 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (0 ∈
(0(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ Σ𝑛
∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)))‘0) = 0) |
390 | 346, 389 | mp1i 13 |
. . . . . . . . 9
⊢ (⊤
→ ((𝑦 ∈
(0(ball‘(abs ∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)))‘0) = 0) |
391 | 358, 390 | eqtr4d 2647 |
. . . . . . . 8
⊢ (⊤
→ ((𝑦 ∈
(0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘0) = ((𝑦 ∈ (0(ball‘(abs
∘ − ))1) ↦ Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)))‘0)) |
392 | 47, 48, 49, 81, 198, 287, 344, 347, 391 | dv11cn 23568 |
. . . . . . 7
⊢ (⊤
→ (𝑦 ∈
(0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦))) = (𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ Σ𝑛
∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)))) |
393 | 392 | fveq1d 6105 |
. . . . . 6
⊢ (⊤
→ ((𝑦 ∈
(0(ball‘(abs ∘ − ))1) ↦ -(log‘(1 − 𝑦)))‘𝐴) = ((𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ Σ𝑛
∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)))‘𝐴)) |
394 | 46, 393 | mp1i 13 |
. . . . 5
⊢ (𝐴 ∈ (0(ball‘(abs
∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ -(log‘(1 − 𝑦)))‘𝐴) = ((𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ Σ𝑛
∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)))‘𝐴)) |
395 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (1 − 𝑦) = (1 − 𝐴)) |
396 | 395 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (log‘(1 − 𝑦)) = (log‘(1 − 𝐴))) |
397 | 396 | negeqd 10154 |
. . . . . 6
⊢ (𝑦 = 𝐴 → -(log‘(1 − 𝑦)) = -(log‘(1 −
𝐴))) |
398 | | negex 10158 |
. . . . . 6
⊢
-(log‘(1 − 𝐴)) ∈ V |
399 | 397, 80, 398 | fvmpt 6191 |
. . . . 5
⊢ (𝐴 ∈ (0(ball‘(abs
∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ -(log‘(1 − 𝑦)))‘𝐴) = -(log‘(1 − 𝐴))) |
400 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (𝑦↑𝑛) = (𝐴↑𝑛)) |
401 | 400 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛))) |
402 | 401 | sumeq2sdv 14282 |
. . . . . 6
⊢ (𝑦 = 𝐴 → Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛))) |
403 | | sumex 14266 |
. . . . . 6
⊢
Σ𝑛 ∈
ℕ0 (if(𝑛 =
0, 0, (1 / 𝑛)) ·
(𝐴↑𝑛)) ∈ V |
404 | 402, 197,
403 | fvmpt 6191 |
. . . . 5
⊢ (𝐴 ∈ (0(ball‘(abs
∘ − ))1) → ((𝑦 ∈ (0(ball‘(abs ∘ −
))1) ↦ Σ𝑛
∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝑦↑𝑛)))‘𝐴) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛))) |
405 | 394, 399,
404 | 3eqtr3d 2652 |
. . . 4
⊢ (𝐴 ∈ (0(ball‘(abs
∘ − ))1) → -(log‘(1 − 𝐴)) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛))) |
406 | 45, 405 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ -(log‘(1 − 𝐴)) = Σ𝑛 ∈ ℕ0 (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛))) |
407 | 26, 406 | breqtrrd 4611 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , (𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))) ⇝ -(log‘(1 − 𝐴))) |
408 | | seqex 12665 |
. . . 4
⊢ seq0( + ,
(𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))) ∈ V |
409 | 408 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , (𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))) ∈ V) |
410 | | seqex 12665 |
. . . 4
⊢ seq1( + ,
(𝑘 ∈ ℕ ↦
((𝐴↑𝑘) / 𝑘))) ∈ V |
411 | 410 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , (𝑘 ∈
ℕ ↦ ((𝐴↑𝑘) / 𝑘))) ∈ V) |
412 | | 1zzd 11285 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 1 ∈ ℤ) |
413 | | elnnuz 11600 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘1)) |
414 | | fvres 6117 |
. . . . . 6
⊢ (𝑛 ∈
(ℤ≥‘1) → ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))) ↾
(ℤ≥‘1))‘𝑛) = (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘))))‘𝑛)) |
415 | 413, 414 | sylbi 206 |
. . . . 5
⊢ (𝑛 ∈ ℕ → ((seq0( +
, (𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))) ↾
(ℤ≥‘1))‘𝑛) = (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘))))‘𝑛)) |
416 | 415 | eqcomd 2616 |
. . . 4
⊢ (𝑛 ∈ ℕ → (seq0( +
, (𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘))))‘𝑛) = ((seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))) ↾
(ℤ≥‘1))‘𝑛)) |
417 | | addid2 10098 |
. . . . . . . 8
⊢ (𝑛 ∈ ℂ → (0 +
𝑛) = 𝑛) |
418 | 417 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℂ) → (0
+ 𝑛) = 𝑛) |
419 | | 0cnd 9912 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 0 ∈ ℂ) |
420 | | 1eluzge0 11608 |
. . . . . . . 8
⊢ 1 ∈
(ℤ≥‘0) |
421 | 420 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 1 ∈ (ℤ≥‘0)) |
422 | | 0cnd 9912 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) ∧ 𝑘 = 0) → 0 ∈
ℂ) |
423 | | nn0cn 11179 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
424 | 423 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → 𝑘 ∈ ℂ) |
425 | | df-ne 2782 |
. . . . . . . . . . . . 13
⊢ (𝑘 ≠ 0 ↔ ¬ 𝑘 = 0) |
426 | 425 | biimpri 217 |
. . . . . . . . . . . 12
⊢ (¬
𝑘 = 0 → 𝑘 ≠ 0) |
427 | | reccl 10571 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) → (1 / 𝑘) ∈
ℂ) |
428 | 424, 426,
427 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) ∧ ¬ 𝑘 = 0) → (1 / 𝑘) ∈ ℂ) |
429 | 422, 428 | ifclda 4070 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → if(𝑘 = 0, 0, (1 / 𝑘)) ∈ ℂ) |
430 | | expcl 12740 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℂ) |
431 | 430 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → (𝐴↑𝑘) ∈ ℂ) |
432 | 429, 431 | mulcld 9939 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)) ∈ ℂ) |
433 | 432, 8 | fmptd 6292 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘))):ℕ0⟶ℂ) |
434 | | 1nn0 11185 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
435 | | ffvelrn 6265 |
. . . . . . . 8
⊢ (((𝑘 ∈ ℕ0
↦ (if(𝑘 = 0, 0, (1 /
𝑘)) · (𝐴↑𝑘))):ℕ0⟶ℂ ∧
1 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))‘1) ∈ ℂ) |
436 | 433, 434,
435 | sylancl 693 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ ((𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))‘1) ∈ ℂ) |
437 | | elfz1eq 12223 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (0...0) → 𝑛 = 0) |
438 | | 1m1e0 10966 |
. . . . . . . . . . 11
⊢ (1
− 1) = 0 |
439 | 438 | oveq2i 6560 |
. . . . . . . . . 10
⊢ (0...(1
− 1)) = (0...0) |
440 | 437, 439 | eleq2s 2706 |
. . . . . . . . 9
⊢ (𝑛 ∈ (0...(1 − 1))
→ 𝑛 =
0) |
441 | 440 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑛 ∈ (0...(1 − 1))
→ ((𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))‘𝑛) = ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))‘0)) |
442 | | 0nn0 11184 |
. . . . . . . . . 10
⊢ 0 ∈
ℕ0 |
443 | | iftrue 4042 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → if(𝑘 = 0, 0, (1 / 𝑘)) = 0) |
444 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (𝐴↑𝑘) = (𝐴↑0)) |
445 | 443, 444 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)) = (0 · (𝐴↑0))) |
446 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (0
· (𝐴↑0)) ∈
V |
447 | 445, 8, 446 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (0 ∈
ℕ0 → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))‘0) = (0 · (𝐴↑0))) |
448 | 442, 447 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
↦ (if(𝑘 = 0, 0, (1 /
𝑘)) · (𝐴↑𝑘)))‘0) = (0 · (𝐴↑0)) |
449 | | expcl 12740 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 ∈
ℕ0) → (𝐴↑0) ∈ ℂ) |
450 | 27, 442, 449 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (𝐴↑0) ∈
ℂ) |
451 | 450 | mul02d 10113 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (0 · (𝐴↑0)) = 0) |
452 | 448, 451 | syl5eq 2656 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ ((𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))‘0) = 0) |
453 | 441, 452 | sylan9eqr 2666 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ (0...(1 −
1))) → ((𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))‘𝑛) = 0) |
454 | 418, 419,
421, 436, 453 | seqid 12708 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (seq0( + , (𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))) ↾
(ℤ≥‘1)) = seq1( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘))))) |
455 | 308 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
𝑛 ≠ 0) |
456 | 455 | neneqd 2787 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
¬ 𝑛 =
0) |
457 | 456 | iffalsed 4047 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
if(𝑛 = 0, 0, (1 / 𝑛)) = (1 / 𝑛)) |
458 | 457 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
(if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)) = ((1 / 𝑛) · (𝐴↑𝑛))) |
459 | 299, 23 | sylan2 490 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
(𝐴↑𝑛) ∈ ℂ) |
460 | 314 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
𝑛 ∈
ℂ) |
461 | 459, 460,
455 | divrec2d 10684 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
((𝐴↑𝑛) / 𝑛) = ((1 / 𝑛) · (𝐴↑𝑛))) |
462 | 458, 461 | eqtr4d 2647 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
(if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)) = ((𝐴↑𝑛) / 𝑛)) |
463 | 299, 11 | sylan2 490 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
((𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))‘𝑛) = (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛))) |
464 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → 𝑘 = 𝑛) |
465 | 6, 464 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑛 → ((𝐴↑𝑘) / 𝑘) = ((𝐴↑𝑛) / 𝑛)) |
466 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ ↦ ((𝐴↑𝑘) / 𝑘)) = (𝑘 ∈ ℕ ↦ ((𝐴↑𝑘) / 𝑘)) |
467 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((𝐴↑𝑛) / 𝑛) ∈ V |
468 | 465, 466,
467 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((𝐴↑𝑘) / 𝑘))‘𝑛) = ((𝐴↑𝑛) / 𝑛)) |
469 | 468 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
((𝑘 ∈ ℕ ↦
((𝐴↑𝑘) / 𝑘))‘𝑛) = ((𝐴↑𝑛) / 𝑛)) |
470 | 462, 463,
469 | 3eqtr4d 2654 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
((𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))‘𝑛) = ((𝑘 ∈ ℕ ↦ ((𝐴↑𝑘) / 𝑘))‘𝑛)) |
471 | 413, 470 | sylan2br 492 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
(ℤ≥‘1)) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))‘𝑛) = ((𝑘 ∈ ℕ ↦ ((𝐴↑𝑘) / 𝑘))‘𝑛)) |
472 | 412, 471 | seqfeq 12688 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , (𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))) = seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴↑𝑘) / 𝑘)))) |
473 | 454, 472 | eqtrd 2644 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (seq0( + , (𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))) ↾
(ℤ≥‘1)) = seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴↑𝑘) / 𝑘)))) |
474 | 473 | fveq1d 6105 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ ((seq0( + , (𝑘
∈ ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))) ↾
(ℤ≥‘1))‘𝑛) = (seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴↑𝑘) / 𝑘)))‘𝑛)) |
475 | 416, 474 | sylan9eqr 2666 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈ ℕ) →
(seq0( + , (𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘))))‘𝑛) = (seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴↑𝑘) / 𝑘)))‘𝑛)) |
476 | 325, 409,
411, 412, 475 | climeq 14146 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (seq0( + , (𝑘 ∈
ℕ0 ↦ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)))) ⇝ -(log‘(1 − 𝐴)) ↔ seq1( + , (𝑘 ∈ ℕ ↦ ((𝐴↑𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴)))) |
477 | 407, 476 | mpbid 221 |
1
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq1( + , (𝑘 ∈
ℕ ↦ ((𝐴↑𝑘) / 𝑘))) ⇝ -(log‘(1 − 𝐴))) |