Step | Hyp | Ref
| Expression |
1 | | pire 25831 |
. . 3
β’ Ο
β β |
2 | | 3re 12240 |
. . . 4
β’ 3 β
β |
3 | | halfpire 25837 |
. . . 4
β’ (Ο /
2) β β |
4 | 2, 3 | remulcli 11178 |
. . 3
β’ (3
Β· (Ο / 2)) β β |
5 | | rexr 11208 |
. . . 4
β’ (Ο
β β β Ο β β*) |
6 | | rexr 11208 |
. . . 4
β’ ((3
Β· (Ο / 2)) β β β (3 Β· (Ο / 2)) β
β*) |
7 | | elioo2 13312 |
. . . 4
β’ ((Ο
β β* β§ (3 Β· (Ο / 2)) β
β*) β (π΄ β (Ο(,)(3 Β· (Ο / 2)))
β (π΄ β β
β§ Ο < π΄ β§
π΄ < (3 Β· (Ο /
2))))) |
8 | 5, 6, 7 | syl2an 597 |
. . 3
β’ ((Ο
β β β§ (3 Β· (Ο / 2)) β β) β (π΄ β (Ο(,)(3 Β·
(Ο / 2))) β (π΄
β β β§ Ο < π΄ β§ π΄ < (3 Β· (Ο /
2))))) |
9 | 1, 4, 8 | mp2an 691 |
. 2
β’ (π΄ β (Ο(,)(3 Β·
(Ο / 2))) β (π΄
β β β§ Ο < π΄ β§ π΄ < (3 Β· (Ο /
2)))) |
10 | | pidiv2halves 25840 |
. . . . . . . . 9
β’ ((Ο /
2) + (Ο / 2)) = Ο |
11 | 10 | breq1i 5117 |
. . . . . . . 8
β’ (((Ο /
2) + (Ο / 2)) < π΄
β Ο < π΄) |
12 | | ltaddsub 11636 |
. . . . . . . . 9
β’ (((Ο /
2) β β β§ (Ο / 2) β β β§ π΄ β β) β (((Ο / 2) + (Ο
/ 2)) < π΄ β (Ο /
2) < (π΄ β (Ο /
2)))) |
13 | 3, 3, 12 | mp3an12 1452 |
. . . . . . . 8
β’ (π΄ β β β (((Ο /
2) + (Ο / 2)) < π΄
β (Ο / 2) < (π΄
β (Ο / 2)))) |
14 | 11, 13 | bitr3id 285 |
. . . . . . 7
β’ (π΄ β β β (Ο
< π΄ β (Ο / 2)
< (π΄ β (Ο /
2)))) |
15 | | ltsubadd 11632 |
. . . . . . . . 9
β’ ((π΄ β β β§ (Ο / 2)
β β β§ Ο β β) β ((π΄ β (Ο / 2)) < Ο β π΄ < (Ο + (Ο /
2)))) |
16 | 3, 1, 15 | mp3an23 1454 |
. . . . . . . 8
β’ (π΄ β β β ((π΄ β (Ο / 2)) < Ο
β π΄ < (Ο + (Ο
/ 2)))) |
17 | | df-3 12224 |
. . . . . . . . . . 11
β’ 3 = (2 +
1) |
18 | 17 | oveq1i 7372 |
. . . . . . . . . 10
β’ (3
Β· (Ο / 2)) = ((2 + 1) Β· (Ο / 2)) |
19 | | 2cn 12235 |
. . . . . . . . . . 11
β’ 2 β
β |
20 | | ax-1cn 11116 |
. . . . . . . . . . 11
β’ 1 β
β |
21 | 3 | recni 11176 |
. . . . . . . . . . 11
β’ (Ο /
2) β β |
22 | 19, 20, 21 | adddiri 11175 |
. . . . . . . . . 10
β’ ((2 + 1)
Β· (Ο / 2)) = ((2 Β· (Ο / 2)) + (1 Β· (Ο /
2))) |
23 | 1 | recni 11176 |
. . . . . . . . . . . 12
β’ Ο
β β |
24 | | 2ne0 12264 |
. . . . . . . . . . . 12
β’ 2 β
0 |
25 | 23, 19, 24 | divcan2i 11905 |
. . . . . . . . . . 11
β’ (2
Β· (Ο / 2)) = Ο |
26 | 21 | mulid2i 11167 |
. . . . . . . . . . 11
β’ (1
Β· (Ο / 2)) = (Ο / 2) |
27 | 25, 26 | oveq12i 7374 |
. . . . . . . . . 10
β’ ((2
Β· (Ο / 2)) + (1 Β· (Ο / 2))) = (Ο + (Ο /
2)) |
28 | 18, 22, 27 | 3eqtrri 2770 |
. . . . . . . . 9
β’ (Ο +
(Ο / 2)) = (3 Β· (Ο / 2)) |
29 | 28 | breq2i 5118 |
. . . . . . . 8
β’ (π΄ < (Ο + (Ο / 2)) β
π΄ < (3 Β· (Ο /
2))) |
30 | 16, 29 | bitr2di 288 |
. . . . . . 7
β’ (π΄ β β β (π΄ < (3 Β· (Ο / 2))
β (π΄ β (Ο /
2)) < Ο)) |
31 | 14, 30 | anbi12d 632 |
. . . . . 6
β’ (π΄ β β β ((Ο
< π΄ β§ π΄ < (3 Β· (Ο / 2)))
β ((Ο / 2) < (π΄
β (Ο / 2)) β§ (π΄ β (Ο / 2)) <
Ο))) |
32 | | resubcl 11472 |
. . . . . . . . 9
β’ ((π΄ β β β§ (Ο / 2)
β β) β (π΄
β (Ο / 2)) β β) |
33 | 3, 32 | mpan2 690 |
. . . . . . . 8
β’ (π΄ β β β (π΄ β (Ο / 2)) β
β) |
34 | | sincosq2sgn 25872 |
. . . . . . . . 9
β’ ((π΄ β (Ο / 2)) β
((Ο / 2)(,)Ο) β (0 < (sinβ(π΄ β (Ο / 2))) β§
(cosβ(π΄ β (Ο
/ 2))) < 0)) |
35 | | rexr 11208 |
. . . . . . . . . . 11
β’ ((Ο /
2) β β β (Ο / 2) β
β*) |
36 | | elioo2 13312 |
. . . . . . . . . . 11
β’ (((Ο /
2) β β* β§ Ο β β*) β
((π΄ β (Ο / 2))
β ((Ο / 2)(,)Ο) β ((π΄ β (Ο / 2)) β β β§
(Ο / 2) < (π΄ β
(Ο / 2)) β§ (π΄
β (Ο / 2)) < Ο))) |
37 | 35, 5, 36 | syl2an 597 |
. . . . . . . . . 10
β’ (((Ο /
2) β β β§ Ο β β) β ((π΄ β (Ο / 2)) β ((Ο /
2)(,)Ο) β ((π΄
β (Ο / 2)) β β β§ (Ο / 2) < (π΄ β (Ο / 2)) β§ (π΄ β (Ο / 2)) <
Ο))) |
38 | 3, 1, 37 | mp2an 691 |
. . . . . . . . 9
β’ ((π΄ β (Ο / 2)) β
((Ο / 2)(,)Ο) β ((π΄ β (Ο / 2)) β β β§
(Ο / 2) < (π΄ β
(Ο / 2)) β§ (π΄
β (Ο / 2)) < Ο)) |
39 | | ancom 462 |
. . . . . . . . 9
β’ ((0 <
(sinβ(π΄ β (Ο
/ 2))) β§ (cosβ(π΄
β (Ο / 2))) < 0) β ((cosβ(π΄ β (Ο / 2))) < 0 β§ 0 <
(sinβ(π΄ β (Ο
/ 2))))) |
40 | 34, 38, 39 | 3imtr3i 291 |
. . . . . . . 8
β’ (((π΄ β (Ο / 2)) β
β β§ (Ο / 2) < (π΄ β (Ο / 2)) β§ (π΄ β (Ο / 2)) < Ο)
β ((cosβ(π΄
β (Ο / 2))) < 0 β§ 0 < (sinβ(π΄ β (Ο / 2))))) |
41 | 33, 40 | syl3an1 1164 |
. . . . . . 7
β’ ((π΄ β β β§ (Ο / 2)
< (π΄ β (Ο / 2))
β§ (π΄ β (Ο /
2)) < Ο) β ((cosβ(π΄ β (Ο / 2))) < 0 β§ 0 <
(sinβ(π΄ β (Ο
/ 2))))) |
42 | 41 | 3expib 1123 |
. . . . . 6
β’ (π΄ β β β (((Ο /
2) < (π΄ β (Ο /
2)) β§ (π΄ β (Ο
/ 2)) < Ο) β ((cosβ(π΄ β (Ο / 2))) < 0 β§ 0 <
(sinβ(π΄ β (Ο
/ 2)))))) |
43 | 31, 42 | sylbid 239 |
. . . . 5
β’ (π΄ β β β ((Ο
< π΄ β§ π΄ < (3 Β· (Ο / 2)))
β ((cosβ(π΄
β (Ο / 2))) < 0 β§ 0 < (sinβ(π΄ β (Ο / 2)))))) |
44 | 33 | resincld 16032 |
. . . . . . 7
β’ (π΄ β β β
(sinβ(π΄ β (Ο
/ 2))) β β) |
45 | 44 | lt0neg2d 11732 |
. . . . . 6
β’ (π΄ β β β (0 <
(sinβ(π΄ β (Ο
/ 2))) β -(sinβ(π΄ β (Ο / 2))) <
0)) |
46 | 45 | anbi2d 630 |
. . . . 5
β’ (π΄ β β β
(((cosβ(π΄ β
(Ο / 2))) < 0 β§ 0 < (sinβ(π΄ β (Ο / 2)))) β
((cosβ(π΄ β
(Ο / 2))) < 0 β§ -(sinβ(π΄ β (Ο / 2))) <
0))) |
47 | 43, 46 | sylibd 238 |
. . . 4
β’ (π΄ β β β ((Ο
< π΄ β§ π΄ < (3 Β· (Ο / 2)))
β ((cosβ(π΄
β (Ο / 2))) < 0 β§ -(sinβ(π΄ β (Ο / 2))) <
0))) |
48 | | recn 11148 |
. . . . . . . . 9
β’ (π΄ β β β π΄ β
β) |
49 | | pncan3 11416 |
. . . . . . . . 9
β’ (((Ο /
2) β β β§ π΄
β β) β ((Ο / 2) + (π΄ β (Ο / 2))) = π΄) |
50 | 21, 48, 49 | sylancr 588 |
. . . . . . . 8
β’ (π΄ β β β ((Ο /
2) + (π΄ β (Ο /
2))) = π΄) |
51 | 50 | fveq2d 6851 |
. . . . . . 7
β’ (π΄ β β β
(sinβ((Ο / 2) + (π΄
β (Ο / 2)))) = (sinβπ΄)) |
52 | 33 | recnd 11190 |
. . . . . . . 8
β’ (π΄ β β β (π΄ β (Ο / 2)) β
β) |
53 | | sinhalfpip 25865 |
. . . . . . . 8
β’ ((π΄ β (Ο / 2)) β
β β (sinβ((Ο / 2) + (π΄ β (Ο / 2)))) = (cosβ(π΄ β (Ο /
2)))) |
54 | 52, 53 | syl 17 |
. . . . . . 7
β’ (π΄ β β β
(sinβ((Ο / 2) + (π΄
β (Ο / 2)))) = (cosβ(π΄ β (Ο / 2)))) |
55 | 51, 54 | eqtr3d 2779 |
. . . . . 6
β’ (π΄ β β β
(sinβπ΄) =
(cosβ(π΄ β (Ο
/ 2)))) |
56 | 55 | breq1d 5120 |
. . . . 5
β’ (π΄ β β β
((sinβπ΄) < 0
β (cosβ(π΄
β (Ο / 2))) < 0)) |
57 | 50 | fveq2d 6851 |
. . . . . . 7
β’ (π΄ β β β
(cosβ((Ο / 2) + (π΄
β (Ο / 2)))) = (cosβπ΄)) |
58 | | coshalfpip 25867 |
. . . . . . . 8
β’ ((π΄ β (Ο / 2)) β
β β (cosβ((Ο / 2) + (π΄ β (Ο / 2)))) = -(sinβ(π΄ β (Ο /
2)))) |
59 | 52, 58 | syl 17 |
. . . . . . 7
β’ (π΄ β β β
(cosβ((Ο / 2) + (π΄
β (Ο / 2)))) = -(sinβ(π΄ β (Ο / 2)))) |
60 | 57, 59 | eqtr3d 2779 |
. . . . . 6
β’ (π΄ β β β
(cosβπ΄) =
-(sinβ(π΄ β
(Ο / 2)))) |
61 | 60 | breq1d 5120 |
. . . . 5
β’ (π΄ β β β
((cosβπ΄) < 0
β -(sinβ(π΄
β (Ο / 2))) < 0)) |
62 | 56, 61 | anbi12d 632 |
. . . 4
β’ (π΄ β β β
(((sinβπ΄) < 0
β§ (cosβπ΄) < 0)
β ((cosβ(π΄
β (Ο / 2))) < 0 β§ -(sinβ(π΄ β (Ο / 2))) <
0))) |
63 | 47, 62 | sylibrd 259 |
. . 3
β’ (π΄ β β β ((Ο
< π΄ β§ π΄ < (3 Β· (Ο / 2)))
β ((sinβπ΄) <
0 β§ (cosβπ΄) <
0))) |
64 | 63 | 3impib 1117 |
. 2
β’ ((π΄ β β β§ Ο <
π΄ β§ π΄ < (3 Β· (Ο / 2))) β
((sinβπ΄) < 0 β§
(cosβπ΄) <
0)) |
65 | 9, 64 | sylbi 216 |
1
β’ (π΄ β (Ο(,)(3 Β·
(Ο / 2))) β ((sinβπ΄) < 0 β§ (cosβπ΄) < 0)) |