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+

Metamath Proof Explorer

Theorem reeff1o

Proof