Step | Hyp | Ref
| Expression |
1 | | cnelprrecn 10029 |
. . . 4
⊢ ℂ
∈ {ℝ, ℂ} |
2 | 1 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℂ → ℂ
∈ {ℝ, ℂ}) |
3 | | dvcncxp1.d |
. . . . . . 7
⊢ 𝐷 = (ℂ ∖
(-∞(,]0)) |
4 | | difss 3737 |
. . . . . . 7
⊢ (ℂ
∖ (-∞(,]0)) ⊆ ℂ |
5 | 3, 4 | eqsstri 3635 |
. . . . . 6
⊢ 𝐷 ⊆
ℂ |
6 | 5 | sseli 3599 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
7 | 3 | logdmn0 24386 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → 𝑥 ≠ 0) |
8 | 6, 7 | logcld 24317 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → (log‘𝑥) ∈ ℂ) |
9 | 8 | adantl 482 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (log‘𝑥) ∈ ℂ) |
10 | 6, 7 | reccld 10794 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → (1 / 𝑥) ∈ ℂ) |
11 | 10 | adantl 482 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (1 / 𝑥) ∈ ℂ) |
12 | | mulcl 10020 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐴 · 𝑦) ∈ ℂ) |
13 | | efcl 14813 |
. . . 4
⊢ ((𝐴 · 𝑦) ∈ ℂ → (exp‘(𝐴 · 𝑦)) ∈ ℂ) |
14 | 12, 13 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(exp‘(𝐴 ·
𝑦)) ∈
ℂ) |
15 | | ovexd 6680 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((exp‘(𝐴 ·
𝑦)) · 𝐴) ∈ V) |
16 | 3 | dvlog 24397 |
. . . 4
⊢ (ℂ
D (log ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) |
17 | 3 | logcn 24393 |
. . . . . . . 8
⊢ (log
↾ 𝐷) ∈ (𝐷–cn→ℂ) |
18 | | cncff 22696 |
. . . . . . . 8
⊢ ((log
↾ 𝐷) ∈ (𝐷–cn→ℂ) → (log ↾ 𝐷):𝐷⟶ℂ) |
19 | 17, 18 | mp1i 13 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (log
↾ 𝐷):𝐷⟶ℂ) |
20 | 19 | feqmptd 6249 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (log
↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((log ↾ 𝐷)‘𝑥))) |
21 | | fvres 6207 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → ((log ↾ 𝐷)‘𝑥) = (log‘𝑥)) |
22 | 21 | mpteq2ia 4740 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 ↦ ((log ↾ 𝐷)‘𝑥)) = (𝑥 ∈ 𝐷 ↦ (log‘𝑥)) |
23 | 20, 22 | syl6eq 2672 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (log
↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (log‘𝑥))) |
24 | 23 | oveq2d 6666 |
. . . 4
⊢ (𝐴 ∈ ℂ → (ℂ
D (log ↾ 𝐷)) =
(ℂ D (𝑥 ∈ 𝐷 ↦ (log‘𝑥)))) |
25 | 16, 24 | syl5reqr 2671 |
. . 3
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ 𝐷 ↦ (log‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥))) |
26 | | simpl 473 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝐴 ∈
ℂ) |
27 | | efcl 14813 |
. . . . 5
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) |
28 | 27 | adantl 482 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) →
(exp‘𝑥) ∈
ℂ) |
29 | | simpr 477 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝑦 ∈
ℂ) |
30 | | 1cnd 10056 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 1 ∈
ℂ) |
31 | 2 | dvmptid 23720 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
𝑦)) = (𝑦 ∈ ℂ ↦ 1)) |
32 | | id 22 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
33 | 2, 29, 30, 31, 32 | dvmptcmul 23727 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ (𝐴 · 1))) |
34 | | mulid1 10037 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) |
35 | 34 | mpteq2dv 4745 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝐴 · 1)) = (𝑦 ∈ ℂ ↦ 𝐴)) |
36 | 33, 35 | eqtrd 2656 |
. . . 4
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(𝐴 · 𝑦))) = (𝑦 ∈ ℂ ↦ 𝐴)) |
37 | | dvef 23743 |
. . . . 5
⊢ (ℂ
D exp) = exp |
38 | | eff 14812 |
. . . . . . . 8
⊢
exp:ℂ⟶ℂ |
39 | 38 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
exp:ℂ⟶ℂ) |
40 | 39 | feqmptd 6249 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → exp =
(𝑥 ∈ ℂ ↦
(exp‘𝑥))) |
41 | 40 | oveq2d 6666 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (ℂ
D exp) = (ℂ D (𝑥
∈ ℂ ↦ (exp‘𝑥)))) |
42 | 37, 41, 40 | 3eqtr3a 2680 |
. . . 4
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ ℂ ↦
(exp‘𝑥))) = (𝑥 ∈ ℂ ↦
(exp‘𝑥))) |
43 | | fveq2 6191 |
. . . 4
⊢ (𝑥 = (𝐴 · 𝑦) → (exp‘𝑥) = (exp‘(𝐴 · 𝑦))) |
44 | 2, 2, 12, 26, 28, 28, 36, 42, 43, 43 | dvmptco 23735 |
. . 3
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(exp‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ ((exp‘(𝐴 · 𝑦)) · 𝐴))) |
45 | | oveq2 6658 |
. . . 4
⊢ (𝑦 = (log‘𝑥) → (𝐴 · 𝑦) = (𝐴 · (log‘𝑥))) |
46 | 45 | fveq2d 6195 |
. . 3
⊢ (𝑦 = (log‘𝑥) → (exp‘(𝐴 · 𝑦)) = (exp‘(𝐴 · (log‘𝑥)))) |
47 | 46 | oveq1d 6665 |
. . 3
⊢ (𝑦 = (log‘𝑥) → ((exp‘(𝐴 · 𝑦)) · 𝐴) = ((exp‘(𝐴 · (log‘𝑥))) · 𝐴)) |
48 | 2, 2, 9, 11, 14, 15, 25, 44, 46, 47 | dvmptco 23735 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ 𝐷 ↦ (exp‘(𝐴 · (log‘𝑥))))) = (𝑥 ∈ 𝐷 ↦ (((exp‘(𝐴 · (log‘𝑥))) · 𝐴) · (1 / 𝑥)))) |
49 | 6 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℂ) |
50 | 7 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → 𝑥 ≠ 0) |
51 | | simpl 473 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ ℂ) |
52 | 49, 50, 51 | cxpefd 24458 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝑥↑𝑐𝐴) = (exp‘(𝐴 · (log‘𝑥)))) |
53 | 52 | mpteq2dva 4744 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝐷 ↦ (𝑥↑𝑐𝐴)) = (𝑥 ∈ 𝐷 ↦ (exp‘(𝐴 · (log‘𝑥))))) |
54 | 53 | oveq2d 6666 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ 𝐷 ↦ (𝑥↑𝑐𝐴))) = (ℂ D (𝑥 ∈ 𝐷 ↦ (exp‘(𝐴 · (log‘𝑥)))))) |
55 | | 1cnd 10056 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → 1 ∈ ℂ) |
56 | 49, 50, 51, 55 | cxpsubd 24464 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝑥↑𝑐(𝐴 − 1)) = ((𝑥↑𝑐𝐴) / (𝑥↑𝑐1))) |
57 | 49 | cxp1d 24452 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝑥↑𝑐1) = 𝑥) |
58 | 57 | oveq2d 6666 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → ((𝑥↑𝑐𝐴) / (𝑥↑𝑐1)) = ((𝑥↑𝑐𝐴) / 𝑥)) |
59 | 49, 51 | cxpcld 24454 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝑥↑𝑐𝐴) ∈ ℂ) |
60 | 59, 49, 50 | divrecd 10804 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → ((𝑥↑𝑐𝐴) / 𝑥) = ((𝑥↑𝑐𝐴) · (1 / 𝑥))) |
61 | 56, 58, 60 | 3eqtrd 2660 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝑥↑𝑐(𝐴 − 1)) = ((𝑥↑𝑐𝐴) · (1 / 𝑥))) |
62 | 61 | oveq2d 6666 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝐴 · (𝑥↑𝑐(𝐴 − 1))) = (𝐴 · ((𝑥↑𝑐𝐴) · (1 / 𝑥)))) |
63 | 51, 59, 11 | mul12d 10245 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝐴 · ((𝑥↑𝑐𝐴) · (1 / 𝑥))) = ((𝑥↑𝑐𝐴) · (𝐴 · (1 / 𝑥)))) |
64 | 59, 51, 11 | mulassd 10063 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (((𝑥↑𝑐𝐴) · 𝐴) · (1 / 𝑥)) = ((𝑥↑𝑐𝐴) · (𝐴 · (1 / 𝑥)))) |
65 | 63, 64 | eqtr4d 2659 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝐴 · ((𝑥↑𝑐𝐴) · (1 / 𝑥))) = (((𝑥↑𝑐𝐴) · 𝐴) · (1 / 𝑥))) |
66 | 52 | oveq1d 6665 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → ((𝑥↑𝑐𝐴) · 𝐴) = ((exp‘(𝐴 · (log‘𝑥))) · 𝐴)) |
67 | 66 | oveq1d 6665 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (((𝑥↑𝑐𝐴) · 𝐴) · (1 / 𝑥)) = (((exp‘(𝐴 · (log‘𝑥))) · 𝐴) · (1 / 𝑥))) |
68 | 62, 65, 67 | 3eqtrd 2660 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷) → (𝐴 · (𝑥↑𝑐(𝐴 − 1))) = (((exp‘(𝐴 · (log‘𝑥))) · 𝐴) · (1 / 𝑥))) |
69 | 68 | mpteq2dva 4744 |
. 2
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ 𝐷 ↦ (𝐴 · (𝑥↑𝑐(𝐴 − 1)))) = (𝑥 ∈ 𝐷 ↦ (((exp‘(𝐴 · (log‘𝑥))) · 𝐴) · (1 / 𝑥)))) |
70 | 48, 54, 69 | 3eqtr4d 2666 |
1
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ 𝐷 ↦ (𝑥↑𝑐𝐴))) = (𝑥 ∈ 𝐷 ↦ (𝐴 · (𝑥↑𝑐(𝐴 − 1))))) |