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	$$⊢A\in ℂ\to {\mathrm{e}}^A={\mathrm{e}}^A$$

Proof

Step	Hyp	Ref	Expression
1		ere	$$⊢\mathrm{e}\in ℝ$$
2	1	recni	$$⊢\mathrm{e}\in ℂ$$
3		ene0	$$⊢\mathrm{e}\ne 0$$
4		cxpef	$$⊢\left(\mathrm{e}\in ℂ\wedge \mathrm{e}\ne 0\wedge A\in ℂ\right)\to {\mathrm{e}}^A={\mathrm{e}}^{A\log \mathrm{e}}$$
5	2 3 4	mp3an12	$$⊢A\in ℂ\to {\mathrm{e}}^A={\mathrm{e}}^{A\log \mathrm{e}}$$
6		loge	$$⊢\log \mathrm{e}=1$$
7	6	oveq2i	$$⊢A\log \mathrm{e}=A\cdot 1$$
8		mulid1	$$⊢A\in ℂ\to A\cdot 1=A$$
9	7 8	eqtrid	$$⊢A\in ℂ\to A\log \mathrm{e}=A$$
10	9	fveq2d	$$⊢A\in ℂ\to {\mathrm{e}}^{A\log \mathrm{e}}={\mathrm{e}}^A$$
11	5 10	eqtrd	$$⊢A\in ℂ\to {\mathrm{e}}^A={\mathrm{e}}^A$$