This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvcxp2

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

Ref Expression
Assertion dvcxp2 ( 𝐴 ∈ ℝ+ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 ↑𝑐 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( log ‘ 𝐴 ) · ( 𝐴 ↑𝑐 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
2 1 a1i ⊢ ( 𝐴 ∈ ℝ+ → ℂ ∈ { ℝ , ℂ } )
3 simpr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
4 relogcl ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
5 4 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℂ ) → ( log ‘ 𝐴 ) ∈ ℝ )
6 5 recnd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℂ ) → ( log ‘ 𝐴 ) ∈ ℂ )
7 3 6 mulcld ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 · ( log ‘ 𝐴 ) ) ∈ ℂ )
8 efcl ⊢ ( 𝑦 ∈ ℂ → ( exp ‘ 𝑦 ) ∈ ℂ )
9 8 adantl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑦 ∈ ℂ ) → ( exp ‘ 𝑦 ) ∈ ℂ )
10 3 6 mulcomd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 · ( log ‘ 𝐴 ) ) = ( ( log ‘ 𝐴 ) · 𝑥 ) )
11 10 mpteq2dva ⊢ ( 𝐴 ∈ ℝ+ → ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( log ‘ 𝐴 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( log ‘ 𝐴 ) · 𝑥 ) ) )
12 11 oveq2d ⊢ ( 𝐴 ∈ ℝ+ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( log ‘ 𝐴 ) ) ) ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( log ‘ 𝐴 ) · 𝑥 ) ) ) )
13 1cnd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℂ ) → 1 ∈ ℂ )
14 2 dvmptid ⊢ ( 𝐴 ∈ ℝ+ → ( ℂ D ( 𝑥 ∈ ℂ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ 1 ) )
15 4 recnd ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℂ )
16 2 3 13 14 15 dvmptcmul ⊢ ( 𝐴 ∈ ℝ+ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( log ‘ 𝐴 ) · 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( log ‘ 𝐴 ) · 1 ) ) )
17 6 mulridd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℂ ) → ( ( log ‘ 𝐴 ) · 1 ) = ( log ‘ 𝐴 ) )
18 17 mpteq2dva ⊢ ( 𝐴 ∈ ℝ+ → ( 𝑥 ∈ ℂ ↦ ( ( log ‘ 𝐴 ) · 1 ) ) = ( 𝑥 ∈ ℂ ↦ ( log ‘ 𝐴 ) ) )
19 12 16 18 3eqtrd ⊢ ( 𝐴 ∈ ℝ+ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( log ‘ 𝐴 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( log ‘ 𝐴 ) ) )
20 dvef ⊢ ( ℂ D exp ) = exp
21 eff ⊢ exp : ℂ ⟶ ℂ
22 21 a1i ⊢ ( 𝐴 ∈ ℝ+ → exp : ℂ ⟶ ℂ )
23 22 feqmptd ⊢ ( 𝐴 ∈ ℝ+ → exp = ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) )
24 23 eqcomd ⊢ ( 𝐴 ∈ ℝ+ → ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) = exp )
25 24 oveq2d ⊢ ( 𝐴 ∈ ℝ+ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) ) = ( ℂ D exp ) )
26 20 25 24 3eqtr4a ⊢ ( 𝐴 ∈ ℝ+ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) )
27 fveq2 ⊢ ( 𝑦 = ( 𝑥 · ( log ‘ 𝐴 ) ) → ( exp ‘ 𝑦 ) = ( exp ‘ ( 𝑥 · ( log ‘ 𝐴 ) ) ) )
28 2 2 7 5 9 9 19 26 27 27 dvmptco ⊢ ( 𝐴 ∈ ℝ+ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( exp ‘ ( 𝑥 · ( log ‘ 𝐴 ) ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( 𝑥 · ( log ‘ 𝐴 ) ) ) · ( log ‘ 𝐴 ) ) ) )
29 rpcn ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
30 29 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℂ ) → 𝐴 ∈ ℂ )
31 rpne0 ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ≠ 0 )
32 31 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℂ ) → 𝐴 ≠ 0 )
33 30 32 3 cxpefd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝑥 ) = ( exp ‘ ( 𝑥 · ( log ‘ 𝐴 ) ) ) )
34 33 mpteq2dva ⊢ ( 𝐴 ∈ ℝ+ → ( 𝑥 ∈ ℂ ↦ ( 𝐴 ↑𝑐 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( exp ‘ ( 𝑥 · ( log ‘ 𝐴 ) ) ) ) )
35 34 oveq2d ⊢ ( 𝐴 ∈ ℝ+ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 ↑𝑐 𝑥 ) ) ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( exp ‘ ( 𝑥 · ( log ‘ 𝐴 ) ) ) ) ) )
36 30 3 cxpcld ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝑥 ) ∈ ℂ )
37 6 36 mulcomd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℂ ) → ( ( log ‘ 𝐴 ) · ( 𝐴 ↑𝑐 𝑥 ) ) = ( ( 𝐴 ↑𝑐 𝑥 ) · ( log ‘ 𝐴 ) ) )
38 33 oveq1d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℂ ) → ( ( 𝐴 ↑𝑐 𝑥 ) · ( log ‘ 𝐴 ) ) = ( ( exp ‘ ( 𝑥 · ( log ‘ 𝐴 ) ) ) · ( log ‘ 𝐴 ) ) )
39 37 38 eqtrd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℂ ) → ( ( log ‘ 𝐴 ) · ( 𝐴 ↑𝑐 𝑥 ) ) = ( ( exp ‘ ( 𝑥 · ( log ‘ 𝐴 ) ) ) · ( log ‘ 𝐴 ) ) )
40 39 mpteq2dva ⊢ ( 𝐴 ∈ ℝ+ → ( 𝑥 ∈ ℂ ↦ ( ( log ‘ 𝐴 ) · ( 𝐴 ↑𝑐 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( 𝑥 · ( log ‘ 𝐴 ) ) ) · ( log ‘ 𝐴 ) ) ) )
41 28 35 40 3eqtr4d ⊢ ( 𝐴 ∈ ℝ+ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 ↑𝑐 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( log ‘ 𝐴 ) · ( 𝐴 ↑𝑐 𝑥 ) ) ) )