Step | Hyp | Ref
| Expression |
1 | | 0xr 11226 |
. . 3
β’ 0 β
β* |
2 | | pire 25867 |
. . . 4
β’ Ο
β β |
3 | 2 | rexri 11237 |
. . 3
β’ Ο
β β* |
4 | | elioo2 13330 |
. . 3
β’ ((0
β β* β§ Ο β β*) β (π΄ β (0(,)Ο) β (π΄ β β β§ 0 <
π΄ β§ π΄ < Ο))) |
5 | 1, 3, 4 | mp2an 690 |
. 2
β’ (π΄ β (0(,)Ο) β (π΄ β β β§ 0 <
π΄ β§ π΄ < Ο)) |
6 | | rehalfcl 12403 |
. . . . . 6
β’ (π΄ β β β (π΄ / 2) β
β) |
7 | 6 | 3ad2ant1 1133 |
. . . . 5
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β (π΄ / 2) β β) |
8 | | halfpos2 12406 |
. . . . . . 7
β’ (π΄ β β β (0 <
π΄ β 0 < (π΄ / 2))) |
9 | 8 | biimpa 477 |
. . . . . 6
β’ ((π΄ β β β§ 0 <
π΄) β 0 < (π΄ / 2)) |
10 | 9 | 3adant3 1132 |
. . . . 5
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β 0 < (π΄ / 2)) |
11 | | 2re 12251 |
. . . . . . . . 9
β’ 2 β
β |
12 | | 2pos 12280 |
. . . . . . . . 9
β’ 0 <
2 |
13 | 11, 12 | pm3.2i 471 |
. . . . . . . 8
β’ (2 β
β β§ 0 < 2) |
14 | | ltdiv1 12043 |
. . . . . . . 8
β’ ((π΄ β β β§ Ο
β β β§ (2 β β β§ 0 < 2)) β (π΄ < Ο β (π΄ / 2) < (Ο /
2))) |
15 | 2, 13, 14 | mp3an23 1453 |
. . . . . . 7
β’ (π΄ β β β (π΄ < Ο β (π΄ / 2) < (Ο /
2))) |
16 | 15 | adantr 481 |
. . . . . 6
β’ ((π΄ β β β§ 0 <
π΄) β (π΄ < Ο β (π΄ / 2) < (Ο /
2))) |
17 | 16 | biimp3a 1469 |
. . . . 5
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β (π΄ / 2) < (Ο / 2)) |
18 | | sincosq1lem 25906 |
. . . . 5
β’ (((π΄ / 2) β β β§ 0
< (π΄ / 2) β§ (π΄ / 2) < (Ο / 2)) β 0
< (sinβ(π΄ /
2))) |
19 | 7, 10, 17, 18 | syl3anc 1371 |
. . . 4
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β 0 < (sinβ(π΄ / 2))) |
20 | | resubcl 11489 |
. . . . . . . . 9
β’ ((Ο
β β β§ π΄
β β) β (Ο β π΄) β β) |
21 | 2, 20 | mpan 688 |
. . . . . . . 8
β’ (π΄ β β β (Ο
β π΄) β
β) |
22 | | rehalfcl 12403 |
. . . . . . . 8
β’ ((Ο
β π΄) β β
β ((Ο β π΄) /
2) β β) |
23 | 21, 22 | syl 17 |
. . . . . . 7
β’ (π΄ β β β ((Ο
β π΄) / 2) β
β) |
24 | 23 | 3ad2ant1 1133 |
. . . . . 6
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β ((Ο β π΄) / 2) β
β) |
25 | | posdif 11672 |
. . . . . . . . . 10
β’ ((π΄ β β β§ Ο
β β) β (π΄
< Ο β 0 < (Ο β π΄))) |
26 | 2, 25 | mpan2 689 |
. . . . . . . . 9
β’ (π΄ β β β (π΄ < Ο β 0 < (Ο
β π΄))) |
27 | | halfpos2 12406 |
. . . . . . . . . 10
β’ ((Ο
β π΄) β β
β (0 < (Ο β π΄) β 0 < ((Ο β π΄) / 2))) |
28 | 21, 27 | syl 17 |
. . . . . . . . 9
β’ (π΄ β β β (0 <
(Ο β π΄) β 0
< ((Ο β π΄) /
2))) |
29 | 26, 28 | bitrd 278 |
. . . . . . . 8
β’ (π΄ β β β (π΄ < Ο β 0 < ((Ο
β π΄) /
2))) |
30 | 29 | adantr 481 |
. . . . . . 7
β’ ((π΄ β β β§ 0 <
π΄) β (π΄ < Ο β 0 < ((Ο
β π΄) /
2))) |
31 | 30 | biimp3a 1469 |
. . . . . 6
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β 0 < ((Ο β
π΄) / 2)) |
32 | | ltsubpos 11671 |
. . . . . . . . . 10
β’ ((π΄ β β β§ Ο
β β) β (0 < π΄ β (Ο β π΄) < Ο)) |
33 | 2, 32 | mpan2 689 |
. . . . . . . . 9
β’ (π΄ β β β (0 <
π΄ β (Ο β
π΄) <
Ο)) |
34 | | ltdiv1 12043 |
. . . . . . . . . . 11
β’ (((Ο
β π΄) β β
β§ Ο β β β§ (2 β β β§ 0 < 2)) β
((Ο β π΄) < Ο
β ((Ο β π΄) /
2) < (Ο / 2))) |
35 | 2, 13, 34 | mp3an23 1453 |
. . . . . . . . . 10
β’ ((Ο
β π΄) β β
β ((Ο β π΄)
< Ο β ((Ο β π΄) / 2) < (Ο / 2))) |
36 | 21, 35 | syl 17 |
. . . . . . . . 9
β’ (π΄ β β β ((Ο
β π΄) < Ο β
((Ο β π΄) / 2) <
(Ο / 2))) |
37 | 33, 36 | bitrd 278 |
. . . . . . . 8
β’ (π΄ β β β (0 <
π΄ β ((Ο β
π΄) / 2) < (Ο /
2))) |
38 | 37 | biimpa 477 |
. . . . . . 7
β’ ((π΄ β β β§ 0 <
π΄) β ((Ο β
π΄) / 2) < (Ο /
2)) |
39 | 38 | 3adant3 1132 |
. . . . . 6
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β ((Ο β π΄) / 2) < (Ο /
2)) |
40 | | sincosq1lem 25906 |
. . . . . 6
β’ ((((Ο
β π΄) / 2) β
β β§ 0 < ((Ο β π΄) / 2) β§ ((Ο β π΄) / 2) < (Ο / 2)) β 0
< (sinβ((Ο β π΄) / 2))) |
41 | 24, 31, 39, 40 | syl3anc 1371 |
. . . . 5
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β 0 < (sinβ((Ο
β π΄) /
2))) |
42 | | recn 11165 |
. . . . . . . . 9
β’ (π΄ β β β π΄ β
β) |
43 | | picn 25868 |
. . . . . . . . . 10
β’ Ο
β β |
44 | | 2cnne0 12387 |
. . . . . . . . . 10
β’ (2 β
β β§ 2 β 0) |
45 | | divsubdir 11873 |
. . . . . . . . . 10
β’ ((Ο
β β β§ π΄
β β β§ (2 β β β§ 2 β 0)) β ((Ο β
π΄) / 2) = ((Ο / 2)
β (π΄ /
2))) |
46 | 43, 44, 45 | mp3an13 1452 |
. . . . . . . . 9
β’ (π΄ β β β ((Ο
β π΄) / 2) = ((Ο /
2) β (π΄ /
2))) |
47 | 42, 46 | syl 17 |
. . . . . . . 8
β’ (π΄ β β β ((Ο
β π΄) / 2) = ((Ο /
2) β (π΄ /
2))) |
48 | 47 | fveq2d 6866 |
. . . . . . 7
β’ (π΄ β β β
(sinβ((Ο β π΄) / 2)) = (sinβ((Ο / 2) β
(π΄ / 2)))) |
49 | 6 | recnd 11207 |
. . . . . . . 8
β’ (π΄ β β β (π΄ / 2) β
β) |
50 | | sinhalfpim 25902 |
. . . . . . . 8
β’ ((π΄ / 2) β β β
(sinβ((Ο / 2) β (π΄ / 2))) = (cosβ(π΄ / 2))) |
51 | 49, 50 | syl 17 |
. . . . . . 7
β’ (π΄ β β β
(sinβ((Ο / 2) β (π΄ / 2))) = (cosβ(π΄ / 2))) |
52 | 48, 51 | eqtrd 2771 |
. . . . . 6
β’ (π΄ β β β
(sinβ((Ο β π΄) / 2)) = (cosβ(π΄ / 2))) |
53 | 52 | 3ad2ant1 1133 |
. . . . 5
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β (sinβ((Ο β
π΄) / 2)) =
(cosβ(π΄ /
2))) |
54 | 41, 53 | breqtrd 5151 |
. . . 4
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β 0 < (cosβ(π΄ / 2))) |
55 | | resincl 16048 |
. . . . . . . 8
β’ ((π΄ / 2) β β β
(sinβ(π΄ / 2)) β
β) |
56 | | recoscl 16049 |
. . . . . . . 8
β’ ((π΄ / 2) β β β
(cosβ(π΄ / 2)) β
β) |
57 | 55, 56 | jca 512 |
. . . . . . 7
β’ ((π΄ / 2) β β β
((sinβ(π΄ / 2)) β
β β§ (cosβ(π΄
/ 2)) β β)) |
58 | | axmulgt0 11253 |
. . . . . . 7
β’
(((sinβ(π΄ /
2)) β β β§ (cosβ(π΄ / 2)) β β) β ((0 <
(sinβ(π΄ / 2)) β§ 0
< (cosβ(π΄ / 2)))
β 0 < ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))))) |
59 | 6, 57, 58 | 3syl 18 |
. . . . . 6
β’ (π΄ β β β ((0 <
(sinβ(π΄ / 2)) β§ 0
< (cosβ(π΄ / 2)))
β 0 < ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))))) |
60 | | remulcl 11160 |
. . . . . . . . 9
β’
(((sinβ(π΄ /
2)) β β β§ (cosβ(π΄ / 2)) β β) β
((sinβ(π΄ / 2))
Β· (cosβ(π΄ /
2))) β β) |
61 | 6, 57, 60 | 3syl 18 |
. . . . . . . 8
β’ (π΄ β β β
((sinβ(π΄ / 2))
Β· (cosβ(π΄ /
2))) β β) |
62 | | axmulgt0 11253 |
. . . . . . . 8
β’ ((2
β β β§ ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))) β β) β
((0 < 2 β§ 0 < ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2)))) β 0 < (2
Β· ((sinβ(π΄ /
2)) Β· (cosβ(π΄
/ 2)))))) |
63 | 11, 61, 62 | sylancr 587 |
. . . . . . 7
β’ (π΄ β β β ((0 <
2 β§ 0 < ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2)))) β 0 < (2
Β· ((sinβ(π΄ /
2)) Β· (cosβ(π΄
/ 2)))))) |
64 | 12, 63 | mpani 694 |
. . . . . 6
β’ (π΄ β β β (0 <
((sinβ(π΄ / 2))
Β· (cosβ(π΄ /
2))) β 0 < (2 Β· ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2)))))) |
65 | 59, 64 | syld 47 |
. . . . 5
β’ (π΄ β β β ((0 <
(sinβ(π΄ / 2)) β§ 0
< (cosβ(π΄ / 2)))
β 0 < (2 Β· ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2)))))) |
66 | 65 | 3ad2ant1 1133 |
. . . 4
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β ((0 <
(sinβ(π΄ / 2)) β§ 0
< (cosβ(π΄ / 2)))
β 0 < (2 Β· ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2)))))) |
67 | 19, 54, 66 | mp2and 697 |
. . 3
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β 0 < (2 Β·
((sinβ(π΄ / 2))
Β· (cosβ(π΄ /
2))))) |
68 | | 2cn 12252 |
. . . . . . . 8
β’ 2 β
β |
69 | | 2ne0 12281 |
. . . . . . . 8
β’ 2 β
0 |
70 | | divcan2 11845 |
. . . . . . . 8
β’ ((π΄ β β β§ 2 β
β β§ 2 β 0) β (2 Β· (π΄ / 2)) = π΄) |
71 | 68, 69, 70 | mp3an23 1453 |
. . . . . . 7
β’ (π΄ β β β (2
Β· (π΄ / 2)) = π΄) |
72 | 42, 71 | syl 17 |
. . . . . 6
β’ (π΄ β β β (2
Β· (π΄ / 2)) = π΄) |
73 | 72 | fveq2d 6866 |
. . . . 5
β’ (π΄ β β β
(sinβ(2 Β· (π΄ /
2))) = (sinβπ΄)) |
74 | | sin2t 16085 |
. . . . . 6
β’ ((π΄ / 2) β β β
(sinβ(2 Β· (π΄ /
2))) = (2 Β· ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))))) |
75 | 49, 74 | syl 17 |
. . . . 5
β’ (π΄ β β β
(sinβ(2 Β· (π΄ /
2))) = (2 Β· ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))))) |
76 | 73, 75 | eqtr3d 2773 |
. . . 4
β’ (π΄ β β β
(sinβπ΄) = (2 Β·
((sinβ(π΄ / 2))
Β· (cosβ(π΄ /
2))))) |
77 | 76 | 3ad2ant1 1133 |
. . 3
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β (sinβπ΄) = (2 Β·
((sinβ(π΄ / 2))
Β· (cosβ(π΄ /
2))))) |
78 | 67, 77 | breqtrrd 5153 |
. 2
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β 0 < (sinβπ΄)) |
79 | 5, 78 | sylbi 216 |
1
β’ (π΄ β (0(,)Ο) β 0 <
(sinβπ΄)) |