Step | Hyp | Ref
| Expression |
1 | | 0xr 11209 |
. . . . . . 7
β’ 0 β
β* |
2 | | 2re 12234 |
. . . . . . 7
β’ 2 β
β |
3 | | elioc2 13334 |
. . . . . . 7
β’ ((0
β β* β§ 2 β β) β (π΄ β (0(,]2) β (π΄ β β β§ 0 < π΄ β§ π΄ β€ 2))) |
4 | 1, 2, 3 | mp2an 691 |
. . . . . 6
β’ (π΄ β (0(,]2) β (π΄ β β β§ 0 <
π΄ β§ π΄ β€ 2)) |
5 | | rehalfcl 12386 |
. . . . . . 7
β’ (π΄ β β β (π΄ / 2) β
β) |
6 | 5 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ β€ 2) β (π΄ / 2) β β) |
7 | 4, 6 | sylbi 216 |
. . . . 5
β’ (π΄ β (0(,]2) β (π΄ / 2) β
β) |
8 | | resincl 16029 |
. . . . . 6
β’ ((π΄ / 2) β β β
(sinβ(π΄ / 2)) β
β) |
9 | | recoscl 16030 |
. . . . . 6
β’ ((π΄ / 2) β β β
(cosβ(π΄ / 2)) β
β) |
10 | 8, 9 | remulcld 11192 |
. . . . 5
β’ ((π΄ / 2) β β β
((sinβ(π΄ / 2))
Β· (cosβ(π΄ /
2))) β β) |
11 | 7, 10 | syl 17 |
. . . 4
β’ (π΄ β (0(,]2) β
((sinβ(π΄ / 2))
Β· (cosβ(π΄ /
2))) β β) |
12 | | 2pos 12263 |
. . . . . . . . . 10
β’ 0 <
2 |
13 | | divgt0 12030 |
. . . . . . . . . 10
β’ (((π΄ β β β§ 0 <
π΄) β§ (2 β β
β§ 0 < 2)) β 0 < (π΄ / 2)) |
14 | 2, 12, 13 | mpanr12 704 |
. . . . . . . . 9
β’ ((π΄ β β β§ 0 <
π΄) β 0 < (π΄ / 2)) |
15 | 14 | 3adant3 1133 |
. . . . . . . 8
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ β€ 2) β 0 < (π΄ / 2)) |
16 | 2, 12 | pm3.2i 472 |
. . . . . . . . . . . 12
β’ (2 β
β β§ 0 < 2) |
17 | | lediv1 12027 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ 2 β
β β§ (2 β β β§ 0 < 2)) β (π΄ β€ 2 β (π΄ / 2) β€ (2 / 2))) |
18 | 2, 16, 17 | mp3an23 1454 |
. . . . . . . . . . 11
β’ (π΄ β β β (π΄ β€ 2 β (π΄ / 2) β€ (2 /
2))) |
19 | 18 | biimpa 478 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΄ β€ 2) β (π΄ / 2) β€ (2 /
2)) |
20 | | 2div2e1 12301 |
. . . . . . . . . 10
β’ (2 / 2) =
1 |
21 | 19, 20 | breqtrdi 5151 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΄ β€ 2) β (π΄ / 2) β€ 1) |
22 | 21 | 3adant2 1132 |
. . . . . . . 8
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ β€ 2) β (π΄ / 2) β€ 1) |
23 | 6, 15, 22 | 3jca 1129 |
. . . . . . 7
β’ ((π΄ β β β§ 0 <
π΄ β§ π΄ β€ 2) β ((π΄ / 2) β β β§ 0 < (π΄ / 2) β§ (π΄ / 2) β€ 1)) |
24 | | 1re 11162 |
. . . . . . . 8
β’ 1 β
β |
25 | | elioc2 13334 |
. . . . . . . 8
β’ ((0
β β* β§ 1 β β) β ((π΄ / 2) β (0(,]1) β ((π΄ / 2) β β β§ 0
< (π΄ / 2) β§ (π΄ / 2) β€ 1))) |
26 | 1, 24, 25 | mp2an 691 |
. . . . . . 7
β’ ((π΄ / 2) β (0(,]1) β
((π΄ / 2) β β
β§ 0 < (π΄ / 2) β§
(π΄ / 2) β€
1)) |
27 | 23, 4, 26 | 3imtr4i 292 |
. . . . . 6
β’ (π΄ β (0(,]2) β (π΄ / 2) β
(0(,]1)) |
28 | | sin01gt0 16079 |
. . . . . 6
β’ ((π΄ / 2) β (0(,]1) β 0
< (sinβ(π΄ /
2))) |
29 | 27, 28 | syl 17 |
. . . . 5
β’ (π΄ β (0(,]2) β 0 <
(sinβ(π΄ /
2))) |
30 | | cos01gt0 16080 |
. . . . . 6
β’ ((π΄ / 2) β (0(,]1) β 0
< (cosβ(π΄ /
2))) |
31 | 27, 30 | syl 17 |
. . . . 5
β’ (π΄ β (0(,]2) β 0 <
(cosβ(π΄ /
2))) |
32 | | axmulgt0 11236 |
. . . . . . 7
β’
(((sinβ(π΄ /
2)) β β β§ (cosβ(π΄ / 2)) β β) β ((0 <
(sinβ(π΄ / 2)) β§ 0
< (cosβ(π΄ / 2)))
β 0 < ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))))) |
33 | 8, 9, 32 | syl2anc 585 |
. . . . . 6
β’ ((π΄ / 2) β β β ((0
< (sinβ(π΄ / 2))
β§ 0 < (cosβ(π΄
/ 2))) β 0 < ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))))) |
34 | 7, 33 | syl 17 |
. . . . 5
β’ (π΄ β (0(,]2) β ((0 <
(sinβ(π΄ / 2)) β§ 0
< (cosβ(π΄ / 2)))
β 0 < ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))))) |
35 | 29, 31, 34 | mp2and 698 |
. . . 4
β’ (π΄ β (0(,]2) β 0 <
((sinβ(π΄ / 2))
Β· (cosβ(π΄ /
2)))) |
36 | | axmulgt0 11236 |
. . . . . 6
β’ ((2
β β β§ ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))) β β) β
((0 < 2 β§ 0 < ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2)))) β 0 < (2
Β· ((sinβ(π΄ /
2)) Β· (cosβ(π΄
/ 2)))))) |
37 | 2, 36 | mpan 689 |
. . . . 5
β’
(((sinβ(π΄ /
2)) Β· (cosβ(π΄
/ 2))) β β β ((0 < 2 β§ 0 < ((sinβ(π΄ / 2)) Β·
(cosβ(π΄ / 2))))
β 0 < (2 Β· ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2)))))) |
38 | 12, 37 | mpani 695 |
. . . 4
β’
(((sinβ(π΄ /
2)) Β· (cosβ(π΄
/ 2))) β β β (0 < ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))) β 0 < (2
Β· ((sinβ(π΄ /
2)) Β· (cosβ(π΄
/ 2)))))) |
39 | 11, 35, 38 | sylc 65 |
. . 3
β’ (π΄ β (0(,]2) β 0 < (2
Β· ((sinβ(π΄ /
2)) Β· (cosβ(π΄
/ 2))))) |
40 | 7 | recnd 11190 |
. . . 4
β’ (π΄ β (0(,]2) β (π΄ / 2) β
β) |
41 | | sin2t 16066 |
. . . 4
β’ ((π΄ / 2) β β β
(sinβ(2 Β· (π΄ /
2))) = (2 Β· ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))))) |
42 | 40, 41 | syl 17 |
. . 3
β’ (π΄ β (0(,]2) β
(sinβ(2 Β· (π΄ /
2))) = (2 Β· ((sinβ(π΄ / 2)) Β· (cosβ(π΄ / 2))))) |
43 | 39, 42 | breqtrrd 5138 |
. 2
β’ (π΄ β (0(,]2) β 0 <
(sinβ(2 Β· (π΄ /
2)))) |
44 | 4 | simp1bi 1146 |
. . . . 5
β’ (π΄ β (0(,]2) β π΄ β
β) |
45 | 44 | recnd 11190 |
. . . 4
β’ (π΄ β (0(,]2) β π΄ β
β) |
46 | | 2cn 12235 |
. . . . 5
β’ 2 β
β |
47 | | 2ne0 12264 |
. . . . 5
β’ 2 β
0 |
48 | | divcan2 11828 |
. . . . 5
β’ ((π΄ β β β§ 2 β
β β§ 2 β 0) β (2 Β· (π΄ / 2)) = π΄) |
49 | 46, 47, 48 | mp3an23 1454 |
. . . 4
β’ (π΄ β β β (2
Β· (π΄ / 2)) = π΄) |
50 | 45, 49 | syl 17 |
. . 3
β’ (π΄ β (0(,]2) β (2
Β· (π΄ / 2)) = π΄) |
51 | 50 | fveq2d 6851 |
. 2
β’ (π΄ β (0(,]2) β
(sinβ(2 Β· (π΄ /
2))) = (sinβπ΄)) |
52 | 43, 51 | breqtrd 5136 |
1
β’ (π΄ β (0(,]2) β 0 <
(sinβπ΄)) |