Step | Hyp | Ref
| Expression |
1 | | recosf1o 24085 |
. . 3
⊢ (cos
↾ (0[,]π)):(0[,]π)–1-1-onto→(-1[,]1) |
2 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥)) = (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥)) |
3 | | halfpire 24020 |
. . . . . . . 8
⊢ (π /
2) ∈ ℝ |
4 | | neghalfpire 24021 |
. . . . . . . . . 10
⊢ -(π /
2) ∈ ℝ |
5 | | iccssre 12126 |
. . . . . . . . . 10
⊢ ((-(π
/ 2) ∈ ℝ ∧ (π / 2) ∈ ℝ) → (-(π /
2)[,](π / 2)) ⊆ ℝ) |
6 | 4, 3, 5 | mp2an 704 |
. . . . . . . . 9
⊢ (-(π /
2)[,](π / 2)) ⊆ ℝ |
7 | 6 | sseli 3564 |
. . . . . . . 8
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → 𝑥 ∈
ℝ) |
8 | | resubcl 10224 |
. . . . . . . 8
⊢ (((π /
2) ∈ ℝ ∧ 𝑥
∈ ℝ) → ((π / 2) − 𝑥) ∈ ℝ) |
9 | 3, 7, 8 | sylancr 694 |
. . . . . . 7
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → ((π / 2) − 𝑥) ∈ ℝ) |
10 | 4, 3 | elicc2i 12110 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) ↔ (𝑥 ∈
ℝ ∧ -(π / 2) ≤ 𝑥 ∧ 𝑥 ≤ (π / 2))) |
11 | 10 | simp3bi 1071 |
. . . . . . . 8
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → 𝑥 ≤ (π /
2)) |
12 | | subge0 10420 |
. . . . . . . . 9
⊢ (((π /
2) ∈ ℝ ∧ 𝑥
∈ ℝ) → (0 ≤ ((π / 2) − 𝑥) ↔ 𝑥 ≤ (π / 2))) |
13 | 3, 7, 12 | sylancr 694 |
. . . . . . . 8
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → (0 ≤ ((π / 2) − 𝑥) ↔ 𝑥 ≤ (π / 2))) |
14 | 11, 13 | mpbird 246 |
. . . . . . 7
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → 0 ≤ ((π / 2) − 𝑥)) |
15 | 3 | recni 9931 |
. . . . . . . . . 10
⊢ (π /
2) ∈ ℂ |
16 | | picn 24015 |
. . . . . . . . . 10
⊢ π
∈ ℂ |
17 | 15 | negcli 10228 |
. . . . . . . . . 10
⊢ -(π /
2) ∈ ℂ |
18 | 16, 15 | negsubi 10238 |
. . . . . . . . . . 11
⊢ (π +
-(π / 2)) = (π − (π / 2)) |
19 | | pidiv2halves 24023 |
. . . . . . . . . . . 12
⊢ ((π /
2) + (π / 2)) = π |
20 | 16, 15, 15, 19 | subaddrii 10249 |
. . . . . . . . . . 11
⊢ (π
− (π / 2)) = (π / 2) |
21 | 18, 20 | eqtri 2632 |
. . . . . . . . . 10
⊢ (π +
-(π / 2)) = (π / 2) |
22 | 15, 16, 17, 21 | subaddrii 10249 |
. . . . . . . . 9
⊢ ((π /
2) − π) = -(π / 2) |
23 | 10 | simp2bi 1070 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → -(π / 2) ≤ 𝑥) |
24 | 22, 23 | syl5eqbr 4618 |
. . . . . . . 8
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → ((π / 2) − π) ≤ 𝑥) |
25 | | pire 24014 |
. . . . . . . . . 10
⊢ π
∈ ℝ |
26 | | suble 10385 |
. . . . . . . . . 10
⊢ (((π /
2) ∈ ℝ ∧ π ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((π / 2) −
π) ≤ 𝑥 ↔ ((π
/ 2) − 𝑥) ≤
π)) |
27 | 3, 25, 26 | mp3an12 1406 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → (((π /
2) − π) ≤ 𝑥
↔ ((π / 2) − 𝑥) ≤ π)) |
28 | 7, 27 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → (((π / 2) − π) ≤ 𝑥 ↔ ((π / 2) − 𝑥) ≤ π)) |
29 | 24, 28 | mpbid 221 |
. . . . . . 7
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → ((π / 2) − 𝑥) ≤ π) |
30 | | 0re 9919 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
31 | 30, 25 | elicc2i 12110 |
. . . . . . 7
⊢ (((π /
2) − 𝑥) ∈
(0[,]π) ↔ (((π / 2) − 𝑥) ∈ ℝ ∧ 0 ≤ ((π / 2)
− 𝑥) ∧ ((π /
2) − 𝑥) ≤
π)) |
32 | 9, 14, 29, 31 | syl3anbrc 1239 |
. . . . . 6
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → ((π / 2) − 𝑥) ∈ (0[,]π)) |
33 | 32 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (-(π / 2)[,](π / 2))) → ((π / 2) − 𝑥) ∈
(0[,]π)) |
34 | 30, 25 | elicc2i 12110 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0[,]π) ↔ (𝑦 ∈ ℝ ∧ 0 ≤
𝑦 ∧ 𝑦 ≤ π)) |
35 | 34 | simp1bi 1069 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]π) → 𝑦 ∈
ℝ) |
36 | | resubcl 10224 |
. . . . . . . 8
⊢ (((π /
2) ∈ ℝ ∧ 𝑦
∈ ℝ) → ((π / 2) − 𝑦) ∈ ℝ) |
37 | 3, 35, 36 | sylancr 694 |
. . . . . . 7
⊢ (𝑦 ∈ (0[,]π) → ((π
/ 2) − 𝑦) ∈
ℝ) |
38 | 34 | simp3bi 1071 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0[,]π) → 𝑦 ≤ π) |
39 | 15, 15 | subnegi 10239 |
. . . . . . . . . 10
⊢ ((π /
2) − -(π / 2)) = ((π / 2) + (π / 2)) |
40 | 39, 19 | eqtri 2632 |
. . . . . . . . 9
⊢ ((π /
2) − -(π / 2)) = π |
41 | 38, 40 | syl6breqr 4625 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]π) → 𝑦 ≤ ((π / 2) − -(π
/ 2))) |
42 | | lesub 10386 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ ∧ (π / 2)
∈ ℝ ∧ -(π / 2) ∈ ℝ) → (𝑦 ≤ ((π / 2) − -(π / 2)) ↔
-(π / 2) ≤ ((π / 2) − 𝑦))) |
43 | 3, 4, 42 | mp3an23 1408 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → (𝑦 ≤ ((π / 2) − -(π
/ 2)) ↔ -(π / 2) ≤ ((π / 2) − 𝑦))) |
44 | 35, 43 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]π) → (𝑦 ≤ ((π / 2) − -(π
/ 2)) ↔ -(π / 2) ≤ ((π / 2) − 𝑦))) |
45 | 41, 44 | mpbid 221 |
. . . . . . 7
⊢ (𝑦 ∈ (0[,]π) → -(π
/ 2) ≤ ((π / 2) − 𝑦)) |
46 | 15 | subidi 10231 |
. . . . . . . . 9
⊢ ((π /
2) − (π / 2)) = 0 |
47 | 34 | simp2bi 1070 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0[,]π) → 0 ≤
𝑦) |
48 | 46, 47 | syl5eqbr 4618 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]π) → ((π
/ 2) − (π / 2)) ≤ 𝑦) |
49 | | suble 10385 |
. . . . . . . . . 10
⊢ (((π /
2) ∈ ℝ ∧ (π / 2) ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((π / 2) −
(π / 2)) ≤ 𝑦 ↔
((π / 2) − 𝑦) ≤
(π / 2))) |
50 | 3, 3, 49 | mp3an12 1406 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → (((π /
2) − (π / 2)) ≤ 𝑦 ↔ ((π / 2) − 𝑦) ≤ (π /
2))) |
51 | 35, 50 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]π) →
(((π / 2) − (π / 2)) ≤ 𝑦 ↔ ((π / 2) − 𝑦) ≤ (π /
2))) |
52 | 48, 51 | mpbid 221 |
. . . . . . 7
⊢ (𝑦 ∈ (0[,]π) → ((π
/ 2) − 𝑦) ≤ (π
/ 2)) |
53 | 4, 3 | elicc2i 12110 |
. . . . . . 7
⊢ (((π /
2) − 𝑦) ∈
(-(π / 2)[,](π / 2)) ↔ (((π / 2) − 𝑦) ∈ ℝ ∧ -(π / 2) ≤
((π / 2) − 𝑦)
∧ ((π / 2) − 𝑦) ≤ (π / 2))) |
54 | 37, 45, 52, 53 | syl3anbrc 1239 |
. . . . . 6
⊢ (𝑦 ∈ (0[,]π) → ((π
/ 2) − 𝑦) ∈
(-(π / 2)[,](π / 2))) |
55 | 54 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ (0[,]π)) → ((π / 2) − 𝑦) ∈ (-(π / 2)[,](π /
2))) |
56 | | iccssre 12126 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ π ∈ ℝ) → (0[,]π) ⊆
ℝ) |
57 | 30, 25, 56 | mp2an 704 |
. . . . . . . . . 10
⊢
(0[,]π) ⊆ ℝ |
58 | | ax-resscn 9872 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
59 | 57, 58 | sstri 3577 |
. . . . . . . . 9
⊢
(0[,]π) ⊆ ℂ |
60 | 59 | sseli 3564 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]π) → 𝑦 ∈
ℂ) |
61 | 6, 58 | sstri 3577 |
. . . . . . . . 9
⊢ (-(π /
2)[,](π / 2)) ⊆ ℂ |
62 | 61 | sseli 3564 |
. . . . . . . 8
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → 𝑥 ∈
ℂ) |
63 | | subsub23 10165 |
. . . . . . . . 9
⊢ (((π /
2) ∈ ℂ ∧ 𝑦
∈ ℂ ∧ 𝑥
∈ ℂ) → (((π / 2) − 𝑦) = 𝑥 ↔ ((π / 2) − 𝑥) = 𝑦)) |
64 | 15, 63 | mp3an1 1403 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (((π
/ 2) − 𝑦) = 𝑥 ↔ ((π / 2) −
𝑥) = 𝑦)) |
65 | 60, 62, 64 | syl2anr 494 |
. . . . . . 7
⊢ ((𝑥 ∈ (-(π / 2)[,](π /
2)) ∧ 𝑦 ∈
(0[,]π)) → (((π / 2) − 𝑦) = 𝑥 ↔ ((π / 2) − 𝑥) = 𝑦)) |
66 | 65 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ (𝑥
∈ (-(π / 2)[,](π / 2)) ∧ 𝑦 ∈ (0[,]π))) → (((π / 2)
− 𝑦) = 𝑥 ↔ ((π / 2) −
𝑥) = 𝑦)) |
67 | | eqcom 2617 |
. . . . . 6
⊢ (𝑥 = ((π / 2) − 𝑦) ↔ ((π / 2) −
𝑦) = 𝑥) |
68 | | eqcom 2617 |
. . . . . 6
⊢ (𝑦 = ((π / 2) − 𝑥) ↔ ((π / 2) −
𝑥) = 𝑦) |
69 | 66, 67, 68 | 3bitr4g 302 |
. . . . 5
⊢
((⊤ ∧ (𝑥
∈ (-(π / 2)[,](π / 2)) ∧ 𝑦 ∈ (0[,]π))) → (𝑥 = ((π / 2) − 𝑦) ↔ 𝑦 = ((π / 2) − 𝑥))) |
70 | 2, 33, 55, 69 | f1o2d 6785 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ (-(π /
2)[,](π / 2)) ↦ ((π / 2) − 𝑥)):(-(π / 2)[,](π / 2))–1-1-onto→(0[,]π)) |
71 | 70 | trud 1484 |
. . 3
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥)):(-(π / 2)[,](π / 2))–1-1-onto→(0[,]π) |
72 | | f1oco 6072 |
. . 3
⊢ (((cos
↾ (0[,]π)):(0[,]π)–1-1-onto→(-1[,]1) ∧ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥)):(-(π / 2)[,](π / 2))–1-1-onto→(0[,]π)) → ((cos ↾ (0[,]π))
∘ (𝑥 ∈ (-(π /
2)[,](π / 2)) ↦ ((π / 2) − 𝑥))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1)) |
73 | 1, 71, 72 | mp2an 704 |
. 2
⊢ ((cos
↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) |
74 | | cosf 14694 |
. . . . . . . 8
⊢
cos:ℂ⟶ℂ |
75 | | ffn 5958 |
. . . . . . . 8
⊢
(cos:ℂ⟶ℂ → cos Fn ℂ) |
76 | 74, 75 | ax-mp 5 |
. . . . . . 7
⊢ cos Fn
ℂ |
77 | | fnssres 5918 |
. . . . . . 7
⊢ ((cos Fn
ℂ ∧ (0[,]π) ⊆ ℂ) → (cos ↾ (0[,]π)) Fn
(0[,]π)) |
78 | 76, 59, 77 | mp2an 704 |
. . . . . 6
⊢ (cos
↾ (0[,]π)) Fn (0[,]π) |
79 | 2, 32 | fmpti 6291 |
. . . . . 6
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥)):(-(π / 2)[,](π /
2))⟶(0[,]π) |
80 | | fnfco 5982 |
. . . . . 6
⊢ (((cos
↾ (0[,]π)) Fn (0[,]π) ∧ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥)):(-(π / 2)[,](π /
2))⟶(0[,]π)) → ((cos ↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥))) Fn (-(π / 2)[,](π /
2))) |
81 | 78, 79, 80 | mp2an 704 |
. . . . 5
⊢ ((cos
↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))) Fn
(-(π / 2)[,](π / 2)) |
82 | | sinf 14693 |
. . . . . . 7
⊢
sin:ℂ⟶ℂ |
83 | | ffn 5958 |
. . . . . . 7
⊢
(sin:ℂ⟶ℂ → sin Fn ℂ) |
84 | 82, 83 | ax-mp 5 |
. . . . . 6
⊢ sin Fn
ℂ |
85 | | fnssres 5918 |
. . . . . 6
⊢ ((sin Fn
ℂ ∧ (-(π / 2)[,](π / 2)) ⊆ ℂ) → (sin ↾
(-(π / 2)[,](π / 2))) Fn (-(π / 2)[,](π / 2))) |
86 | 84, 61, 85 | mp2an 704 |
. . . . 5
⊢ (sin
↾ (-(π / 2)[,](π / 2))) Fn (-(π / 2)[,](π /
2)) |
87 | | eqfnfv 6219 |
. . . . 5
⊢ ((((cos
↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))) Fn
(-(π / 2)[,](π / 2)) ∧ (sin ↾ (-(π / 2)[,](π / 2))) Fn
(-(π / 2)[,](π / 2))) → (((cos ↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥))) = (sin ↾ (-(π / 2)[,](π /
2))) ↔ ∀𝑦
∈ (-(π / 2)[,](π / 2))(((cos ↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥)))‘𝑦) = ((sin ↾ (-(π / 2)[,](π /
2)))‘𝑦))) |
88 | 81, 86, 87 | mp2an 704 |
. . . 4
⊢ (((cos
↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))) =
(sin ↾ (-(π / 2)[,](π / 2))) ↔ ∀𝑦 ∈ (-(π / 2)[,](π / 2))(((cos
↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥)))‘𝑦) = ((sin ↾ (-(π / 2)[,](π /
2)))‘𝑦)) |
89 | 79 | ffvelrni 6266 |
. . . . . . 7
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → ((𝑥 ∈
(-(π / 2)[,](π / 2)) ↦ ((π / 2) − 𝑥))‘𝑦) ∈ (0[,]π)) |
90 | | fvres 6117 |
. . . . . . 7
⊢ (((𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥))‘𝑦) ∈ (0[,]π) → ((cos ↾
(0[,]π))‘((𝑥
∈ (-(π / 2)[,](π / 2)) ↦ ((π / 2) − 𝑥))‘𝑦)) = (cos‘((𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))‘𝑦))) |
91 | 89, 90 | syl 17 |
. . . . . 6
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → ((cos ↾ (0[,]π))‘((𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))‘𝑦)) = (cos‘((𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))‘𝑦))) |
92 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((π / 2) − 𝑥) = ((π / 2) − 𝑦)) |
93 | | ovex 6577 |
. . . . . . . 8
⊢ ((π /
2) − 𝑦) ∈
V |
94 | 92, 2, 93 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → ((𝑥 ∈
(-(π / 2)[,](π / 2)) ↦ ((π / 2) − 𝑥))‘𝑦) = ((π / 2) − 𝑦)) |
95 | 94 | fveq2d 6107 |
. . . . . 6
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → (cos‘((𝑥
∈ (-(π / 2)[,](π / 2)) ↦ ((π / 2) − 𝑥))‘𝑦)) = (cos‘((π / 2) − 𝑦))) |
96 | 61 | sseli 3564 |
. . . . . . 7
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → 𝑦 ∈
ℂ) |
97 | | coshalfpim 24051 |
. . . . . . 7
⊢ (𝑦 ∈ ℂ →
(cos‘((π / 2) − 𝑦)) = (sin‘𝑦)) |
98 | 96, 97 | syl 17 |
. . . . . 6
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → (cos‘((π / 2) − 𝑦)) = (sin‘𝑦)) |
99 | 91, 95, 98 | 3eqtrd 2648 |
. . . . 5
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → ((cos ↾ (0[,]π))‘((𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))‘𝑦)) = (sin‘𝑦)) |
100 | | fvco3 6185 |
. . . . . 6
⊢ (((𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥)):(-(π / 2)[,](π /
2))⟶(0[,]π) ∧ 𝑦 ∈ (-(π / 2)[,](π / 2))) →
(((cos ↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥)))‘𝑦) = ((cos ↾ (0[,]π))‘((𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥))‘𝑦))) |
101 | 79, 100 | mpan 702 |
. . . . 5
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → (((cos ↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥)))‘𝑦) = ((cos ↾ (0[,]π))‘((𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥))‘𝑦))) |
102 | | fvres 6117 |
. . . . 5
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → ((sin ↾ (-(π / 2)[,](π / 2)))‘𝑦) = (sin‘𝑦)) |
103 | 99, 101, 102 | 3eqtr4d 2654 |
. . . 4
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → (((cos ↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥)))‘𝑦) = ((sin ↾ (-(π / 2)[,](π /
2)))‘𝑦)) |
104 | 88, 103 | mprgbir 2911 |
. . 3
⊢ ((cos
↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))) =
(sin ↾ (-(π / 2)[,](π / 2))) |
105 | | f1oeq1 6040 |
. . 3
⊢ (((cos
↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))) =
(sin ↾ (-(π / 2)[,](π / 2))) → (((cos ↾ (0[,]π))
∘ (𝑥 ∈ (-(π /
2)[,](π / 2)) ↦ ((π / 2) − 𝑥))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) ↔ (sin ↾ (-(π /
2)[,](π / 2))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1))) |
106 | 104, 105 | ax-mp 5 |
. 2
⊢ (((cos
↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) ↔ (sin ↾ (-(π /
2)[,](π / 2))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1)) |
107 | 73, 106 | mpbi 219 |
1
⊢ (sin
↾ (-(π / 2)[,](π / 2))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) |