Theorem ecxp

Description: Write the exponential function as an exponent to the power _e . (Contributed by Mario Carneiro, 2-Aug-2014)

	Ref	Expression
Assertion	ecxp	⊢ ( 𝐴 ∈ ℂ → ( e ↑𝑐 𝐴 ) = ( exp ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ere	⊢ e ∈ ℝ
2	1	recni	⊢ e ∈ ℂ
3		ene0	⊢ e ≠ 0
4		cxpef	⊢ ( ( e ∈ ℂ ∧ e ≠ 0 ∧ 𝐴 ∈ ℂ ) → ( e ↑𝑐 𝐴 ) = ( exp ‘ ( 𝐴 · ( log ‘ e ) ) ) )
5	2 3 4	mp3an12	⊢ ( 𝐴 ∈ ℂ → ( e ↑𝑐 𝐴 ) = ( exp ‘ ( 𝐴 · ( log ‘ e ) ) ) )
6		loge	⊢ ( log ‘ e ) = 1
7	6	oveq2i	⊢ ( 𝐴 · ( log ‘ e ) ) = ( 𝐴 · 1 )
8		mulid1	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) = 𝐴 )
9	7 8	eqtrid	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · ( log ‘ e ) ) = 𝐴 )
10	9	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( 𝐴 · ( log ‘ e ) ) ) = ( exp ‘ 𝐴 ) )
11	5 10	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( e ↑𝑐 𝐴 ) = ( exp ‘ 𝐴 ) )