eflog

Description: Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008)

		Ref	Expression
	Assertion	eflog	$⊢ (A \in ℂ \land A \neq 0) \to e^{\log A} = A$

Step	Hyp	Ref	Expression
1		dflog2	$⊢ log = {({\exp ↾}_{ran log})}^{-1}$
2	1	fveq1i	$⊢ \log A = {({\exp ↾}_{ran log})}^{-1} (A)$
3	2	fveq2i	$⊢ ({\exp ↾}_{ran log}) (\log A) = ({\exp ↾}_{ran log}) ({({\exp ↾}_{ran log})}^{-1} (A))$
4		logrncl	$⊢ (A \in ℂ \land A \neq 0) \to \log A \in ran log$
5	4	fvresd	$⊢ (A \in ℂ \land A \neq 0) \to ({\exp ↾}_{ran log}) (\log A) = e^{\log A}$
6		eldifsn	$⊢ A \in (ℂ ∖ \{0\}) \leftrightarrow (A \in ℂ \land A \neq 0)$
7		eff1o2	$⊢ ({\exp ↾}_{ran log}) : ran log \underset{1-1 onto}{⟶} ℂ ∖ \{0\}$
8		f1ocnvfv2	$⊢ (({\exp ↾}_{ran log}) : ran log \underset{1-1 onto}{⟶} ℂ ∖ \{0\} \land A \in (ℂ ∖ \{0\})) \to ({\exp ↾}_{ran log}) ({({\exp ↾}_{ran log})}^{-1} (A)) = A$
9	7 8	mpan	$⊢ A \in (ℂ ∖ \{0\}) \to ({\exp ↾}_{ran log}) ({({\exp ↾}_{ran log})}^{-1} (A)) = A$
10	6 9	sylbir	$⊢ (A \in ℂ \land A \neq 0) \to ({\exp ↾}_{ran log}) ({({\exp ↾}_{ran log})}^{-1} (A)) = A$
11	3 5 10	3eqtr3a	$⊢ (A \in ℂ \land A \neq 0) \to e^{\log A} = A$

Metamath Proof Explorer