Metamath Proof Explorer

Theorem dvcncxp1

Description: Derivative of complex power with respect to first argument on the complex plane. (Contributed by Brendan Leahy, 18-Dec-2018)

Ref Expression
Hypothesis dvcncxp1.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
Assertion dvcncxp1 ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 · ( 𝑥 ↑𝑐 ( 𝐴 − 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dvcncxp1.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
3 2 a1i ⊢ ( 𝐴 ∈ ℂ → ℂ ∈ { ℝ , ℂ } )
4 difss ⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ
5 1 4 eqsstri ⊢ 𝐷 ⊆ ℂ
6 5 sseli ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ )
7 1 logdmn0 ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ≠ 0 )
8 6 7 logcld ⊢ ( 𝑥 ∈ 𝐷 → ( log ‘ 𝑥 ) ∈ ℂ )
9 8 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → ( log ‘ 𝑥 ) ∈ ℂ )
10 6 7 reccld ⊢ ( 𝑥 ∈ 𝐷 → ( 1 / 𝑥 ) ∈ ℂ )
11 10 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → ( 1 / 𝑥 ) ∈ ℂ )
12 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝐴 · 𝑦 ) ∈ ℂ )
13 efcl ⊢ ( ( 𝐴 · 𝑦 ) ∈ ℂ → ( exp ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
14 12 13 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( exp ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
15 ovexd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( exp ‘ ( 𝐴 · 𝑦 ) ) · 𝐴 ) ∈ V )
16 1 logcn ⊢ ( log ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℂ )
17 cncff ⊢ ( ( log ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℂ ) → ( log ↾ 𝐷 ) : 𝐷 ⟶ ℂ )
18 16 17 mp1i ⊢ ( 𝐴 ∈ ℂ → ( log ↾ 𝐷 ) : 𝐷 ⟶ ℂ )
19 18 feqmptd ⊢ ( 𝐴 ∈ ℂ → ( log ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( ( log ↾ 𝐷 ) ‘ 𝑥 ) ) )
20 fvres ⊢ ( 𝑥 ∈ 𝐷 → ( ( log ↾ 𝐷 ) ‘ 𝑥 ) = ( log ‘ 𝑥 ) )
21 20 mpteq2ia ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ( log ↾ 𝐷 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( log ‘ 𝑥 ) )
22 19 21 eqtrdi ⊢ ( 𝐴 ∈ ℂ → ( log ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( log ‘ 𝑥 ) ) )
23 22 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( log ↾ 𝐷 ) ) = ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( log ‘ 𝑥 ) ) ) )
24 1 dvlog ⊢ ( ℂ D ( log ↾ 𝐷 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / 𝑥 ) )
25 23 24 eqtr3di ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / 𝑥 ) ) )
26 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → 𝐴 ∈ ℂ )
27 efcl ⊢ ( 𝑥 ∈ ℂ → ( exp ‘ 𝑥 ) ∈ ℂ )
28 27 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( exp ‘ 𝑥 ) ∈ ℂ )
29 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
30 1cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → 1 ∈ ℂ )
31 3 dvmptid ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) = ( 𝑦 ∈ ℂ ↦ 1 ) )
32 id ⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
33 3 29 30 31 32 dvmptcmul ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 1 ) ) )
34 mulid1 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) = 𝐴 )
35 34 mpteq2dv ⊢ ( 𝐴 ∈ ℂ → ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 1 ) ) = ( 𝑦 ∈ ℂ ↦ 𝐴 ) )
36 33 35 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ 𝐴 ) )
37 dvef ⊢ ( ℂ D exp ) = exp
38 eff ⊢ exp : ℂ ⟶ ℂ
39 38 a1i ⊢ ( 𝐴 ∈ ℂ → exp : ℂ ⟶ ℂ )
40 39 feqmptd ⊢ ( 𝐴 ∈ ℂ → exp = ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) )
41 40 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( ℂ D exp ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) ) )
42 37 41 40 3eqtr3a ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( exp ‘ 𝑥 ) ) )
43 fveq2 ⊢ ( 𝑥 = ( 𝐴 · 𝑦 ) → ( exp ‘ 𝑥 ) = ( exp ‘ ( 𝐴 · 𝑦 ) ) )
44 3 3 12 26 28 28 36 42 43 43 dvmptco ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( exp ‘ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( exp ‘ ( 𝐴 · 𝑦 ) ) · 𝐴 ) ) )
45 oveq2 ⊢ ( 𝑦 = ( log ‘ 𝑥 ) → ( 𝐴 · 𝑦 ) = ( 𝐴 · ( log ‘ 𝑥 ) ) )
46 45 fveq2d ⊢ ( 𝑦 = ( log ‘ 𝑥 ) → ( exp ‘ ( 𝐴 · 𝑦 ) ) = ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) )
47 46 oveq1d ⊢ ( 𝑦 = ( log ‘ 𝑥 ) → ( ( exp ‘ ( 𝐴 · 𝑦 ) ) · 𝐴 ) = ( ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) · 𝐴 ) )
48 3 3 9 11 14 15 25 44 46 47 dvmptco ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) · 𝐴 ) · ( 1 / 𝑥 ) ) ) )
49 6 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ℂ )
50 7 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ≠ 0 )
51 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ ℂ )
52 49 50 51 cxpefd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ↑𝑐 𝐴 ) = ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) )
53 52 mpteq2dva ⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝐴 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) ) )
54 53 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ) = ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) ) ) )
55 1cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → 1 ∈ ℂ )
56 49 50 51 55 cxpsubd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ↑𝑐 ( 𝐴 − 1 ) ) = ( ( 𝑥 ↑𝑐 𝐴 ) / ( 𝑥 ↑𝑐 1 ) ) )
57 49 cxp1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ↑𝑐 1 ) = 𝑥 )
58 57 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ↑𝑐 𝐴 ) / ( 𝑥 ↑𝑐 1 ) ) = ( ( 𝑥 ↑𝑐 𝐴 ) / 𝑥 ) )
59 49 51 cxpcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ↑𝑐 𝐴 ) ∈ ℂ )
60 59 49 50 divrecd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ↑𝑐 𝐴 ) / 𝑥 ) = ( ( 𝑥 ↑𝑐 𝐴 ) · ( 1 / 𝑥 ) ) )
61 56 58 60 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ↑𝑐 ( 𝐴 − 1 ) ) = ( ( 𝑥 ↑𝑐 𝐴 ) · ( 1 / 𝑥 ) ) )
62 61 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 · ( 𝑥 ↑𝑐 ( 𝐴 − 1 ) ) ) = ( 𝐴 · ( ( 𝑥 ↑𝑐 𝐴 ) · ( 1 / 𝑥 ) ) ) )
63 51 59 11 mul12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 · ( ( 𝑥 ↑𝑐 𝐴 ) · ( 1 / 𝑥 ) ) ) = ( ( 𝑥 ↑𝑐 𝐴 ) · ( 𝐴 · ( 1 / 𝑥 ) ) ) )
64 59 51 11 mulassd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → ( ( ( 𝑥 ↑𝑐 𝐴 ) · 𝐴 ) · ( 1 / 𝑥 ) ) = ( ( 𝑥 ↑𝑐 𝐴 ) · ( 𝐴 · ( 1 / 𝑥 ) ) ) )
65 63 64 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 · ( ( 𝑥 ↑𝑐 𝐴 ) · ( 1 / 𝑥 ) ) ) = ( ( ( 𝑥 ↑𝑐 𝐴 ) · 𝐴 ) · ( 1 / 𝑥 ) ) )
66 52 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ↑𝑐 𝐴 ) · 𝐴 ) = ( ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) · 𝐴 ) )
67 66 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → ( ( ( 𝑥 ↑𝑐 𝐴 ) · 𝐴 ) · ( 1 / 𝑥 ) ) = ( ( ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) · 𝐴 ) · ( 1 / 𝑥 ) ) )
68 62 65 67 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 · ( 𝑥 ↑𝑐 ( 𝐴 − 1 ) ) ) = ( ( ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) · 𝐴 ) · ( 1 / 𝑥 ) ) )
69 68 mpteq2dva ⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 · ( 𝑥 ↑𝑐 ( 𝐴 − 1 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( ( exp ‘ ( 𝐴 · ( log ‘ 𝑥 ) ) ) · 𝐴 ) · ( 1 / 𝑥 ) ) ) )
70 48 54 69 3eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 · ( 𝑥 ↑𝑐 ( 𝐴 − 1 ) ) ) ) )