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	⊢ ( 𝑧 ∈ ℝ+ ↔ ( 𝑧 ∈ ℝ ∧ 0 < 𝑧 ) )
8		reclt1	⊢ ( ( 𝑧 ∈ ℝ ∧ 0 < 𝑧 ) → ( 𝑧 < 1 ↔ 1 < ( 1 / 𝑧 ) ) )
9	7 8	sylbi	⊢ ( 𝑧 ∈ ℝ+ → ( 𝑧 < 1 ↔ 1 < ( 1 / 𝑧 ) ) )
10		rpre	⊢ ( 𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ )
11		rpne0	⊢ ( 𝑧 ∈ ℝ+ → 𝑧 ≠ 0 )
12	10 11	rereccld	⊢ ( 𝑧 ∈ ℝ+ → ( 1 / 𝑧 ) ∈ ℝ )
13		reeff1olem	⊢ ( ( ( 1 / 𝑧 ) ∈ ℝ ∧ 1 < ( 1 / 𝑧 ) ) → ∃ 𝑦 ∈ ℝ ( exp ‘ 𝑦 ) = ( 1 / 𝑧 ) )
14	12 13	sylan	⊢ ( ( 𝑧 ∈ ℝ+ ∧ 1 < ( 1 / 𝑧 ) ) → ∃ 𝑦 ∈ ℝ ( exp ‘ 𝑦 ) = ( 1 / 𝑧 ) )
15		eqcom	⊢ ( ( 1 / 𝑧 ) = ( exp ‘ 𝑦 ) ↔ ( exp ‘ 𝑦 ) = ( 1 / 𝑧 ) )
16		rpcnne0	⊢ ( 𝑧 ∈ ℝ+ → ( 𝑧 ∈ ℂ ∧ 𝑧 ≠ 0 ) )
17		recn	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
18		efcl	⊢ ( 𝑦 ∈ ℂ → ( exp ‘ 𝑦 ) ∈ ℂ )
19	17 18	syl	⊢ ( 𝑦 ∈ ℝ → ( exp ‘ 𝑦 ) ∈ ℂ )
20		efne0	⊢ ( 𝑦 ∈ ℂ → ( exp ‘ 𝑦 ) ≠ 0 )
21	17 20	syl	⊢ ( 𝑦 ∈ ℝ → ( exp ‘ 𝑦 ) ≠ 0 )
22	19 21	jca	⊢ ( 𝑦 ∈ ℝ → ( ( exp ‘ 𝑦 ) ∈ ℂ ∧ ( exp ‘ 𝑦 ) ≠ 0 ) )
23		rec11r	⊢ ( ( ( 𝑧 ∈ ℂ ∧ 𝑧 ≠ 0 ) ∧ ( ( exp ‘ 𝑦 ) ∈ ℂ ∧ ( exp ‘ 𝑦 ) ≠ 0 ) ) → ( ( 1 / 𝑧 ) = ( exp ‘ 𝑦 ) ↔ ( 1 / ( exp ‘ 𝑦 ) ) = 𝑧 ) )
24	16 22 23	syl2an	⊢ ( ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ ℝ ) → ( ( 1 / 𝑧 ) = ( exp ‘ 𝑦 ) ↔ ( 1 / ( exp ‘ 𝑦 ) ) = 𝑧 ) )
25		efcan	⊢ ( 𝑦 ∈ ℂ → ( ( exp ‘ 𝑦 ) · ( exp ‘ - 𝑦 ) ) = 1 )
26	25	eqcomd	⊢ ( 𝑦 ∈ ℂ → 1 = ( ( exp ‘ 𝑦 ) · ( exp ‘ - 𝑦 ) ) )
27		negcl	⊢ ( 𝑦 ∈ ℂ → - 𝑦 ∈ ℂ )
28		efcl	⊢ ( - 𝑦 ∈ ℂ → ( exp ‘ - 𝑦 ) ∈ ℂ )
29	27 28	syl	⊢ ( 𝑦 ∈ ℂ → ( exp ‘ - 𝑦 ) ∈ ℂ )
30		ax-1cn	⊢ 1 ∈ ℂ
31		divmul2	⊢ ( ( 1 ∈ ℂ ∧ ( exp ‘ - 𝑦 ) ∈ ℂ ∧ ( ( exp ‘ 𝑦 ) ∈ ℂ ∧ ( exp ‘ 𝑦 ) ≠ 0 ) ) → ( ( 1 / ( exp ‘ 𝑦 ) ) = ( exp ‘ - 𝑦 ) ↔ 1 = ( ( exp ‘ 𝑦 ) · ( exp ‘ - 𝑦 ) ) ) )
32	30 31	mp3an1	⊢ ( ( ( exp ‘ - 𝑦 ) ∈ ℂ ∧ ( ( exp ‘ 𝑦 ) ∈ ℂ ∧ ( exp ‘ 𝑦 ) ≠ 0 ) ) → ( ( 1 / ( exp ‘ 𝑦 ) ) = ( exp ‘ - 𝑦 ) ↔ 1 = ( ( exp ‘ 𝑦 ) · ( exp ‘ - 𝑦 ) ) ) )
33	29 18 20 32	syl12anc	⊢ ( 𝑦 ∈ ℂ → ( ( 1 / ( exp ‘ 𝑦 ) ) = ( exp ‘ - 𝑦 ) ↔ 1 = ( ( exp ‘ 𝑦 ) · ( exp ‘ - 𝑦 ) ) ) )
34	26 33	mpbird	⊢ ( 𝑦 ∈ ℂ → ( 1 / ( exp ‘ 𝑦 ) ) = ( exp ‘ - 𝑦 ) )
35	17 34	syl	⊢ ( 𝑦 ∈ ℝ → ( 1 / ( exp ‘ 𝑦 ) ) = ( exp ‘ - 𝑦 ) )
36	35	eqeq1d	⊢ ( 𝑦 ∈ ℝ → ( ( 1 / ( exp ‘ 𝑦 ) ) = 𝑧 ↔ ( exp ‘ - 𝑦 ) = 𝑧 ) )
37	36	adantl	⊢ ( ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ ℝ ) → ( ( 1 / ( exp ‘ 𝑦 ) ) = 𝑧 ↔ ( exp ‘ - 𝑦 ) = 𝑧 ) )
38	24 37	bitrd	⊢ ( ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ ℝ ) → ( ( 1 / 𝑧 ) = ( exp ‘ 𝑦 ) ↔ ( exp ‘ - 𝑦 ) = 𝑧 ) )
39	15 38	bitr3id	⊢ ( ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ ℝ ) → ( ( exp ‘ 𝑦 ) = ( 1 / 𝑧 ) ↔ ( exp ‘ - 𝑦 ) = 𝑧 ) )
40	39	biimpd	⊢ ( ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ ℝ ) → ( ( exp ‘ 𝑦 ) = ( 1 / 𝑧 ) → ( exp ‘ - 𝑦 ) = 𝑧 ) )
41	40	reximdva	⊢ ( 𝑧 ∈ ℝ+ → ( ∃ 𝑦 ∈ ℝ ( exp ‘ 𝑦 ) = ( 1 / 𝑧 ) → ∃ 𝑦 ∈ ℝ ( exp ‘ - 𝑦 ) = 𝑧 ) )
42	41	adantr	⊢ ( ( 𝑧 ∈ ℝ+ ∧ 1 < ( 1 / 𝑧 ) ) → ( ∃ 𝑦 ∈ ℝ ( exp ‘ 𝑦 ) = ( 1 / 𝑧 ) → ∃ 𝑦 ∈ ℝ ( exp ‘ - 𝑦 ) = 𝑧 ) )
43	14 42	mpd	⊢ ( ( 𝑧 ∈ ℝ+ ∧ 1 < ( 1 / 𝑧 ) ) → ∃ 𝑦 ∈ ℝ ( exp ‘ - 𝑦 ) = 𝑧 )
44		renegcl	⊢ ( 𝑦 ∈ ℝ → - 𝑦 ∈ ℝ )
45		infm3lem	⊢ ( 𝑥 ∈ ℝ → ∃ 𝑦 ∈ ℝ 𝑥 = - 𝑦 )
46		fveqeq2	⊢ ( 𝑥 = - 𝑦 → ( ( exp ‘ 𝑥 ) = 𝑧 ↔ ( exp ‘ - 𝑦 ) = 𝑧 ) )
47	44 45 46	rexxfr	⊢ ( ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑧 ↔ ∃ 𝑦 ∈ ℝ ( exp ‘ - 𝑦 ) = 𝑧 )
48	43 47	sylibr	⊢ ( ( 𝑧 ∈ ℝ+ ∧ 1 < ( 1 / 𝑧 ) ) → ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑧 )
49	48	ex	⊢ ( 𝑧 ∈ ℝ+ → ( 1 < ( 1 / 𝑧 ) → ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑧 ) )
50	9 49	sylbid	⊢ ( 𝑧 ∈ ℝ+ → ( 𝑧 < 1 → ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑧 ) )
51	50	imp	⊢ ( ( 𝑧 ∈ ℝ+ ∧ 𝑧 < 1 ) → ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑧 )
52		ef0	⊢ ( exp ‘ 0 ) = 1
53	52	eqeq2i	⊢ ( 𝑧 = ( exp ‘ 0 ) ↔ 𝑧 = 1 )
54		0re	⊢ 0 ∈ ℝ
55		fveqeq2	⊢ ( 𝑥 = 0 → ( ( exp ‘ 𝑥 ) = 𝑧 ↔ ( exp ‘ 0 ) = 𝑧 ) )
56	55	rspcev	⊢ ( ( 0 ∈ ℝ ∧ ( exp ‘ 0 ) = 𝑧 ) → ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑧 )
57	54 56	mpan	⊢ ( ( exp ‘ 0 ) = 𝑧 → ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑧 )
58	57	eqcoms	⊢ ( 𝑧 = ( exp ‘ 0 ) → ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑧 )
59	53 58	sylbir	⊢ ( 𝑧 = 1 → ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑧 )
60	59	adantl	⊢ ( ( 𝑧 ∈ ℝ+ ∧ 𝑧 = 1 ) → ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑧 )
61		reeff1olem	⊢ ( ( 𝑧 ∈ ℝ ∧ 1 < 𝑧 ) → ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑧 )
62	10 61	sylan	⊢ ( ( 𝑧 ∈ ℝ+ ∧ 1 < 𝑧 ) → ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑧 )
63		1re	⊢ 1 ∈ ℝ
64		lttri4	⊢ ( ( 𝑧 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑧 < 1 ∨ 𝑧 = 1 ∨ 1 < 𝑧 ) )
65	10 63 64	sylancl	⊢ ( 𝑧 ∈ ℝ+ → ( 𝑧 < 1 ∨ 𝑧 = 1 ∨ 1 < 𝑧 ) )
66	51 60 62 65	mpjao3dan	⊢ ( 𝑧 ∈ ℝ+ → ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑧 )
67		fvres	⊢ ( 𝑥 ∈ ℝ → ( ( exp ↾ ℝ ) ‘ 𝑥 ) = ( exp ‘ 𝑥 ) )
68	67	eqeq1d	⊢ ( 𝑥 ∈ ℝ → ( ( ( exp ↾ ℝ ) ‘ 𝑥 ) = 𝑧 ↔ ( exp ‘ 𝑥 ) = 𝑧 ) )
69	68	rexbiia	⊢ ( ∃ 𝑥 ∈ ℝ ( ( exp ↾ ℝ ) ‘ 𝑥 ) = 𝑧 ↔ ∃ 𝑥 ∈ ℝ ( exp ‘ 𝑥 ) = 𝑧 )
70	66 69	sylibr	⊢ ( 𝑧 ∈ ℝ+ → ∃ 𝑥 ∈ ℝ ( ( exp ↾ ℝ ) ‘ 𝑥 ) = 𝑧 )
71		fvelrnb	⊢ ( ( exp ↾ ℝ ) Fn ℝ → ( 𝑧 ∈ ran ( exp ↾ ℝ ) ↔ ∃ 𝑥 ∈ ℝ ( ( exp ↾ ℝ ) ‘ 𝑥 ) = 𝑧 ) )
72	4 71	ax-mp	⊢ ( 𝑧 ∈ ran ( exp ↾ ℝ ) ↔ ∃ 𝑥 ∈ ℝ ( ( exp ↾ ℝ ) ‘ 𝑥 ) = 𝑧 )
73	70 72	sylibr	⊢ ( 𝑧 ∈ ℝ+ → 𝑧 ∈ 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→ ℝ+