Metamath Proof Explorer

Theorem dvcxp1

Description: The derivative of a complex power with respect to the first argument. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Assertion dvcxp1 ( 𝐴 ∈ ℂ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 𝐴 · ( 𝑥 ↑𝑐 ( 𝐴 − 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
2 1 a1i ⊢ ( 𝐴 ∈ ℂ → ℝ ∈ { ℝ , ℂ } )
3 relogcl ⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
4 3 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
5 rpreccl ⊢ ( 𝑥 ∈ ℝ+ → ( 1 / 𝑥 ) ∈ ℝ+ )
6 5 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℝ+ )
7 recn ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
8 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝐴 · 𝑦 ) ∈ ℂ )
9 efcl ⊢ ( ( 𝐴 · 𝑦 ) ∈ ℂ → ( exp ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
10 8 9 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( exp ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
11 7 10 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℝ ) → ( exp ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
12 ovexd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℝ ) → ( ( exp ‘ ( 𝐴 · 𝑦 ) ) · 𝐴 ) ∈ V )
13 relogf1o ⊢ ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ
14 f1of ⊢ ( ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ )
15 13 14 mp1i ⊢ ( 𝐴 ∈ ℂ → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ )
16 15 feqmptd ⊢ ( 𝐴 ∈ ℂ → ( log ↾ ℝ+ ) = ( 𝑥 ∈ ℝ+ ↦ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) ) )
17 fvres ⊢ ( 𝑥 ∈ ℝ+ → ( ( log ↾ ℝ+ ) ‘ 𝑥 ) = ( log ‘ 𝑥 ) )
18 17 mpteq2ia ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) )
19 16 18 eqtrdi ⊢ ( 𝐴 ∈ ℂ → ( log ↾ ℝ+ ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) )
20 19 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( ℝ D ( log ↾ ℝ+ ) ) = ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ) )
21 dvrelog ⊢ ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) )
22 20 21 eqtr3di ⊢ ( 𝐴 ∈ ℂ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) )
23 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
24 23 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
25 toponmax ⊢ ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) → ℂ ∈ ( TopOpen ‘ ℂfld ) )
26 24 25 mp1i ⊢ ( 𝐴 ∈ ℂ → ℂ ∈ ( TopOpen ‘ ℂfld ) )
27 ax-resscn ⊢ ℝ ⊆ ℂ
28 27 a1i ⊢ ( 𝐴 ∈ ℂ → ℝ ⊆ ℂ )
29 dfss2 ⊢ ( ℝ ⊆ ℂ ↔ ( ℝ ∩ ℂ ) = ℝ )
30 28 29 sylib ⊢ ( 𝐴 ∈ ℂ → ( ℝ ∩ ℂ ) = ℝ )
31 ovexd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( exp ‘ ( 𝐴 · 𝑦 ) ) · 𝐴 ) ∈ V )
32 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
33 32 a1i ⊢ ( 𝐴 ∈ ℂ → ℂ ∈ { ℝ , ℂ } )
34 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → 𝐴 ∈ ℂ )
35 efcl ⊢ ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ∈ ℂ )
36 35 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( exp ‘ 𝑥 ) ∈ ℂ )
37 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
38 1cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → 1 ∈ ℂ )
39 33 dvmptid ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) = ( 𝑦 ∈ ℂ ↦ 1 ) )
40 id ⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
41 33 37 38 39 40 dvmptcmul ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 1 ) ) )
42 mulrid ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) = 𝐴 )
43 42 mpteq2dv ⊢ ( 𝐴 ∈ ℂ → ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 1 ) ) = ( 𝑦 ∈ ℂ ↦ 𝐴 ) )
44 41 43 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ 𝐴 ) )
45 dvef ⊢ ( ℂ D exp ) = exp
46 eff ⊢ exp : ℂ ⟶ ℂ
47 46 a1i ⊢ ( 𝐴 ∈ ℂ → exp : ℂ ⟶ ℂ )
48 47 feqmptd ⊢ ( 𝐴 ∈ ℂ → exp = ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) )
49 48 eqcomd ⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) = exp )
50 49 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) ) = ( ℂ D exp ) )
51 45 50 49 3eqtr4a ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) )
52 fveq2 ⊢ ( 𝑥 = ( 𝐴 · 𝑦 ) → ( exp ‘ 𝑥 ) = ( exp ‘ ( 𝐴 · 𝑦 ) ) )
53 33 33 8 34 36 36 44 51 52 52 dvmptco ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( exp ‘ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( exp ‘ ( 𝐴 · 𝑦 ) ) · 𝐴 ) ) )
54 23 2 26 30 10 31 53 dvmptres3 ⊢ ( 𝐴 ∈ ℂ → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( exp ‘ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( 𝐴 · 𝑦 ) ) · 𝐴 ) ) )
55 oveq2 ⊢ ( 𝑦 = ( log ‘ 𝑥 ) → ( 𝐴 · 𝑦 ) = ( 𝐴 · ( log ‘ 𝑥 ) ) )
56 55 fveq2d ⊢ ( 𝑦 = ( log ‘ 𝑥 ) → ( exp ‘ ( 𝐴 · 𝑦 ) ) = ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) )
57 56 oveq1d ⊢ ( 𝑦 = ( log ‘ 𝑥 ) → ( ( exp ‘ ( 𝐴 · 𝑦 ) ) · 𝐴 ) = ( ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) · 𝐴 ) )
58 2 2 4 6 11 12 22 54 56 57 dvmptco ⊢ ( 𝐴 ∈ ℂ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) · 𝐴 ) · ( 1 / 𝑥 ) ) ) )
59 rpcn ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
60 59 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
61 rpne0 ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 )
62 61 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ≠ 0 )
63 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
64 60 62 63 cxpefd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑𝑐 𝐴 ) = ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) )
65 64 mpteq2dva ⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 ↑𝑐 𝐴 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) ) )
66 65 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ) = ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) ) ) )
67 1cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℂ )
68 60 62 63 67 cxpsubd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑𝑐 ( 𝐴 − 1 ) ) = ( ( 𝑥 ↑𝑐 𝐴 ) / ( 𝑥 ↑𝑐 1 ) ) )
69 60 cxp1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑𝑐 1 ) = 𝑥 )
70 69 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑥 ↑𝑐 𝐴 ) / ( 𝑥 ↑𝑐 1 ) ) = ( ( 𝑥 ↑𝑐 𝐴 ) / 𝑥 ) )
71 60 63 cxpcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑𝑐 𝐴 ) ∈ ℂ )
72 71 60 62 divrecd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑥 ↑𝑐 𝐴 ) / 𝑥 ) = ( ( 𝑥 ↑𝑐 𝐴 ) · ( 1 / 𝑥 ) ) )
73 68 70 72 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑𝑐 ( 𝐴 − 1 ) ) = ( ( 𝑥 ↑𝑐 𝐴 ) · ( 1 / 𝑥 ) ) )
74 73 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 · ( 𝑥 ↑𝑐 ( 𝐴 − 1 ) ) ) = ( 𝐴 · ( ( 𝑥 ↑𝑐 𝐴 ) · ( 1 / 𝑥 ) ) ) )
75 6 rpcnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℂ )
76 63 71 75 mul12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 · ( ( 𝑥 ↑𝑐 𝐴 ) · ( 1 / 𝑥 ) ) ) = ( ( 𝑥 ↑𝑐 𝐴 ) · ( 𝐴 · ( 1 / 𝑥 ) ) ) )
77 71 63 75 mulassd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( 𝑥 ↑𝑐 𝐴 ) · 𝐴 ) · ( 1 / 𝑥 ) ) = ( ( 𝑥 ↑𝑐 𝐴 ) · ( 𝐴 · ( 1 / 𝑥 ) ) ) )
78 76 77 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 · ( ( 𝑥 ↑𝑐 𝐴 ) · ( 1 / 𝑥 ) ) ) = ( ( ( 𝑥 ↑𝑐 𝐴 ) · 𝐴 ) · ( 1 / 𝑥 ) ) )
79 64 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑥 ↑𝑐 𝐴 ) · 𝐴 ) = ( ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) · 𝐴 ) )
80 79 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( 𝑥 ↑𝑐 𝐴 ) · 𝐴 ) · ( 1 / 𝑥 ) ) = ( ( ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) · 𝐴 ) · ( 1 / 𝑥 ) ) )
81 74 78 80 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 · ( 𝑥 ↑𝑐 ( 𝐴 − 1 ) ) ) = ( ( ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) · 𝐴 ) · ( 1 / 𝑥 ) ) )
82 81 mpteq2dva ⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℝ+ ↦ ( 𝐴 · ( 𝑥 ↑𝑐 ( 𝐴 − 1 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) · 𝐴 ) · ( 1 / 𝑥 ) ) ) )
83 58 66 82 3eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 𝐴 · ( 𝑥 ↑𝑐 ( 𝐴 − 1 ) ) ) ) )