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 exp : 1-1 onto +

Proof

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