Step | Hyp | Ref
| Expression |
1 | | reeff1 14689 |
. 2
⊢ (exp
↾ ℝ):ℝ–1-1→ℝ+ |
2 | | f1f 6014 |
. . . 4
⊢ ((exp
↾ ℝ):ℝ–1-1→ℝ+ → (exp ↾
ℝ):ℝ⟶ℝ+) |
3 | | ffn 5958 |
. . . 4
⊢ ((exp
↾ ℝ):ℝ⟶ℝ+ → (exp ↾
ℝ) Fn ℝ) |
4 | 1, 2, 3 | mp2b 10 |
. . 3
⊢ (exp
↾ ℝ) Fn ℝ |
5 | | frn 5966 |
. . . . 5
⊢ ((exp
↾ ℝ):ℝ⟶ℝ+ → ran (exp ↾
ℝ) ⊆ ℝ+) |
6 | 1, 2, 5 | mp2b 10 |
. . . 4
⊢ ran (exp
↾ ℝ) ⊆ ℝ+ |
7 | | elrp 11710 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℝ+
↔ (𝑧 ∈ ℝ
∧ 0 < 𝑧)) |
8 | | reclt1 10797 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ ∧ 0 <
𝑧) → (𝑧 < 1 ↔ 1 < (1 / 𝑧))) |
9 | 7, 8 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ+
→ (𝑧 < 1 ↔ 1
< (1 / 𝑧))) |
10 | | rpre 11715 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℝ+
→ 𝑧 ∈
ℝ) |
11 | | rpne0 11724 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℝ+
→ 𝑧 ≠
0) |
12 | 10, 11 | rereccld 10731 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℝ+
→ (1 / 𝑧) ∈
ℝ) |
13 | | reeff1olem 24004 |
. . . . . . . . . . . . . 14
⊢ (((1 /
𝑧) ∈ ℝ ∧ 1
< (1 / 𝑧)) →
∃𝑦 ∈ ℝ
(exp‘𝑦) = (1 / 𝑧)) |
14 | 12, 13 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℝ+
∧ 1 < (1 / 𝑧))
→ ∃𝑦 ∈
ℝ (exp‘𝑦) = (1
/ 𝑧)) |
15 | | eqcom 2617 |
. . . . . . . . . . . . . . . . 17
⊢ ((1 /
𝑧) = (exp‘𝑦) ↔ (exp‘𝑦) = (1 / 𝑧)) |
16 | | rpcnne0 11726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ℝ+
→ (𝑧 ∈ ℂ
∧ 𝑧 ≠
0)) |
17 | | recn 9905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
18 | | efcl 14652 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℂ →
(exp‘𝑦) ∈
ℂ) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ →
(exp‘𝑦) ∈
ℂ) |
20 | | efne0 14666 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℂ →
(exp‘𝑦) ≠
0) |
21 | 17, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ →
(exp‘𝑦) ≠
0) |
22 | 19, 21 | jca 553 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ →
((exp‘𝑦) ∈
ℂ ∧ (exp‘𝑦)
≠ 0)) |
23 | | rec11r 10603 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑧 ∈ ℂ ∧ 𝑧 ≠ 0) ∧ ((exp‘𝑦) ∈ ℂ ∧
(exp‘𝑦) ≠ 0))
→ ((1 / 𝑧) =
(exp‘𝑦) ↔ (1 /
(exp‘𝑦)) = 𝑧)) |
24 | 16, 22, 23 | syl2an 493 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℝ+
∧ 𝑦 ∈ ℝ)
→ ((1 / 𝑧) =
(exp‘𝑦) ↔ (1 /
(exp‘𝑦)) = 𝑧)) |
25 | | efcan 14665 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℂ →
((exp‘𝑦) ·
(exp‘-𝑦)) =
1) |
26 | 25 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ℂ → 1 =
((exp‘𝑦) ·
(exp‘-𝑦))) |
27 | | negcl 10160 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℂ → -𝑦 ∈
ℂ) |
28 | | efcl 14652 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (-𝑦 ∈ ℂ →
(exp‘-𝑦) ∈
ℂ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℂ →
(exp‘-𝑦) ∈
ℂ) |
30 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
ℂ |
31 | | divmul2 10568 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((1
∈ ℂ ∧ (exp‘-𝑦) ∈ ℂ ∧ ((exp‘𝑦) ∈ ℂ ∧
(exp‘𝑦) ≠ 0))
→ ((1 / (exp‘𝑦))
= (exp‘-𝑦) ↔ 1 =
((exp‘𝑦) ·
(exp‘-𝑦)))) |
32 | 30, 31 | mp3an1 1403 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((exp‘-𝑦)
∈ ℂ ∧ ((exp‘𝑦) ∈ ℂ ∧ (exp‘𝑦) ≠ 0)) → ((1 /
(exp‘𝑦)) =
(exp‘-𝑦) ↔ 1 =
((exp‘𝑦) ·
(exp‘-𝑦)))) |
33 | 29, 18, 20, 32 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ℂ → ((1 /
(exp‘𝑦)) =
(exp‘-𝑦) ↔ 1 =
((exp‘𝑦) ·
(exp‘-𝑦)))) |
34 | 26, 33 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℂ → (1 /
(exp‘𝑦)) =
(exp‘-𝑦)) |
35 | 17, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ → (1 /
(exp‘𝑦)) =
(exp‘-𝑦)) |
36 | 35 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ → ((1 /
(exp‘𝑦)) = 𝑧 ↔ (exp‘-𝑦) = 𝑧)) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℝ+
∧ 𝑦 ∈ ℝ)
→ ((1 / (exp‘𝑦))
= 𝑧 ↔
(exp‘-𝑦) = 𝑧)) |
38 | 24, 37 | bitrd 267 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℝ+
∧ 𝑦 ∈ ℝ)
→ ((1 / 𝑧) =
(exp‘𝑦) ↔
(exp‘-𝑦) = 𝑧)) |
39 | 15, 38 | syl5bbr 273 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℝ+
∧ 𝑦 ∈ ℝ)
→ ((exp‘𝑦) = (1
/ 𝑧) ↔
(exp‘-𝑦) = 𝑧)) |
40 | 39 | biimpd 218 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℝ+
∧ 𝑦 ∈ ℝ)
→ ((exp‘𝑦) = (1
/ 𝑧) →
(exp‘-𝑦) = 𝑧)) |
41 | 40 | reximdva 3000 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℝ+
→ (∃𝑦 ∈
ℝ (exp‘𝑦) = (1
/ 𝑧) → ∃𝑦 ∈ ℝ
(exp‘-𝑦) = 𝑧)) |
42 | 41 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℝ+
∧ 1 < (1 / 𝑧))
→ (∃𝑦 ∈
ℝ (exp‘𝑦) = (1
/ 𝑧) → ∃𝑦 ∈ ℝ
(exp‘-𝑦) = 𝑧)) |
43 | 14, 42 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℝ+
∧ 1 < (1 / 𝑧))
→ ∃𝑦 ∈
ℝ (exp‘-𝑦) =
𝑧) |
44 | | renegcl 10223 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → -𝑦 ∈
ℝ) |
45 | | infm3lem 10860 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ →
∃𝑦 ∈ ℝ
𝑥 = -𝑦) |
46 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = -𝑦 → (exp‘𝑥) = (exp‘-𝑦)) |
47 | 46 | eqeq1d 2612 |
. . . . . . . . . . . . 13
⊢ (𝑥 = -𝑦 → ((exp‘𝑥) = 𝑧 ↔ (exp‘-𝑦) = 𝑧)) |
48 | 44, 45, 47 | rexxfr 4814 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
ℝ (exp‘𝑥) =
𝑧 ↔ ∃𝑦 ∈ ℝ
(exp‘-𝑦) = 𝑧) |
49 | 43, 48 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ+
∧ 1 < (1 / 𝑧))
→ ∃𝑥 ∈
ℝ (exp‘𝑥) =
𝑧) |
50 | 49 | ex 449 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ+
→ (1 < (1 / 𝑧)
→ ∃𝑥 ∈
ℝ (exp‘𝑥) =
𝑧)) |
51 | 9, 50 | sylbid 229 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℝ+
→ (𝑧 < 1 →
∃𝑥 ∈ ℝ
(exp‘𝑥) = 𝑧)) |
52 | 51 | imp 444 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℝ+
∧ 𝑧 < 1) →
∃𝑥 ∈ ℝ
(exp‘𝑥) = 𝑧) |
53 | | ef0 14660 |
. . . . . . . . . . 11
⊢
(exp‘0) = 1 |
54 | 53 | eqeq2i 2622 |
. . . . . . . . . 10
⊢ (𝑧 = (exp‘0) ↔ 𝑧 = 1) |
55 | | 0re 9919 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
56 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 0 → (exp‘𝑥) =
(exp‘0)) |
57 | 56 | eqeq1d 2612 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → ((exp‘𝑥) = 𝑧 ↔ (exp‘0) = 𝑧)) |
58 | 57 | rspcev 3282 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ (exp‘0) = 𝑧) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑧) |
59 | 55, 58 | mpan 702 |
. . . . . . . . . . 11
⊢
((exp‘0) = 𝑧
→ ∃𝑥 ∈
ℝ (exp‘𝑥) =
𝑧) |
60 | 59 | eqcoms 2618 |
. . . . . . . . . 10
⊢ (𝑧 = (exp‘0) →
∃𝑥 ∈ ℝ
(exp‘𝑥) = 𝑧) |
61 | 54, 60 | sylbir 224 |
. . . . . . . . 9
⊢ (𝑧 = 1 → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑧) |
62 | 61 | adantl 481 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℝ+
∧ 𝑧 = 1) →
∃𝑥 ∈ ℝ
(exp‘𝑥) = 𝑧) |
63 | | reeff1olem 24004 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℝ ∧ 1 <
𝑧) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑧) |
64 | 10, 63 | sylan 487 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℝ+
∧ 1 < 𝑧) →
∃𝑥 ∈ ℝ
(exp‘𝑥) = 𝑧) |
65 | | 1re 9918 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
66 | | lttri4 10001 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℝ ∧ 1 ∈
ℝ) → (𝑧 < 1
∨ 𝑧 = 1 ∨ 1 <
𝑧)) |
67 | 10, 65, 66 | sylancl 693 |
. . . . . . . 8
⊢ (𝑧 ∈ ℝ+
→ (𝑧 < 1 ∨ 𝑧 = 1 ∨ 1 < 𝑧)) |
68 | 52, 62, 64, 67 | mpjao3dan 1387 |
. . . . . . 7
⊢ (𝑧 ∈ ℝ+
→ ∃𝑥 ∈
ℝ (exp‘𝑥) =
𝑧) |
69 | | fvres 6117 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → ((exp
↾ ℝ)‘𝑥) =
(exp‘𝑥)) |
70 | 69 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ → (((exp
↾ ℝ)‘𝑥) =
𝑧 ↔ (exp‘𝑥) = 𝑧)) |
71 | 70 | rexbiia 3022 |
. . . . . . 7
⊢
(∃𝑥 ∈
ℝ ((exp ↾ ℝ)‘𝑥) = 𝑧 ↔ ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑧) |
72 | 68, 71 | sylibr 223 |
. . . . . 6
⊢ (𝑧 ∈ ℝ+
→ ∃𝑥 ∈
ℝ ((exp ↾ ℝ)‘𝑥) = 𝑧) |
73 | | fvelrnb 6153 |
. . . . . . 7
⊢ ((exp
↾ ℝ) Fn ℝ → (𝑧 ∈ ran (exp ↾ ℝ) ↔
∃𝑥 ∈ ℝ
((exp ↾ ℝ)‘𝑥) = 𝑧)) |
74 | 4, 73 | ax-mp 5 |
. . . . . 6
⊢ (𝑧 ∈ ran (exp ↾
ℝ) ↔ ∃𝑥
∈ ℝ ((exp ↾ ℝ)‘𝑥) = 𝑧) |
75 | 72, 74 | sylibr 223 |
. . . . 5
⊢ (𝑧 ∈ ℝ+
→ 𝑧 ∈ ran (exp
↾ ℝ)) |
76 | 75 | ssriv 3572 |
. . . 4
⊢
ℝ+ ⊆ ran (exp ↾ ℝ) |
77 | 6, 76 | eqssi 3584 |
. . 3
⊢ ran (exp
↾ ℝ) = ℝ+ |
78 | | df-fo 5810 |
. . 3
⊢ ((exp
↾ ℝ):ℝ–onto→ℝ+ ↔ ((exp ↾
ℝ) Fn ℝ ∧ ran (exp ↾ ℝ) =
ℝ+)) |
79 | 4, 77, 78 | mpbir2an 957 |
. 2
⊢ (exp
↾ ℝ):ℝ–onto→ℝ+ |
80 | | df-f1o 5811 |
. 2
⊢ ((exp
↾ ℝ):ℝ–1-1-onto→ℝ+ ↔ ((exp
↾ ℝ):ℝ–1-1→ℝ+ ∧ (exp ↾
ℝ):ℝ–onto→ℝ+)) |
81 | 1, 79, 80 | mpbir2an 957 |
1
⊢ (exp
↾ ℝ):ℝ–1-1-onto→ℝ+ |