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→ ℝ+