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

Metamath Proof Explorer

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 mulrid ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) = 𝐴 )
9 7 8 eqtrid ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · ( log ‘ e ) ) = 𝐴 )
10 9 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( 𝐴 · ( log ‘ e ) ) ) = ( exp ‘ 𝐴 ) )
11 5 10 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( e ↑𝑐 𝐴 ) = ( exp ‘ 𝐴 ) )