Theorem reeflog

Description: Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007)

	Ref	Expression
Assertion	reeflog	$$⊢A\in {ℝ}^{+}\to {\mathrm{e}}^{\log A}=A$$

Proof

Step	Hyp	Ref	Expression
1		rpcnne0	$$⊢A\in {ℝ}^{+}\to \left(A\in ℂ\wedge A\ne 0\right)$$
2		eflog	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\log A}=A$$
3	1 2	syl	$$⊢A\in {ℝ}^{+}\to {\mathrm{e}}^{\log A}=A$$