Step | Hyp | Ref
| Expression |
1 | | 0re 11164 |
. . . . . 6
β’ 0 β
β |
2 | | 2re 12234 |
. . . . . . 7
β’ 2 β
β |
3 | | pire 25831 |
. . . . . . 7
β’ Ο
β β |
4 | 2, 3 | remulcli 11178 |
. . . . . 6
β’ (2
Β· Ο) β β |
5 | | iccssre 13353 |
. . . . . 6
β’ ((0
β β β§ (2 Β· Ο) β β) β (0[,](2 Β·
Ο)) β β) |
6 | 1, 4, 5 | mp2an 691 |
. . . . 5
β’ (0[,](2
Β· Ο)) β β |
7 | 6 | sseli 3945 |
. . . 4
β’ (π΄ β (0[,](2 Β· Ο))
β π΄ β
β) |
8 | 7 | rehalfcld 12407 |
. . 3
β’ (π΄ β (0[,](2 Β· Ο))
β (π΄ / 2) β
β) |
9 | 8 | resincld 16032 |
. 2
β’ (π΄ β (0[,](2 Β· Ο))
β (sinβ(π΄ / 2))
β β) |
10 | | 1re 11162 |
. . . . . 6
β’ 1 β
β |
11 | | recoscl 16030 |
. . . . . 6
β’ (π΄ β β β
(cosβπ΄) β
β) |
12 | | resubcl 11472 |
. . . . . 6
β’ ((1
β β β§ (cosβπ΄) β β) β (1 β
(cosβπ΄)) β
β) |
13 | 10, 11, 12 | sylancr 588 |
. . . . 5
β’ (π΄ β β β (1
β (cosβπ΄))
β β) |
14 | 13 | rehalfcld 12407 |
. . . 4
β’ (π΄ β β β ((1
β (cosβπ΄)) / 2)
β β) |
15 | | cosbnd 16070 |
. . . . . 6
β’ (π΄ β β β (-1 β€
(cosβπ΄) β§
(cosβπ΄) β€
1)) |
16 | 15 | simprd 497 |
. . . . 5
β’ (π΄ β β β
(cosβπ΄) β€
1) |
17 | | subge0 11675 |
. . . . . . 7
β’ ((1
β β β§ (cosβπ΄) β β) β (0 β€ (1 β
(cosβπ΄)) β
(cosβπ΄) β€
1)) |
18 | 10, 11, 17 | sylancr 588 |
. . . . . 6
β’ (π΄ β β β (0 β€
(1 β (cosβπ΄))
β (cosβπ΄) β€
1)) |
19 | | halfnneg2 12391 |
. . . . . . 7
β’ ((1
β (cosβπ΄))
β β β (0 β€ (1 β (cosβπ΄)) β 0 β€ ((1 β
(cosβπ΄)) /
2))) |
20 | 13, 19 | syl 17 |
. . . . . 6
β’ (π΄ β β β (0 β€
(1 β (cosβπ΄))
β 0 β€ ((1 β (cosβπ΄)) / 2))) |
21 | 18, 20 | bitr3d 281 |
. . . . 5
β’ (π΄ β β β
((cosβπ΄) β€ 1
β 0 β€ ((1 β (cosβπ΄)) / 2))) |
22 | 16, 21 | mpbid 231 |
. . . 4
β’ (π΄ β β β 0 β€
((1 β (cosβπ΄))
/ 2)) |
23 | 14, 22 | resqrtcld 15309 |
. . 3
β’ (π΄ β β β
(ββ((1 β (cosβπ΄)) / 2)) β β) |
24 | 7, 23 | syl 17 |
. 2
β’ (π΄ β (0[,](2 Β· Ο))
β (ββ((1 β (cosβπ΄)) / 2)) β β) |
25 | 1, 4 | elicc2i 13337 |
. . . 4
β’ (π΄ β (0[,](2 Β· Ο))
β (π΄ β β
β§ 0 β€ π΄ β§ π΄ β€ (2 Β·
Ο))) |
26 | | halfnneg2 12391 |
. . . . . . . 8
β’ (π΄ β β β (0 β€
π΄ β 0 β€ (π΄ / 2))) |
27 | | 2pos 12263 |
. . . . . . . . . . 11
β’ 0 <
2 |
28 | 2, 27 | pm3.2i 472 |
. . . . . . . . . 10
β’ (2 β
β β§ 0 < 2) |
29 | | ledivmul 12038 |
. . . . . . . . . 10
β’ ((π΄ β β β§ Ο
β β β§ (2 β β β§ 0 < 2)) β ((π΄ / 2) β€ Ο β π΄ β€ (2 Β·
Ο))) |
30 | 3, 28, 29 | mp3an23 1454 |
. . . . . . . . 9
β’ (π΄ β β β ((π΄ / 2) β€ Ο β π΄ β€ (2 Β·
Ο))) |
31 | 30 | bicomd 222 |
. . . . . . . 8
β’ (π΄ β β β (π΄ β€ (2 Β· Ο) β
(π΄ / 2) β€
Ο)) |
32 | 26, 31 | anbi12d 632 |
. . . . . . 7
β’ (π΄ β β β ((0 β€
π΄ β§ π΄ β€ (2 Β· Ο)) β (0 β€
(π΄ / 2) β§ (π΄ / 2) β€
Ο))) |
33 | | rehalfcl 12386 |
. . . . . . . . 9
β’ (π΄ β β β (π΄ / 2) β
β) |
34 | 33 | rexrd 11212 |
. . . . . . . 8
β’ (π΄ β β β (π΄ / 2) β
β*) |
35 | | 0xr 11209 |
. . . . . . . . 9
β’ 0 β
β* |
36 | 3 | rexri 11220 |
. . . . . . . . 9
β’ Ο
β β* |
37 | | elicc4 13338 |
. . . . . . . . 9
β’ ((0
β β* β§ Ο β β* β§ (π΄ / 2) β
β*) β ((π΄ / 2) β (0[,]Ο) β (0 β€
(π΄ / 2) β§ (π΄ / 2) β€
Ο))) |
38 | 35, 36, 37 | mp3an12 1452 |
. . . . . . . 8
β’ ((π΄ / 2) β β*
β ((π΄ / 2) β
(0[,]Ο) β (0 β€ (π΄ / 2) β§ (π΄ / 2) β€ Ο))) |
39 | 34, 38 | syl 17 |
. . . . . . 7
β’ (π΄ β β β ((π΄ / 2) β (0[,]Ο) β
(0 β€ (π΄ / 2) β§
(π΄ / 2) β€
Ο))) |
40 | 32, 39 | bitr4d 282 |
. . . . . 6
β’ (π΄ β β β ((0 β€
π΄ β§ π΄ β€ (2 Β· Ο)) β (π΄ / 2) β
(0[,]Ο))) |
41 | 40 | biimpd 228 |
. . . . 5
β’ (π΄ β β β ((0 β€
π΄ β§ π΄ β€ (2 Β· Ο)) β (π΄ / 2) β
(0[,]Ο))) |
42 | 41 | 3impib 1117 |
. . . 4
β’ ((π΄ β β β§ 0 β€
π΄ β§ π΄ β€ (2 Β· Ο)) β (π΄ / 2) β
(0[,]Ο)) |
43 | 25, 42 | sylbi 216 |
. . 3
β’ (π΄ β (0[,](2 Β· Ο))
β (π΄ / 2) β
(0[,]Ο)) |
44 | | sinq12ge0 25881 |
. . 3
β’ ((π΄ / 2) β (0[,]Ο) β 0
β€ (sinβ(π΄ /
2))) |
45 | 43, 44 | syl 17 |
. 2
β’ (π΄ β (0[,](2 Β· Ο))
β 0 β€ (sinβ(π΄
/ 2))) |
46 | 14, 22 | sqrtge0d 15312 |
. . 3
β’ (π΄ β β β 0 β€
(ββ((1 β (cosβπ΄)) / 2))) |
47 | 7, 46 | syl 17 |
. 2
β’ (π΄ β (0[,](2 Β· Ο))
β 0 β€ (ββ((1 β (cosβπ΄)) / 2))) |
48 | 7 | recnd 11190 |
. . 3
β’ (π΄ β (0[,](2 Β· Ο))
β π΄ β
β) |
49 | | ax-1cn 11116 |
. . . . . . 7
β’ 1 β
β |
50 | | coscl 16016 |
. . . . . . 7
β’ (π΄ β β β
(cosβπ΄) β
β) |
51 | | subcl 11407 |
. . . . . . 7
β’ ((1
β β β§ (cosβπ΄) β β) β (1 β
(cosβπ΄)) β
β) |
52 | 49, 50, 51 | sylancr 588 |
. . . . . 6
β’ (π΄ β β β (1
β (cosβπ΄))
β β) |
53 | 52 | halfcld 12405 |
. . . . 5
β’ (π΄ β β β ((1
β (cosβπ΄)) / 2)
β β) |
54 | 53 | sqsqrtd 15331 |
. . . 4
β’ (π΄ β β β
((ββ((1 β (cosβπ΄)) / 2))β2) = ((1 β
(cosβπ΄)) /
2)) |
55 | | halfcl 12385 |
. . . . . . 7
β’ (π΄ β β β (π΄ / 2) β
β) |
56 | | coscl 16016 |
. . . . . . . . . . . . 13
β’ ((π΄ / 2) β β β
(cosβ(π΄ / 2)) β
β) |
57 | 56 | sqcld 14056 |
. . . . . . . . . . . 12
β’ ((π΄ / 2) β β β
((cosβ(π΄ /
2))β2) β β) |
58 | | 2cn 12235 |
. . . . . . . . . . . 12
β’ 2 β
β |
59 | | mulcom 11144 |
. . . . . . . . . . . 12
β’
((((cosβ(π΄ /
2))β2) β β β§ 2 β β) β (((cosβ(π΄ / 2))β2) Β· 2) = (2
Β· ((cosβ(π΄ /
2))β2))) |
60 | 57, 58, 59 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π΄ / 2) β β β
(((cosβ(π΄ /
2))β2) Β· 2) = (2 Β· ((cosβ(π΄ / 2))β2))) |
61 | 60 | oveq2d 7378 |
. . . . . . . . . 10
β’ ((π΄ / 2) β β β ((1
Β· 2) β (((cosβ(π΄ / 2))β2) Β· 2)) = ((1 Β·
2) β (2 Β· ((cosβ(π΄ / 2))β2)))) |
62 | 58 | mulid2i 11167 |
. . . . . . . . . . . 12
β’ (1
Β· 2) = 2 |
63 | | df-2 12223 |
. . . . . . . . . . . 12
β’ 2 = (1 +
1) |
64 | 62, 63 | eqtri 2765 |
. . . . . . . . . . 11
β’ (1
Β· 2) = (1 + 1) |
65 | 64 | oveq1i 7372 |
. . . . . . . . . 10
β’ ((1
Β· 2) β (2 Β· ((cosβ(π΄ / 2))β2))) = ((1 + 1) β (2
Β· ((cosβ(π΄ /
2))β2))) |
66 | 61, 65 | eqtrdi 2793 |
. . . . . . . . 9
β’ ((π΄ / 2) β β β ((1
Β· 2) β (((cosβ(π΄ / 2))β2) Β· 2)) = ((1 + 1)
β (2 Β· ((cosβ(π΄ / 2))β2)))) |
67 | | subdir 11596 |
. . . . . . . . . . 11
β’ ((1
β β β§ ((cosβ(π΄ / 2))β2) β β β§ 2 β
β) β ((1 β ((cosβ(π΄ / 2))β2)) Β· 2) = ((1 Β·
2) β (((cosβ(π΄
/ 2))β2) Β· 2))) |
68 | 49, 58, 67 | mp3an13 1453 |
. . . . . . . . . 10
β’
(((cosβ(π΄ /
2))β2) β β β ((1 β ((cosβ(π΄ / 2))β2)) Β· 2) = ((1 Β·
2) β (((cosβ(π΄
/ 2))β2) Β· 2))) |
69 | 57, 68 | syl 17 |
. . . . . . . . 9
β’ ((π΄ / 2) β β β ((1
β ((cosβ(π΄ /
2))β2)) Β· 2) = ((1 Β· 2) β (((cosβ(π΄ / 2))β2) Β·
2))) |
70 | | mulcl 11142 |
. . . . . . . . . . 11
β’ ((2
β β β§ ((cosβ(π΄ / 2))β2) β β) β (2
Β· ((cosβ(π΄ /
2))β2)) β β) |
71 | 58, 57, 70 | sylancr 588 |
. . . . . . . . . 10
β’ ((π΄ / 2) β β β (2
Β· ((cosβ(π΄ /
2))β2)) β β) |
72 | | subsub3 11440 |
. . . . . . . . . . 11
β’ ((1
β β β§ (2 Β· ((cosβ(π΄ / 2))β2)) β β β§ 1
β β) β (1 β ((2 Β· ((cosβ(π΄ / 2))β2)) β 1)) = ((1 + 1)
β (2 Β· ((cosβ(π΄ / 2))β2)))) |
73 | 49, 49, 72 | mp3an13 1453 |
. . . . . . . . . 10
β’ ((2
Β· ((cosβ(π΄ /
2))β2)) β β β (1 β ((2 Β· ((cosβ(π΄ / 2))β2)) β 1)) =
((1 + 1) β (2 Β· ((cosβ(π΄ / 2))β2)))) |
74 | 71, 73 | syl 17 |
. . . . . . . . 9
β’ ((π΄ / 2) β β β (1
β ((2 Β· ((cosβ(π΄ / 2))β2)) β 1)) = ((1 + 1)
β (2 Β· ((cosβ(π΄ / 2))β2)))) |
75 | 66, 69, 74 | 3eqtr4d 2787 |
. . . . . . . 8
β’ ((π΄ / 2) β β β ((1
β ((cosβ(π΄ /
2))β2)) Β· 2) = (1 β ((2 Β· ((cosβ(π΄ / 2))β2)) β
1))) |
76 | | sincl 16015 |
. . . . . . . . . . . 12
β’ ((π΄ / 2) β β β
(sinβ(π΄ / 2)) β
β) |
77 | 76 | sqcld 14056 |
. . . . . . . . . . 11
β’ ((π΄ / 2) β β β
((sinβ(π΄ /
2))β2) β β) |
78 | 77, 57 | pncand 11520 |
. . . . . . . . . 10
β’ ((π΄ / 2) β β β
((((sinβ(π΄ /
2))β2) + ((cosβ(π΄ / 2))β2)) β ((cosβ(π΄ / 2))β2)) =
((sinβ(π΄ /
2))β2)) |
79 | | sincossq 16065 |
. . . . . . . . . . 11
β’ ((π΄ / 2) β β β
(((sinβ(π΄ /
2))β2) + ((cosβ(π΄ / 2))β2)) = 1) |
80 | 79 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((π΄ / 2) β β β
((((sinβ(π΄ /
2))β2) + ((cosβ(π΄ / 2))β2)) β ((cosβ(π΄ / 2))β2)) = (1 β
((cosβ(π΄ /
2))β2))) |
81 | 78, 80 | eqtr3d 2779 |
. . . . . . . . 9
β’ ((π΄ / 2) β β β
((sinβ(π΄ /
2))β2) = (1 β ((cosβ(π΄ / 2))β2))) |
82 | 81 | oveq1d 7377 |
. . . . . . . 8
β’ ((π΄ / 2) β β β
(((sinβ(π΄ /
2))β2) Β· 2) = ((1 β ((cosβ(π΄ / 2))β2)) Β·
2)) |
83 | | cos2t 16067 |
. . . . . . . . 9
β’ ((π΄ / 2) β β β
(cosβ(2 Β· (π΄ /
2))) = ((2 Β· ((cosβ(π΄ / 2))β2)) β 1)) |
84 | 83 | oveq2d 7378 |
. . . . . . . 8
β’ ((π΄ / 2) β β β (1
β (cosβ(2 Β· (π΄ / 2)))) = (1 β ((2 Β·
((cosβ(π΄ /
2))β2)) β 1))) |
85 | 75, 82, 84 | 3eqtr4d 2787 |
. . . . . . 7
β’ ((π΄ / 2) β β β
(((sinβ(π΄ /
2))β2) Β· 2) = (1 β (cosβ(2 Β· (π΄ / 2))))) |
86 | 55, 85 | syl 17 |
. . . . . 6
β’ (π΄ β β β
(((sinβ(π΄ /
2))β2) Β· 2) = (1 β (cosβ(2 Β· (π΄ / 2))))) |
87 | | 2ne0 12264 |
. . . . . . . . 9
β’ 2 β
0 |
88 | | divcan2 11828 |
. . . . . . . . 9
β’ ((π΄ β β β§ 2 β
β β§ 2 β 0) β (2 Β· (π΄ / 2)) = π΄) |
89 | 58, 87, 88 | mp3an23 1454 |
. . . . . . . 8
β’ (π΄ β β β (2
Β· (π΄ / 2)) = π΄) |
90 | 89 | fveq2d 6851 |
. . . . . . 7
β’ (π΄ β β β
(cosβ(2 Β· (π΄ /
2))) = (cosβπ΄)) |
91 | 90 | oveq2d 7378 |
. . . . . 6
β’ (π΄ β β β (1
β (cosβ(2 Β· (π΄ / 2)))) = (1 β (cosβπ΄))) |
92 | 86, 91 | eqtrd 2777 |
. . . . 5
β’ (π΄ β β β
(((sinβ(π΄ /
2))β2) Β· 2) = (1 β (cosβπ΄))) |
93 | 92 | oveq1d 7377 |
. . . 4
β’ (π΄ β β β
((((sinβ(π΄ /
2))β2) Β· 2) / 2) = ((1 β (cosβπ΄)) / 2)) |
94 | 55 | sincld 16019 |
. . . . . 6
β’ (π΄ β β β
(sinβ(π΄ / 2)) β
β) |
95 | 94 | sqcld 14056 |
. . . . 5
β’ (π΄ β β β
((sinβ(π΄ /
2))β2) β β) |
96 | | divcan4 11847 |
. . . . . 6
β’
((((sinβ(π΄ /
2))β2) β β β§ 2 β β β§ 2 β 0) β
((((sinβ(π΄ /
2))β2) Β· 2) / 2) = ((sinβ(π΄ / 2))β2)) |
97 | 58, 87, 96 | mp3an23 1454 |
. . . . 5
β’
(((sinβ(π΄ /
2))β2) β β β ((((sinβ(π΄ / 2))β2) Β· 2) / 2) =
((sinβ(π΄ /
2))β2)) |
98 | 95, 97 | syl 17 |
. . . 4
β’ (π΄ β β β
((((sinβ(π΄ /
2))β2) Β· 2) / 2) = ((sinβ(π΄ / 2))β2)) |
99 | 54, 93, 98 | 3eqtr2rd 2784 |
. . 3
β’ (π΄ β β β
((sinβ(π΄ /
2))β2) = ((ββ((1 β (cosβπ΄)) / 2))β2)) |
100 | 48, 99 | syl 17 |
. 2
β’ (π΄ β (0[,](2 Β· Ο))
β ((sinβ(π΄ /
2))β2) = ((ββ((1 β (cosβπ΄)) / 2))β2)) |
101 | 9, 24, 45, 47, 100 | sq11d 14168 |
1
β’ (π΄ β (0[,](2 Β· Ο))
β (sinβ(π΄ / 2))
= (ββ((1 β (cosβπ΄)) / 2))) |