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 ‘ 𝐴 ) · ( 𝐴 ↑𝑐 𝑥 ) ) ) )