Step | Hyp | Ref
| Expression |
1 | | 0xr 8004 |
. . 3
β’ 0 β
β* |
2 | | pire 14210 |
. . . 4
β’ Ο
β β |
3 | 2 | rexri 8015 |
. . 3
β’ Ο
β β* |
4 | | elioo2 9921 |
. . 3
β’ ((0
β β* β§ Ο β β*) β (π΄ β (0(,)Ο) β (π΄ β β β§ 0 <
π΄ β§ π΄ < Ο))) |
5 | 1, 3, 4 | mp2an 426 |
. 2
β’ (π΄ β (0(,)Ο) β (π΄ β β β§ 0 <
π΄ β§ π΄ < Ο)) |
6 | | rehalfcl 9146 |
. . . . . 6
β’ (π΄ β β β (π΄ / 2) β
β) |
7 | 6 | 3ad2ant1 1018 |
. . . . 5
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β (π΄ / 2) β β) |
8 | | halfpos2 9149 |
. . . . . . 7
β’ (π΄ β β β (0 <
π΄ β 0 < (π΄ / 2))) |
9 | 8 | biimpa 296 |
. . . . . 6
β’ ((π΄ β β β§ 0 <
π΄) β 0 < (π΄ / 2)) |
10 | 9 | 3adant3 1017 |
. . . . 5
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β 0 < (π΄ / 2)) |
11 | | 2re 8989 |
. . . . . . . . 9
β’ 2 β
β |
12 | | 2pos 9010 |
. . . . . . . . 9
β’ 0 <
2 |
13 | 11, 12 | pm3.2i 272 |
. . . . . . . 8
β’ (2 β
β β§ 0 < 2) |
14 | | ltdiv1 8825 |
. . . . . . . 8
β’ ((π΄ β β β§ Ο
β β β§ (2 β β β§ 0 < 2)) β (π΄ < Ο β (π΄ / 2) < (Ο /
2))) |
15 | 2, 13, 14 | mp3an23 1329 |
. . . . . . 7
β’ (π΄ β β β (π΄ < Ο β (π΄ / 2) < (Ο /
2))) |
16 | 15 | adantr 276 |
. . . . . 6
β’ ((π΄ β β β§ 0 <
π΄) β (π΄ < Ο β (π΄ / 2) < (Ο /
2))) |
17 | 16 | biimp3a 1345 |
. . . . 5
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β (π΄ / 2) < (Ο / 2)) |
18 | | sincosq1lem 14249 |
. . . . 5
β’ (((π΄ / 2) β β β§ 0
< (π΄ / 2) β§ (π΄ / 2) < (Ο / 2)) β 0
< (sinβ(π΄ /
2))) |
19 | 7, 10, 17, 18 | syl3anc 1238 |
. . . 4
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β 0 < (sinβ(π΄ / 2))) |
20 | | resubcl 8221 |
. . . . . . . . 9
β’ ((Ο
β β β§ π΄
β β) β (Ο β π΄) β β) |
21 | 2, 20 | mpan 424 |
. . . . . . . 8
β’ (π΄ β β β (Ο
β π΄) β
β) |
22 | | rehalfcl 9146 |
. . . . . . . 8
β’ ((Ο
β π΄) β β
β ((Ο β π΄) /
2) β β) |
23 | 21, 22 | syl 14 |
. . . . . . 7
β’ (π΄ β β β ((Ο
β π΄) / 2) β
β) |
24 | 23 | 3ad2ant1 1018 |
. . . . . 6
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β ((Ο β π΄) / 2) β
β) |
25 | | posdif 8412 |
. . . . . . . . . 10
β’ ((π΄ β β β§ Ο
β β) β (π΄
< Ο β 0 < (Ο β π΄))) |
26 | 2, 25 | mpan2 425 |
. . . . . . . . 9
β’ (π΄ β β β (π΄ < Ο β 0 < (Ο
β π΄))) |
27 | | halfpos2 9149 |
. . . . . . . . . 10
β’ ((Ο
β π΄) β β
β (0 < (Ο β π΄) β 0 < ((Ο β π΄) / 2))) |
28 | 21, 27 | syl 14 |
. . . . . . . . 9
β’ (π΄ β β β (0 <
(Ο β π΄) β 0
< ((Ο β π΄) /
2))) |
29 | 26, 28 | bitrd 188 |
. . . . . . . 8
β’ (π΄ β β β (π΄ < Ο β 0 < ((Ο
β π΄) /
2))) |
30 | 29 | adantr 276 |
. . . . . . 7
β’ ((π΄ β β β§ 0 <
π΄) β (π΄ < Ο β 0 < ((Ο
β π΄) /
2))) |
31 | 30 | biimp3a 1345 |
. . . . . 6
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β 0 < ((Ο β
π΄) / 2)) |
32 | | ltsubpos 8411 |
. . . . . . . . . 10
β’ ((π΄ β β β§ Ο
β β) β (0 < π΄ β (Ο β π΄) < Ο)) |
33 | 2, 32 | mpan2 425 |
. . . . . . . . 9
β’ (π΄ β β β (0 <
π΄ β (Ο β
π΄) <
Ο)) |
34 | | ltdiv1 8825 |
. . . . . . . . . . 11
β’ (((Ο
β π΄) β β
β§ Ο β β β§ (2 β β β§ 0 < 2)) β
((Ο β π΄) < Ο
β ((Ο β π΄) /
2) < (Ο / 2))) |
35 | 2, 13, 34 | mp3an23 1329 |
. . . . . . . . . 10
β’ ((Ο
β π΄) β β
β ((Ο β π΄)
< Ο β ((Ο β π΄) / 2) < (Ο / 2))) |
36 | 21, 35 | syl 14 |
. . . . . . . . 9
β’ (π΄ β β β ((Ο
β π΄) < Ο β
((Ο β π΄) / 2) <
(Ο / 2))) |
37 | 33, 36 | bitrd 188 |
. . . . . . . 8
β’ (π΄ β β β (0 <
π΄ β ((Ο β
π΄) / 2) < (Ο /
2))) |
38 | 37 | biimpa 296 |
. . . . . . 7
β’ ((π΄ β β β§ 0 <
π΄) β ((Ο β
π΄) / 2) < (Ο /
2)) |
39 | 38 | 3adant3 1017 |
. . . . . 6
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β ((Ο β π΄) / 2) < (Ο /
2)) |
40 | | sincosq1lem 14249 |
. . . . . 6
β’ ((((Ο
β π΄) / 2) β
β β§ 0 < ((Ο β π΄) / 2) β§ ((Ο β π΄) / 2) < (Ο / 2)) β 0
< (sinβ((Ο β π΄) / 2))) |
41 | 24, 31, 39, 40 | syl3anc 1238 |
. . . . 5
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β 0 < (sinβ((Ο
β π΄) /
2))) |
42 | | recn 7944 |
. . . . . . . . 9
β’ (π΄ β β β π΄ β
β) |
43 | | picn 14211 |
. . . . . . . . . 10
β’ Ο
β β |
44 | | 2cn 8990 |
. . . . . . . . . . 11
β’ 2 β
β |
45 | | 2ap0 9012 |
. . . . . . . . . . 11
β’ 2 #
0 |
46 | 44, 45 | pm3.2i 272 |
. . . . . . . . . 10
β’ (2 β
β β§ 2 # 0) |
47 | | divsubdirap 8665 |
. . . . . . . . . 10
β’ ((Ο
β β β§ π΄
β β β§ (2 β β β§ 2 # 0)) β ((Ο β
π΄) / 2) = ((Ο / 2)
β (π΄ /
2))) |
48 | 43, 46, 47 | mp3an13 1328 |
. . . . . . . . 9
β’ (π΄ β β β ((Ο
β π΄) / 2) = ((Ο /
2) β (π΄ /
2))) |
49 | 42, 48 | syl 14 |
. . . . . . . 8
β’ (π΄ β β β ((Ο
β π΄) / 2) = ((Ο /
2) β (π΄ /
2))) |
50 | 49 | fveq2d 5520 |
. . . . . . 7
β’ (π΄ β β β
(sinβ((Ο β π΄) / 2)) = (sinβ((Ο / 2) β
(π΄ / 2)))) |
51 | 6 | recnd 7986 |
. . . . . . . 8
β’ (π΄ β β β (π΄ / 2) β
β) |
52 | | sinhalfpim 14245 |
. . . . . . . 8
β’ ((π΄ / 2) β β β
(sinβ((Ο / 2) β (π΄ / 2))) = (cosβ(π΄ / 2))) |
53 | 51, 52 | syl 14 |
. . . . . . 7
β’ (π΄ β β β
(sinβ((Ο / 2) β (π΄ / 2))) = (cosβ(π΄ / 2))) |
54 | 50, 53 | eqtrd 2210 |
. . . . . 6
β’ (π΄ β β β
(sinβ((Ο β π΄) / 2)) = (cosβ(π΄ / 2))) |
55 | 54 | 3ad2ant1 1018 |
. . . . 5
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β (sinβ((Ο β
π΄) / 2)) =
(cosβ(π΄ /
2))) |
56 | 41, 55 | breqtrd 4030 |
. . . 4
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β 0 < (cosβ(π΄ / 2))) |
57 | | resincl 11728 |
. . . . . . . 8
β’ ((π΄ / 2) β β β
(sinβ(π΄ / 2)) β
β) |
58 | | recoscl 11729 |
. . . . . . . 8
β’ ((π΄ / 2) β β β
(cosβ(π΄ / 2)) β
β) |
59 | 57, 58 | jca 306 |
. . . . . . 7
β’ ((π΄ / 2) β β β
((sinβ(π΄ / 2)) β
β β§ (cosβ(π΄
/ 2)) β β)) |
60 | | axmulgt0 8029 |
. . . . . . 7
β’
(((sinβ(π΄ /
2)) β β β§ (cosβ(π΄ / 2)) β β) β ((0 <
(sinβ(π΄ / 2)) β§ 0
< (cosβ(π΄ / 2)))
β 0 < ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))))) |
61 | 6, 59, 60 | 3syl 17 |
. . . . . 6
β’ (π΄ β β β ((0 <
(sinβ(π΄ / 2)) β§ 0
< (cosβ(π΄ / 2)))
β 0 < ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))))) |
62 | | remulcl 7939 |
. . . . . . . . 9
β’
(((sinβ(π΄ /
2)) β β β§ (cosβ(π΄ / 2)) β β) β
((sinβ(π΄ / 2))
Β· (cosβ(π΄ /
2))) β β) |
63 | 6, 59, 62 | 3syl 17 |
. . . . . . . 8
β’ (π΄ β β β
((sinβ(π΄ / 2))
Β· (cosβ(π΄ /
2))) β β) |
64 | | axmulgt0 8029 |
. . . . . . . 8
β’ ((2
β β β§ ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))) β β) β
((0 < 2 β§ 0 < ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2)))) β 0 < (2
Β· ((sinβ(π΄ /
2)) Β· (cosβ(π΄
/ 2)))))) |
65 | 11, 63, 64 | sylancr 414 |
. . . . . . 7
β’ (π΄ β β β ((0 <
2 β§ 0 < ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2)))) β 0 < (2
Β· ((sinβ(π΄ /
2)) Β· (cosβ(π΄
/ 2)))))) |
66 | 12, 65 | mpani 430 |
. . . . . 6
β’ (π΄ β β β (0 <
((sinβ(π΄ / 2))
Β· (cosβ(π΄ /
2))) β 0 < (2 Β· ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2)))))) |
67 | 61, 66 | syld 45 |
. . . . 5
β’ (π΄ β β β ((0 <
(sinβ(π΄ / 2)) β§ 0
< (cosβ(π΄ / 2)))
β 0 < (2 Β· ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2)))))) |
68 | 67 | 3ad2ant1 1018 |
. . . 4
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β ((0 <
(sinβ(π΄ / 2)) β§ 0
< (cosβ(π΄ / 2)))
β 0 < (2 Β· ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2)))))) |
69 | 19, 56, 68 | mp2and 433 |
. . 3
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β 0 < (2 Β·
((sinβ(π΄ / 2))
Β· (cosβ(π΄ /
2))))) |
70 | | divcanap2 8637 |
. . . . . . . 8
β’ ((π΄ β β β§ 2 β
β β§ 2 # 0) β (2 Β· (π΄ / 2)) = π΄) |
71 | 44, 45, 70 | mp3an23 1329 |
. . . . . . 7
β’ (π΄ β β β (2
Β· (π΄ / 2)) = π΄) |
72 | 42, 71 | syl 14 |
. . . . . 6
β’ (π΄ β β β (2
Β· (π΄ / 2)) = π΄) |
73 | 72 | fveq2d 5520 |
. . . . 5
β’ (π΄ β β β
(sinβ(2 Β· (π΄ /
2))) = (sinβπ΄)) |
74 | | sin2t 11757 |
. . . . . 6
β’ ((π΄ / 2) β β β
(sinβ(2 Β· (π΄ /
2))) = (2 Β· ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))))) |
75 | 51, 74 | syl 14 |
. . . . 5
β’ (π΄ β β β
(sinβ(2 Β· (π΄ /
2))) = (2 Β· ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))))) |
76 | 73, 75 | eqtr3d 2212 |
. . . 4
β’ (π΄ β β β
(sinβπ΄) = (2 Β·
((sinβ(π΄ / 2))
Β· (cosβ(π΄ /
2))))) |
77 | 76 | 3ad2ant1 1018 |
. . 3
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β (sinβπ΄) = (2 Β·
((sinβ(π΄ / 2))
Β· (cosβ(π΄ /
2))))) |
78 | 69, 77 | breqtrrd 4032 |
. 2
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ < Ο) β 0 < (sinβπ΄)) |
79 | 5, 78 | sylbi 121 |
1
β’ (π΄ β (0(,)Ο) β 0 <
(sinβπ΄)) |