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 |` RR ) : RR -1-1-onto-> RR+

Proof

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