Metamath Proof Explorer

Theorem logeftb

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

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

Proof

Step	Hyp	Ref	Expression
1		eldifsn	$⊢ A \in (ℂ ∖ \{0\}) \leftrightarrow (A \in ℂ \land A \neq 0)$
2		dflog2	$⊢ log = {({\exp ↾}_{ran log})}^{-1}$
3	2	fveq1i	$⊢ \log A = {({\exp ↾}_{ran log})}^{-1} (A)$
4	3	eqeq1i	$⊢ \log A = B \leftrightarrow {({\exp ↾}_{ran log})}^{-1} (A) = B$
5		fvres	$⊢ B \in ran log \to ({\exp ↾}_{ran log}) (B) = e^{B}$
6	5	eqeq1d	$⊢ B \in ran log \to (({\exp ↾}_{ran log}) (B) = A \leftrightarrow e^{B} = A)$
7	6	adantr	$⊢ (B \in ran log \land A \in (ℂ ∖ \{0\})) \to (({\exp ↾}_{ran log}) (B) = A \leftrightarrow e^{B} = A)$
8		eff1o2	$⊢ ({\exp ↾}_{ran log}) : ran log \underset{1-1 onto}{⟶} ℂ ∖ \{0\}$
9		f1ocnvfvb	$⊢ (({\exp ↾}_{ran log}) : ran log \underset{1-1 onto}{⟶} ℂ ∖ \{0\} \land B \in ran log \land A \in (ℂ ∖ \{0\})) \to (({\exp ↾}_{ran log}) (B) = A \leftrightarrow {({\exp ↾}_{ran log})}^{-1} (A) = B)$
10	8 9	mp3an1	$⊢ (B \in ran log \land A \in (ℂ ∖ \{0\})) \to (({\exp ↾}_{ran log}) (B) = A \leftrightarrow {({\exp ↾}_{ran log})}^{-1} (A) = B)$
11	7 10	bitr3d	$⊢ (B \in ran log \land A \in (ℂ ∖ \{0\})) \to (e^{B} = A \leftrightarrow {({\exp ↾}_{ran log})}^{-1} (A) = B)$
12	11	ancoms	$⊢ (A \in (ℂ ∖ \{0\}) \land B \in ran log) \to (e^{B} = A \leftrightarrow {({\exp ↾}_{ran log})}^{-1} (A) = B)$
13	4 12	bitr4id	$⊢ (A \in (ℂ ∖ \{0\}) \land B \in ran log) \to (\log A = B \leftrightarrow e^{B} = A)$
14	1 13	sylanbr	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ran log) \to (\log A = B \leftrightarrow e^{B} = A)$
15	14	3impa	$⊢ (A \in ℂ \land A \neq 0 \land B \in ran log) \to (\log A = B \leftrightarrow e^{B} = A)$