Step | Hyp | Ref
| Expression |
1 | | reelprrecn 9907 |
. . . 4
⊢ ℝ
∈ {ℝ, ℂ} |
2 | 1 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℂ → ℝ
∈ {ℝ, ℂ}) |
3 | | relogcl 24126 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
4 | 3 | adantl 481 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ (log‘𝑥) ∈
ℝ) |
5 | | rpreccl 11733 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ+) |
6 | 5 | adantl 481 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ (1 / 𝑥) ∈
ℝ+) |
7 | | recn 9905 |
. . . 4
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
8 | | mulcl 9899 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐴 · 𝑦) ∈ ℂ) |
9 | | efcl 14652 |
. . . . 5
⊢ ((𝐴 · 𝑦) ∈ ℂ → (exp‘(𝐴 · 𝑦)) ∈ ℂ) |
10 | 8, 9 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(exp‘(𝐴 ·
𝑦)) ∈
ℂ) |
11 | 7, 10 | sylan2 490 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℝ) →
(exp‘(𝐴 ·
𝑦)) ∈
ℂ) |
12 | | ovex 6577 |
. . . 4
⊢
((exp‘(𝐴
· 𝑦)) · 𝐴) ∈ V |
13 | 12 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℝ) →
((exp‘(𝐴 ·
𝑦)) · 𝐴) ∈ V) |
14 | | dvrelog 24183 |
. . . 4
⊢ (ℝ
D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥)) |
15 | | relogf1o 24117 |
. . . . . . . 8
⊢ (log
↾ ℝ+):ℝ+–1-1-onto→ℝ |
16 | | f1of 6050 |
. . . . . . . 8
⊢ ((log
↾ ℝ+):ℝ+–1-1-onto→ℝ → (log ↾
ℝ+):ℝ+⟶ℝ) |
17 | 15, 16 | mp1i 13 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (log
↾
ℝ+):ℝ+⟶ℝ) |
18 | 17 | feqmptd 6159 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (log
↾ ℝ+) = (𝑥 ∈ ℝ+ ↦ ((log
↾ ℝ+)‘𝑥))) |
19 | | fvres 6117 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ ((log ↾ ℝ+)‘𝑥) = (log‘𝑥)) |
20 | 19 | mpteq2ia 4668 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
↦ ((log ↾ ℝ+)‘𝑥)) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) |
21 | 18, 20 | syl6eq 2660 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (log
↾ ℝ+) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥))) |
22 | 21 | oveq2d 6565 |
. . . 4
⊢ (𝐴 ∈ ℂ → (ℝ
D (log ↾ ℝ+)) = (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘𝑥)))) |
23 | 14, 22 | syl5reqr 2659 |
. . 3
⊢ (𝐴 ∈ ℂ → (ℝ
D (𝑥 ∈
ℝ+ ↦ (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) |
24 | | eqid 2610 |
. . . 4
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
25 | 24 | cnfldtopon 22396 |
. . . . 5
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
26 | | toponmax 20543 |
. . . . 5
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ℂ ∈ (TopOpen‘ℂfld)) |
27 | 25, 26 | mp1i 13 |
. . . 4
⊢ (𝐴 ∈ ℂ → ℂ
∈ (TopOpen‘ℂfld)) |
28 | | ax-resscn 9872 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
29 | 28 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ℝ
⊆ ℂ) |
30 | | df-ss 3554 |
. . . . 5
⊢ (ℝ
⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ) |
31 | 29, 30 | sylib 207 |
. . . 4
⊢ (𝐴 ∈ ℂ → (ℝ
∩ ℂ) = ℝ) |
32 | 12 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((exp‘(𝐴 ·
𝑦)) · 𝐴) ∈ V) |
33 | | cnelprrecn 9908 |
. . . . . 6
⊢ ℂ
∈ {ℝ, ℂ} |
34 | 33 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ℂ
∈ {ℝ, ℂ}) |
35 | | simpl 472 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝐴 ∈
ℂ) |
36 | | efcl 14652 |
. . . . . 6
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) |
37 | 36 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) →
(exp‘𝑥) ∈
ℂ) |
38 | | simpr 476 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝑦 ∈
ℂ) |
39 | | 1cnd 9935 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 1 ∈
ℂ) |
40 | 34 | dvmptid 23526 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
𝑦)) = (𝑦 ∈ ℂ ↦ 1)) |
41 | | id 22 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
42 | 34, 38, 39, 40, 41 | dvmptcmul 23533 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ (𝐴 · 1))) |
43 | | mulid1 9916 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) |
44 | 43 | mpteq2dv 4673 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 1)) = (𝑦 ∈ ℂ ↦ 𝐴)) |
45 | 42, 44 | eqtrd 2644 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ 𝐴)) |
46 | | dvef 23547 |
. . . . . 6
⊢ (ℂ
D exp) = exp |
47 | | eff 14651 |
. . . . . . . . . 10
⊢
exp:ℂ⟶ℂ |
48 | 47 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
exp:ℂ⟶ℂ) |
49 | 48 | feqmptd 6159 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → exp =
(𝑥 ∈ ℂ ↦
(exp‘𝑥))) |
50 | 49 | eqcomd 2616 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦
(exp‘𝑥)) =
exp) |
51 | 50 | oveq2d 6565 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ ℂ ↦
(exp‘𝑥))) = (ℂ
D exp)) |
52 | 46, 51, 50 | 3eqtr4a 2670 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ ℂ ↦
(exp‘𝑥))) = (𝑥 ∈ ℂ ↦
(exp‘𝑥))) |
53 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = (𝐴 · 𝑦) → (exp‘𝑥) = (exp‘(𝐴 · 𝑦))) |
54 | 34, 34, 8, 35, 37, 37, 45, 52, 53, 53 | dvmptco 23541 |
. . . 4
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(exp‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ ((exp‘(𝐴 · 𝑦)) · 𝐴))) |
55 | 24, 2, 27, 31, 10, 32, 54 | dvmptres3 23525 |
. . 3
⊢ (𝐴 ∈ ℂ → (ℝ
D (𝑦 ∈ ℝ ↦
(exp‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℝ ↦ ((exp‘(𝐴 · 𝑦)) · 𝐴))) |
56 | | oveq2 6557 |
. . . 4
⊢ (𝑦 = (log‘𝑥) → (𝐴 · 𝑦) = (𝐴 · (log‘𝑥))) |
57 | 56 | fveq2d 6107 |
. . 3
⊢ (𝑦 = (log‘𝑥) → (exp‘(𝐴 · 𝑦)) = (exp‘(𝐴 · (log‘𝑥)))) |
58 | 57 | oveq1d 6564 |
. . 3
⊢ (𝑦 = (log‘𝑥) → ((exp‘(𝐴 · 𝑦)) · 𝐴) = ((exp‘(𝐴 · (log‘𝑥))) · 𝐴)) |
59 | 2, 2, 4, 6, 11, 13, 23, 55, 57, 58 | dvmptco 23541 |
. 2
⊢ (𝐴 ∈ ℂ → (ℝ
D (𝑥 ∈
ℝ+ ↦ (exp‘(𝐴 · (log‘𝑥))))) = (𝑥 ∈ ℝ+ ↦
(((exp‘(𝐴 ·
(log‘𝑥))) ·
𝐴) · (1 / 𝑥)))) |
60 | | rpcn 11717 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
61 | 60 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ 𝑥 ∈
ℂ) |
62 | | rpne0 11724 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
63 | 62 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ 𝑥 ≠
0) |
64 | | simpl 472 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ 𝐴 ∈
ℂ) |
65 | 61, 63, 64 | cxpefd 24258 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ (𝑥↑𝑐𝐴) = (exp‘(𝐴 · (log‘𝑥)))) |
66 | 65 | mpteq2dva 4672 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℝ+
↦ (𝑥↑𝑐𝐴)) = (𝑥 ∈ ℝ+ ↦
(exp‘(𝐴 ·
(log‘𝑥))))) |
67 | 66 | oveq2d 6565 |
. 2
⊢ (𝐴 ∈ ℂ → (ℝ
D (𝑥 ∈
ℝ+ ↦ (𝑥↑𝑐𝐴))) = (ℝ D (𝑥 ∈ ℝ+ ↦
(exp‘(𝐴 ·
(log‘𝑥)))))) |
68 | | 1cnd 9935 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ 1 ∈ ℂ) |
69 | 61, 63, 64, 68 | cxpsubd 24264 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ (𝑥↑𝑐(𝐴 − 1)) = ((𝑥↑𝑐𝐴) / (𝑥↑𝑐1))) |
70 | 61 | cxp1d 24252 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ (𝑥↑𝑐1) = 𝑥) |
71 | 70 | oveq2d 6565 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ ((𝑥↑𝑐𝐴) / (𝑥↑𝑐1)) = ((𝑥↑𝑐𝐴) / 𝑥)) |
72 | 61, 64 | cxpcld 24254 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ (𝑥↑𝑐𝐴) ∈ ℂ) |
73 | 72, 61, 63 | divrecd 10683 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ ((𝑥↑𝑐𝐴) / 𝑥) = ((𝑥↑𝑐𝐴) · (1 / 𝑥))) |
74 | 69, 71, 73 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ (𝑥↑𝑐(𝐴 − 1)) = ((𝑥↑𝑐𝐴) · (1 / 𝑥))) |
75 | 74 | oveq2d 6565 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ (𝐴 · (𝑥↑𝑐(𝐴 − 1))) = (𝐴 · ((𝑥↑𝑐𝐴) · (1 / 𝑥)))) |
76 | 6 | rpcnd 11750 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ (1 / 𝑥) ∈
ℂ) |
77 | 64, 72, 76 | mul12d 10124 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ (𝐴 · ((𝑥↑𝑐𝐴) · (1 / 𝑥))) = ((𝑥↑𝑐𝐴) · (𝐴 · (1 / 𝑥)))) |
78 | 72, 64, 76 | mulassd 9942 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ (((𝑥↑𝑐𝐴) · 𝐴) · (1 / 𝑥)) = ((𝑥↑𝑐𝐴) · (𝐴 · (1 / 𝑥)))) |
79 | 77, 78 | eqtr4d 2647 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ (𝐴 · ((𝑥↑𝑐𝐴) · (1 / 𝑥))) = (((𝑥↑𝑐𝐴) · 𝐴) · (1 / 𝑥))) |
80 | 65 | oveq1d 6564 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ ((𝑥↑𝑐𝐴) · 𝐴) = ((exp‘(𝐴 · (log‘𝑥))) · 𝐴)) |
81 | 80 | oveq1d 6564 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ (((𝑥↑𝑐𝐴) · 𝐴) · (1 / 𝑥)) = (((exp‘(𝐴 · (log‘𝑥))) · 𝐴) · (1 / 𝑥))) |
82 | 75, 79, 81 | 3eqtrd 2648 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ (𝐴 · (𝑥↑𝑐(𝐴 − 1))) =
(((exp‘(𝐴 ·
(log‘𝑥))) ·
𝐴) · (1 / 𝑥))) |
83 | 82 | mpteq2dva 4672 |
. 2
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℝ+
↦ (𝐴 · (𝑥↑𝑐(𝐴 − 1)))) = (𝑥 ∈ ℝ+
↦ (((exp‘(𝐴
· (log‘𝑥)))
· 𝐴) · (1 /
𝑥)))) |
84 | 59, 67, 83 | 3eqtr4d 2654 |
1
⊢ (𝐴 ∈ ℂ → (ℝ
D (𝑥 ∈
ℝ+ ↦ (𝑥↑𝑐𝐴))) = (𝑥 ∈ ℝ+ ↦ (𝐴 · (𝑥↑𝑐(𝐴 − 1))))) |