Step | Hyp | Ref
| Expression |
1 | | rge0ssre 12151 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℝ |
2 | | ax-resscn 9872 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
3 | 1, 2 | sstri 3577 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℂ |
4 | 3 | sseli 3564 |
. . . . . 6
⊢ (𝑥 ∈ (0[,)+∞) →
𝑥 ∈
ℂ) |
5 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → 𝐴 ∈
ℂ) |
6 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → 1 ∈
ℂ) |
7 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → 𝑥 ∈
ℂ) |
8 | | ax-1ne0 9884 |
. . . . . . . . . . . 12
⊢ 1 ≠
0 |
9 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → 1 ≠
0) |
10 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → ¬ 𝑥 = 0) |
11 | 10 | neqned 2789 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → 𝑥 ≠ 0) |
12 | 5, 6, 7, 9, 11 | divdiv2d 10712 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → (𝐴 / (1 / 𝑥)) = ((𝐴 · 𝑥) / 1)) |
13 | | mulcl 9899 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴 · 𝑥) ∈ ℂ) |
14 | 13 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → (𝐴 · 𝑥) ∈ ℂ) |
15 | 14 | div1d 10672 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → ((𝐴 · 𝑥) / 1) = (𝐴 · 𝑥)) |
16 | 12, 15 | eqtrd 2644 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → (𝐴 / (1 / 𝑥)) = (𝐴 · 𝑥)) |
17 | 16 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → (1 + (𝐴 / (1 / 𝑥))) = (1 + (𝐴 · 𝑥))) |
18 | 17 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → ((1 + (𝐴 / (1 / 𝑥)))↑𝑐(1 / 𝑥)) = ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) |
19 | 18 | ifeq2da 4067 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑𝑐(1 / 𝑥))) = if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) |
20 | 4, 19 | sylan2 490 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ (0[,)+∞)) →
if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑𝑐(1 / 𝑥))) = if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) |
21 | 20 | mpteq2dva 4672 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ (0[,)+∞) ↦
if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑𝑐(1 / 𝑥)))) = (𝑥 ∈ (0[,)+∞) ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))))) |
22 | | resmpt 5369 |
. . . . 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 | syl6eqr 2662 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ (0[,)+∞) ↦
if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑𝑐(1 / 𝑥)))) = ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ↾
(0[,)+∞))) |
25 | 3 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(0[,)+∞) ⊆ ℂ) |
26 | | 0e0icopnf 12153 |
. . . . 5
⊢ 0 ∈
(0[,)+∞) |
27 | 26 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → 0 ∈
(0[,)+∞)) |
28 | | eqeq2 2621 |
. . . . . . . . 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 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))))) |
29 | | eqeq2 2621 |
. . . . . . . . 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 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))))) |
30 | | efrlim.1 |
. . . . . . . . . . . . . 14
⊢ 𝑆 = (0(ball‘(abs ∘
− ))(1 / ((abs‘𝐴) + 1))) |
31 | | cnxmet 22386 |
. . . . . . . . . . . . . . . 16
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → (abs
∘ − ) ∈ (∞Met‘ℂ)) |
33 | | 0cnd 9912 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → 0 ∈
ℂ) |
34 | | abscl 13866 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
35 | | peano2re 10088 |
. . . . . . . . . . . . . . . . . . 19
⊢
((abs‘𝐴)
∈ ℝ → ((abs‘𝐴) + 1) ∈ ℝ) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) + 1) ∈
ℝ) |
37 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ → 0 ∈
ℝ) |
38 | | absge0 13875 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ → 0 ≤
(abs‘𝐴)) |
39 | 34 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) <
((abs‘𝐴) +
1)) |
40 | 37, 34, 36, 38, 39 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ → 0 <
((abs‘𝐴) +
1)) |
41 | 36, 40 | elrpd 11745 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) + 1) ∈
ℝ+) |
42 | 41 | rpreccld 11758 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → (1 /
((abs‘𝐴) + 1)) ∈
ℝ+) |
43 | 42 | rpxrd 11749 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → (1 /
((abs‘𝐴) + 1)) ∈
ℝ*) |
44 | | blssm 22033 |
. . . . . . . . . . . . . . 15
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ (1 / ((abs‘𝐴) +
1)) ∈ ℝ*) → (0(ball‘(abs ∘ − ))(1
/ ((abs‘𝐴) + 1)))
⊆ ℂ) |
45 | 32, 33, 43, 44 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1))) ⊆ ℂ) |
46 | 30, 45 | syl5eqss 3612 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → 𝑆 ⊆
ℂ) |
47 | 46 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ℂ) |
48 | | mul0or 10546 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝐴 · 𝑥) = 0 ↔ (𝐴 = 0 ∨ 𝑥 = 0))) |
49 | 47, 48 | syldan 486 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((𝐴 · 𝑥) = 0 ↔ (𝐴 = 0 ∨ 𝑥 = 0))) |
50 | 49 | biimpa 500 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 · 𝑥) = 0) → (𝐴 = 0 ∨ 𝑥 = 0)) |
51 | | simpl 472 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℂ) |
52 | 51, 47 | jca 553 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ)) |
53 | 7, 11 | reccld 10673 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → (1 / 𝑥) ∈
ℂ) |
54 | 52, 53 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ 𝑥 = 0) → (1 / 𝑥) ∈ ℂ) |
55 | 54 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (1 / 𝑥) ∈ ℂ) |
56 | 55 | 1cxpd 24253 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (1↑𝑐(1 /
𝑥)) = 1) |
57 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → 𝐴 = 0) |
58 | 57 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (𝐴 · 𝑥) = (0 · 𝑥)) |
59 | 47 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → 𝑥 ∈ ℂ) |
60 | 59 | mul02d 10113 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (0 · 𝑥) = 0) |
61 | 58, 60 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (𝐴 · 𝑥) = 0) |
62 | 61 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (1 + (𝐴 · 𝑥)) = (1 + 0)) |
63 | | 1p0e1 11010 |
. . . . . . . . . . . . . . . . 17
⊢ (1 + 0) =
1 |
64 | 62, 63 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (1 + (𝐴 · 𝑥)) = 1) |
65 | 64 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)) =
(1↑𝑐(1 / 𝑥))) |
66 | 57 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (exp‘𝐴) = (exp‘0)) |
67 | | ef0 14660 |
. . . . . . . . . . . . . . . 16
⊢
(exp‘0) = 1 |
68 | 66, 67 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → (exp‘𝐴) = 1) |
69 | 56, 65, 68 | 3eqtr4d 2654 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) ∧ ¬ 𝑥 = 0) → ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)) = (exp‘𝐴)) |
70 | 69 | ifeq2da 4067 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = if(𝑥 = 0, (exp‘𝐴), (exp‘𝐴))) |
71 | | ifid 4075 |
. . . . . . . . . . . . 13
⊢ if(𝑥 = 0, (exp‘𝐴), (exp‘𝐴)) = (exp‘𝐴) |
72 | 70, 71 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘𝐴)) |
73 | | iftrue 4042 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘𝐴)) |
74 | 73 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ 𝑥 = 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘𝐴)) |
75 | 72, 74 | jaodan 822 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 = 0 ∨ 𝑥 = 0)) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘𝐴)) |
76 | | mulid1 9916 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) |
77 | 76 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 = 0 ∨ 𝑥 = 0)) → (𝐴 · 1) = 𝐴) |
78 | 77 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 = 0 ∨ 𝑥 = 0)) → (exp‘(𝐴 · 1)) = (exp‘𝐴)) |
79 | 75, 78 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 = 0 ∨ 𝑥 = 0)) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘(𝐴 · 1))) |
80 | 50, 79 | syldan 486 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 · 𝑥) = 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘(𝐴 · 1))) |
81 | | mulne0b 10547 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝐴 ≠ 0 ∧ 𝑥 ≠ 0) ↔ (𝐴 · 𝑥) ≠ 0)) |
82 | 47, 81 | syldan 486 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((𝐴 ≠ 0 ∧ 𝑥 ≠ 0) ↔ (𝐴 · 𝑥) ≠ 0)) |
83 | | df-ne 2782 |
. . . . . . . . . . . 12
⊢ ((𝐴 · 𝑥) ≠ 0 ↔ ¬ (𝐴 · 𝑥) = 0) |
84 | 82, 83 | syl6bb 275 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((𝐴 ≠ 0 ∧ 𝑥 ≠ 0) ↔ ¬ (𝐴 · 𝑥) = 0)) |
85 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → 𝑥 ≠ 0) |
86 | 85 | neneqd 2787 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ¬ 𝑥 = 0) |
87 | 86 | iffalsed 4047 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) |
88 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
89 | 47, 13 | syldan 486 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝐴 · 𝑥) ∈ ℂ) |
90 | | addcl 9897 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ (𝐴
· 𝑥) ∈ ℂ)
→ (1 + (𝐴 ·
𝑥)) ∈
ℂ) |
91 | 88, 89, 90 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (1 + (𝐴 · 𝑥)) ∈ ℂ) |
92 | 91 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (1 + (𝐴 · 𝑥)) ∈ ℂ) |
93 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘
− ))1) |
94 | 93 | dvlog2lem 24198 |
. . . . . . . . . . . . . . . . . 18
⊢
(1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖
(-∞(,]0)) |
95 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
96 | 95 | logdmss 24188 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℂ
∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}) |
97 | 94, 96 | sstri 3577 |
. . . . . . . . . . . . . . . . 17
⊢
(1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖
{0}) |
98 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (abs
∘ − ) = (abs ∘ − ) |
99 | 98 | cnmetdval 22384 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((1 +
(𝐴 · 𝑥)) ∈ ℂ ∧ 1 ∈
ℂ) → ((1 + (𝐴
· 𝑥))(abs ∘
− )1) = (abs‘((1 + (𝐴 · 𝑥)) − 1))) |
100 | 91, 88, 99 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥))(abs ∘ − )1) = (abs‘((1 +
(𝐴 · 𝑥)) − 1))) |
101 | | pncan2 10167 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℂ ∧ (𝐴
· 𝑥) ∈ ℂ)
→ ((1 + (𝐴 ·
𝑥)) − 1) = (𝐴 · 𝑥)) |
102 | 88, 89, 101 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥)) − 1) = (𝐴 · 𝑥)) |
103 | 102 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘((1 + (𝐴 · 𝑥)) − 1)) = (abs‘(𝐴 · 𝑥))) |
104 | 100, 103 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥))(abs ∘ − )1) =
(abs‘(𝐴 ·
𝑥))) |
105 | 89 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘(𝐴 · 𝑥)) ∈ ℝ) |
106 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((abs‘𝐴) + 1) ∈ ℝ) |
107 | 47 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘𝑥) ∈ ℝ) |
108 | 106, 107 | remulcld 9949 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (((abs‘𝐴) + 1) · (abs‘𝑥)) ∈
ℝ) |
109 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℝ) |
110 | | absmul 13882 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) →
(abs‘(𝐴 ·
𝑥)) = ((abs‘𝐴) · (abs‘𝑥))) |
111 | 47, 110 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘(𝐴 · 𝑥)) = ((abs‘𝐴) · (abs‘𝑥))) |
112 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘𝐴) ∈ ℝ) |
113 | 112, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((abs‘𝐴) + 1) ∈ ℝ) |
114 | 47 | absge0d 14031 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 0 ≤ (abs‘𝑥)) |
115 | 112 | lep1d 10834 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘𝐴) ≤ ((abs‘𝐴) + 1)) |
116 | 112, 113,
107, 114, 115 | lemul1ad 10842 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((abs‘𝐴) · (abs‘𝑥)) ≤ (((abs‘𝐴) + 1) · (abs‘𝑥))) |
117 | 111, 116 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘(𝐴 · 𝑥)) ≤ (((abs‘𝐴) + 1) · (abs‘𝑥))) |
118 | | 0cn 9911 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
ℂ |
119 | 98 | cnmetdval 22384 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℂ ∧ 0 ∈
ℂ) → (𝑥(abs
∘ − )0) = (abs‘(𝑥 − 0))) |
120 | 47, 118, 119 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝑥(abs ∘ − )0) = (abs‘(𝑥 − 0))) |
121 | 47 | subid1d 10260 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝑥 − 0) = 𝑥) |
122 | 121 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘(𝑥 − 0)) = (abs‘𝑥)) |
123 | 120, 122 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝑥(abs ∘ − )0) = (abs‘𝑥)) |
124 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
125 | 124, 30 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (0(ball‘(abs ∘ −
))(1 / ((abs‘𝐴) +
1)))) |
126 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
127 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (1 / ((abs‘𝐴) + 1)) ∈
ℝ*) |
128 | | 0cnd 9912 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 0 ∈ ℂ) |
129 | | elbl3 22007 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (1 /
((abs‘𝐴) + 1)) ∈
ℝ*) ∧ (0 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ (0(ball‘(abs ∘ −
))(1 / ((abs‘𝐴) +
1))) ↔ (𝑥(abs ∘
− )0) < (1 / ((abs‘𝐴) + 1)))) |
130 | 126, 127,
128, 47, 129 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ (0(ball‘(abs ∘ −
))(1 / ((abs‘𝐴) +
1))) ↔ (𝑥(abs ∘
− )0) < (1 / ((abs‘𝐴) + 1)))) |
131 | 125, 130 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (𝑥(abs ∘ − )0) < (1 /
((abs‘𝐴) +
1))) |
132 | 123, 131 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘𝑥) < (1 / ((abs‘𝐴) + 1))) |
133 | 40 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 0 < ((abs‘𝐴) + 1)) |
134 | | ltmuldiv2 10776 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((abs‘𝑥)
∈ ℝ ∧ 1 ∈ ℝ ∧ (((abs‘𝐴) + 1) ∈ ℝ ∧ 0 <
((abs‘𝐴) + 1)))
→ ((((abs‘𝐴) +
1) · (abs‘𝑥))
< 1 ↔ (abs‘𝑥)
< (1 / ((abs‘𝐴) +
1)))) |
135 | 107, 109,
113, 133, 134 | syl112anc 1322 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((((abs‘𝐴) + 1) · (abs‘𝑥)) < 1 ↔
(abs‘𝑥) < (1 /
((abs‘𝐴) +
1)))) |
136 | 132, 135 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (((abs‘𝐴) + 1) · (abs‘𝑥)) < 1) |
137 | 105, 108,
109, 117, 136 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (abs‘(𝐴 · 𝑥)) < 1) |
138 | 104, 137 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥))(abs ∘ − )1) <
1) |
139 | | 1rp 11712 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℝ+ |
140 | | rpxr 11716 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) |
141 | 139, 140 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 1 ∈
ℝ*) |
142 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → 1 ∈ ℂ) |
143 | | elbl3 22007 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (1 ∈ ℂ ∧ (1 + (𝐴 · 𝑥)) ∈ ℂ)) → ((1 + (𝐴 · 𝑥)) ∈ (1(ball‘(abs ∘ −
))1) ↔ ((1 + (𝐴
· 𝑥))(abs ∘
− )1) < 1)) |
144 | 126, 141,
142, 91, 143 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥)) ∈ (1(ball‘(abs ∘ −
))1) ↔ ((1 + (𝐴
· 𝑥))(abs ∘
− )1) < 1)) |
145 | 138, 144 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (1 + (𝐴 · 𝑥)) ∈ (1(ball‘(abs ∘ −
))1)) |
146 | 97, 145 | sseldi 3566 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (1 + (𝐴 · 𝑥)) ∈ (ℂ ∖
{0})) |
147 | | eldifsni 4261 |
. . . . . . . . . . . . . . . 16
⊢ ((1 +
(𝐴 · 𝑥)) ∈ (ℂ ∖ {0})
→ (1 + (𝐴 ·
𝑥)) ≠
0) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (1 + (𝐴 · 𝑥)) ≠ 0) |
149 | 148 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (1 + (𝐴 · 𝑥)) ≠ 0) |
150 | 47 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → 𝑥 ∈ ℂ) |
151 | 150, 85 | reccld 10673 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) ∈ ℂ) |
152 | 92, 149, 151 | cxpefd 24258 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)) = (exp‘((1 / 𝑥) · (log‘(1 +
(𝐴 · 𝑥)))))) |
153 | 91, 148 | logcld 24121 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (log‘(1 + (𝐴 · 𝑥))) ∈ ℂ) |
154 | 153 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (log‘(1 + (𝐴 · 𝑥))) ∈ ℂ) |
155 | 151, 154 | mulcomd 9940 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((1 / 𝑥) · (log‘(1 + (𝐴 · 𝑥)))) = ((log‘(1 + (𝐴 · 𝑥))) · (1 / 𝑥))) |
156 | | simpll 786 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → 𝐴 ∈ ℂ) |
157 | | simprl 790 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → 𝐴 ≠ 0) |
158 | 156, 157 | dividd 10678 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (𝐴 / 𝐴) = 1) |
159 | 158 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((𝐴 / 𝐴) / 𝑥) = (1 / 𝑥)) |
160 | 156, 156,
150, 157, 85 | divdiv1d 10711 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((𝐴 / 𝐴) / 𝑥) = (𝐴 / (𝐴 · 𝑥))) |
161 | 159, 160 | eqtr3d 2646 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (1 / 𝑥) = (𝐴 / (𝐴 · 𝑥))) |
162 | 161 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((log‘(1 + (𝐴 · 𝑥))) · (1 / 𝑥)) = ((log‘(1 + (𝐴 · 𝑥))) · (𝐴 / (𝐴 · 𝑥)))) |
163 | 89 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (𝐴 · 𝑥) ∈ ℂ) |
164 | 82 | biimpa 500 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (𝐴 · 𝑥) ≠ 0) |
165 | 154, 156,
163, 164 | div12d 10716 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((log‘(1 + (𝐴 · 𝑥))) · (𝐴 / (𝐴 · 𝑥))) = (𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) |
166 | 155, 162,
165 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → ((1 / 𝑥) · (log‘(1 + (𝐴 · 𝑥)))) = (𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) |
167 | 166 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → (exp‘((1 / 𝑥) · (log‘(1 +
(𝐴 · 𝑥))))) = (exp‘(𝐴 · ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
168 | 87, 152, 167 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 ≠ 0 ∧ 𝑥 ≠ 0)) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘(𝐴 · ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
169 | 168 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((𝐴 ≠ 0 ∧ 𝑥 ≠ 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘(𝐴 · ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥)))))) |
170 | 84, 169 | sylbird 249 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → (¬ (𝐴 · 𝑥) = 0 → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘(𝐴 · ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥)))))) |
171 | 170 | imp 444 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = (exp‘(𝐴 · ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
172 | 28, 29, 80, 171 | ifbothda 4073 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) = if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))) |
173 | 172 | mpteq2dva 4672 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))))) |
174 | 46 | resmptd 5371 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ↾ 𝑆) = (𝑥 ∈ 𝑆 ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))))) |
175 | | 1cnd 9935 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ (𝐴 · 𝑥) = 0) → 1 ∈
ℂ) |
176 | 153 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → (log‘(1 + (𝐴 · 𝑥))) ∈ ℂ) |
177 | 89 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → (𝐴 · 𝑥) ∈ ℂ) |
178 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → ¬ (𝐴 · 𝑥) = 0) |
179 | 178 | neqned 2789 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → (𝐴 · 𝑥) ≠ 0) |
180 | 176, 177,
179 | divcld 10680 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) ∧ ¬ (𝐴 · 𝑥) = 0) → ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)) ∈ ℂ) |
181 | 175, 180 | ifclda 4070 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) ∈ ℂ) |
182 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
183 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦
(exp‘(𝐴 ·
𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘(𝐴 · 𝑦)))) |
184 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑦 = if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) → (𝐴 · 𝑦) = (𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
185 | 184 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑦 = if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) → (exp‘(𝐴 · 𝑦)) = (exp‘(𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))) |
186 | | oveq2 6557 |
. . . . . . . . . . 11
⊢
(if((𝐴 ·
𝑥) = 0, 1, ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥))) = 1 → (𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) = (𝐴 · 1)) |
187 | 186 | fveq2d 6107 |
. . . . . . . . . 10
⊢
(if((𝐴 ·
𝑥) = 0, 1, ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥))) = 1 → (exp‘(𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) = (exp‘(𝐴 · 1))) |
188 | | oveq2 6557 |
. . . . . . . . . . 11
⊢
(if((𝐴 ·
𝑥) = 0, 1, ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥))) = ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)) → (𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) = (𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) |
189 | 188 | fveq2d 6107 |
. . . . . . . . . 10
⊢
(if((𝐴 ·
𝑥) = 0, 1, ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥))) = ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)) → (exp‘(𝐴 · if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) = (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
190 | 187, 189 | ifsb 4049 |
. . . . . . . . 9
⊢
(exp‘(𝐴
· if((𝐴 ·
𝑥) = 0, 1, ((log‘(1 +
(𝐴 · 𝑥))) / (𝐴 · 𝑥))))) = if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
191 | 185, 190 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑦 = if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) → (exp‘(𝐴 · 𝑦)) = if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))) |
192 | 181, 182,
183, 191 | fmptco 6303 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ ℂ ↦
(exp‘(𝐴 ·
𝑦))) ∘ (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, (exp‘(𝐴 · 1)), (exp‘(𝐴 · ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))))) |
193 | 173, 174,
192 | 3eqtr4d 2654 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ↾ 𝑆) = ((𝑦 ∈ ℂ ↦ (exp‘(𝐴 · 𝑦))) ∘ (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))))) |
194 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) = (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))) |
195 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) = (𝑦 ∈ (1(ball‘(abs ∘ −
))1) ↦ if(𝑦 = 1, 1,
((log‘𝑦) / (𝑦 − 1))))) |
196 | | eqeq1 2614 |
. . . . . . . . . . 11
⊢ (𝑦 = (1 + (𝐴 · 𝑥)) → (𝑦 = 1 ↔ (1 + (𝐴 · 𝑥)) = 1)) |
197 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑦 = (1 + (𝐴 · 𝑥)) → (log‘𝑦) = (log‘(1 + (𝐴 · 𝑥)))) |
198 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑦 = (1 + (𝐴 · 𝑥)) → (𝑦 − 1) = ((1 + (𝐴 · 𝑥)) − 1)) |
199 | 197, 198 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑦 = (1 + (𝐴 · 𝑥)) → ((log‘𝑦) / (𝑦 − 1)) = ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1))) |
200 | 196, 199 | ifbieq2d 4061 |
. . . . . . . . . 10
⊢ (𝑦 = (1 + (𝐴 · 𝑥)) → if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1))) = if((1 + (𝐴 · 𝑥)) = 1, 1, ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1)))) |
201 | 145, 194,
195, 200 | fmptco 6303 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∘ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))) = (𝑥 ∈ 𝑆 ↦ if((1 + (𝐴 · 𝑥)) = 1, 1, ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1))))) |
202 | 63 | eqeq2i 2622 |
. . . . . . . . . . . 12
⊢ ((1 +
(𝐴 · 𝑥)) = (1 + 0) ↔ (1 + (𝐴 · 𝑥)) = 1) |
203 | 142, 89, 128 | addcand 10118 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥)) = (1 + 0) ↔ (𝐴 · 𝑥) = 0)) |
204 | 202, 203 | syl5bbr 273 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((1 + (𝐴 · 𝑥)) = 1 ↔ (𝐴 · 𝑥) = 0)) |
205 | 102 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1)) = ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))) |
206 | 204, 205 | ifbieq2d 4061 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆) → if((1 + (𝐴 · 𝑥)) = 1, 1, ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1))) = if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) |
207 | 206 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ if((1 + (𝐴 · 𝑥)) = 1, 1, ((log‘(1 + (𝐴 · 𝑥))) / ((1 + (𝐴 · 𝑥)) − 1)))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
208 | 201, 207 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∘ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) |
209 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t 𝑆) =
((TopOpen‘ℂfld) ↾t 𝑆) |
210 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
211 | 210 | cnfldtopon 22396 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
212 | 211 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
213 | | 1cnd 9935 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → 1 ∈
ℂ) |
214 | 212, 212,
213 | cnmptc 21275 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ 1)
∈ ((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
215 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
216 | 212, 212,
215 | cnmptc 21275 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ 𝐴) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
217 | 212 | cnmptid 21274 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ 𝑥) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
218 | 210 | mulcn 22478 |
. . . . . . . . . . . . . . 15
⊢ ·
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
219 | 218 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → ·
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
220 | 212, 216,
217, 219 | cnmpt12f 21279 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
221 | 210 | addcn 22476 |
. . . . . . . . . . . . . 14
⊢ + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
222 | 221 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → + ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
223 | 212, 214,
220, 222 | cnmpt12f 21279 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ (1 +
(𝐴 · 𝑥))) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
224 | 209, 212,
46, 223 | cnmpt1res 21289 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn
(TopOpen‘ℂfld))) |
225 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) = (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) |
226 | 145, 225 | fmptd 6292 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))):𝑆⟶(1(ball‘(abs ∘ −
))1)) |
227 | | frn 5966 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))):𝑆⟶(1(ball‘(abs ∘ −
))1) → ran (𝑥 ∈
𝑆 ↦ (1 + (𝐴 · 𝑥))) ⊆ (1(ball‘(abs ∘
− ))1)) |
228 | 226, 227 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → ran
(𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ⊆ (1(ball‘(abs ∘
− ))1)) |
229 | | difss 3699 |
. . . . . . . . . . . . . 14
⊢ (ℂ
∖ {0}) ⊆ ℂ |
230 | 97, 229 | sstri 3577 |
. . . . . . . . . . . . 13
⊢
(1(ball‘(abs ∘ − ))1) ⊆ ℂ |
231 | 230 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(1(ball‘(abs ∘ − ))1) ⊆ ℂ) |
232 | | cnrest2 20900 |
. . . . . . . . . . . 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))))) |
233 | 212, 228,
231, 232 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld))
↔ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn ((TopOpen‘ℂfld)
↾t (1(ball‘(abs ∘ −
))1))))) |
234 | 224, 233 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn ((TopOpen‘ℂfld)
↾t (1(ball‘(abs ∘ − ))1)))) |
235 | | blcntr 22028 |
. . . . . . . . . . . . 13
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ (1 / ((abs‘𝐴) +
1)) ∈ ℝ+) → 0 ∈ (0(ball‘(abs ∘
− ))(1 / ((abs‘𝐴) + 1)))) |
236 | 32, 33, 42, 235 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → 0 ∈
(0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1)))) |
237 | 236, 30 | syl6eleqr 2699 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → 0 ∈
𝑆) |
238 | | resttopon 20775 |
. . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) |
239 | 211, 46, 238 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) |
240 | | toponuni 20542 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
241 | 239, 240 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
242 | 237, 241 | eleqtrd 2690 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → 0 ∈
∪ ((TopOpen‘ℂfld)
↾t 𝑆)) |
243 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ∪ ((TopOpen‘ℂfld)
↾t 𝑆) =
∪ ((TopOpen‘ℂfld)
↾t 𝑆) |
244 | 243 | cncnpi 20892 |
. . . . . . . . . 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)) |
245 | 234, 242,
244 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥))) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP ((TopOpen‘ℂfld)
↾t (1(ball‘(abs ∘ −
))1)))‘0)) |
246 | | cnelprrecn 9908 |
. . . . . . . . . . 11
⊢ ℂ
∈ {ℝ, ℂ} |
247 | | logf1o 24115 |
. . . . . . . . . . . . . 14
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
248 | | f1of 6050 |
. . . . . . . . . . . . . 14
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})⟶ran log) |
249 | 247, 248 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
log:(ℂ ∖ {0})⟶ran log |
250 | | logrncn 24113 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ran log → 𝑥 ∈
ℂ) |
251 | 250 | ssriv 3572 |
. . . . . . . . . . . . 13
⊢ ran log
⊆ ℂ |
252 | | fss 5969 |
. . . . . . . . . . . . 13
⊢
((log:(ℂ ∖ {0})⟶ran log ∧ ran log ⊆
ℂ) → log:(ℂ ∖ {0})⟶ℂ) |
253 | 249, 251,
252 | mp2an 704 |
. . . . . . . . . . . 12
⊢
log:(ℂ ∖ {0})⟶ℂ |
254 | | fssres 5983 |
. . . . . . . . . . . 12
⊢
((log:(ℂ ∖ {0})⟶ℂ ∧ (1(ball‘(abs
∘ − ))1) ⊆ (ℂ ∖ {0})) → (log ↾
(1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘ −
))1)⟶ℂ) |
255 | 253, 97, 254 | mp2an 704 |
. . . . . . . . . . 11
⊢ (log
↾ (1(ball‘(abs ∘ − ))1)):(1(ball‘(abs ∘
− ))1)⟶ℂ |
256 | | blcntr 22028 |
. . . . . . . . . . . . . 14
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℂ
∧ 1 ∈ ℝ+) → 1 ∈ (1(ball‘(abs ∘
− ))1)) |
257 | 31, 88, 139, 256 | mp3an 1416 |
. . . . . . . . . . . . 13
⊢ 1 ∈
(1(ball‘(abs ∘ − ))1) |
258 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ (1 /
𝑦) ∈
V |
259 | 93 | dvlog2 24199 |
. . . . . . . . . . . . . 14
⊢ (ℂ
D (log ↾ (1(ball‘(abs ∘ − ))1))) = (𝑦 ∈ (1(ball‘(abs ∘ −
))1) ↦ (1 / 𝑦)) |
260 | 258, 259 | dmmpti 5936 |
. . . . . . . . . . . . 13
⊢ dom
(ℂ D (log ↾ (1(ball‘(abs ∘ − ))1))) =
(1(ball‘(abs ∘ − ))1) |
261 | 257, 260 | eleqtrri 2687 |
. . . . . . . . . . . 12
⊢ 1 ∈
dom (ℂ D (log ↾ (1(ball‘(abs ∘ −
))1))) |
262 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ↾t
(1(ball‘(abs ∘ − ))1)) =
((TopOpen‘ℂfld) ↾t (1(ball‘(abs
∘ − ))1)) |
263 | 259 | fveq1i 6104 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℂ
D (log ↾ (1(ball‘(abs ∘ − ))1)))‘1) = ((𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ (1 / 𝑦))‘1) |
264 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 1 → (1 / 𝑦) = (1 / 1)) |
265 | | 1div1e1 10596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 / 1) =
1 |
266 | 264, 265 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 1 → (1 / 𝑦) = 1) |
267 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ (1 / 𝑦)) = (𝑦 ∈ (1(ball‘(abs ∘ −
))1) ↦ (1 / 𝑦)) |
268 | | 1ex 9914 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
V |
269 | 266, 267,
268 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
(1(ball‘(abs ∘ − ))1) → ((𝑦 ∈ (1(ball‘(abs ∘ −
))1) ↦ (1 / 𝑦))‘1) = 1) |
270 | 257, 269 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ (1 / 𝑦))‘1) = 1 |
271 | 263, 270 | eqtr2i 2633 |
. . . . . . . . . . . . . . . 16
⊢ 1 =
((ℂ D (log ↾ (1(ball‘(abs ∘ −
))1)))‘1) |
272 | 271 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → 1 = ((ℂ D (log ↾ (1(ball‘(abs
∘ − ))1)))‘1)) |
273 | | fvres 6117 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → ((log ↾ (1(ball‘(abs ∘ −
))1))‘𝑦) =
(log‘𝑦)) |
274 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 ∈
(1(ball‘(abs ∘ − ))1) → ((log ↾ (1(ball‘(abs
∘ − ))1))‘1) = (log‘1)) |
275 | 257, 274 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → ((log ↾ (1(ball‘(abs ∘ −
))1))‘1) = (log‘1)) |
276 | | log1 24136 |
. . . . . . . . . . . . . . . . . . 19
⊢
(log‘1) = 0 |
277 | 275, 276 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → ((log ↾ (1(ball‘(abs ∘ −
))1))‘1) = 0) |
278 | 273, 277 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → (((log ↾ (1(ball‘(abs ∘ −
))1))‘𝑦) −
((log ↾ (1(ball‘(abs ∘ − ))1))‘1)) =
((log‘𝑦) −
0)) |
279 | 97 | sseli 3564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → 𝑦 ∈ (ℂ ∖
{0})) |
280 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (ℂ ∖ {0})
↔ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) |
281 | 279, 280 | sylib 207 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) |
282 | | logcl 24119 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (log‘𝑦) ∈
ℂ) |
283 | 281, 282 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → (log‘𝑦) ∈ ℂ) |
284 | 283 | subid1d 10260 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → ((log‘𝑦) − 0) = (log‘𝑦)) |
285 | 278, 284 | eqtr2d 2645 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → (log‘𝑦) = (((log ↾ (1(ball‘(abs ∘
− ))1))‘𝑦)
− ((log ↾ (1(ball‘(abs ∘ −
))1))‘1))) |
286 | 285 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) → ((log‘𝑦) / (𝑦 − 1)) = ((((log ↾
(1(ball‘(abs ∘ − ))1))‘𝑦) − ((log ↾ (1(ball‘(abs
∘ − ))1))‘1)) / (𝑦 − 1))) |
287 | 272, 286 | ifeq12d 4056 |
. . . . . . . . . . . . . 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)))) |
288 | 287 | mpteq2ia 4668 |
. . . . . . . . . . . . 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)))) |
289 | 262, 210,
288 | dvcnp 23488 |
. . . . . . . . . . . 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)) |
290 | 261, 289 | mpan2 703 |
. . . . . . . . . . 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)) |
291 | 246, 255,
230, 290 | mp3an 1416 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∈
((((TopOpen‘ℂfld) ↾t (1(ball‘(abs
∘ − ))1)) CnP
(TopOpen‘ℂfld))‘1) |
292 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 0 → (𝐴 · 𝑥) = (𝐴 · 0)) |
293 | 292 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 0 → (1 + (𝐴 · 𝑥)) = (1 + (𝐴 · 0))) |
294 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ (1 +
(𝐴 · 0)) ∈
V |
295 | 293, 225,
294 | fvmpt 6191 |
. . . . . . . . . . . . 13
⊢ (0 ∈
𝑆 → ((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))‘0) = (1 + (𝐴 · 0))) |
296 | 237, 295 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))‘0) = (1 + (𝐴 · 0))) |
297 | | mul01 10094 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) =
0) |
298 | 297 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (1 +
(𝐴 · 0)) = (1 +
0)) |
299 | 298, 63 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (1 +
(𝐴 · 0)) =
1) |
300 | 296, 299 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))‘0) = 1) |
301 | 300 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
((((TopOpen‘ℂfld) ↾t (1(ball‘(abs
∘ − ))1)) CnP (TopOpen‘ℂfld))‘((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))‘0)) =
((((TopOpen‘ℂfld) ↾t (1(ball‘(abs
∘ − ))1)) CnP
(TopOpen‘ℂfld))‘1)) |
302 | 291, 301 | syl5eleqr 2695 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∈
((((TopOpen‘ℂfld) ↾t (1(ball‘(abs
∘ − ))1)) CnP (TopOpen‘ℂfld))‘((𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))‘0))) |
303 | | cnpco 20881 |
. . . . . . . . 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)) |
304 | 245, 302,
303 | syl2anc 691 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ (1(ball‘(abs
∘ − ))1) ↦ if(𝑦 = 1, 1, ((log‘𝑦) / (𝑦 − 1)))) ∘ (𝑥 ∈ 𝑆 ↦ (1 + (𝐴 · 𝑥)))) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘0)) |
305 | 208, 304 | eqeltrrd 2689 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘0)) |
306 | 212, 212,
215 | cnmptc 21275 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ 𝐴) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
307 | 212 | cnmptid 21274 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ 𝑦) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
308 | 212, 306,
307, 219 | cnmpt12f 21279 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 𝑦)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
309 | | efcn 24001 |
. . . . . . . . . . 11
⊢ exp
∈ (ℂ–cn→ℂ) |
310 | 210 | cncfcn1 22521 |
. . . . . . . . . . 11
⊢
(ℂ–cn→ℂ) =
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
311 | 309, 310 | eleqtri 2686 |
. . . . . . . . . 10
⊢ exp
∈ ((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
312 | 311 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → exp
∈ ((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
313 | 212, 308,
312 | cnmpt11f 21277 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦
(exp‘(𝐴 ·
𝑦))) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
314 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) = (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))) |
315 | 181, 314 | fmptd 6292 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥)))):𝑆⟶ℂ) |
316 | 315, 237 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))‘0) ∈
ℂ) |
317 | 211 | toponunii 20547 |
. . . . . . . . 9
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
318 | 317 | cncnpi 20892 |
. . . . . . . 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))) |
319 | 313, 316,
318 | syl2anc 691 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦
(exp‘(𝐴 ·
𝑦))) ∈
(((TopOpen‘ℂfld) CnP
(TopOpen‘ℂfld))‘((𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))‘0))) |
320 | | cnpco 20881 |
. . . . . . 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)) |
321 | 305, 319,
320 | syl2anc 691 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ ℂ ↦
(exp‘(𝐴 ·
𝑦))) ∘ (𝑥 ∈ 𝑆 ↦ if((𝐴 · 𝑥) = 0, 1, ((log‘(1 + (𝐴 · 𝑥))) / (𝐴 · 𝑥))))) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘0)) |
322 | 193, 321 | eqeltrd 2688 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ↾ 𝑆) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘0)) |
323 | 210 | cnfldtop 22397 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) ∈ Top |
324 | 323 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(TopOpen‘ℂfld) ∈ Top) |
325 | 210 | cnfldtopn 22395 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
326 | 325 | blopn 22115 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ (1 / ((abs‘𝐴) +
1)) ∈ ℝ*) → (0(ball‘(abs ∘ − ))(1
/ ((abs‘𝐴) + 1)))
∈ (TopOpen‘ℂfld)) |
327 | 32, 33, 43, 326 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1))) ∈
(TopOpen‘ℂfld)) |
328 | 30, 327 | syl5eqel 2692 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → 𝑆 ∈
(TopOpen‘ℂfld)) |
329 | | isopn3i 20696 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ∈
(TopOpen‘ℂfld)) →
((int‘(TopOpen‘ℂfld))‘𝑆) = 𝑆) |
330 | 323, 328,
329 | sylancr 694 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((int‘(TopOpen‘ℂfld))‘𝑆) = 𝑆) |
331 | 237, 330 | eleqtrrd 2691 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → 0 ∈
((int‘(TopOpen‘ℂfld))‘𝑆)) |
332 | | efcl 14652 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(exp‘𝐴) ∈
ℂ) |
333 | 332 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ 𝑥 = 0) → (exp‘𝐴) ∈
ℂ) |
334 | 88, 14, 90 | sylancr 694 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → (1 + (𝐴 · 𝑥)) ∈ ℂ) |
335 | 334, 53 | cxpcld 24254 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ ¬
𝑥 = 0) → ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)) ∈
ℂ) |
336 | 333, 335 | ifclda 4070 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥))) ∈
ℂ) |
337 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) = (𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) |
338 | 336, 337 | fmptd 6292 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))):ℂ⟶ℂ) |
339 | 317, 317 | cnprest 20903 |
. . . . . 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))) |
340 | 324, 46, 331, 338, 339 | syl22anc 1319 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ∈
(((TopOpen‘ℂfld) CnP
(TopOpen‘ℂfld))‘0) ↔ ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ↾ 𝑆) ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘0))) |
341 | 322, 340 | mpbird 246 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ∈
(((TopOpen‘ℂfld) CnP
(TopOpen‘ℂfld))‘0)) |
342 | 317 | cnpresti 20902 |
. . . 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)) |
343 | 25, 27, 341, 342 | syl3anc 1318 |
. . 3
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦ if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 · 𝑥))↑𝑐(1 / 𝑥)))) ↾ (0[,)+∞))
∈ ((((TopOpen‘ℂfld) ↾t
(0[,)+∞)) CnP
(TopOpen‘ℂfld))‘0)) |
344 | 24, 343 | eqeltrd 2688 |
. 2
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ (0[,)+∞) ↦
if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑𝑐(1 / 𝑥)))) ∈
((((TopOpen‘ℂfld) ↾t (0[,)+∞))
CnP (TopOpen‘ℂfld))‘0)) |
345 | | simpl 472 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ+)
→ 𝐴 ∈
ℂ) |
346 | | rpcn 11717 |
. . . . . . 7
⊢ (𝑘 ∈ ℝ+
→ 𝑘 ∈
ℂ) |
347 | 346 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ+)
→ 𝑘 ∈
ℂ) |
348 | | rpne0 11724 |
. . . . . . 7
⊢ (𝑘 ∈ ℝ+
→ 𝑘 ≠
0) |
349 | 348 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ+)
→ 𝑘 ≠
0) |
350 | 345, 347,
349 | divcld 10680 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ+)
→ (𝐴 / 𝑘) ∈
ℂ) |
351 | | addcl 9897 |
. . . . 5
⊢ ((1
∈ ℂ ∧ (𝐴 /
𝑘) ∈ ℂ) →
(1 + (𝐴 / 𝑘)) ∈
ℂ) |
352 | 88, 350, 351 | sylancr 694 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ+)
→ (1 + (𝐴 / 𝑘)) ∈
ℂ) |
353 | 352, 347 | cxpcld 24254 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℝ+)
→ ((1 + (𝐴 / 𝑘))↑𝑐𝑘) ∈
ℂ) |
354 | | oveq2 6557 |
. . . . 5
⊢ (𝑘 = (1 / 𝑥) → (𝐴 / 𝑘) = (𝐴 / (1 / 𝑥))) |
355 | 354 | oveq2d 6565 |
. . . 4
⊢ (𝑘 = (1 / 𝑥) → (1 + (𝐴 / 𝑘)) = (1 + (𝐴 / (1 / 𝑥)))) |
356 | | id 22 |
. . . 4
⊢ (𝑘 = (1 / 𝑥) → 𝑘 = (1 / 𝑥)) |
357 | 355, 356 | oveq12d 6567 |
. . 3
⊢ (𝑘 = (1 / 𝑥) → ((1 + (𝐴 / 𝑘))↑𝑐𝑘) = ((1 + (𝐴 / (1 / 𝑥)))↑𝑐(1 / 𝑥))) |
358 | | eqid 2610 |
. . 3
⊢
((TopOpen‘ℂfld) ↾t
(0[,)+∞)) = ((TopOpen‘ℂfld) ↾t
(0[,)+∞)) |
359 | 332, 353,
357, 210, 358 | rlimcnp3 24494 |
. 2
⊢ (𝐴 ∈ ℂ → ((𝑘 ∈ ℝ+
↦ ((1 + (𝐴 / 𝑘))↑𝑐𝑘)) ⇝𝑟
(exp‘𝐴) ↔ (𝑥 ∈ (0[,)+∞) ↦
if(𝑥 = 0, (exp‘𝐴), ((1 + (𝐴 / (1 / 𝑥)))↑𝑐(1 / 𝑥)))) ∈
((((TopOpen‘ℂfld) ↾t (0[,)+∞))
CnP (TopOpen‘ℂfld))‘0))) |
360 | 344, 359 | mpbird 246 |
1
⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℝ+
↦ ((1 + (𝐴 / 𝑘))↑𝑐𝑘)) ⇝𝑟
(exp‘𝐴)) |