Step | Hyp | Ref
| Expression |
1 | | 3re 12240 |
. . . . 5
β’ 3 β
β |
2 | | halfpire 25837 |
. . . . 5
β’ (Ο /
2) β β |
3 | 1, 2 | remulcli 11178 |
. . . 4
β’ (3
Β· (Ο / 2)) β β |
4 | 3 | rexri 11220 |
. . 3
β’ (3
Β· (Ο / 2)) β β* |
5 | | 2re 12234 |
. . . . 5
β’ 2 β
β |
6 | | pire 25831 |
. . . . 5
β’ Ο
β β |
7 | 5, 6 | remulcli 11178 |
. . . 4
β’ (2
Β· Ο) β β |
8 | 7 | rexri 11220 |
. . 3
β’ (2
Β· Ο) β β* |
9 | | elioo2 13312 |
. . 3
β’ (((3
Β· (Ο / 2)) β β* β§ (2 Β· Ο) β
β*) β (π΄ β ((3 Β· (Ο / 2))(,)(2
Β· Ο)) β (π΄
β β β§ (3 Β· (Ο / 2)) < π΄ β§ π΄ < (2 Β· Ο)))) |
10 | 4, 8, 9 | mp2an 691 |
. 2
β’ (π΄ β ((3 Β· (Ο /
2))(,)(2 Β· Ο)) β (π΄ β β β§ (3 Β· (Ο /
2)) < π΄ β§ π΄ < (2 Β·
Ο))) |
11 | | df-3 12224 |
. . . . . . . . . . . 12
β’ 3 = (2 +
1) |
12 | 11 | oveq1i 7372 |
. . . . . . . . . . 11
β’ (3
Β· (Ο / 2)) = ((2 + 1) Β· (Ο / 2)) |
13 | | 2cn 12235 |
. . . . . . . . . . . 12
β’ 2 β
β |
14 | | ax-1cn 11116 |
. . . . . . . . . . . 12
β’ 1 β
β |
15 | 2 | recni 11176 |
. . . . . . . . . . . 12
β’ (Ο /
2) β β |
16 | 13, 14, 15 | adddiri 11175 |
. . . . . . . . . . 11
β’ ((2 + 1)
Β· (Ο / 2)) = ((2 Β· (Ο / 2)) + (1 Β· (Ο /
2))) |
17 | 6 | recni 11176 |
. . . . . . . . . . . . 13
β’ Ο
β β |
18 | | 2ne0 12264 |
. . . . . . . . . . . . 13
β’ 2 β
0 |
19 | 17, 13, 18 | divcan2i 11905 |
. . . . . . . . . . . 12
β’ (2
Β· (Ο / 2)) = Ο |
20 | 15 | mulid2i 11167 |
. . . . . . . . . . . 12
β’ (1
Β· (Ο / 2)) = (Ο / 2) |
21 | 19, 20 | oveq12i 7374 |
. . . . . . . . . . 11
β’ ((2
Β· (Ο / 2)) + (1 Β· (Ο / 2))) = (Ο + (Ο /
2)) |
22 | 12, 16, 21 | 3eqtrri 2770 |
. . . . . . . . . 10
β’ (Ο +
(Ο / 2)) = (3 Β· (Ο / 2)) |
23 | 22 | breq1i 5117 |
. . . . . . . . 9
β’ ((Ο +
(Ο / 2)) < π΄ β
(3 Β· (Ο / 2)) < π΄) |
24 | | ltaddsub 11636 |
. . . . . . . . . 10
β’ ((Ο
β β β§ (Ο / 2) β β β§ π΄ β β) β ((Ο + (Ο / 2))
< π΄ β Ο <
(π΄ β (Ο /
2)))) |
25 | 6, 2, 24 | mp3an12 1452 |
. . . . . . . . 9
β’ (π΄ β β β ((Ο +
(Ο / 2)) < π΄ β
Ο < (π΄ β (Ο
/ 2)))) |
26 | 23, 25 | bitr3id 285 |
. . . . . . . 8
β’ (π΄ β β β ((3
Β· (Ο / 2)) < π΄
β Ο < (π΄ β
(Ο / 2)))) |
27 | | ltsubadd 11632 |
. . . . . . . . . 10
β’ ((π΄ β β β§ (Ο / 2)
β β β§ (3 Β· (Ο / 2)) β β) β ((π΄ β (Ο / 2)) < (3
Β· (Ο / 2)) β π΄ < ((3 Β· (Ο / 2)) + (Ο /
2)))) |
28 | 2, 3, 27 | mp3an23 1454 |
. . . . . . . . 9
β’ (π΄ β β β ((π΄ β (Ο / 2)) < (3
Β· (Ο / 2)) β π΄ < ((3 Β· (Ο / 2)) + (Ο /
2)))) |
29 | | df-4 12225 |
. . . . . . . . . . . . 13
β’ 4 = (3 +
1) |
30 | 29 | oveq1i 7372 |
. . . . . . . . . . . 12
β’ (4
Β· (Ο / 2)) = ((3 + 1) Β· (Ο / 2)) |
31 | 1 | recni 11176 |
. . . . . . . . . . . . 13
β’ 3 β
β |
32 | 31, 14, 15 | adddiri 11175 |
. . . . . . . . . . . 12
β’ ((3 + 1)
Β· (Ο / 2)) = ((3 Β· (Ο / 2)) + (1 Β· (Ο /
2))) |
33 | 20 | oveq2i 7373 |
. . . . . . . . . . . 12
β’ ((3
Β· (Ο / 2)) + (1 Β· (Ο / 2))) = ((3 Β· (Ο / 2)) +
(Ο / 2)) |
34 | 30, 32, 33 | 3eqtrri 2770 |
. . . . . . . . . . 11
β’ ((3
Β· (Ο / 2)) + (Ο / 2)) = (4 Β· (Ο / 2)) |
35 | | 4cn 12245 |
. . . . . . . . . . . . 13
β’ 4 β
β |
36 | | 2cnne0 12370 |
. . . . . . . . . . . . 13
β’ (2 β
β β§ 2 β 0) |
37 | | div12 11842 |
. . . . . . . . . . . . 13
β’ ((4
β β β§ Ο β β β§ (2 β β β§ 2 β
0)) β (4 Β· (Ο / 2)) = (Ο Β· (4 / 2))) |
38 | 35, 17, 36, 37 | mp3an 1462 |
. . . . . . . . . . . 12
β’ (4
Β· (Ο / 2)) = (Ο Β· (4 / 2)) |
39 | | 4d2e2 12330 |
. . . . . . . . . . . . . 14
β’ (4 / 2) =
2 |
40 | 39 | oveq2i 7373 |
. . . . . . . . . . . . 13
β’ (Ο
Β· (4 / 2)) = (Ο Β· 2) |
41 | 17, 13 | mulcomi 11170 |
. . . . . . . . . . . . 13
β’ (Ο
Β· 2) = (2 Β· Ο) |
42 | 40, 41 | eqtri 2765 |
. . . . . . . . . . . 12
β’ (Ο
Β· (4 / 2)) = (2 Β· Ο) |
43 | 38, 42 | eqtri 2765 |
. . . . . . . . . . 11
β’ (4
Β· (Ο / 2)) = (2 Β· Ο) |
44 | 34, 43 | eqtri 2765 |
. . . . . . . . . 10
β’ ((3
Β· (Ο / 2)) + (Ο / 2)) = (2 Β· Ο) |
45 | 44 | breq2i 5118 |
. . . . . . . . 9
β’ (π΄ < ((3 Β· (Ο / 2)) +
(Ο / 2)) β π΄ <
(2 Β· Ο)) |
46 | 28, 45 | bitr2di 288 |
. . . . . . . 8
β’ (π΄ β β β (π΄ < (2 Β· Ο) β
(π΄ β (Ο / 2)) <
(3 Β· (Ο / 2)))) |
47 | 26, 46 | anbi12d 632 |
. . . . . . 7
β’ (π΄ β β β (((3
Β· (Ο / 2)) < π΄
β§ π΄ < (2 Β·
Ο)) β (Ο < (π΄
β (Ο / 2)) β§ (π΄ β (Ο / 2)) < (3 Β· (Ο
/ 2))))) |
48 | | resubcl 11472 |
. . . . . . . . . 10
β’ ((π΄ β β β§ (Ο / 2)
β β) β (π΄
β (Ο / 2)) β β) |
49 | 2, 48 | mpan2 690 |
. . . . . . . . 9
β’ (π΄ β β β (π΄ β (Ο / 2)) β
β) |
50 | 6 | rexri 11220 |
. . . . . . . . . . 11
β’ Ο
β β* |
51 | | elioo2 13312 |
. . . . . . . . . . 11
β’ ((Ο
β β* β§ (3 Β· (Ο / 2)) β
β*) β ((π΄ β (Ο / 2)) β (Ο(,)(3
Β· (Ο / 2))) β ((π΄ β (Ο / 2)) β β β§
Ο < (π΄ β (Ο
/ 2)) β§ (π΄ β
(Ο / 2)) < (3 Β· (Ο / 2))))) |
52 | 50, 4, 51 | mp2an 691 |
. . . . . . . . . 10
β’ ((π΄ β (Ο / 2)) β
(Ο(,)(3 Β· (Ο / 2))) β ((π΄ β (Ο / 2)) β β β§
Ο < (π΄ β (Ο
/ 2)) β§ (π΄ β
(Ο / 2)) < (3 Β· (Ο / 2)))) |
53 | | sincosq3sgn 25873 |
. . . . . . . . . 10
β’ ((π΄ β (Ο / 2)) β
(Ο(,)(3 Β· (Ο / 2))) β ((sinβ(π΄ β (Ο / 2))) < 0 β§
(cosβ(π΄ β (Ο
/ 2))) < 0)) |
54 | 52, 53 | sylbir 234 |
. . . . . . . . 9
β’ (((π΄ β (Ο / 2)) β
β β§ Ο < (π΄
β (Ο / 2)) β§ (π΄ β (Ο / 2)) < (3 Β· (Ο
/ 2))) β ((sinβ(π΄ β (Ο / 2))) < 0 β§
(cosβ(π΄ β (Ο
/ 2))) < 0)) |
55 | 49, 54 | syl3an1 1164 |
. . . . . . . 8
β’ ((π΄ β β β§ Ο <
(π΄ β (Ο / 2))
β§ (π΄ β (Ο /
2)) < (3 Β· (Ο / 2))) β ((sinβ(π΄ β (Ο / 2))) < 0 β§
(cosβ(π΄ β (Ο
/ 2))) < 0)) |
56 | 55 | 3expib 1123 |
. . . . . . 7
β’ (π΄ β β β ((Ο
< (π΄ β (Ο / 2))
β§ (π΄ β (Ο /
2)) < (3 Β· (Ο / 2))) β ((sinβ(π΄ β (Ο / 2))) < 0 β§
(cosβ(π΄ β (Ο
/ 2))) < 0))) |
57 | 47, 56 | sylbid 239 |
. . . . . 6
β’ (π΄ β β β (((3
Β· (Ο / 2)) < π΄
β§ π΄ < (2 Β·
Ο)) β ((sinβ(π΄ β (Ο / 2))) < 0 β§
(cosβ(π΄ β (Ο
/ 2))) < 0))) |
58 | 49 | resincld 16032 |
. . . . . . . 8
β’ (π΄ β β β
(sinβ(π΄ β (Ο
/ 2))) β β) |
59 | 58 | lt0neg1d 11731 |
. . . . . . 7
β’ (π΄ β β β
((sinβ(π΄ β
(Ο / 2))) < 0 β 0 < -(sinβ(π΄ β (Ο / 2))))) |
60 | 59 | anbi1d 631 |
. . . . . 6
β’ (π΄ β β β
(((sinβ(π΄ β
(Ο / 2))) < 0 β§ (cosβ(π΄ β (Ο / 2))) < 0) β (0 <
-(sinβ(π΄ β
(Ο / 2))) β§ (cosβ(π΄ β (Ο / 2))) <
0))) |
61 | 57, 60 | sylibd 238 |
. . . . 5
β’ (π΄ β β β (((3
Β· (Ο / 2)) < π΄
β§ π΄ < (2 Β·
Ο)) β (0 < -(sinβ(π΄ β (Ο / 2))) β§
(cosβ(π΄ β (Ο
/ 2))) < 0))) |
62 | | recn 11148 |
. . . . . . . . . 10
β’ (π΄ β β β π΄ β
β) |
63 | | pncan3 11416 |
. . . . . . . . . 10
β’ (((Ο /
2) β β β§ π΄
β β) β ((Ο / 2) + (π΄ β (Ο / 2))) = π΄) |
64 | 15, 62, 63 | sylancr 588 |
. . . . . . . . 9
β’ (π΄ β β β ((Ο /
2) + (π΄ β (Ο /
2))) = π΄) |
65 | 64 | fveq2d 6851 |
. . . . . . . 8
β’ (π΄ β β β
(cosβ((Ο / 2) + (π΄
β (Ο / 2)))) = (cosβπ΄)) |
66 | 49 | recnd 11190 |
. . . . . . . . 9
β’ (π΄ β β β (π΄ β (Ο / 2)) β
β) |
67 | | coshalfpip 25867 |
. . . . . . . . 9
β’ ((π΄ β (Ο / 2)) β
β β (cosβ((Ο / 2) + (π΄ β (Ο / 2)))) = -(sinβ(π΄ β (Ο /
2)))) |
68 | 66, 67 | syl 17 |
. . . . . . . 8
β’ (π΄ β β β
(cosβ((Ο / 2) + (π΄
β (Ο / 2)))) = -(sinβ(π΄ β (Ο / 2)))) |
69 | 65, 68 | eqtr3d 2779 |
. . . . . . 7
β’ (π΄ β β β
(cosβπ΄) =
-(sinβ(π΄ β
(Ο / 2)))) |
70 | 69 | breq2d 5122 |
. . . . . 6
β’ (π΄ β β β (0 <
(cosβπ΄) β 0 <
-(sinβ(π΄ β
(Ο / 2))))) |
71 | 64 | fveq2d 6851 |
. . . . . . . 8
β’ (π΄ β β β
(sinβ((Ο / 2) + (π΄
β (Ο / 2)))) = (sinβπ΄)) |
72 | | sinhalfpip 25865 |
. . . . . . . . 9
β’ ((π΄ β (Ο / 2)) β
β β (sinβ((Ο / 2) + (π΄ β (Ο / 2)))) = (cosβ(π΄ β (Ο /
2)))) |
73 | 66, 72 | syl 17 |
. . . . . . . 8
β’ (π΄ β β β
(sinβ((Ο / 2) + (π΄
β (Ο / 2)))) = (cosβ(π΄ β (Ο / 2)))) |
74 | 71, 73 | eqtr3d 2779 |
. . . . . . 7
β’ (π΄ β β β
(sinβπ΄) =
(cosβ(π΄ β (Ο
/ 2)))) |
75 | 74 | breq1d 5120 |
. . . . . 6
β’ (π΄ β β β
((sinβπ΄) < 0
β (cosβ(π΄
β (Ο / 2))) < 0)) |
76 | 70, 75 | anbi12d 632 |
. . . . 5
β’ (π΄ β β β ((0 <
(cosβπ΄) β§
(sinβπ΄) < 0)
β (0 < -(sinβ(π΄ β (Ο / 2))) β§
(cosβ(π΄ β (Ο
/ 2))) < 0))) |
77 | 61, 76 | sylibrd 259 |
. . . 4
β’ (π΄ β β β (((3
Β· (Ο / 2)) < π΄
β§ π΄ < (2 Β·
Ο)) β (0 < (cosβπ΄) β§ (sinβπ΄) < 0))) |
78 | 77 | 3impib 1117 |
. . 3
β’ ((π΄ β β β§ (3
Β· (Ο / 2)) < π΄
β§ π΄ < (2 Β·
Ο)) β (0 < (cosβπ΄) β§ (sinβπ΄) < 0)) |
79 | 78 | ancomd 463 |
. 2
β’ ((π΄ β β β§ (3
Β· (Ο / 2)) < π΄
β§ π΄ < (2 Β·
Ο)) β ((sinβπ΄) < 0 β§ 0 < (cosβπ΄))) |
80 | 10, 79 | sylbi 216 |
1
β’ (π΄ β ((3 Β· (Ο /
2))(,)(2 Β· Ο)) β ((sinβπ΄) < 0 β§ 0 < (cosβπ΄))) |