Step | Hyp | Ref
| Expression |
1 | | rge0ssre 13440 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℝ |
2 | | ax-resscn 11173 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
3 | 1, 2 | sstri 3991 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℂ |
4 | 3 | sseli 3978 |
. . . . . 6
⊢ (𝑥 ∈ (0[,)+∞) →
𝑥 ∈
ℂ) |
5 | | simpll 764 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → 𝐴 ∈
ℂ) |
6 | | 1cnd 11216 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → 1 ∈
ℂ) |
7 | | simplr 766 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → 𝑥 ∈
ℂ) |
8 | | ax-1ne0 11185 |
. . . . . . . . . . . 12
⊢ 1 ≠
0 |
9 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → 1 ≠
0) |
10 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → ¬ 𝑥 = 0) |
11 | 10 | neqned 2946 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → 𝑥 ≠ 0) |
12 | 5, 6, 7, 9, 11 | divdiv2d 12029 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → (𝐴 / (1 / 𝑥)) = ((𝐴 · 𝑥) / 1)) |
13 | | mulcl 11200 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴 · 𝑥) ∈ ℂ) |
14 | 13 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → (𝐴 · 𝑥) ∈ ℂ) |
15 | 14 | div1d 11989 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → ((𝐴 · 𝑥) / 1) = (𝐴 · 𝑥)) |
16 | 12, 15 | eqtrd 2771 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → (𝐴 / (1 / 𝑥)) = (𝐴 · 𝑥)) |
17 | 16 | oveq2d 7428 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → (1 + (𝐴 / (1 / 𝑥))) = (1 + (𝐴 · 𝑥))) |
18 | 17 | oveq1d 7427 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → ((1 + (𝐴 / (1 / 𝑥)))↑𝑐(1 / 𝑥)) = ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) |
19 | 18 | ifeq2da 4560 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑𝑐(1 / 𝑥))) = if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) |
20 | 4, 19 | sylan2 592 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ (0[,)+∞)) →
if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑𝑐(1 / 𝑥))) = if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) |
21 | 20 | mpteq2dva 5248 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ (0[,)+∞) ↦
if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑𝑐(1 / 𝑥)))) = (𝑥 ∈ (0[,)+∞) ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))))) |
22 | | resmpt 6037 |
. . . . 5
⊢
((0[,)+∞) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ↾ (0[,)+∞)) =
(𝑥 ∈ (0[,)+∞)
↦ if(𝑥 = 0,
(exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))))) |
23 | 3, 22 | ax-mp 5 |
. . . 4
⊢ ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ↾ (0[,)+∞)) =
(𝑥 ∈ (0[,)+∞)
↦ if(𝑥 = 0,
(exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) |
24 | 21, 23 | eqtr4di 2789 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ (0[,)+∞) ↦
if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑𝑐(1 / 𝑥)))) = ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ↾
(0[,)+∞))) |
25 | | 0e0icopnf 13442 |
. . . . 5
⊢ 0 ∈
(0[,)+∞) |
26 | 25 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → 0 ∈
(0[,)+∞)) |
27 | | eqeq2 2743 |
. . . . . . . . 9
⊢
((exp‘(𝐴
· 1)) = if((𝐴
· 𝑥) = 0,
(exp‘(𝐴 · 1)),
(exp‘(𝐴 ·
((log‘(1 + (𝐴
· 𝑥))) / (𝐴 · 𝑥))))) → (if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘(𝐴 · 1)) ↔ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))))) |
28 | | eqeq2 2743 |
. . . . . . . . 9
⊢
((exp‘(𝐴
· ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) = if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) → (if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘(𝐴 · ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥)))) ↔ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))))) |
29 | | efrlim.1 |
. . . . . . . . . . . . 13
⊢ 𝑆 = (0(ball‘(abs ∘
− ))(1 / ((abs‘𝐴) + 1))) |
30 | | cnxmet 24610 |
. . . . . . . . . . . . . 14
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
31 | | 0cnd 11214 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → 0 ∈
ℂ) |
32 | | abscl 15232 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
33 | | peano2re 11394 |
. . . . . . . . . . . . . . . . . 18
⊢
((abs‘𝐴)
∈ ℝ → ((abs‘𝐴) + 1) ∈ ℝ) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) + 1) ∈
ℝ) |
35 | | 0red 11224 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ → 0 ∈
ℝ) |
36 | | absge0 15241 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ → 0 ≤
(abs‘𝐴)) |
37 | 32 | ltp1d 12151 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) <
((abs‘𝐴) +
1)) |
38 | 35, 32, 34, 36, 37 | lelttrd 11379 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ → 0 <
((abs‘𝐴) +
1)) |
39 | 34, 38 | elrpd 13020 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) + 1) ∈
ℝ+) |
40 | 39 | rpreccld 13033 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → (1 /
((abs‘𝐴) + 1)) ∈
ℝ+) |
41 | 40 | rpxrd 13024 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → (1 /
((abs‘𝐴) + 1)) ∈
ℝ*) |
42 | | blssm 24245 |
. . . . . . . . . . . . . 14
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ (1 / ((abs‘𝐴) +
1)) ∈ ℝ*) → (0(ball‘(abs ∘ − ))(1
/ ((abs‘𝐴) + 1)))
⊆ ℂ) |
43 | 30, 31, 41, 42 | mp3an2i 1465 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1))) ⊆ ℂ) |
44 | 29, 43 | eqsstrid 4030 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → 𝑆 ⊆
ℂ) |
45 | 44 | sselda 3982 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℂ) |
46 | | mul0or 11861 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝐴 · 𝑥) = 0 ↔ (𝐴 = 0 ∨ 𝑥 = 0))) |
47 | 45, 46 | syldan 590 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((𝐴 · 𝑥) = 0 ↔ (𝐴 = 0 ∨ 𝑥 = 0))) |
48 | 7, 11 | reccld 11990 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → (1 / 𝑥) ∈
ℂ) |
49 | 45, 48 | syldanl 601 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 = 0) → (1 / 𝑥) ∈ ℂ) |
50 | 49 | adantlr 712 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (1 / 𝑥) ∈ ℂ) |
51 | 50 | 1cxpd 26556 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (1↑𝑐(1 /
𝑥)) = 1) |
52 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → 𝐴 = 0) |
53 | 52 | oveq1d 7427 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (𝐴 · 𝑥) = (0 · 𝑥)) |
54 | 45 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → 𝑥 ∈ ℂ) |
55 | 54 | mul02d 11419 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (0 · 𝑥) = 0) |
56 | 53, 55 | eqtrd 2771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (𝐴 · 𝑥) = 0) |
57 | 56 | oveq2d 7428 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (1 + (𝐴 · 𝑥)) = (1 + 0)) |
58 | | 1p0e1 12343 |
. . . . . . . . . . . . . . . . 17
⊢ (1 + 0) =
1 |
59 | 57, 58 | eqtrdi 2787 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (1 + (𝐴 · 𝑥)) = 1) |
60 | 59 | oveq1d 7427 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)) =
(1↑𝑐(1 / 𝑥))) |
61 | 52 | fveq2d 6895 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (exp‘𝐴) = (exp‘0)) |
62 | | ef0 16041 |
. . . . . . . . . . . . . . . 16
⊢
(exp‘0) = 1 |
63 | 61, 62 | eqtrdi 2787 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (exp‘𝐴) = 1) |
64 | 51, 60, 63 | 3eqtr4d 2781 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)) = (exp‘𝐴)) |
65 | 64 | ifeq2da 4560 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = if(𝑥 = 0, (exp‘𝐴), (exp‘𝐴))) |
66 | | ifid 4568 |
. . . . . . . . . . . . 13
⊢ if(𝑥 = 0, (exp‘𝐴), (exp‘𝐴)) = (exp‘𝐴) |
67 | 65, 66 | eqtrdi 2787 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘𝐴)) |
68 | | iftrue 4534 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘𝐴)) |
69 | 68 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 = 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘𝐴)) |
70 | 67, 69 | jaodan 955 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 = 0 ∨ 𝑥 = 0)) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘𝐴)) |
71 | | mulrid 11219 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) |
72 | 71 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 = 0 ∨ 𝑥 = 0)) → (𝐴 · 1) = 𝐴) |
73 | 72 | fveq2d 6895 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 = 0 ∨ 𝑥 = 0)) → (exp‘(𝐴 · 1)) = (exp‘𝐴)) |
74 | 70, 73 | eqtr4d 2774 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 = 0 ∨ 𝑥 = 0)) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘(𝐴 · 1))) |
75 | 47, 74 | sylbida 591 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 · 𝑥) = 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘(𝐴 · 1))) |
76 | | mulne0b 11862 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝐴 ≠ 0 ∧ 𝑥 ≠ 0) ↔ (𝐴 · 𝑥) ≠ 0)) |
77 | 45, 76 | syldan 590 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((𝐴 ≠ 0 ∧ 𝑥 ≠ 0) ↔ (𝐴 · 𝑥) ≠ 0)) |
78 | | df-ne 2940 |
. . . . . . . . . . . 12
⊢ ((𝐴 · 𝑥) ≠ 0 ↔ ¬ (𝐴 · 𝑥) = 0) |
79 | 77, 78 | bitrdi 287 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((𝐴 ≠ 0 ∧ 𝑥 ≠ 0) ↔ ¬ (𝐴 · 𝑥) = 0)) |
80 | | simprr 770 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → 𝑥 ≠ 0) |
81 | 80 | neneqd 2944 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ¬ 𝑥 = 0) |
82 | 81 | iffalsed 4539 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) |
83 | | ax-1cn 11174 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
84 | 45, 13 | syldan 590 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝐴 · 𝑥) ∈ ℂ) |
85 | | addcl 11198 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ (𝐴
· 𝑥) ∈ ℂ)
→ (1 + (𝐴 ·
𝑥)) ∈
ℂ) |
86 | 83, 84, 85 | sylancr 586 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (1 + (𝐴 · 𝑥)) ∈ ℂ) |
87 | 86 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (1 + (𝐴 · 𝑥)) ∈ ℂ) |
88 | | eqid 2731 |
. . . . . . . . . . . . . . . . . . 19
⊢
(1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘
− ))1) |
89 | 88 | dvlog2lem 26501 |
. . . . . . . . . . . . . . . . . 18
⊢
(1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖
(-∞(,]0)) |
90 | | eqid 2731 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
91 | 90 | logdmss 26491 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℂ
∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}) |
92 | 89, 91 | sstri 3991 |
. . . . . . . . . . . . . . . . 17
⊢
(1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖
{0}) |
93 | | eqid 2731 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (abs
∘ − ) = (abs ∘ − ) |
94 | 93 | cnmetdval 24608 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((1 +
(𝐴 · 𝑥)) ∈ ℂ ∧ 1 ∈
ℂ) → ((1 + (𝐴
· 𝑥))(abs ∘
− )1) = (abs‘((1 + (𝐴 · 𝑥)) − 1))) |
95 | 86, 83, 94 | sylancl 585 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥))(abs ∘ − )1) = (abs‘((1 +
(𝐴 · 𝑥)) − 1))) |
96 | | pncan2 11474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℂ ∧ (𝐴
· 𝑥) ∈ ℂ)
→ ((1 + (𝐴 ·
𝑥)) − 1) = (𝐴 · 𝑥)) |
97 | 83, 84, 96 | sylancr 586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥)) − 1) = (𝐴 · 𝑥)) |
98 | 97 | fveq2d 6895 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘((1 + (𝐴 · 𝑥)) − 1)) = (abs‘(𝐴 · 𝑥))) |
99 | 95, 98 | eqtrd 2771 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥))(abs ∘ − )1) =
(abs‘(𝐴 ·
𝑥))) |
100 | 84 | abscld 15390 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘(𝐴 · 𝑥)) ∈ ℝ) |
101 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((abs‘𝐴) + 1) ∈ ℝ) |
102 | 45 | abscld 15390 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘𝑥) ∈ ℝ) |
103 | 101, 102 | remulcld 11251 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (((abs‘𝐴) + 1) · (abs‘𝑥)) ∈
ℝ) |
104 | | 1red 11222 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℝ) |
105 | | absmul 15248 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) →
(abs‘(𝐴 ·
𝑥)) = ((abs‘𝐴) · (abs‘𝑥))) |
106 | 45, 105 | syldan 590 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘(𝐴 · 𝑥)) = ((abs‘𝐴) · (abs‘𝑥))) |
107 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘𝐴) ∈ ℝ) |
108 | 107, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((abs‘𝐴) + 1) ∈ ℝ) |
109 | 45 | absge0d 15398 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 0 ≤ (abs‘𝑥)) |
110 | 107 | lep1d 12152 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘𝐴) ≤ ((abs‘𝐴) + 1)) |
111 | 107, 108,
102, 109, 110 | lemul1ad 12160 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((abs‘𝐴) · (abs‘𝑥)) ≤ (((abs‘𝐴) + 1) · (abs‘𝑥))) |
112 | 106, 111 | eqbrtrd 5170 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘(𝐴 · 𝑥)) ≤ (((abs‘𝐴) + 1) · (abs‘𝑥))) |
113 | | 0cn 11213 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
ℂ |
114 | 93 | cnmetdval 24608 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℂ ∧ 0 ∈
ℂ) → (𝑥(abs
∘ − )0) = (abs‘(𝑥 − 0))) |
115 | 45, 113, 114 | sylancl 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝑥(abs ∘ − )0) = (abs‘(𝑥 − 0))) |
116 | 45 | subid1d 11567 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝑥 − 0) = 𝑥) |
117 | 116 | fveq2d 6895 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘(𝑥 − 0)) = (abs‘𝑥)) |
118 | 115, 117 | eqtrd 2771 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝑥(abs ∘ − )0) = (abs‘𝑥)) |
119 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
120 | 119, 29 | eleqtrdi 2842 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (0(ball‘(abs ∘ −
))(1 / ((abs‘𝐴) +
1)))) |
121 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
122 | 41 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (1 / ((abs‘𝐴) + 1)) ∈
ℝ*) |
123 | | 0cnd 11214 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 0 ∈ ℂ) |
124 | | elbl3 24219 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (1 /
((abs‘𝐴) + 1)) ∈
ℝ*) ∧ (0 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ (0(ball‘(abs ∘ −
))(1 / ((abs‘𝐴) +
1))) ↔ (𝑥(abs ∘
− )0) < (1 / ((abs‘𝐴) + 1)))) |
125 | 121, 122,
123, 45, 124 | syl22anc 836 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ (0(ball‘(abs ∘ −
))(1 / ((abs‘𝐴) +
1))) ↔ (𝑥(abs ∘
− )0) < (1 / ((abs‘𝐴) + 1)))) |
126 | 120, 125 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝑥(abs ∘ − )0) < (1 /
((abs‘𝐴) +
1))) |
127 | 118, 126 | eqbrtrrd 5172 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘𝑥) < (1 / ((abs‘𝐴) + 1))) |
128 | 38 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 0 < ((abs‘𝐴) + 1)) |
129 | | ltmuldiv2 12095 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((abs‘𝑥)
∈ ℝ ∧ 1 ∈ ℝ ∧ (((abs‘𝐴) + 1) ∈ ℝ ∧ 0 <
((abs‘𝐴) + 1)))
→ ((((abs‘𝐴) +
1) · (abs‘𝑥))
< 1 ↔ (abs‘𝑥)
< (1 / ((abs‘𝐴) +
1)))) |
130 | 102, 104,
108, 128, 129 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((((abs‘𝐴) + 1) · (abs‘𝑥)) < 1 ↔
(abs‘𝑥) < (1 /
((abs‘𝐴) +
1)))) |
131 | 127, 130 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (((abs‘𝐴) + 1) · (abs‘𝑥)) < 1) |
132 | 100, 103,
104, 112, 131 | lelttrd 11379 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘(𝐴 · 𝑥)) < 1) |
133 | 99, 132 | eqbrtrd 5170 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥))(abs ∘ − )1) <
1) |
134 | | 1rp 12985 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℝ+ |
135 | | rpxr 12990 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) |
136 | 134, 135 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 1 ∈
ℝ*) |
137 | | 1cnd 11216 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℂ) |
138 | | elbl3 24219 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (1 ∈ ℂ ∧ (1 + (𝐴 · 𝑥)) ∈ ℂ)) → ((1 + (𝐴 · 𝑥)) ∈ (1(ball‘(abs ∘ −
))1) ↔ ((1 + (𝐴
· 𝑥))(abs ∘
− )1) < 1)) |
139 | 121, 136,
137, 86, 138 | syl22anc 836 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥)) ∈ (1(ball‘(abs ∘ −
))1) ↔ ((1 + (𝐴
· 𝑥))(abs ∘
− )1) < 1)) |
140 | 133, 139 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (1 + (𝐴 · 𝑥)) ∈ (1(ball‘(abs ∘ −
))1)) |
141 | 92, 140 | sselid 3980 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (1 + (𝐴 · 𝑥)) ∈ (ℂ ∖
{0})) |
142 | | eldifsni 4793 |
. . . . . . . . . . . . . . . 16
⊢ ((1 +
(𝐴 · 𝑥)) ∈ (ℂ ∖ {0})
→ (1 + (𝐴 ·
𝑥)) ≠
0) |
143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (1 + (𝐴 · 𝑥)) ≠ 0) |
144 | 143 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (1 + (𝐴 · 𝑥)) ≠ 0) |
145 | 45 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → 𝑥 ∈ ℂ) |
146 | 145, 80 | reccld 11990 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ ℂ) |
147 | 87, 144, 146 | cxpefd 26561 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)) = (exp‘((1 / 𝑥) · (log‘(1 +
(𝐴 · 𝑥)))))) |
148 | 86, 143 | logcld 26420 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (log‘(1 + (𝐴 · 𝑥))) ∈ ℂ) |
149 | 148 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (log‘(1 + (𝐴 · 𝑥))) ∈ ℂ) |
150 | 146, 149 | mulcomd 11242 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((1 / 𝑥) · (log‘(1 + (𝐴 · 𝑥)))) = ((log‘(1 + (𝐴 · 𝑥))) · (1 / 𝑥))) |
151 | | simpll 764 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → 𝐴 ∈ ℂ) |
152 | | simprl 768 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → 𝐴 ≠ 0) |
153 | 151, 152 | dividd 11995 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (𝐴 / 𝐴) = 1) |
154 | 153 | oveq1d 7427 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((𝐴 / 𝐴) / 𝑥) = (1 / 𝑥)) |
155 | 151, 151,
145, 152, 80 | divdiv1d 12028 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((𝐴 / 𝐴) / 𝑥) = (𝐴 / (𝐴 · 𝑥))) |
156 | 154, 155 | eqtr3d 2773 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) = (𝐴 / (𝐴 · 𝑥))) |
157 | 156 | oveq2d 7428 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((log‘(1 + (𝐴 · 𝑥))) · (1 / 𝑥)) = ((log‘(1 + (𝐴 · 𝑥))) · (𝐴 / (𝐴 · 𝑥)))) |
158 | 84 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (𝐴 · 𝑥) ∈ ℂ) |
159 | 77 | biimpa 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (𝐴 · 𝑥) ≠ 0) |
160 | 149, 151,
158, 159 | div12d 12033 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((log‘(1 + (𝐴 · 𝑥))) · (𝐴 / (𝐴 · 𝑥))) = (𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) |
161 | 150, 157,
160 | 3eqtrd 2775 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((1 / 𝑥) · (log‘(1 + (𝐴 · 𝑥)))) = (𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) |
162 | 161 | fveq2d 6895 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (exp‘((1 / 𝑥) · (log‘(1 +
(𝐴 · 𝑥))))) = (exp‘(𝐴 · ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
163 | 82, 147, 162 | 3eqtrd 2775 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘(𝐴 · ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
164 | 163 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((𝐴 ≠ 0 ∧ 𝑥 ≠ 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘(𝐴 · ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥)))))) |
165 | 79, 164 | sylbird 260 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (¬ (𝐴 · 𝑥) = 0 → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘(𝐴 · ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥)))))) |
166 | 165 | imp 406 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘(𝐴 · ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
167 | 27, 28, 75, 166 | ifbothda 4566 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))) |
168 | 167 | mpteq2dva 5248 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))))) |
169 | 44 | resmptd 6040 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ↾ 𝑆) = (𝑥 ∈ 𝑆 ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))))) |
170 | | 1cnd 11216 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 · 𝑥) = 0) → 1 ∈
ℂ) |
171 | 148 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → (log‘(1 + (𝐴 · 𝑥))) ∈ ℂ) |
172 | 84 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → (𝐴 · 𝑥) ∈ ℂ) |
173 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → ¬ (𝐴 · 𝑥) = 0) |
174 | 173 | neqned 2946 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → (𝐴 · 𝑥) ≠ 0) |
175 | 171, 172,
174 | divcld 11997 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)) ∈ ℂ) |
176 | 170, 175 | ifclda 4563 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) ∈ ℂ) |
177 | | eqidd 2732 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
178 | | eqidd 2732 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦
(exp‘(𝐴 ·
𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘(𝐴 · 𝑦)))) |
179 | | oveq2 7420 |
. . . . . . . . . 10
⊢ (𝑦 = if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) → (𝐴 · 𝑦) = (𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
180 | 179 | fveq2d 6895 |
. . . . . . . . 9
⊢ (𝑦 = if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) → (exp‘(𝐴 · 𝑦)) = (exp‘(𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))) |
181 | | oveq2 7420 |
. . . . . . . . . . 11
⊢
(if((𝐴 ·
𝑥) = 0, 1, ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥))) = 1 → (𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) = (𝐴 · 1)) |
182 | 181 | fveq2d 6895 |
. . . . . . . . . 10
⊢
(if((𝐴 ·
𝑥) = 0, 1, ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥))) = 1 → (exp‘(𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) = (exp‘(𝐴 · 1))) |
183 | | oveq2 7420 |
. . . . . . . . . . 11
⊢
(if((𝐴 ·
𝑥) = 0, 1, ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥))) = ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)) → (𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) = (𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) |
184 | 183 | fveq2d 6895 |
. . . . . . . . . 10
⊢
(if((𝐴 ·
𝑥) = 0, 1, ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥))) = ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)) → (exp‘(𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) = (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
185 | 182, 184 | ifsb 4541 |
. . . . . . . . 9
⊢
(exp‘(𝐴
· if((𝐴 ·
𝑥) = 0, 1, ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥))))) = if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
186 | 180, 185 | eqtrdi 2787 |
. . . . . . . 8
⊢ (𝑦 = if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) → (exp‘(𝐴 · 𝑦)) = if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))) |
187 | 176, 177,
178, 186 | fmptco 7129 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ ℂ ↦
(exp‘(𝐴 ·
𝑦))) ∘ (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))))) |
188 | 168, 169,
187 | 3eqtr4d 2781 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ↾ 𝑆) = ((𝑦 ∈ ℂ ↦ (exp‘(𝐴 · 𝑦))) ∘ (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))) |
189 | | eqidd 2732 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) = (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))) |
190 | | eqidd 2732 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) = (𝑦 ∈ (1(ball‘(abs ∘ −
))1) ↦ if(𝑦 = 1, 1,
((log‘𝑦) / (𝑦 − 1))))) |
191 | | eqeq1 2735 |
. . . . . . . . . . 11
⊢ (𝑦 = (1 + (𝐴 · 𝑥)) → (𝑦 = 1 ↔ (1 + (𝐴 · 𝑥)) = 1)) |
192 | | fveq2 6891 |
. . . . . . . . . . . 12
⊢ (𝑦 = (1 + (𝐴 · 𝑥)) → (log‘𝑦) = (log‘(1 + (𝐴 · 𝑥)))) |
193 | | oveq1 7419 |
. . . . . . . . . . . 12
⊢ (𝑦 = (1 + (𝐴 · 𝑥)) → (𝑦 − 1) = ((1 + (𝐴 · 𝑥)) − 1)) |
194 | 192, 193 | oveq12d 7430 |
. . . . . . . . . . 11
⊢ (𝑦 = (1 + (𝐴 · 𝑥)) → ((log‘𝑦) / (𝑦 − 1)) = ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1))) |
195 | 191, 194 | ifbieq2d 4554 |
. . . . . . . . . 10
⊢ (𝑦 = (1 + (𝐴 · 𝑥)) → if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1))) = if((1 + (𝐴 · 𝑥)) = 1, 1, ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1)))) |
196 | 140, 189,
190, 195 | fmptco 7129 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∘ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))) = (𝑥 ∈ 𝑆 ↦ if((1 + (𝐴 · 𝑥)) = 1, 1, ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1))))) |
197 | 58 | eqeq2i 2744 |
. . . . . . . . . . . 12
⊢ ((1 +
(𝐴 · 𝑥)) = (1 + 0) ↔ (1 + (𝐴 · 𝑥)) = 1) |
198 | 137, 84, 123 | addcand 11424 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥)) = (1 + 0) ↔ (𝐴 · 𝑥) = 0)) |
199 | 197, 198 | bitr3id 285 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥)) = 1 ↔ (𝐴 · 𝑥) = 0)) |
200 | 97 | oveq2d 7428 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1)) = ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) |
201 | 199, 200 | ifbieq2d 4554 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → if((1 + (𝐴 · 𝑥)) = 1, 1, ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1))) = if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) |
202 | 201 | mpteq2dva 5248 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ if((1 + (𝐴 · 𝑥)) = 1, 1, ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1)))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
203 | 196, 202 | eqtrd 2771 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∘ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
204 | | eqid 2731 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t 𝑆) =
((TopOpen‘ℂfld) ↾t 𝑆) |
205 | | eqid 2731 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
206 | 205 | cnfldtopon 24620 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
207 | 206 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
208 | | 1cnd 11216 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → 1 ∈
ℂ) |
209 | 207, 207,
208 | cnmptc 23487 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ 1)
∈ ((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
210 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
211 | 207, 207,
210 | cnmptc 23487 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ 𝐴) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
212 | 207 | cnmptid 23486 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ 𝑥) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
213 | 205 | mpomulcn 24706 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
214 | 213 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
215 | | oveq12 7421 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = 𝐴 ∧ 𝑣 = 𝑥) → (𝑢 · 𝑣) = (𝐴 · 𝑥)) |
216 | 207, 211,
212, 207, 207, 214, 215 | cnmpt12 23492 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
217 | 205 | addcn 24702 |
. . . . . . . . . . . . . 14
⊢ + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
218 | 217 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
219 | 207, 209,
216, 218 | cnmpt12f 23491 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ (1 +
(𝐴 · 𝑥))) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
220 | 204, 207,
44, 219 | cnmpt1res 23501 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn
(TopOpen‘ℂfld))) |
221 | 140 | fmpttd 7116 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))):𝑆⟶(1(ball‘(abs ∘ −
))1)) |
222 | 221 | frnd 6725 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → ran
(𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ⊆ (1(ball‘(abs ∘
− ))1)) |
223 | | difss 4131 |
. . . . . . . . . . . . . 14
⊢ (ℂ
∖ {0}) ⊆ ℂ |
224 | 92, 223 | sstri 3991 |
. . . . . . . . . . . . 13
⊢
(1(ball‘(abs ∘ − ))1) ⊆ ℂ |
225 | 224 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(1(ball‘(abs ∘ − ))1) ⊆ ℂ) |
226 | | cnrest2 23111 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ran (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ⊆ (1(ball‘(abs ∘
− ))1) ∧ (1(ball‘(abs ∘ − ))1) ⊆ ℂ)
→ ((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld))
↔ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn ((TopOpen‘ℂfld)
↾t (1(ball‘(abs ∘ −
))1))))) |
227 | 206, 222,
225, 226 | mp3an2i 1465 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld))
↔ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn ((TopOpen‘ℂfld)
↾t (1(ball‘(abs ∘ −
))1))))) |
228 | 220, 227 | mpbid 231 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn ((TopOpen‘ℂfld)
↾t (1(ball‘(abs ∘ − ))1)))) |
229 | | blcntr 24240 |
. . . . . . . . . . . . 13
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ (1 / ((abs‘𝐴) +
1)) ∈ ℝ+) → 0 ∈ (0(ball‘(abs ∘
− ))(1 / ((abs‘𝐴) + 1)))) |
230 | 30, 31, 40, 229 | mp3an2i 1465 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → 0 ∈
(0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1)))) |
231 | 230, 29 | eleqtrrdi 2843 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → 0 ∈
𝑆) |
232 | | resttopon 22986 |
. . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) |
233 | 206, 44, 232 | sylancr 586 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) |
234 | | toponuni 22737 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
235 | 233, 234 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
236 | 231, 235 | eleqtrd 2834 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → 0 ∈
∪ ((TopOpen‘ℂfld)
↾t 𝑆)) |
237 | | eqid 2731 |
. . . . . . . . . . 11
⊢ ∪ ((TopOpen‘ℂfld)
↾t 𝑆) =
∪ ((TopOpen‘ℂfld)
↾t 𝑆) |
238 | 237 | cncnpi 23103 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn ((TopOpen‘ℂfld)
↾t (1(ball‘(abs ∘ − ))1))) ∧ 0 ∈
∪ ((TopOpen‘ℂfld)
↾t 𝑆))
→ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP ((TopOpen‘ℂfld)
↾t (1(ball‘(abs ∘ −
))1)))‘0)) |
239 | 228, 236,
238 | syl2anc 583 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP ((TopOpen‘ℂfld)
↾t (1(ball‘(abs ∘ −
))1)))‘0)) |
240 | | cnelprrecn 11209 |
. . . . . . . . . . 11
⊢ ℂ
∈ {ℝ, ℂ} |
241 | | logf1o 26414 |
. . . . . . . . . . . . . 14
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
242 | | f1of 6833 |
. . . . . . . . . . . . . 14
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})⟶ran log) |
243 | 241, 242 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
log:(ℂ ∖ {0})⟶ran log |
244 | | logrncn 26412 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ran log → 𝑥 ∈
ℂ) |
245 | 244 | ssriv 3986 |
. . . . . . . . . . . . 13
⊢ ran log
⊆ ℂ |
246 | | fss 6734 |
. . . . . . . . . . . . 13
⊢
((log:(ℂ ∖ {0})⟶ran log ∧ ran log ⊆
ℂ) → log:(ℂ ∖ {0})⟶ℂ) |
247 | 243, 245,
246 | mp2an 689 |
. . . . . . . . . . . 12
⊢
log:(ℂ ∖ {0})⟶ℂ |
248 | | fssres 6757 |
. . . . . . . . . . . 12
⊢
((log:(ℂ ∖ {0})⟶ℂ ∧ (1(ball‘(abs
∘ − ))1) ⊆ (ℂ ∖ {0})) → (log ↾
(1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ −
))1)⟶ℂ) |
249 | 247, 92, 248 | mp2an 689 |
. . . . . . . . . . 11
⊢ (log
↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘
− ))1)⟶ℂ |
250 | | blcntr 24240 |
. . . . . . . . . . . . . 14
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℂ
∧ 1 ∈ ℝ+) → 1 ∈ (1(ball‘(abs ∘
− ))1)) |
251 | 30, 83, 134, 250 | mp3an 1460 |
. . . . . . . . . . . . 13
⊢ 1 ∈
(1(ball‘(abs ∘ − ))1) |
252 | | ovex 7445 |
. . . . . . . . . . . . . 14
⊢ (1 /
𝑦) ∈
V |
253 | 88 | dvlog2 26502 |
. . . . . . . . . . . . . 14
⊢ (ℂ
D (log ↾ (1(ball‘(abs ∘ − ))1))) = (𝑦 ∈ (1(ball‘(abs ∘ −
))1) ↦ (1 / 𝑦)) |
254 | 252, 253 | dmmpti 6694 |
. . . . . . . . . . . . 13
⊢ dom
(ℂ D (log ↾ (1(ball‘(abs ∘ − ))1))) =
(1(ball‘(abs ∘ − ))1) |
255 | 251, 254 | eleqtrri 2831 |
. . . . . . . . . . . 12
⊢ 1 ∈
dom (ℂ D (log ↾ (1(ball‘(abs ∘ −
))1))) |
256 | | eqid 2731 |
. . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ↾t
(1(ball‘(abs ∘ − ))1)) =
((TopOpen‘ℂfld) ↾t (1(ball‘(abs
∘ − ))1)) |
257 | 253 | fveq1i 6892 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℂ
D (log ↾ (1(ball‘(abs ∘ − ))1)))‘1) = ((𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ (1 / 𝑦))‘1) |
258 | | oveq2 7420 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 1 → (1 / 𝑦) = (1 / 1)) |
259 | | 1div1e1 11911 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 / 1) =
1 |
260 | 258, 259 | eqtrdi 2787 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 1 → (1 / 𝑦) = 1) |
261 | | eqid 2731 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ (1 / 𝑦)) = (𝑦 ∈ (1(ball‘(abs ∘ −
))1) ↦ (1 / 𝑦)) |
262 | | 1ex 11217 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
V |
263 | 260, 261,
262 | fvmpt 6998 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
(1(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (1(ball‘(abs ∘ −
))1) ↦ (1 / 𝑦))‘1) = 1) |
264 | 251, 263 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ (1 / 𝑦))‘1) = 1 |
265 | 257, 264 | eqtr2i 2760 |
. . . . . . . . . . . . . . . 16
⊢ 1 =
((ℂ D (log ↾ (1(ball‘(abs ∘ −
))1)))‘1) |
266 | 265 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → 1 = ((ℂ D (log ↾ (1(ball‘(abs
∘ − ))1)))‘1)) |
267 | | fvres 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → ((log ↾ (1(ball‘(abs ∘ −
))1))‘𝑦) =
(log‘𝑦)) |
268 | | fvres 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 ∈
(1(ball‘(abs ∘ − ))1) → ((log ↾ (1(ball‘(abs
∘ − ))1))‘1) = (log‘1)) |
269 | 251, 268 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → ((log ↾ (1(ball‘(abs ∘ −
))1))‘1) = (log‘1)) |
270 | | log1 26435 |
. . . . . . . . . . . . . . . . . . 19
⊢
(log‘1) = 0 |
271 | 269, 270 | eqtrdi 2787 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → ((log ↾ (1(ball‘(abs ∘ −
))1))‘1) = 0) |
272 | 267, 271 | oveq12d 7430 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → (((log ↾ (1(ball‘(abs ∘ −
))1))‘𝑦) −
((log ↾ (1(ball‘(abs ∘ − ))1))‘1)) =
((log‘𝑦) −
0)) |
273 | 92 | sseli 3978 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → 𝑦 ∈ (ℂ ∖
{0})) |
274 | | eldifsn 4790 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (ℂ ∖ {0})
↔ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) |
275 | 273, 274 | sylib 217 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) |
276 | | logcl 26418 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (log‘𝑦) ∈
ℂ) |
277 | 275, 276 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → (log‘𝑦) ∈ ℂ) |
278 | 277 | subid1d 11567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → ((log‘𝑦) − 0) = (log‘𝑦)) |
279 | 272, 278 | eqtr2d 2772 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → (log‘𝑦) = (((log ↾ (1(ball‘(abs ∘
− ))1))‘𝑦)
− ((log ↾ (1(ball‘(abs ∘ −
))1))‘1))) |
280 | 279 | oveq1d 7427 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → ((log‘𝑦) / (𝑦 − 1)) = ((((log ↾
(1(ball‘(abs ∘ − ))1))‘𝑦) − ((log ↾ (1(ball‘(abs
∘ − ))1))‘1)) / (𝑦 − 1))) |
281 | 266, 280 | ifeq12d 4549 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1))) = if(𝑦 = 1, ((ℂ D (log ↾
(1(ball‘(abs ∘ − ))1)))‘1), ((((log ↾
(1(ball‘(abs ∘ − ))1))‘𝑦) − ((log ↾ (1(ball‘(abs
∘ − ))1))‘1)) / (𝑦 − 1)))) |
282 | 281 | mpteq2ia 5251 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) = (𝑦 ∈ (1(ball‘(abs ∘ −
))1) ↦ if(𝑦 = 1,
((ℂ D (log ↾ (1(ball‘(abs ∘ − ))1)))‘1),
((((log ↾ (1(ball‘(abs ∘ − ))1))‘𝑦) − ((log ↾
(1(ball‘(abs ∘ − ))1))‘1)) / (𝑦 − 1)))) |
283 | 256, 205,
282 | dvcnp 25769 |
. . . . . . . . . . . 12
⊢
(((ℂ ∈ {ℝ, ℂ} ∧ (log ↾
(1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ −
))1)⟶ℂ ∧ (1(ball‘(abs ∘ − ))1) ⊆
ℂ) ∧ 1 ∈ dom (ℂ D (log ↾ (1(ball‘(abs ∘
− ))1)))) → (𝑦
∈ (1(ball‘(abs ∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∈
((((TopOpen‘ℂfld) ↾t (1(ball‘(abs
∘ − ))1)) CnP
(TopOpen‘ℂfld))‘1)) |
284 | 255, 283 | mpan2 688 |
. . . . . . . . . . 11
⊢ ((ℂ
∈ {ℝ, ℂ} ∧ (log ↾ (1(ball‘(abs ∘ −
))1)):(1(ball‘(abs ∘ − ))1)⟶ℂ ∧
(1(ball‘(abs ∘ − ))1) ⊆ ℂ) → (𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∈
((((TopOpen‘ℂfld) ↾t (1(ball‘(abs
∘ − ))1)) CnP
(TopOpen‘ℂfld))‘1)) |
285 | 240, 249,
224, 284 | mp3an 1460 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∈
((((TopOpen‘ℂfld) ↾t (1(ball‘(abs
∘ − ))1)) CnP
(TopOpen‘ℂfld))‘1) |
286 | | oveq2 7420 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 0 → (𝐴 · 𝑥) = (𝐴 · 0)) |
287 | 286 | oveq2d 7428 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 0 → (1 + (𝐴 · 𝑥)) = (1 + (𝐴 · 0))) |
288 | | eqid 2731 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) = (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) |
289 | | ovex 7445 |
. . . . . . . . . . . . . 14
⊢ (1 +
(𝐴 · 0)) ∈
V |
290 | 287, 288,
289 | fvmpt 6998 |
. . . . . . . . . . . . 13
⊢ (0 ∈
𝑆 → ((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))‘0) = (1 + (𝐴 · 0))) |
291 | 231, 290 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))‘0) = (1 + (𝐴 · 0))) |
292 | | mul01 11400 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) =
0) |
293 | 292 | oveq2d 7428 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (1 +
(𝐴 · 0)) = (1 +
0)) |
294 | 293, 58 | eqtrdi 2787 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (1 +
(𝐴 · 0)) =
1) |
295 | 291, 294 | eqtrd 2771 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))‘0) = 1) |
296 | 295 | fveq2d 6895 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
((((TopOpen‘ℂfld) ↾t (1(ball‘(abs
∘ − ))1)) CnP (TopOpen‘ℂfld))‘((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))‘0)) =
((((TopOpen‘ℂfld) ↾t (1(ball‘(abs
∘ − ))1)) CnP
(TopOpen‘ℂfld))‘1)) |
297 | 285, 296 | eleqtrrid 2839 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∈
((((TopOpen‘ℂfld) ↾t (1(ball‘(abs
∘ − ))1)) CnP (TopOpen‘ℂfld))‘((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))‘0))) |
298 | | cnpco 23092 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP ((TopOpen‘ℂfld)
↾t (1(ball‘(abs ∘ − ))1)))‘0) ∧
(𝑦 ∈
(1(ball‘(abs ∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∈
((((TopOpen‘ℂfld) ↾t (1(ball‘(abs
∘ − ))1)) CnP (TopOpen‘ℂfld))‘((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))‘0))) → ((𝑦 ∈ (1(ball‘(abs ∘ −
))1) ↦ if(𝑦 = 1, 1,
((log‘𝑦) / (𝑦 − 1)))) ∘ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘0)) |
299 | 239, 297,
298 | syl2anc 583 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∘ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘0)) |
300 | 203, 299 | eqeltrrd 2833 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘0)) |
301 | 207, 207,
210 | cnmptc 23487 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ 𝐴) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
302 | 207 | cnmptid 23486 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ 𝑦) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
303 | | oveq12 7421 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝐴 ∧ 𝑣 = 𝑦) → (𝑢 · 𝑣) = (𝐴 · 𝑦)) |
304 | 207, 301,
302, 207, 207, 214, 303 | cnmpt12 23492 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
305 | | efcn 26296 |
. . . . . . . . . . 11
⊢ exp
∈ (ℂ–cn→ℂ) |
306 | 205 | cncfcn1 24752 |
. . . . . . . . . . 11
⊢
(ℂ–cn→ℂ) =
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
307 | 305, 306 | eleqtri 2830 |
. . . . . . . . . 10
⊢ exp
∈ ((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
308 | 307 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → exp
∈ ((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
309 | 207, 304,
308 | cnmpt11f 23489 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦
(exp‘(𝐴 ·
𝑦))) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
310 | 176 | fmpttd 7116 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))):𝑆⟶ℂ) |
311 | 310, 231 | ffvelcdmd 7087 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))‘0) ∈
ℂ) |
312 | | unicntop 24623 |
. . . . . . . . 9
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
313 | 312 | cncnpi 23103 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℂ ↦
(exp‘(𝐴 ·
𝑦))) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) ∧ ((𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))‘0) ∈ ℂ) → (𝑦 ∈ ℂ ↦
(exp‘(𝐴 ·
𝑦))) ∈
(((TopOpen‘ℂfld) CnP
(TopOpen‘ℂfld))‘((𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))‘0))) |
314 | 309, 311,
313 | syl2anc 583 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦
(exp‘(𝐴 ·
𝑦))) ∈
(((TopOpen‘ℂfld) CnP
(TopOpen‘ℂfld))‘((𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))‘0))) |
315 | | cnpco 23092 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘0) ∧ (𝑦 ∈ ℂ ↦ (exp‘(𝐴 · 𝑦))) ∈
(((TopOpen‘ℂfld) CnP
(TopOpen‘ℂfld))‘((𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))‘0))) → ((𝑦 ∈ ℂ ↦ (exp‘(𝐴 · 𝑦))) ∘ (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘0)) |
316 | 300, 314,
315 | syl2anc 583 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ ℂ ↦
(exp‘(𝐴 ·
𝑦))) ∘ (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘0)) |
317 | 188, 316 | eqeltrd 2832 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ↾ 𝑆) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘0)) |
318 | 205 | cnfldtop 24621 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) ∈ Top |
319 | 318 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(TopOpen‘ℂfld) ∈ Top) |
320 | 205 | cnfldtopn 24619 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
321 | 320 | blopn 24330 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ (1 / ((abs‘𝐴) +
1)) ∈ ℝ*) → (0(ball‘(abs ∘ − ))(1
/ ((abs‘𝐴) + 1)))
∈ (TopOpen‘ℂfld)) |
322 | 30, 31, 41, 321 | mp3an2i 1465 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1))) ∈
(TopOpen‘ℂfld)) |
323 | 29, 322 | eqeltrid 2836 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → 𝑆 ∈
(TopOpen‘ℂfld)) |
324 | | isopn3i 22907 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ∈
(TopOpen‘ℂfld)) →
((int‘(TopOpen‘ℂfld))‘𝑆) = 𝑆) |
325 | 318, 323,
324 | sylancr 586 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((int‘(TopOpen‘ℂfld))‘𝑆) = 𝑆) |
326 | 231, 325 | eleqtrrd 2835 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → 0 ∈
((int‘(TopOpen‘ℂfld))‘𝑆)) |
327 | | efcl 16033 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(exp‘𝐴) ∈
ℂ) |
328 | 327 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ 𝑥 = 0) → (exp‘𝐴) ∈
ℂ) |
329 | 83, 14, 85 | sylancr 586 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → (1 + (𝐴 · 𝑥)) ∈ ℂ) |
330 | 329, 48 | cxpcld 26557 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)) ∈
ℂ) |
331 | 328, 330 | ifclda 4563 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) ∈
ℂ) |
332 | 331 | fmpttd 7116 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))):ℂ⟶ℂ) |
333 | 312, 312 | cnprest 23114 |
. . . . . 6
⊢
((((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ⊆ ℂ) ∧ (0
∈ ((int‘(TopOpen‘ℂfld))‘𝑆) ∧ (𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))):ℂ⟶ℂ))
→ ((𝑥 ∈ ℂ
↦ if(𝑥 = 0,
(exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ∈
(((TopOpen‘ℂfld) CnP
(TopOpen‘ℂfld))‘0) ↔ ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ↾ 𝑆) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘0))) |
334 | 319, 44, 326, 332, 333 | syl22anc 836 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ∈
(((TopOpen‘ℂfld) CnP
(TopOpen‘ℂfld))‘0) ↔ ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ↾ 𝑆) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘0))) |
335 | 317, 334 | mpbird 257 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ∈
(((TopOpen‘ℂfld) CnP
(TopOpen‘ℂfld))‘0)) |
336 | 312 | cnpresti 23113 |
. . . 4
⊢
(((0[,)+∞) ⊆ ℂ ∧ 0 ∈ (0[,)+∞) ∧
(𝑥 ∈ ℂ ↦
if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ∈
(((TopOpen‘ℂfld) CnP
(TopOpen‘ℂfld))‘0)) → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ↾ (0[,)+∞))
∈ ((((TopOpen‘ℂfld) ↾t
(0[,)+∞)) CnP
(TopOpen‘ℂfld))‘0)) |
337 | 3, 26, 335, 336 | mp3an2i 1465 |
. . 3
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ↾ (0[,)+∞))
∈ ((((TopOpen‘ℂfld) ↾t
(0[,)+∞)) CnP
(TopOpen‘ℂfld))‘0)) |
338 | 24, 337 | eqeltrd 2832 |
. 2
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ (0[,)+∞) ↦
if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑𝑐(1 / 𝑥)))) ∈
((((TopOpen‘ℂfld) ↾t (0[,)+∞))
CnP (TopOpen‘ℂfld))‘0)) |
339 | | simpl 482 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ+)
→ 𝐴 ∈
ℂ) |
340 | | rpcn 12991 |
. . . . . . 7
⊢ (𝑘 ∈ ℝ+
→ 𝑘 ∈
ℂ) |
341 | 340 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ+)
→ 𝑘 ∈
ℂ) |
342 | | rpne0 12997 |
. . . . . . 7
⊢ (𝑘 ∈ ℝ+
→ 𝑘 ≠
0) |
343 | 342 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ+)
→ 𝑘 ≠
0) |
344 | 339, 341,
343 | divcld 11997 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ+)
→ (𝐴 / 𝑘) ∈
ℂ) |
345 | | addcl 11198 |
. . . . 5
⊢ ((1
∈ ℂ ∧ (𝐴 /
𝑘) ∈ ℂ) →
(1 + (𝐴 / 𝑘)) ∈
ℂ) |
346 | 83, 344, 345 | sylancr 586 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ+)
→ (1 + (𝐴 / 𝑘)) ∈
ℂ) |
347 | 346, 341 | cxpcld 26557 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ+)
→ ((1 + (𝐴 / 𝑘))↑𝑐𝑘) ∈
ℂ) |
348 | | oveq2 7420 |
. . . . 5
⊢ (𝑘 = (1 / 𝑥) → (𝐴 / 𝑘) = (𝐴 / (1 / 𝑥))) |
349 | 348 | oveq2d 7428 |
. . . 4
⊢ (𝑘 = (1 / 𝑥) → (1 + (𝐴 / 𝑘)) = (1 + (𝐴 / (1 / 𝑥)))) |
350 | | id 22 |
. . . 4
⊢ (𝑘 = (1 / 𝑥) → 𝑘 = (1 / 𝑥)) |
351 | 349, 350 | oveq12d 7430 |
. . 3
⊢ (𝑘 = (1 / 𝑥) → ((1 + (𝐴 / 𝑘))↑𝑐𝑘) = ((1 + (𝐴 / (1 / 𝑥)))↑𝑐(1 / 𝑥))) |
352 | | eqid 2731 |
. . 3
⊢
((TopOpen‘ℂfld) ↾t
(0[,)+∞)) = ((TopOpen‘ℂfld) ↾t
(0[,)+∞)) |
353 | 327, 347,
351, 205, 352 | rlimcnp3 26814 |
. 2
⊢ (𝐴 ∈ ℂ → ((𝑘 ∈ ℝ+
↦ ((1 + (𝐴 / 𝑘))↑𝑐𝑘)) ⇝𝑟
(exp‘𝐴) ↔ (𝑥 ∈ (0[,)+∞) ↦
if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑𝑐(1 / 𝑥)))) ∈
((((TopOpen‘ℂfld) ↾t (0[,)+∞))
CnP (TopOpen‘ℂfld))‘0))) |
354 | 338, 353 | mpbird 257 |
1
⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℝ+
↦ ((1 + (𝐴 / 𝑘))↑𝑐𝑘)) ⇝𝑟
(exp‘𝐴)) |