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 e^{A} = e^{A}$

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

Metamath Proof Explorer