# Metamath Proof Explorer

## Theorem reeff1o

Description: The real exponential function is one-to-one onto. (Contributed by Paul Chapman, 18-Oct-2007) (Revised by Mario Carneiro, 10-Nov-2013)

Ref Expression
Assertion reeff1o ${⊢}\left({\mathrm{exp}↾}_{ℝ}\right):ℝ\underset{1-1 onto}{⟶}{ℝ}^{+}$

### Proof

Step Hyp Ref Expression
1 reeff1 ${⊢}\left({\mathrm{exp}↾}_{ℝ}\right):ℝ\underset{1-1}{⟶}{ℝ}^{+}$
2 f1f ${⊢}\left({\mathrm{exp}↾}_{ℝ}\right):ℝ\underset{1-1}{⟶}{ℝ}^{+}\to \left({\mathrm{exp}↾}_{ℝ}\right):ℝ⟶{ℝ}^{+}$
3 ffn ${⊢}\left({\mathrm{exp}↾}_{ℝ}\right):ℝ⟶{ℝ}^{+}\to \left({\mathrm{exp}↾}_{ℝ}\right)Fnℝ$
4 1 2 3 mp2b ${⊢}\left({\mathrm{exp}↾}_{ℝ}\right)Fnℝ$
5 frn ${⊢}\left({\mathrm{exp}↾}_{ℝ}\right):ℝ⟶{ℝ}^{+}\to \mathrm{ran}\left({\mathrm{exp}↾}_{ℝ}\right)\subseteq {ℝ}^{+}$
6 1 2 5 mp2b ${⊢}\mathrm{ran}\left({\mathrm{exp}↾}_{ℝ}\right)\subseteq {ℝ}^{+}$
7 elrp ${⊢}{z}\in {ℝ}^{+}↔\left({z}\in ℝ\wedge 0<{z}\right)$
8 reclt1 ${⊢}\left({z}\in ℝ\wedge 0<{z}\right)\to \left({z}<1↔1<\frac{1}{{z}}\right)$
9 7 8 sylbi ${⊢}{z}\in {ℝ}^{+}\to \left({z}<1↔1<\frac{1}{{z}}\right)$
10 rpre ${⊢}{z}\in {ℝ}^{+}\to {z}\in ℝ$
11 rpne0 ${⊢}{z}\in {ℝ}^{+}\to {z}\ne 0$
12 10 11 rereccld ${⊢}{z}\in {ℝ}^{+}\to \frac{1}{{z}}\in ℝ$
13 reeff1olem ${⊢}\left(\frac{1}{{z}}\in ℝ\wedge 1<\frac{1}{{z}}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{y}}=\frac{1}{{z}}$
14 12 13 sylan ${⊢}\left({z}\in {ℝ}^{+}\wedge 1<\frac{1}{{z}}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{y}}=\frac{1}{{z}}$
15 eqcom ${⊢}\frac{1}{{z}}={\mathrm{e}}^{{y}}↔{\mathrm{e}}^{{y}}=\frac{1}{{z}}$
16 rpcnne0 ${⊢}{z}\in {ℝ}^{+}\to \left({z}\in ℂ\wedge {z}\ne 0\right)$
17 recn ${⊢}{y}\in ℝ\to {y}\in ℂ$
18 efcl ${⊢}{y}\in ℂ\to {\mathrm{e}}^{{y}}\in ℂ$
19 17 18 syl ${⊢}{y}\in ℝ\to {\mathrm{e}}^{{y}}\in ℂ$
20 efne0 ${⊢}{y}\in ℂ\to {\mathrm{e}}^{{y}}\ne 0$
21 17 20 syl ${⊢}{y}\in ℝ\to {\mathrm{e}}^{{y}}\ne 0$
22 19 21 jca ${⊢}{y}\in ℝ\to \left({\mathrm{e}}^{{y}}\in ℂ\wedge {\mathrm{e}}^{{y}}\ne 0\right)$
23 rec11r ${⊢}\left(\left({z}\in ℂ\wedge {z}\ne 0\right)\wedge \left({\mathrm{e}}^{{y}}\in ℂ\wedge {\mathrm{e}}^{{y}}\ne 0\right)\right)\to \left(\frac{1}{{z}}={\mathrm{e}}^{{y}}↔\frac{1}{{\mathrm{e}}^{{y}}}={z}\right)$
24 16 22 23 syl2an ${⊢}\left({z}\in {ℝ}^{+}\wedge {y}\in ℝ\right)\to \left(\frac{1}{{z}}={\mathrm{e}}^{{y}}↔\frac{1}{{\mathrm{e}}^{{y}}}={z}\right)$
25 efcan ${⊢}{y}\in ℂ\to {\mathrm{e}}^{{y}}{\mathrm{e}}^{-{y}}=1$
26 25 eqcomd ${⊢}{y}\in ℂ\to 1={\mathrm{e}}^{{y}}{\mathrm{e}}^{-{y}}$
27 negcl ${⊢}{y}\in ℂ\to -{y}\in ℂ$
28 efcl ${⊢}-{y}\in ℂ\to {\mathrm{e}}^{-{y}}\in ℂ$
29 27 28 syl ${⊢}{y}\in ℂ\to {\mathrm{e}}^{-{y}}\in ℂ$
30 ax-1cn ${⊢}1\in ℂ$
31 divmul2 ${⊢}\left(1\in ℂ\wedge {\mathrm{e}}^{-{y}}\in ℂ\wedge \left({\mathrm{e}}^{{y}}\in ℂ\wedge {\mathrm{e}}^{{y}}\ne 0\right)\right)\to \left(\frac{1}{{\mathrm{e}}^{{y}}}={\mathrm{e}}^{-{y}}↔1={\mathrm{e}}^{{y}}{\mathrm{e}}^{-{y}}\right)$
32 30 31 mp3an1 ${⊢}\left({\mathrm{e}}^{-{y}}\in ℂ\wedge \left({\mathrm{e}}^{{y}}\in ℂ\wedge {\mathrm{e}}^{{y}}\ne 0\right)\right)\to \left(\frac{1}{{\mathrm{e}}^{{y}}}={\mathrm{e}}^{-{y}}↔1={\mathrm{e}}^{{y}}{\mathrm{e}}^{-{y}}\right)$
33 29 18 20 32 syl12anc ${⊢}{y}\in ℂ\to \left(\frac{1}{{\mathrm{e}}^{{y}}}={\mathrm{e}}^{-{y}}↔1={\mathrm{e}}^{{y}}{\mathrm{e}}^{-{y}}\right)$
34 26 33 mpbird ${⊢}{y}\in ℂ\to \frac{1}{{\mathrm{e}}^{{y}}}={\mathrm{e}}^{-{y}}$
35 17 34 syl ${⊢}{y}\in ℝ\to \frac{1}{{\mathrm{e}}^{{y}}}={\mathrm{e}}^{-{y}}$
36 35 eqeq1d ${⊢}{y}\in ℝ\to \left(\frac{1}{{\mathrm{e}}^{{y}}}={z}↔{\mathrm{e}}^{-{y}}={z}\right)$
37 36 adantl ${⊢}\left({z}\in {ℝ}^{+}\wedge {y}\in ℝ\right)\to \left(\frac{1}{{\mathrm{e}}^{{y}}}={z}↔{\mathrm{e}}^{-{y}}={z}\right)$
38 24 37 bitrd ${⊢}\left({z}\in {ℝ}^{+}\wedge {y}\in ℝ\right)\to \left(\frac{1}{{z}}={\mathrm{e}}^{{y}}↔{\mathrm{e}}^{-{y}}={z}\right)$
39 15 38 syl5bbr ${⊢}\left({z}\in {ℝ}^{+}\wedge {y}\in ℝ\right)\to \left({\mathrm{e}}^{{y}}=\frac{1}{{z}}↔{\mathrm{e}}^{-{y}}={z}\right)$
40 39 biimpd ${⊢}\left({z}\in {ℝ}^{+}\wedge {y}\in ℝ\right)\to \left({\mathrm{e}}^{{y}}=\frac{1}{{z}}\to {\mathrm{e}}^{-{y}}={z}\right)$
41 40 reximdva ${⊢}{z}\in {ℝ}^{+}\to \left(\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{y}}=\frac{1}{{z}}\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{-{y}}={z}\right)$
42 41 adantr ${⊢}\left({z}\in {ℝ}^{+}\wedge 1<\frac{1}{{z}}\right)\to \left(\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{y}}=\frac{1}{{z}}\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{-{y}}={z}\right)$
43 14 42 mpd ${⊢}\left({z}\in {ℝ}^{+}\wedge 1<\frac{1}{{z}}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{-{y}}={z}$
44 renegcl ${⊢}{y}\in ℝ\to -{y}\in ℝ$
45 infm3lem ${⊢}{x}\in ℝ\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{x}=-{y}$
46 fveqeq2 ${⊢}{x}=-{y}\to \left({\mathrm{e}}^{{x}}={z}↔{\mathrm{e}}^{-{y}}={z}\right)$
47 44 45 46 rexxfr ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{x}}={z}↔\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{-{y}}={z}$
48 43 47 sylibr ${⊢}\left({z}\in {ℝ}^{+}\wedge 1<\frac{1}{{z}}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{x}}={z}$
49 48 ex ${⊢}{z}\in {ℝ}^{+}\to \left(1<\frac{1}{{z}}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{x}}={z}\right)$
50 9 49 sylbid ${⊢}{z}\in {ℝ}^{+}\to \left({z}<1\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{x}}={z}\right)$
51 50 imp ${⊢}\left({z}\in {ℝ}^{+}\wedge {z}<1\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{x}}={z}$
52 ef0 ${⊢}{\mathrm{e}}^{0}=1$
53 52 eqeq2i ${⊢}{z}={\mathrm{e}}^{0}↔{z}=1$
54 0re ${⊢}0\in ℝ$
55 fveqeq2 ${⊢}{x}=0\to \left({\mathrm{e}}^{{x}}={z}↔{\mathrm{e}}^{0}={z}\right)$
56 55 rspcev ${⊢}\left(0\in ℝ\wedge {\mathrm{e}}^{0}={z}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{x}}={z}$
57 54 56 mpan ${⊢}{\mathrm{e}}^{0}={z}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{x}}={z}$
58 57 eqcoms ${⊢}{z}={\mathrm{e}}^{0}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{x}}={z}$
59 53 58 sylbir ${⊢}{z}=1\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{x}}={z}$
60 59 adantl ${⊢}\left({z}\in {ℝ}^{+}\wedge {z}=1\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{x}}={z}$
61 reeff1olem ${⊢}\left({z}\in ℝ\wedge 1<{z}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{x}}={z}$
62 10 61 sylan ${⊢}\left({z}\in {ℝ}^{+}\wedge 1<{z}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{x}}={z}$
63 1re ${⊢}1\in ℝ$
64 lttri4 ${⊢}\left({z}\in ℝ\wedge 1\in ℝ\right)\to \left({z}<1\vee {z}=1\vee 1<{z}\right)$
65 10 63 64 sylancl ${⊢}{z}\in {ℝ}^{+}\to \left({z}<1\vee {z}=1\vee 1<{z}\right)$
66 51 60 62 65 mpjao3dan ${⊢}{z}\in {ℝ}^{+}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{x}}={z}$
67 fvres ${⊢}{x}\in ℝ\to \left({\mathrm{exp}↾}_{ℝ}\right)\left({x}\right)={\mathrm{e}}^{{x}}$
68 67 eqeq1d ${⊢}{x}\in ℝ\to \left(\left({\mathrm{exp}↾}_{ℝ}\right)\left({x}\right)={z}↔{\mathrm{e}}^{{x}}={z}\right)$
69 68 rexbiia ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({\mathrm{exp}↾}_{ℝ}\right)\left({x}\right)={z}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{\mathrm{e}}^{{x}}={z}$
70 66 69 sylibr ${⊢}{z}\in {ℝ}^{+}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({\mathrm{exp}↾}_{ℝ}\right)\left({x}\right)={z}$
71 fvelrnb ${⊢}\left({\mathrm{exp}↾}_{ℝ}\right)Fnℝ\to \left({z}\in \mathrm{ran}\left({\mathrm{exp}↾}_{ℝ}\right)↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({\mathrm{exp}↾}_{ℝ}\right)\left({x}\right)={z}\right)$
72 4 71 ax-mp ${⊢}{z}\in \mathrm{ran}\left({\mathrm{exp}↾}_{ℝ}\right)↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({\mathrm{exp}↾}_{ℝ}\right)\left({x}\right)={z}$
73 70 72 sylibr ${⊢}{z}\in {ℝ}^{+}\to {z}\in \mathrm{ran}\left({\mathrm{exp}↾}_{ℝ}\right)$
74 73 ssriv ${⊢}{ℝ}^{+}\subseteq \mathrm{ran}\left({\mathrm{exp}↾}_{ℝ}\right)$
75 6 74 eqssi ${⊢}\mathrm{ran}\left({\mathrm{exp}↾}_{ℝ}\right)={ℝ}^{+}$
76 df-fo ${⊢}\left({\mathrm{exp}↾}_{ℝ}\right):ℝ\underset{onto}{⟶}{ℝ}^{+}↔\left(\left({\mathrm{exp}↾}_{ℝ}\right)Fnℝ\wedge \mathrm{ran}\left({\mathrm{exp}↾}_{ℝ}\right)={ℝ}^{+}\right)$
77 4 75 76 mpbir2an ${⊢}\left({\mathrm{exp}↾}_{ℝ}\right):ℝ\underset{onto}{⟶}{ℝ}^{+}$
78 df-f1o ${⊢}\left({\mathrm{exp}↾}_{ℝ}\right):ℝ\underset{1-1 onto}{⟶}{ℝ}^{+}↔\left(\left({\mathrm{exp}↾}_{ℝ}\right):ℝ\underset{1-1}{⟶}{ℝ}^{+}\wedge \left({\mathrm{exp}↾}_{ℝ}\right):ℝ\underset{onto}{⟶}{ℝ}^{+}\right)$
79 1 77 78 mpbir2an ${⊢}\left({\mathrm{exp}↾}_{ℝ}\right):ℝ\underset{1-1 onto}{⟶}{ℝ}^{+}$