| Step | Hyp | Ref
| Expression |
| 1 | | recosf1o 26577 |
. . 3
⊢ (cos
↾ (0[,]π)):(0[,]π)–1-1-onto→(-1[,]1) |
| 2 | | eqid 2737 |
. . . . 5
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥)) = (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥)) |
| 3 | | halfpire 26506 |
. . . . . . . 8
⊢ (π /
2) ∈ ℝ |
| 4 | | neghalfpire 26507 |
. . . . . . . . . 10
⊢ -(π /
2) ∈ ℝ |
| 5 | | iccssre 13469 |
. . . . . . . . . 10
⊢ ((-(π
/ 2) ∈ ℝ ∧ (π / 2) ∈ ℝ) → (-(π /
2)[,](π / 2)) ⊆ ℝ) |
| 6 | 4, 3, 5 | mp2an 692 |
. . . . . . . . 9
⊢ (-(π /
2)[,](π / 2)) ⊆ ℝ |
| 7 | 6 | sseli 3979 |
. . . . . . . 8
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → 𝑥 ∈
ℝ) |
| 8 | | resubcl 11573 |
. . . . . . . 8
⊢ (((π /
2) ∈ ℝ ∧ 𝑥
∈ ℝ) → ((π / 2) − 𝑥) ∈ ℝ) |
| 9 | 3, 7, 8 | sylancr 587 |
. . . . . . 7
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → ((π / 2) − 𝑥) ∈ ℝ) |
| 10 | 4, 3 | elicc2i 13453 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) ↔ (𝑥 ∈
ℝ ∧ -(π / 2) ≤ 𝑥 ∧ 𝑥 ≤ (π / 2))) |
| 11 | 10 | simp3bi 1148 |
. . . . . . . 8
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → 𝑥 ≤ (π /
2)) |
| 12 | | subge0 11776 |
. . . . . . . . 9
⊢ (((π /
2) ∈ ℝ ∧ 𝑥
∈ ℝ) → (0 ≤ ((π / 2) − 𝑥) ↔ 𝑥 ≤ (π / 2))) |
| 13 | 3, 7, 12 | sylancr 587 |
. . . . . . . 8
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → (0 ≤ ((π / 2) − 𝑥) ↔ 𝑥 ≤ (π / 2))) |
| 14 | 11, 13 | mpbird 257 |
. . . . . . 7
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → 0 ≤ ((π / 2) − 𝑥)) |
| 15 | 3 | recni 11275 |
. . . . . . . . . 10
⊢ (π /
2) ∈ ℂ |
| 16 | | picn 26501 |
. . . . . . . . . 10
⊢ π
∈ ℂ |
| 17 | 15 | negcli 11577 |
. . . . . . . . . 10
⊢ -(π /
2) ∈ ℂ |
| 18 | 16, 15 | negsubi 11587 |
. . . . . . . . . . 11
⊢ (π +
-(π / 2)) = (π − (π / 2)) |
| 19 | | pidiv2halves 26509 |
. . . . . . . . . . . 12
⊢ ((π /
2) + (π / 2)) = π |
| 20 | 16, 15, 15, 19 | subaddrii 11598 |
. . . . . . . . . . 11
⊢ (π
− (π / 2)) = (π / 2) |
| 21 | 18, 20 | eqtri 2765 |
. . . . . . . . . 10
⊢ (π +
-(π / 2)) = (π / 2) |
| 22 | 15, 16, 17, 21 | subaddrii 11598 |
. . . . . . . . 9
⊢ ((π /
2) − π) = -(π / 2) |
| 23 | 10 | simp2bi 1147 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → -(π / 2) ≤ 𝑥) |
| 24 | 22, 23 | eqbrtrid 5178 |
. . . . . . . 8
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → ((π / 2) − π) ≤ 𝑥) |
| 25 | | pire 26500 |
. . . . . . . . 9
⊢ π
∈ ℝ |
| 26 | | suble 11741 |
. . . . . . . . 9
⊢ (((π /
2) ∈ ℝ ∧ π ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((π / 2) −
π) ≤ 𝑥 ↔ ((π
/ 2) − 𝑥) ≤
π)) |
| 27 | 3, 25, 7, 26 | mp3an12i 1467 |
. . . . . . . 8
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → (((π / 2) − π) ≤ 𝑥 ↔ ((π / 2) − 𝑥) ≤ π)) |
| 28 | 24, 27 | mpbid 232 |
. . . . . . 7
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → ((π / 2) − 𝑥) ≤ π) |
| 29 | | 0re 11263 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
| 30 | 29, 25 | elicc2i 13453 |
. . . . . . 7
⊢ (((π /
2) − 𝑥) ∈
(0[,]π) ↔ (((π / 2) − 𝑥) ∈ ℝ ∧ 0 ≤ ((π / 2)
− 𝑥) ∧ ((π /
2) − 𝑥) ≤
π)) |
| 31 | 9, 14, 28, 30 | syl3anbrc 1344 |
. . . . . 6
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → ((π / 2) − 𝑥) ∈ (0[,]π)) |
| 32 | 31 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (-(π / 2)[,](π / 2))) → ((π / 2) − 𝑥) ∈
(0[,]π)) |
| 33 | 29, 25 | elicc2i 13453 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0[,]π) ↔ (𝑦 ∈ ℝ ∧ 0 ≤
𝑦 ∧ 𝑦 ≤ π)) |
| 34 | 33 | simp1bi 1146 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]π) → 𝑦 ∈
ℝ) |
| 35 | | resubcl 11573 |
. . . . . . . 8
⊢ (((π /
2) ∈ ℝ ∧ 𝑦
∈ ℝ) → ((π / 2) − 𝑦) ∈ ℝ) |
| 36 | 3, 34, 35 | sylancr 587 |
. . . . . . 7
⊢ (𝑦 ∈ (0[,]π) → ((π
/ 2) − 𝑦) ∈
ℝ) |
| 37 | 33 | simp3bi 1148 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0[,]π) → 𝑦 ≤ π) |
| 38 | 15, 15 | subnegi 11588 |
. . . . . . . . . 10
⊢ ((π /
2) − -(π / 2)) = ((π / 2) + (π / 2)) |
| 39 | 38, 19 | eqtri 2765 |
. . . . . . . . 9
⊢ ((π /
2) − -(π / 2)) = π |
| 40 | 37, 39 | breqtrrdi 5185 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]π) → 𝑦 ≤ ((π / 2) − -(π
/ 2))) |
| 41 | | lesub 11742 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ ∧ (π / 2)
∈ ℝ ∧ -(π / 2) ∈ ℝ) → (𝑦 ≤ ((π / 2) − -(π / 2)) ↔
-(π / 2) ≤ ((π / 2) − 𝑦))) |
| 42 | 3, 4, 41 | mp3an23 1455 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → (𝑦 ≤ ((π / 2) − -(π
/ 2)) ↔ -(π / 2) ≤ ((π / 2) − 𝑦))) |
| 43 | 34, 42 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]π) → (𝑦 ≤ ((π / 2) − -(π
/ 2)) ↔ -(π / 2) ≤ ((π / 2) − 𝑦))) |
| 44 | 40, 43 | mpbid 232 |
. . . . . . 7
⊢ (𝑦 ∈ (0[,]π) → -(π
/ 2) ≤ ((π / 2) − 𝑦)) |
| 45 | 15 | subidi 11580 |
. . . . . . . . 9
⊢ ((π /
2) − (π / 2)) = 0 |
| 46 | 33 | simp2bi 1147 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0[,]π) → 0 ≤
𝑦) |
| 47 | 45, 46 | eqbrtrid 5178 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]π) → ((π
/ 2) − (π / 2)) ≤ 𝑦) |
| 48 | | suble 11741 |
. . . . . . . . 9
⊢ (((π /
2) ∈ ℝ ∧ (π / 2) ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((π / 2) −
(π / 2)) ≤ 𝑦 ↔
((π / 2) − 𝑦) ≤
(π / 2))) |
| 49 | 3, 3, 34, 48 | mp3an12i 1467 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]π) →
(((π / 2) − (π / 2)) ≤ 𝑦 ↔ ((π / 2) − 𝑦) ≤ (π /
2))) |
| 50 | 47, 49 | mpbid 232 |
. . . . . . 7
⊢ (𝑦 ∈ (0[,]π) → ((π
/ 2) − 𝑦) ≤ (π
/ 2)) |
| 51 | 4, 3 | elicc2i 13453 |
. . . . . . 7
⊢ (((π /
2) − 𝑦) ∈
(-(π / 2)[,](π / 2)) ↔ (((π / 2) − 𝑦) ∈ ℝ ∧ -(π / 2) ≤
((π / 2) − 𝑦)
∧ ((π / 2) − 𝑦) ≤ (π / 2))) |
| 52 | 36, 44, 50, 51 | syl3anbrc 1344 |
. . . . . 6
⊢ (𝑦 ∈ (0[,]π) → ((π
/ 2) − 𝑦) ∈
(-(π / 2)[,](π / 2))) |
| 53 | 52 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑦
∈ (0[,]π)) → ((π / 2) − 𝑦) ∈ (-(π / 2)[,](π /
2))) |
| 54 | | iccssre 13469 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ π ∈ ℝ) → (0[,]π) ⊆
ℝ) |
| 55 | 29, 25, 54 | mp2an 692 |
. . . . . . . . . 10
⊢
(0[,]π) ⊆ ℝ |
| 56 | | ax-resscn 11212 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
| 57 | 55, 56 | sstri 3993 |
. . . . . . . . 9
⊢
(0[,]π) ⊆ ℂ |
| 58 | 57 | sseli 3979 |
. . . . . . . 8
⊢ (𝑦 ∈ (0[,]π) → 𝑦 ∈
ℂ) |
| 59 | 6, 56 | sstri 3993 |
. . . . . . . . 9
⊢ (-(π /
2)[,](π / 2)) ⊆ ℂ |
| 60 | 59 | sseli 3979 |
. . . . . . . 8
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) → 𝑥 ∈
ℂ) |
| 61 | | subsub23 11513 |
. . . . . . . . 9
⊢ (((π /
2) ∈ ℂ ∧ 𝑦
∈ ℂ ∧ 𝑥
∈ ℂ) → (((π / 2) − 𝑦) = 𝑥 ↔ ((π / 2) − 𝑥) = 𝑦)) |
| 62 | 15, 61 | mp3an1 1450 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (((π
/ 2) − 𝑦) = 𝑥 ↔ ((π / 2) −
𝑥) = 𝑦)) |
| 63 | 58, 60, 62 | syl2anr 597 |
. . . . . . 7
⊢ ((𝑥 ∈ (-(π / 2)[,](π /
2)) ∧ 𝑦 ∈
(0[,]π)) → (((π / 2) − 𝑦) = 𝑥 ↔ ((π / 2) − 𝑥) = 𝑦)) |
| 64 | 63 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ (𝑥
∈ (-(π / 2)[,](π / 2)) ∧ 𝑦 ∈ (0[,]π))) → (((π / 2)
− 𝑦) = 𝑥 ↔ ((π / 2) −
𝑥) = 𝑦)) |
| 65 | | eqcom 2744 |
. . . . . 6
⊢ (𝑥 = ((π / 2) − 𝑦) ↔ ((π / 2) −
𝑦) = 𝑥) |
| 66 | | eqcom 2744 |
. . . . . 6
⊢ (𝑦 = ((π / 2) − 𝑥) ↔ ((π / 2) −
𝑥) = 𝑦) |
| 67 | 64, 65, 66 | 3bitr4g 314 |
. . . . 5
⊢
((⊤ ∧ (𝑥
∈ (-(π / 2)[,](π / 2)) ∧ 𝑦 ∈ (0[,]π))) → (𝑥 = ((π / 2) − 𝑦) ↔ 𝑦 = ((π / 2) − 𝑥))) |
| 68 | 2, 32, 53, 67 | f1o2d 7687 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ (-(π /
2)[,](π / 2)) ↦ ((π / 2) − 𝑥)):(-(π / 2)[,](π / 2))–1-1-onto→(0[,]π)) |
| 69 | 68 | mptru 1547 |
. . 3
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥)):(-(π / 2)[,](π / 2))–1-1-onto→(0[,]π) |
| 70 | | f1oco 6871 |
. . 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)) |
| 71 | 1, 69, 70 | mp2an 692 |
. 2
⊢ ((cos
↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) |
| 72 | | cosf 16161 |
. . . . . . . 8
⊢
cos:ℂ⟶ℂ |
| 73 | | ffn 6736 |
. . . . . . . 8
⊢
(cos:ℂ⟶ℂ → cos Fn ℂ) |
| 74 | 72, 73 | ax-mp 5 |
. . . . . . 7
⊢ cos Fn
ℂ |
| 75 | | fnssres 6691 |
. . . . . . 7
⊢ ((cos Fn
ℂ ∧ (0[,]π) ⊆ ℂ) → (cos ↾ (0[,]π)) Fn
(0[,]π)) |
| 76 | 74, 57, 75 | mp2an 692 |
. . . . . 6
⊢ (cos
↾ (0[,]π)) Fn (0[,]π) |
| 77 | 2, 31 | fmpti 7132 |
. . . . . 6
⊢ (𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥)):(-(π / 2)[,](π /
2))⟶(0[,]π) |
| 78 | | fnfco 6773 |
. . . . . 6
⊢ (((cos
↾ (0[,]π)) Fn (0[,]π) ∧ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥)):(-(π / 2)[,](π /
2))⟶(0[,]π)) → ((cos ↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥))) Fn (-(π / 2)[,](π /
2))) |
| 79 | 76, 77, 78 | mp2an 692 |
. . . . 5
⊢ ((cos
↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))) Fn
(-(π / 2)[,](π / 2)) |
| 80 | | sinf 16160 |
. . . . . . 7
⊢
sin:ℂ⟶ℂ |
| 81 | | ffn 6736 |
. . . . . . 7
⊢
(sin:ℂ⟶ℂ → sin Fn ℂ) |
| 82 | 80, 81 | ax-mp 5 |
. . . . . 6
⊢ sin Fn
ℂ |
| 83 | | fnssres 6691 |
. . . . . 6
⊢ ((sin Fn
ℂ ∧ (-(π / 2)[,](π / 2)) ⊆ ℂ) → (sin ↾
(-(π / 2)[,](π / 2))) Fn (-(π / 2)[,](π / 2))) |
| 84 | 82, 59, 83 | mp2an 692 |
. . . . 5
⊢ (sin
↾ (-(π / 2)[,](π / 2))) Fn (-(π / 2)[,](π /
2)) |
| 85 | | eqfnfv 7051 |
. . . . 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)))‘𝑦))) |
| 86 | 79, 84, 85 | mp2an 692 |
. . . 4
⊢ (((cos
↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))) =
(sin ↾ (-(π / 2)[,](π / 2))) ↔ ∀𝑦 ∈ (-(π / 2)[,](π / 2))(((cos
↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥)))‘𝑦) = ((sin ↾ (-(π / 2)[,](π /
2)))‘𝑦)) |
| 87 | 77 | ffvelcdmi 7103 |
. . . . . . 7
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → ((𝑥 ∈
(-(π / 2)[,](π / 2)) ↦ ((π / 2) − 𝑥))‘𝑦) ∈ (0[,]π)) |
| 88 | 87 | fvresd 6926 |
. . . . . 6
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → ((cos ↾ (0[,]π))‘((𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))‘𝑦)) = (cos‘((𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))‘𝑦))) |
| 89 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((π / 2) − 𝑥) = ((π / 2) − 𝑦)) |
| 90 | | ovex 7464 |
. . . . . . . 8
⊢ ((π /
2) − 𝑦) ∈
V |
| 91 | 89, 2, 90 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → ((𝑥 ∈
(-(π / 2)[,](π / 2)) ↦ ((π / 2) − 𝑥))‘𝑦) = ((π / 2) − 𝑦)) |
| 92 | 91 | fveq2d 6910 |
. . . . . 6
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → (cos‘((𝑥
∈ (-(π / 2)[,](π / 2)) ↦ ((π / 2) − 𝑥))‘𝑦)) = (cos‘((π / 2) − 𝑦))) |
| 93 | 59 | sseli 3979 |
. . . . . . 7
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → 𝑦 ∈
ℂ) |
| 94 | | coshalfpim 26537 |
. . . . . . 7
⊢ (𝑦 ∈ ℂ →
(cos‘((π / 2) − 𝑦)) = (sin‘𝑦)) |
| 95 | 93, 94 | syl 17 |
. . . . . 6
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → (cos‘((π / 2) − 𝑦)) = (sin‘𝑦)) |
| 96 | 88, 92, 95 | 3eqtrd 2781 |
. . . . 5
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → ((cos ↾ (0[,]π))‘((𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))‘𝑦)) = (sin‘𝑦)) |
| 97 | | fvco3 7008 |
. . . . . 6
⊢ (((𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥)):(-(π / 2)[,](π /
2))⟶(0[,]π) ∧ 𝑦 ∈ (-(π / 2)[,](π / 2))) →
(((cos ↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥)))‘𝑦) = ((cos ↾ (0[,]π))‘((𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥))‘𝑦))) |
| 98 | 77, 97 | mpan 690 |
. . . . 5
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → (((cos ↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥)))‘𝑦) = ((cos ↾ (0[,]π))‘((𝑥 ∈ (-(π / 2)[,](π /
2)) ↦ ((π / 2) − 𝑥))‘𝑦))) |
| 99 | | fvres 6925 |
. . . . 5
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → ((sin ↾ (-(π / 2)[,](π / 2)))‘𝑦) = (sin‘𝑦)) |
| 100 | 96, 98, 99 | 3eqtr4d 2787 |
. . . 4
⊢ (𝑦 ∈ (-(π / 2)[,](π /
2)) → (((cos ↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥)))‘𝑦) = ((sin ↾ (-(π / 2)[,](π /
2)))‘𝑦)) |
| 101 | 86, 100 | mprgbir 3068 |
. . 3
⊢ ((cos
↾ (0[,]π)) ∘ (𝑥 ∈ (-(π / 2)[,](π / 2)) ↦
((π / 2) − 𝑥))) =
(sin ↾ (-(π / 2)[,](π / 2))) |
| 102 | | f1oeq1 6836 |
. . 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))) |
| 103 | 101, 102 | 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)) |
| 104 | 71, 103 | mpbi 230 |
1
⊢ (sin
↾ (-(π / 2)[,](π / 2))):(-(π / 2)[,](π / 2))–1-1-onto→(-1[,]1) |