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

Metamath Proof Explorer

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

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