Step | Hyp | Ref
| Expression |
1 | | halfpire 25837 |
. . 3
β’ (Ο /
2) β β |
2 | | pire 25831 |
. . 3
β’ Ο
β β |
3 | | rexr 11208 |
. . . 4
β’ ((Ο /
2) β β β (Ο / 2) β
β*) |
4 | | rexr 11208 |
. . . 4
β’ (Ο
β β β Ο β β*) |
5 | | elioo2 13312 |
. . . 4
β’ (((Ο /
2) β β* β§ Ο β β*) β
(π΄ β ((Ο /
2)(,)Ο) β (π΄ β
β β§ (Ο / 2) < π΄ β§ π΄ < Ο))) |
6 | 3, 4, 5 | syl2an 597 |
. . 3
β’ (((Ο /
2) β β β§ Ο β β) β (π΄ β ((Ο / 2)(,)Ο) β (π΄ β β β§ (Ο / 2)
< π΄ β§ π΄ < Ο))) |
7 | 1, 2, 6 | mp2an 691 |
. 2
β’ (π΄ β ((Ο / 2)(,)Ο)
β (π΄ β β
β§ (Ο / 2) < π΄
β§ π΄ <
Ο)) |
8 | | resubcl 11472 |
. . . . . . . . 9
β’ ((π΄ β β β§ (Ο / 2)
β β) β (π΄
β (Ο / 2)) β β) |
9 | 1, 8 | mpan2 690 |
. . . . . . . 8
β’ (π΄ β β β (π΄ β (Ο / 2)) β
β) |
10 | | 0xr 11209 |
. . . . . . . . . 10
β’ 0 β
β* |
11 | 1 | rexri 11220 |
. . . . . . . . . 10
β’ (Ο /
2) β β* |
12 | | elioo2 13312 |
. . . . . . . . . 10
β’ ((0
β β* β§ (Ο / 2) β β*) β
((π΄ β (Ο / 2))
β (0(,)(Ο / 2)) β ((π΄ β (Ο / 2)) β β β§ 0
< (π΄ β (Ο / 2))
β§ (π΄ β (Ο /
2)) < (Ο / 2)))) |
13 | 10, 11, 12 | mp2an 691 |
. . . . . . . . 9
β’ ((π΄ β (Ο / 2)) β
(0(,)(Ο / 2)) β ((π΄
β (Ο / 2)) β β β§ 0 < (π΄ β (Ο / 2)) β§ (π΄ β (Ο / 2)) < (Ο
/ 2))) |
14 | | sincosq1sgn 25871 |
. . . . . . . . 9
β’ ((π΄ β (Ο / 2)) β
(0(,)(Ο / 2)) β (0 < (sinβ(π΄ β (Ο / 2))) β§ 0 <
(cosβ(π΄ β (Ο
/ 2))))) |
15 | 13, 14 | sylbir 234 |
. . . . . . . 8
β’ (((π΄ β (Ο / 2)) β
β β§ 0 < (π΄
β (Ο / 2)) β§ (π΄ β (Ο / 2)) < (Ο / 2)) β
(0 < (sinβ(π΄
β (Ο / 2))) β§ 0 < (cosβ(π΄ β (Ο / 2))))) |
16 | 9, 15 | syl3an1 1164 |
. . . . . . 7
β’ ((π΄ β β β§ 0 <
(π΄ β (Ο / 2))
β§ (π΄ β (Ο /
2)) < (Ο / 2)) β (0 < (sinβ(π΄ β (Ο / 2))) β§ 0 <
(cosβ(π΄ β (Ο
/ 2))))) |
17 | 16 | 3expib 1123 |
. . . . . 6
β’ (π΄ β β β ((0 <
(π΄ β (Ο / 2))
β§ (π΄ β (Ο /
2)) < (Ο / 2)) β (0 < (sinβ(π΄ β (Ο / 2))) β§ 0 <
(cosβ(π΄ β (Ο
/ 2)))))) |
18 | | 0re 11164 |
. . . . . . . . 9
β’ 0 β
β |
19 | | ltsub13 11643 |
. . . . . . . . 9
β’ ((0
β β β§ π΄
β β β§ (Ο / 2) β β) β (0 < (π΄ β (Ο / 2)) β
(Ο / 2) < (π΄ β
0))) |
20 | 18, 1, 19 | mp3an13 1453 |
. . . . . . . 8
β’ (π΄ β β β (0 <
(π΄ β (Ο / 2))
β (Ο / 2) < (π΄
β 0))) |
21 | | recn 11148 |
. . . . . . . . . 10
β’ (π΄ β β β π΄ β
β) |
22 | 21 | subid1d 11508 |
. . . . . . . . 9
β’ (π΄ β β β (π΄ β 0) = π΄) |
23 | 22 | breq2d 5122 |
. . . . . . . 8
β’ (π΄ β β β ((Ο /
2) < (π΄ β 0)
β (Ο / 2) < π΄)) |
24 | 20, 23 | bitrd 279 |
. . . . . . 7
β’ (π΄ β β β (0 <
(π΄ β (Ο / 2))
β (Ο / 2) < π΄)) |
25 | | ltsubadd 11632 |
. . . . . . . . 9
β’ ((π΄ β β β§ (Ο / 2)
β β β§ (Ο / 2) β β) β ((π΄ β (Ο / 2)) < (Ο / 2) β
π΄ < ((Ο / 2) + (Ο
/ 2)))) |
26 | 1, 1, 25 | mp3an23 1454 |
. . . . . . . 8
β’ (π΄ β β β ((π΄ β (Ο / 2)) < (Ο
/ 2) β π΄ < ((Ο /
2) + (Ο / 2)))) |
27 | | pidiv2halves 25840 |
. . . . . . . . 9
β’ ((Ο /
2) + (Ο / 2)) = Ο |
28 | 27 | breq2i 5118 |
. . . . . . . 8
β’ (π΄ < ((Ο / 2) + (Ο / 2))
β π΄ <
Ο) |
29 | 26, 28 | bitrdi 287 |
. . . . . . 7
β’ (π΄ β β β ((π΄ β (Ο / 2)) < (Ο
/ 2) β π΄ <
Ο)) |
30 | 24, 29 | anbi12d 632 |
. . . . . 6
β’ (π΄ β β β ((0 <
(π΄ β (Ο / 2))
β§ (π΄ β (Ο /
2)) < (Ο / 2)) β ((Ο / 2) < π΄ β§ π΄ < Ο))) |
31 | 9 | resincld 16032 |
. . . . . . . 8
β’ (π΄ β β β
(sinβ(π΄ β (Ο
/ 2))) β β) |
32 | 31 | lt0neg2d 11732 |
. . . . . . 7
β’ (π΄ β β β (0 <
(sinβ(π΄ β (Ο
/ 2))) β -(sinβ(π΄ β (Ο / 2))) <
0)) |
33 | 32 | anbi1d 631 |
. . . . . 6
β’ (π΄ β β β ((0 <
(sinβ(π΄ β (Ο
/ 2))) β§ 0 < (cosβ(π΄ β (Ο / 2)))) β
(-(sinβ(π΄ β
(Ο / 2))) < 0 β§ 0 < (cosβ(π΄ β (Ο / 2)))))) |
34 | 17, 30, 33 | 3imtr3d 293 |
. . . . 5
β’ (π΄ β β β (((Ο /
2) < π΄ β§ π΄ < Ο) β
(-(sinβ(π΄ β
(Ο / 2))) < 0 β§ 0 < (cosβ(π΄ β (Ο / 2)))))) |
35 | 1 | recni 11176 |
. . . . . . . . . 10
β’ (Ο /
2) β β |
36 | | pncan3 11416 |
. . . . . . . . . 10
β’ (((Ο /
2) β β β§ π΄
β β) β ((Ο / 2) + (π΄ β (Ο / 2))) = π΄) |
37 | 35, 21, 36 | sylancr 588 |
. . . . . . . . 9
β’ (π΄ β β β ((Ο /
2) + (π΄ β (Ο /
2))) = π΄) |
38 | 37 | fveq2d 6851 |
. . . . . . . 8
β’ (π΄ β β β
(cosβ((Ο / 2) + (π΄
β (Ο / 2)))) = (cosβπ΄)) |
39 | 9 | recnd 11190 |
. . . . . . . . 9
β’ (π΄ β β β (π΄ β (Ο / 2)) β
β) |
40 | | coshalfpip 25867 |
. . . . . . . . 9
β’ ((π΄ β (Ο / 2)) β
β β (cosβ((Ο / 2) + (π΄ β (Ο / 2)))) = -(sinβ(π΄ β (Ο /
2)))) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
β’ (π΄ β β β
(cosβ((Ο / 2) + (π΄
β (Ο / 2)))) = -(sinβ(π΄ β (Ο / 2)))) |
42 | 38, 41 | eqtr3d 2779 |
. . . . . . 7
β’ (π΄ β β β
(cosβπ΄) =
-(sinβ(π΄ β
(Ο / 2)))) |
43 | 42 | breq1d 5120 |
. . . . . 6
β’ (π΄ β β β
((cosβπ΄) < 0
β -(sinβ(π΄
β (Ο / 2))) < 0)) |
44 | 37 | fveq2d 6851 |
. . . . . . . 8
β’ (π΄ β β β
(sinβ((Ο / 2) + (π΄
β (Ο / 2)))) = (sinβπ΄)) |
45 | | sinhalfpip 25865 |
. . . . . . . . 9
β’ ((π΄ β (Ο / 2)) β
β β (sinβ((Ο / 2) + (π΄ β (Ο / 2)))) = (cosβ(π΄ β (Ο /
2)))) |
46 | 39, 45 | syl 17 |
. . . . . . . 8
β’ (π΄ β β β
(sinβ((Ο / 2) + (π΄
β (Ο / 2)))) = (cosβ(π΄ β (Ο / 2)))) |
47 | 44, 46 | eqtr3d 2779 |
. . . . . . 7
β’ (π΄ β β β
(sinβπ΄) =
(cosβ(π΄ β (Ο
/ 2)))) |
48 | 47 | breq2d 5122 |
. . . . . 6
β’ (π΄ β β β (0 <
(sinβπ΄) β 0 <
(cosβ(π΄ β (Ο
/ 2))))) |
49 | 43, 48 | anbi12d 632 |
. . . . 5
β’ (π΄ β β β
(((cosβπ΄) < 0
β§ 0 < (sinβπ΄))
β (-(sinβ(π΄
β (Ο / 2))) < 0 β§ 0 < (cosβ(π΄ β (Ο / 2)))))) |
50 | 34, 49 | sylibrd 259 |
. . . 4
β’ (π΄ β β β (((Ο /
2) < π΄ β§ π΄ < Ο) β
((cosβπ΄) < 0 β§
0 < (sinβπ΄)))) |
51 | 50 | 3impib 1117 |
. . 3
β’ ((π΄ β β β§ (Ο / 2)
< π΄ β§ π΄ < Ο) β
((cosβπ΄) < 0 β§
0 < (sinβπ΄))) |
52 | 51 | ancomd 463 |
. 2
β’ ((π΄ β β β§ (Ο / 2)
< π΄ β§ π΄ < Ο) β (0 <
(sinβπ΄) β§
(cosβπ΄) <
0)) |
53 | 7, 52 | sylbi 216 |
1
β’ (π΄ β ((Ο / 2)(,)Ο)
β (0 < (sinβπ΄) β§ (cosβπ΄) < 0)) |