This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑧 ∈ ℝ+ ↔ ( 𝑧 ∈ ℝ ∧ 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→ ℝ+