Step | Hyp | Ref
| Expression |
1 | | cnelprrecn 9908 |
. . . 4
⊢ ℂ
∈ {ℝ, ℂ} |
2 | 1 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℂ → ℂ
∈ {ℝ, ℂ}) |
3 | | dvcncxp1.d |
. . . . . . 7
⊢ 𝐷 = (ℂ ∖
(-∞(,]0)) |
4 | | difss 3699 |
. . . . . . 7
⊢ (ℂ
∖ (-∞(,]0)) ⊆ ℂ |
5 | 3, 4 | eqsstri 3598 |
. . . . . 6
⊢ 𝐷 ⊆
ℂ |
6 | 5 | sseli 3564 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
7 | 3 | logdmn0 24186 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → 𝑥 ≠ 0) |
8 | 6, 7 | logcld 24121 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) ∈ ℂ) |
9 | 8 | adantl 481 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (log‘𝑥) ∈ ℂ) |
10 | 6, 7 | reccld 10673 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → (1 / 𝑥) ∈ ℂ) |
11 | 10 | adantl 481 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (1 / 𝑥) ∈ ℂ) |
12 | | mulcl 9899 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐴 · 𝑦) ∈ ℂ) |
13 | | efcl 14652 |
. . . 4
⊢ ((𝐴 · 𝑦) ∈ ℂ → (exp‘(𝐴 · 𝑦)) ∈ ℂ) |
14 | 12, 13 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(exp‘(𝐴 ·
𝑦)) ∈
ℂ) |
15 | | ovex 6577 |
. . . 4
⊢
((exp‘(𝐴
· 𝑦)) · 𝐴) ∈ V |
16 | 15 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((exp‘(𝐴 ·
𝑦)) · 𝐴) ∈ V) |
17 | 3 | dvlog 24197 |
. . . 4
⊢ (ℂ
D (log ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) |
18 | 3 | logcn 24193 |
. . . . . . . 8
⊢ (log
↾ 𝐷) ∈ (𝐷–cn→ℂ) |
19 | | cncff 22504 |
. . . . . . . 8
⊢ ((log
↾ 𝐷) ∈ (𝐷–cn→ℂ) → (log ↾ 𝐷):𝐷⟶ℂ) |
20 | 18, 19 | mp1i 13 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (log
↾ 𝐷):𝐷⟶ℂ) |
21 | 20 | feqmptd 6159 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (log
↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((log ↾ 𝐷)‘𝑥))) |
22 | | fvres 6117 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → ((log ↾ 𝐷)‘𝑥) = (log‘𝑥)) |
23 | 22 | mpteq2ia 4668 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↦ ((log ↾ 𝐷)‘𝑥)) = (𝑥 ∈ 𝐷 ↦ (log‘𝑥)) |
24 | 21, 23 | syl6eq 2660 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (log
↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (log‘𝑥))) |
25 | 24 | oveq2d 6565 |
. . . 4
⊢ (𝐴 ∈ ℂ → (ℂ
D (log ↾ 𝐷)) =
(ℂ D (𝑥 ∈ 𝐷 ↦ (log‘𝑥)))) |
26 | 17, 25 | syl5reqr 2659 |
. . 3
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ 𝐷 ↦ (log‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥))) |
27 | | simpl 472 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝐴 ∈
ℂ) |
28 | | efcl 14652 |
. . . . 5
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) |
29 | 28 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) →
(exp‘𝑥) ∈
ℂ) |
30 | | simpr 476 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝑦 ∈
ℂ) |
31 | | 1cnd 9935 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 1 ∈
ℂ) |
32 | 2 | dvmptid 23526 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
𝑦)) = (𝑦 ∈ ℂ ↦ 1)) |
33 | | id 22 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
34 | 2, 30, 31, 32, 33 | dvmptcmul 23533 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ (𝐴 · 1))) |
35 | | mulid1 9916 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) |
36 | 35 | mpteq2dv 4673 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 1)) = (𝑦 ∈ ℂ ↦ 𝐴)) |
37 | 34, 36 | eqtrd 2644 |
. . . 4
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ 𝐴)) |
38 | | dvef 23547 |
. . . . 5
⊢ (ℂ
D exp) = exp |
39 | | eff 14651 |
. . . . . . . 8
⊢
exp:ℂ⟶ℂ |
40 | 39 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
exp:ℂ⟶ℂ) |
41 | 40 | feqmptd 6159 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → exp =
(𝑥 ∈ ℂ ↦
(exp‘𝑥))) |
42 | 41 | oveq2d 6565 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (ℂ
D exp) = (ℂ D (𝑥
∈ ℂ ↦ (exp‘𝑥)))) |
43 | 38, 42, 41 | 3eqtr3a 2668 |
. . . 4
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ ℂ ↦
(exp‘𝑥))) = (𝑥 ∈ ℂ ↦
(exp‘𝑥))) |
44 | | fveq2 6103 |
. . . 4
⊢ (𝑥 = (𝐴 · 𝑦) → (exp‘𝑥) = (exp‘(𝐴 · 𝑦))) |
45 | 2, 2, 12, 27, 29, 29, 37, 43, 44, 44 | dvmptco 23541 |
. . 3
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(exp‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ ((exp‘(𝐴 · 𝑦)) · 𝐴))) |
46 | | oveq2 6557 |
. . . 4
⊢ (𝑦 = (log‘𝑥) → (𝐴 · 𝑦) = (𝐴 · (log‘𝑥))) |
47 | 46 | fveq2d 6107 |
. . 3
⊢ (𝑦 = (log‘𝑥) → (exp‘(𝐴 · 𝑦)) = (exp‘(𝐴 · (log‘𝑥)))) |
48 | 47 | oveq1d 6564 |
. . 3
⊢ (𝑦 = (log‘𝑥) → ((exp‘(𝐴 · 𝑦)) · 𝐴) = ((exp‘(𝐴 · (log‘𝑥))) · 𝐴)) |
49 | 2, 2, 9, 11, 14, 16, 26, 45, 47, 48 | dvmptco 23541 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ 𝐷 ↦ (exp‘(𝐴 · (log‘𝑥))))) = (𝑥 ∈ 𝐷 ↦ (((exp‘(𝐴 · (log‘𝑥))) · 𝐴) · (1 / 𝑥)))) |
50 | 6 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℂ) |
51 | 7 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → 𝑥 ≠ 0) |
52 | | simpl 472 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ ℂ) |
53 | 50, 51, 52 | cxpefd 24258 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝑥↑𝑐𝐴) = (exp‘(𝐴 · (log‘𝑥)))) |
54 | 53 | mpteq2dva 4672 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝐷 ↦ (𝑥↑𝑐𝐴)) = (𝑥 ∈ 𝐷 ↦ (exp‘(𝐴 · (log‘𝑥))))) |
55 | 54 | oveq2d 6565 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ 𝐷 ↦ (𝑥↑𝑐𝐴))) = (ℂ D (𝑥 ∈ 𝐷 ↦ (exp‘(𝐴 · (log‘𝑥)))))) |
56 | | 1cnd 9935 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → 1 ∈ ℂ) |
57 | 50, 51, 52, 56 | cxpsubd 24264 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝑥↑𝑐(𝐴 − 1)) = ((𝑥↑𝑐𝐴) / (𝑥↑𝑐1))) |
58 | 50 | cxp1d 24252 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝑥↑𝑐1) = 𝑥) |
59 | 58 | oveq2d 6565 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → ((𝑥↑𝑐𝐴) / (𝑥↑𝑐1)) = ((𝑥↑𝑐𝐴) / 𝑥)) |
60 | 50, 52 | cxpcld 24254 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝑥↑𝑐𝐴) ∈ ℂ) |
61 | 60, 50, 51 | divrecd 10683 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → ((𝑥↑𝑐𝐴) / 𝑥) = ((𝑥↑𝑐𝐴) · (1 / 𝑥))) |
62 | 57, 59, 61 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝑥↑𝑐(𝐴 − 1)) = ((𝑥↑𝑐𝐴) · (1 / 𝑥))) |
63 | 62 | oveq2d 6565 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝐴 · (𝑥↑𝑐(𝐴 − 1))) = (𝐴 · ((𝑥↑𝑐𝐴) · (1 / 𝑥)))) |
64 | 52, 60, 11 | mul12d 10124 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝐴 · ((𝑥↑𝑐𝐴) · (1 / 𝑥))) = ((𝑥↑𝑐𝐴) · (𝐴 · (1 / 𝑥)))) |
65 | 60, 52, 11 | mulassd 9942 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (((𝑥↑𝑐𝐴) · 𝐴) · (1 / 𝑥)) = ((𝑥↑𝑐𝐴) · (𝐴 · (1 / 𝑥)))) |
66 | 64, 65 | eqtr4d 2647 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝐴 · ((𝑥↑𝑐𝐴) · (1 / 𝑥))) = (((𝑥↑𝑐𝐴) · 𝐴) · (1 / 𝑥))) |
67 | 53 | oveq1d 6564 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → ((𝑥↑𝑐𝐴) · 𝐴) = ((exp‘(𝐴 · (log‘𝑥))) · 𝐴)) |
68 | 67 | oveq1d 6564 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (((𝑥↑𝑐𝐴) · 𝐴) · (1 / 𝑥)) = (((exp‘(𝐴 · (log‘𝑥))) · 𝐴) · (1 / 𝑥))) |
69 | 63, 66, 68 | 3eqtrd 2648 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝐴 · (𝑥↑𝑐(𝐴 − 1))) = (((exp‘(𝐴 · (log‘𝑥))) · 𝐴) · (1 / 𝑥))) |
70 | 69 | mpteq2dva 4672 |
. 2
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝐷 ↦ (𝐴 · (𝑥↑𝑐(𝐴 − 1)))) = (𝑥 ∈ 𝐷 ↦ (((exp‘(𝐴 · (log‘𝑥))) · 𝐴) · (1 / 𝑥)))) |
71 | 49, 55, 70 | 3eqtr4d 2654 |
1
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ 𝐷 ↦ (𝑥↑𝑐𝐴))) = (𝑥 ∈ 𝐷 ↦ (𝐴 · (𝑥↑𝑐(𝐴 − 1))))) |