# Metamath Proof Explorer

## Theorem eflog

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

Ref Expression
Assertion eflog ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to {\mathrm{e}}^{\mathrm{log}{A}}={A}$

### Proof

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