Theorem reeff1o 7368

Description: The real exponential function is one-to-one onto. (Contributed by Paul Chapman, 18-Oct-2007.)

Assertion

Ref	Expression
reeff1o	|- (exp |` RR):RR-1-1-onto->(0(,) +oo)

Proof of Theorem reeff1o

Step	Hyp	Ref	Expression
1		df-f1o 3187	. 2 |- ((exp |` RR):RR-1-1-onto->(0(,) +oo) <-> ((exp |` RR):RR-1-1->(0(,) +oo) /\ (exp |` RR):RR-onto->(0(,) +oo)))
2		reeff1 7350	. 2 |- (exp |` RR):RR-1-1->(0(,) +oo)
3		df-fo 3186	. . 3 |- ((exp |` RR):RR-onto->(0(,) +oo) <-> ((exp |` RR) Fn RR /\ ran (exp |` RR) = (0(,) +oo)))
4		axresscn 5240	. . . 4 |- RR (_ CC
5		sumex 6919	. . . . . 6 |- sum_k e. NN0 ((p^k) / (!` k)) e. V
6		df-ef 7240	. . . . . 6 |- exp = {<.p, q>. | (p e. CC /\ q = sum_k e. NN0 ((p^k) / (!` k)))}
7	5, 6	fnopab2 3604	. . . . 5 |- exp Fn CC
8		fnssresb 3585	. . . . 5 |- (exp Fn CC -> ((exp |` RR) Fn RR <-> RR (_ CC))
9	7, 8	ax-mp 7	. . . 4 |- ((exp |` RR) Fn RR <-> RR (_ CC)
10	4, 9	mpbir 190	. . 3 |- (exp |` RR) Fn RR
11		df-f1 3185	. . . . . . . 8 |- ((exp |` RR):RR-1-1->(0(,) +oo) <-> ((exp |` RR):RR-->(0(,) +oo) /\ Fun `'(exp |` RR)))
12	2, 11	mpbi 189	. . . . . . 7 |- ((exp |` RR):RR-->(0(,) +oo) /\ Fun `'(exp |` RR))
13	12	pm3.26i 320	. . . . . 6 |- (exp |` RR):RR-->(0(,) +oo)
14		df-f 3184	. . . . . 6 |- ((exp |` RR):RR-->(0(,) +oo) <-> ((exp |` RR) Fn RR /\ ran (exp |` RR) (_ (0(,) +oo)))
15	13, 14	mpbi 189	. . . . 5 |- ((exp |` RR) Fn RR /\ ran (exp |` RR) (_ (0(,) +oo))
16	15	pm3.27i 324	. . . 4 |- ran (exp |` RR) (_ (0(,) +oo)
17		1re 5407	. . . . . . . . . 10 |- 1 e. RR
18		lelttrit 5596	. . . . . . . . . . 11 |- ((z e. RR /\ 1 e. RR) -> (z <_ 1 \/ 1 < z))
19		leloet 5491	. . . . . . . . . . . 12 |- ((z e. RR /\ 1 e. RR) -> (z <_ 1 <-> (z < 1 \/ z = 1)))
20	19	orbi1d 613	. . . . . . . . . . 11 |- ((z e. RR /\ 1 e. RR) -> ((z <_ 1 \/ 1 < z) <-> ((z < 1 \/ z = 1) \/ 1 < z)))
21	18, 20	mpbid 195	. . . . . . . . . 10 |- ((z e. RR /\ 1 e. RR) -> ((z < 1 \/ z = 1) \/ 1 < z))
22	17, 21	mpan2 694	. . . . . . . . 9 |- (z e. RR -> ((z < 1 \/ z = 1) \/ 1 < z))
23	22	adantr 389	. . . . . . . 8 |- ((z e. RR /\ 0 < z) -> ((z < 1 \/ z = 1) \/ 1 < z))
24		reclt1t 5846	. . . . . . . . . . . 12 |- ((z e. RR /\ 0 < z) -> (z < 1 <-> 1 < (1 / z)))
25		reeff1olem2OLD 7367	. . . . . . . . . . . . . . . 16 |- (((1 / z) e. RR /\ 1 < (1 / z)) -> E.y e. RR (exp` y) = (1 / z))
26		gt0ne0t 5592	. . . . . . . . . . . . . . . . 17 |- ((z e. RR /\ 0 < z) -> z =/= 0)
27		rerecclt 5759	. . . . . . . . . . . . . . . . 17 |- ((z e. RR /\ z =/= 0) -> (1 / z) e. RR)
28	26, 27	syldan 467	. . . . . . . . . . . . . . . 16 |- ((z e. RR /\ 0 < z) -> (1 / z) e. RR)
29	25, 28	sylan 448	. . . . . . . . . . . . . . 15 |- (((z e. RR /\ 0 < z) /\ 1 < (1 / z)) -> E.y e. RR (exp` y) = (1 / z))
30		rec11rt 5735	. . . . . . . . . . . . . . . . . . . . . 22 |- (((z e. CC /\ (exp` y) e. CC) /\ (z =/= 0 /\ (exp` y) =/= 0)) -> ((1 / z) = (exp` y) <-> (1 / (exp` y)) = z))
31	30	an4s 507	. . . . . . . . . . . . . . . . . . . . 21 |- (((z e. CC /\ z =/= 0) /\ ((exp` y) e. CC /\ (exp` y) =/= 0)) -> ((1 / z) = (exp` y) <-> (1 / (exp` y)) = z))
32		recnt 5285	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z e. RR -> z e. CC)
33	32	adantr 389	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z e. RR /\ 0 < z) -> z e. CC)
34	33, 26	jca 288	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. RR /\ 0 < z) -> (z e. CC /\ z =/= 0))
35		recnt 5285	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. RR -> y e. CC)
36		efclt 7254	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. CC -> (exp` y) e. CC)
37	35, 36	syl 10	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. RR -> (exp` y) e. CC)
38		efne0t 7311	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. CC -> (exp` y) =/= 0)
39	35, 38	syl 10	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. RR -> (exp` y) =/= 0)
40	37, 39	jca 288	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. RR -> ((exp` y) e. CC /\ (exp` y) =/= 0))
41	31, 34, 40	syl2an 454	. . . . . . . . . . . . . . . . . . . 20 |- (((z e. RR /\ 0 < z) /\ y e. RR) -> ((1 / z) = (exp` y) <-> (1 / (exp` y)) = z))
42		efcant 7310	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y e. CC -> ((exp` y) x. (exp` -uy)) = 1)
43	42	eqcomd 1472	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. CC -> 1 = ((exp` y) x. (exp` -uy)))
44		divmul2t 5677	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((1 e. CC /\ (exp` y) e. CC /\ (exp` -uy) e. CC) /\ (exp` y) =/= 0) -> ((1 / (exp` y)) = (exp` -uy) <-> 1 = ((exp` y) x. (exp` -uy))))
45		ax1cn 5241	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- 1 e. CC
46	45	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. CC -> 1 e. CC)
47		negclt 5340	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (y e. CC -> -uy e. CC)
48		efclt 7254	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (-uy e. CC -> (exp` -uy) e. CC)
49	47, 48	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. CC -> (exp` -uy) e. CC)
50	46, 36, 49	3jca 817	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y e. CC -> (1 e. CC /\ (exp` y) e. CC /\ (exp` -uy) e. CC))
51	44, 50, 38	sylanc 471	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. CC -> ((1 / (exp` y)) = (exp` -uy) <-> 1 = ((exp` y) x. (exp` -uy))))
52	43, 51	mpbird 196	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. CC -> (1 / (exp` y)) = (exp` -uy))
53	35, 52	syl 10	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. RR -> (1 / (exp` y)) = (exp` -uy))
54	53	eqeq1d 1475	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. RR -> ((1 / (exp` y)) = z <-> (exp` -uy) = z))
55	54	adantl 388	. . . . . . . . . . . . . . . . . . . 20 |- (((z e. RR /\ 0 < z) /\ y e. RR) -> ((1 / (exp` y)) = z <-> (exp` -uy) = z))
56	41, 55	bitrd 526	. . . . . . . . . . . . . . . . . . 19 |- (((z e. RR /\ 0 < z) /\ y e. RR) -> ((1 / z) = (exp` y) <-> (exp` -uy) = z))
57		eqcom 1469	. . . . . . . . . . . . . . . . . . 19 |- ((1 / z) = (exp` y) <-> (exp` y) = (1 / z))
58	56, 57	syl5bbr 532	. . . . . . . . . . . . . . . . . 18 |- (((z e. RR /\ 0 < z) /\ y e. RR) -> ((exp` y) = (1 / z) <-> (exp` -uy) = z))
59	58	biimpd 153	. . . . . . . . . . . . . . . . 17 |- (((z e. RR /\ 0 < z) /\ y e. RR) -> ((exp` y) = (1 / z) -> (exp` -uy) = z))
60	59	r19.22dva 1731	. . . . . . . . . . . . . . . 16 |- ((z e. RR /\ 0 < z) -> (E.y e. RR (exp` y) = (1 / z) -> E.y e. RR (exp` -uy) = z))
61	60	adantr 389	. . . . . . . . . . . . . . 15 |- (((z e. RR /\ 0 < z) /\ 1 < (1 / z)) -> (E.y e. RR (exp` y) = (1 / z) -> E.y e. RR (exp` -uy) = z))
62	29, 61	mpd 26	. . . . . . . . . . . . . 14 |- (((z e. RR /\ 0 < z) /\ 1 < (1 / z)) -> E.y e. RR (exp` -uy) = z)
63		renegclt 5409	. . . . . . . . . . . . . . 15 |- (y e. RR -> -uy e. RR)
64		infm3lem 6000	. . . . . . . . . . . . . . 15 |- (x e. RR -> E.y e. RR x = -uy)
65		fveq2 3709	. . . . . . . . . . . . . . . 16 |- (x = -uy -> (exp` x) = (exp` -uy))
66	65	eqeq1d 1475	. . . . . . . . . . . . . . 15 |- (x = -uy -> ((exp` x) = z <-> (exp` -uy) = z))
67	63, 64, 66	rexxfr 2891	. . . . . . . . . . . . . 14 |- (E.x e. RR (exp` x) = z <-> E.y e. RR (exp` -uy) = z)
68	62, 67	sylibr 200	. . . . . . . . . . . . 13 |- (((z e. RR /\ 0 < z) /\ 1 < (1 / z)) -> E.x e. RR (exp` x) = z)
69	68	ex 373	. . . . . . . . . . . 12 |- ((z e. RR /\ 0 < z) -> (1 < (1 / z) -> E.x e. RR (exp` x) = z))
70	24, 69	sylbid 203	. . . . . . . . . . 11 |- ((z e. RR /\ 0 < z) -> (z < 1 -> E.x e. RR (exp` x) = z))
71	70	imp 350	. . . . . . . . . 10 |- (((z e. RR /\ 0 < z) /\ z < 1) -> E.x e. RR (exp` x) = z)
72		ef0 7277	. . . . . . . . . . . . 13 |- (exp` 0) = 1
73	72	eqeq2i 1477	. . . . . . . . . . . 12 |- (z = (exp` 0) <-> z = 1)
74		0re 5412	. . . . . . . . . . . . . 14 |- 0 e. RR
75		fveq2 3709	. . . . . . . . . . . . . . . 16 |- (x = 0 -> (exp` x) = (exp` 0))
76	75	eqeq1d 1475	. . . . . . . . . . . . . . 15 |- (x = 0 -> ((exp