Step | Hyp | Ref
| Expression |
1 | | cosf 11579 |
. . . . . 6
⊢
cos:ℂ⟶ℂ |
2 | | ffn 5312 |
. . . . . 6
⊢
(cos:ℂ⟶ℂ → cos Fn ℂ) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ cos Fn
ℂ |
4 | | ioossre 9817 |
. . . . . 6
⊢
(0(,)π) ⊆ ℝ |
5 | | ax-resscn 7803 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
6 | 4, 5 | sstri 3133 |
. . . . 5
⊢
(0(,)π) ⊆ ℂ |
7 | | fnssres 5276 |
. . . . 5
⊢ ((cos Fn
ℂ ∧ (0(,)π) ⊆ ℂ) → (cos ↾ (0(,)π)) Fn
(0(,)π)) |
8 | 3, 6, 7 | mp2an 423 |
. . . 4
⊢ (cos
↾ (0(,)π)) Fn (0(,)π) |
9 | | fvres 5485 |
. . . . . 6
⊢ (𝑥 ∈ (0(,)π) → ((cos
↾ (0(,)π))‘𝑥) = (cos‘𝑥)) |
10 | | cos0pilt1 13112 |
. . . . . 6
⊢ (𝑥 ∈ (0(,)π) →
(cos‘𝑥) ∈
(-1(,)1)) |
11 | 9, 10 | eqeltrd 2231 |
. . . . 5
⊢ (𝑥 ∈ (0(,)π) → ((cos
↾ (0(,)π))‘𝑥) ∈ (-1(,)1)) |
12 | 11 | rgen 2507 |
. . . 4
⊢
∀𝑥 ∈
(0(,)π)((cos ↾ (0(,)π))‘𝑥) ∈ (-1(,)1) |
13 | | ffnfv 5618 |
. . . 4
⊢ ((cos
↾ (0(,)π)):(0(,)π)⟶(-1(,)1) ↔ ((cos ↾ (0(,)π))
Fn (0(,)π) ∧ ∀𝑥 ∈ (0(,)π)((cos ↾
(0(,)π))‘𝑥) ∈
(-1(,)1))) |
14 | 8, 12, 13 | mpbir2an 927 |
. . 3
⊢ (cos
↾ (0(,)π)):(0(,)π)⟶(-1(,)1) |
15 | | fvres 5485 |
. . . . . 6
⊢ (𝑦 ∈ (0(,)π) → ((cos
↾ (0(,)π))‘𝑦) = (cos‘𝑦)) |
16 | 9, 15 | eqeqan12d 2170 |
. . . . 5
⊢ ((𝑥 ∈ (0(,)π) ∧ 𝑦 ∈ (0(,)π)) →
(((cos ↾ (0(,)π))‘𝑥) = ((cos ↾ (0(,)π))‘𝑦) ↔ (cos‘𝑥) = (cos‘𝑦))) |
17 | | ioossicc 9841 |
. . . . . . 7
⊢
(0(,)π) ⊆ (0[,]π) |
18 | 17 | sseli 3120 |
. . . . . 6
⊢ (𝑥 ∈ (0(,)π) → 𝑥 ∈
(0[,]π)) |
19 | 17 | sseli 3120 |
. . . . . 6
⊢ (𝑦 ∈ (0(,)π) → 𝑦 ∈
(0[,]π)) |
20 | | cos11 13113 |
. . . . . . 7
⊢ ((𝑥 ∈ (0[,]π) ∧ 𝑦 ∈ (0[,]π)) →
(𝑥 = 𝑦 ↔ (cos‘𝑥) = (cos‘𝑦))) |
21 | 20 | biimprd 157 |
. . . . . 6
⊢ ((𝑥 ∈ (0[,]π) ∧ 𝑦 ∈ (0[,]π)) →
((cos‘𝑥) =
(cos‘𝑦) → 𝑥 = 𝑦)) |
22 | 18, 19, 21 | syl2an 287 |
. . . . 5
⊢ ((𝑥 ∈ (0(,)π) ∧ 𝑦 ∈ (0(,)π)) →
((cos‘𝑥) =
(cos‘𝑦) → 𝑥 = 𝑦)) |
23 | 16, 22 | sylbid 149 |
. . . 4
⊢ ((𝑥 ∈ (0(,)π) ∧ 𝑦 ∈ (0(,)π)) →
(((cos ↾ (0(,)π))‘𝑥) = ((cos ↾ (0(,)π))‘𝑦) → 𝑥 = 𝑦)) |
24 | 23 | rgen2 2540 |
. . 3
⊢
∀𝑥 ∈
(0(,)π)∀𝑦 ∈
(0(,)π)(((cos ↾ (0(,)π))‘𝑥) = ((cos ↾ (0(,)π))‘𝑦) → 𝑥 = 𝑦) |
25 | | dff13 5709 |
. . 3
⊢ ((cos
↾ (0(,)π)):(0(,)π)–1-1→(-1(,)1) ↔ ((cos ↾
(0(,)π)):(0(,)π)⟶(-1(,)1) ∧ ∀𝑥 ∈ (0(,)π)∀𝑦 ∈ (0(,)π)(((cos ↾
(0(,)π))‘𝑥) =
((cos ↾ (0(,)π))‘𝑦) → 𝑥 = 𝑦))) |
26 | 14, 24, 25 | mpbir2an 927 |
. 2
⊢ (cos
↾ (0(,)π)):(0(,)π)–1-1→(-1(,)1) |
27 | | 0red 7858 |
. . . . . 6
⊢ (𝑥 ∈ (-1(,)1) → 0 ∈
ℝ) |
28 | | pire 13046 |
. . . . . . 7
⊢ π
∈ ℝ |
29 | 28 | a1i 9 |
. . . . . 6
⊢ (𝑥 ∈ (-1(,)1) → π
∈ ℝ) |
30 | | elioore 9794 |
. . . . . 6
⊢ (𝑥 ∈ (-1(,)1) → 𝑥 ∈
ℝ) |
31 | | pipos 13048 |
. . . . . . 7
⊢ 0 <
π |
32 | 31 | a1i 9 |
. . . . . 6
⊢ (𝑥 ∈ (-1(,)1) → 0 <
π) |
33 | | 0re 7857 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
34 | | iccssre 9837 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ π ∈ ℝ) → (0[,]π) ⊆
ℝ) |
35 | 33, 28, 34 | mp2an 423 |
. . . . . . . 8
⊢
(0[,]π) ⊆ ℝ |
36 | 35, 5 | sstri 3133 |
. . . . . . 7
⊢
(0[,]π) ⊆ ℂ |
37 | 36 | a1i 9 |
. . . . . 6
⊢ (𝑥 ∈ (-1(,)1) →
(0[,]π) ⊆ ℂ) |
38 | | coscn 13030 |
. . . . . . 7
⊢ cos
∈ (ℂ–cn→ℂ) |
39 | 38 | a1i 9 |
. . . . . 6
⊢ (𝑥 ∈ (-1(,)1) → cos
∈ (ℂ–cn→ℂ)) |
40 | 35 | sseli 3120 |
. . . . . . . 8
⊢ (𝑧 ∈ (0[,]π) → 𝑧 ∈
ℝ) |
41 | 40 | recoscld 11598 |
. . . . . . 7
⊢ (𝑧 ∈ (0[,]π) →
(cos‘𝑧) ∈
ℝ) |
42 | 41 | adantl 275 |
. . . . . 6
⊢ ((𝑥 ∈ (-1(,)1) ∧ 𝑧 ∈ (0[,]π)) →
(cos‘𝑧) ∈
ℝ) |
43 | | cospi 13060 |
. . . . . . . 8
⊢
(cos‘π) = -1 |
44 | | neg1rr 8918 |
. . . . . . . . . . 11
⊢ -1 ∈
ℝ |
45 | 44 | rexri 7914 |
. . . . . . . . . 10
⊢ -1 ∈
ℝ* |
46 | | 1re 7856 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
47 | 46 | rexri 7914 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ* |
48 | | elioo2 9803 |
. . . . . . . . . 10
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 <
𝑥 ∧ 𝑥 < 1))) |
49 | 45, 47, 48 | mp2an 423 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 <
𝑥 ∧ 𝑥 < 1)) |
50 | 49 | simp2bi 998 |
. . . . . . . 8
⊢ (𝑥 ∈ (-1(,)1) → -1 <
𝑥) |
51 | 43, 50 | eqbrtrid 3995 |
. . . . . . 7
⊢ (𝑥 ∈ (-1(,)1) →
(cos‘π) < 𝑥) |
52 | 49 | simp3bi 999 |
. . . . . . . 8
⊢ (𝑥 ∈ (-1(,)1) → 𝑥 < 1) |
53 | | cos0 11604 |
. . . . . . . 8
⊢
(cos‘0) = 1 |
54 | 52, 53 | breqtrrdi 4002 |
. . . . . . 7
⊢ (𝑥 ∈ (-1(,)1) → 𝑥 <
(cos‘0)) |
55 | 51, 54 | jca 304 |
. . . . . 6
⊢ (𝑥 ∈ (-1(,)1) →
((cos‘π) < 𝑥
∧ 𝑥 <
(cos‘0))) |
56 | | simplr 520 |
. . . . . . 7
⊢ (((𝑥 ∈ (-1(,)1) ∧ 𝑧 ∈ (0[,]π)) ∧ (𝑤 ∈ (0[,]π) ∧ 𝑧 < 𝑤)) → 𝑧 ∈ (0[,]π)) |
57 | | simprl 521 |
. . . . . . 7
⊢ (((𝑥 ∈ (-1(,)1) ∧ 𝑧 ∈ (0[,]π)) ∧ (𝑤 ∈ (0[,]π) ∧ 𝑧 < 𝑤)) → 𝑤 ∈ (0[,]π)) |
58 | | simprr 522 |
. . . . . . 7
⊢ (((𝑥 ∈ (-1(,)1) ∧ 𝑧 ∈ (0[,]π)) ∧ (𝑤 ∈ (0[,]π) ∧ 𝑧 < 𝑤)) → 𝑧 < 𝑤) |
59 | 56, 57, 58 | cosordlem 13109 |
. . . . . 6
⊢ (((𝑥 ∈ (-1(,)1) ∧ 𝑧 ∈ (0[,]π)) ∧ (𝑤 ∈ (0[,]π) ∧ 𝑧 < 𝑤)) → (cos‘𝑤) < (cos‘𝑧)) |
60 | 27, 29, 30, 32, 37, 39, 42, 55, 59 | ivthdec 12961 |
. . . . 5
⊢ (𝑥 ∈ (-1(,)1) →
∃𝑦 ∈
(0(,)π)(cos‘𝑦) =
𝑥) |
61 | | eqcom 2156 |
. . . . . . 7
⊢ (𝑥 = ((cos ↾
(0(,)π))‘𝑦) ↔
((cos ↾ (0(,)π))‘𝑦) = 𝑥) |
62 | 15 | eqeq1d 2163 |
. . . . . . 7
⊢ (𝑦 ∈ (0(,)π) → (((cos
↾ (0(,)π))‘𝑦) = 𝑥 ↔ (cos‘𝑦) = 𝑥)) |
63 | 61, 62 | syl5bb 191 |
. . . . . 6
⊢ (𝑦 ∈ (0(,)π) → (𝑥 = ((cos ↾
(0(,)π))‘𝑦) ↔
(cos‘𝑦) = 𝑥)) |
64 | 63 | rexbiia 2469 |
. . . . 5
⊢
(∃𝑦 ∈
(0(,)π)𝑥 = ((cos ↾
(0(,)π))‘𝑦) ↔
∃𝑦 ∈
(0(,)π)(cos‘𝑦) =
𝑥) |
65 | 60, 64 | sylibr 133 |
. . . 4
⊢ (𝑥 ∈ (-1(,)1) →
∃𝑦 ∈
(0(,)π)𝑥 = ((cos ↾
(0(,)π))‘𝑦)) |
66 | 65 | rgen 2507 |
. . 3
⊢
∀𝑥 ∈
(-1(,)1)∃𝑦 ∈
(0(,)π)𝑥 = ((cos ↾
(0(,)π))‘𝑦) |
67 | | dffo3 5607 |
. . 3
⊢ ((cos
↾ (0(,)π)):(0(,)π)–onto→(-1(,)1) ↔ ((cos ↾
(0(,)π)):(0(,)π)⟶(-1(,)1) ∧ ∀𝑥 ∈ (-1(,)1)∃𝑦 ∈ (0(,)π)𝑥 = ((cos ↾ (0(,)π))‘𝑦))) |
68 | 14, 66, 67 | mpbir2an 927 |
. 2
⊢ (cos
↾ (0(,)π)):(0(,)π)–onto→(-1(,)1) |
69 | | df-f1o 5170 |
. 2
⊢ ((cos
↾ (0(,)π)):(0(,)π)–1-1-onto→(-1(,)1) ↔ ((cos ↾
(0(,)π)):(0(,)π)–1-1→(-1(,)1) ∧ (cos ↾
(0(,)π)):(0(,)π)–onto→(-1(,)1))) |
70 | 26, 68, 69 | mpbir2an 927 |
1
⊢ (cos
↾ (0(,)π)):(0(,)π)–1-1-onto→(-1(,)1) |