Step | Hyp | Ref
| Expression |
1 | | pire 25831 |
. . . . . . 7
โข ฯ
โ โ |
2 | 1 | renegcli 11469 |
. . . . . 6
โข -ฯ
โ โ |
3 | | iccssre 13353 |
. . . . . 6
โข ((-ฯ
โ โ โง ฯ โ โ) โ (-ฯ[,]ฯ) โ
โ) |
4 | 2, 1, 3 | mp2an 691 |
. . . . 5
โข
(-ฯ[,]ฯ) โ โ |
5 | 4 | sseli 3945 |
. . . 4
โข (๐ด โ (-ฯ[,]ฯ) โ
๐ด โ
โ) |
6 | 5 | rehalfcld 12407 |
. . 3
โข (๐ด โ (-ฯ[,]ฯ) โ
(๐ด / 2) โ
โ) |
7 | 6 | recoscld 16033 |
. 2
โข (๐ด โ (-ฯ[,]ฯ) โ
(cosโ(๐ด / 2)) โ
โ) |
8 | | 1re 11162 |
. . . . 5
โข 1 โ
โ |
9 | 5 | recoscld 16033 |
. . . . 5
โข (๐ด โ (-ฯ[,]ฯ) โ
(cosโ๐ด) โ
โ) |
10 | | readdcl 11141 |
. . . . 5
โข ((1
โ โ โง (cosโ๐ด) โ โ) โ (1 +
(cosโ๐ด)) โ
โ) |
11 | 8, 9, 10 | sylancr 588 |
. . . 4
โข (๐ด โ (-ฯ[,]ฯ) โ (1
+ (cosโ๐ด)) โ
โ) |
12 | 11 | rehalfcld 12407 |
. . 3
โข (๐ด โ (-ฯ[,]ฯ) โ
((1 + (cosโ๐ด)) / 2)
โ โ) |
13 | | cosbnd 16070 |
. . . . . 6
โข (๐ด โ โ โ (-1 โค
(cosโ๐ด) โง
(cosโ๐ด) โค
1)) |
14 | 13 | simpld 496 |
. . . . 5
โข (๐ด โ โ โ -1 โค
(cosโ๐ด)) |
15 | | recoscl 16030 |
. . . . . 6
โข (๐ด โ โ โ
(cosโ๐ด) โ
โ) |
16 | | recn 11148 |
. . . . . . . . 9
โข
((cosโ๐ด)
โ โ โ (cosโ๐ด) โ โ) |
17 | | recn 11148 |
. . . . . . . . 9
โข (1 โ
โ โ 1 โ โ) |
18 | | subneg 11457 |
. . . . . . . . . 10
โข
(((cosโ๐ด)
โ โ โง 1 โ โ) โ ((cosโ๐ด) โ -1) = ((cosโ๐ด) + 1)) |
19 | | addcom 11348 |
. . . . . . . . . . 11
โข ((1
โ โ โง (cosโ๐ด) โ โ) โ (1 +
(cosโ๐ด)) =
((cosโ๐ด) +
1)) |
20 | 19 | ancoms 460 |
. . . . . . . . . 10
โข
(((cosโ๐ด)
โ โ โง 1 โ โ) โ (1 + (cosโ๐ด)) = ((cosโ๐ด) + 1)) |
21 | 18, 20 | eqtr4d 2780 |
. . . . . . . . 9
โข
(((cosโ๐ด)
โ โ โง 1 โ โ) โ ((cosโ๐ด) โ -1) = (1 + (cosโ๐ด))) |
22 | 16, 17, 21 | syl2an 597 |
. . . . . . . 8
โข
(((cosโ๐ด)
โ โ โง 1 โ โ) โ ((cosโ๐ด) โ -1) = (1 + (cosโ๐ด))) |
23 | 22 | breq2d 5122 |
. . . . . . 7
โข
(((cosโ๐ด)
โ โ โง 1 โ โ) โ (0 โค ((cosโ๐ด) โ -1) โ 0 โค (1 +
(cosโ๐ด)))) |
24 | | renegcl 11471 |
. . . . . . . 8
โข (1 โ
โ โ -1 โ โ) |
25 | | subge0 11675 |
. . . . . . . 8
โข
(((cosโ๐ด)
โ โ โง -1 โ โ) โ (0 โค ((cosโ๐ด) โ -1) โ -1 โค
(cosโ๐ด))) |
26 | 24, 25 | sylan2 594 |
. . . . . . 7
โข
(((cosโ๐ด)
โ โ โง 1 โ โ) โ (0 โค ((cosโ๐ด) โ -1) โ -1 โค
(cosโ๐ด))) |
27 | 10 | ancoms 460 |
. . . . . . . 8
โข
(((cosโ๐ด)
โ โ โง 1 โ โ) โ (1 + (cosโ๐ด)) โ โ) |
28 | | halfnneg2 12391 |
. . . . . . . 8
โข ((1 +
(cosโ๐ด)) โ
โ โ (0 โค (1 + (cosโ๐ด)) โ 0 โค ((1 + (cosโ๐ด)) / 2))) |
29 | 27, 28 | syl 17 |
. . . . . . 7
โข
(((cosโ๐ด)
โ โ โง 1 โ โ) โ (0 โค (1 + (cosโ๐ด)) โ 0 โค ((1 +
(cosโ๐ด)) /
2))) |
30 | 23, 26, 29 | 3bitr3d 309 |
. . . . . 6
โข
(((cosโ๐ด)
โ โ โง 1 โ โ) โ (-1 โค (cosโ๐ด) โ 0 โค ((1 +
(cosโ๐ด)) /
2))) |
31 | 15, 8, 30 | sylancl 587 |
. . . . 5
โข (๐ด โ โ โ (-1 โค
(cosโ๐ด) โ 0 โค
((1 + (cosโ๐ด)) /
2))) |
32 | 14, 31 | mpbid 231 |
. . . 4
โข (๐ด โ โ โ 0 โค
((1 + (cosโ๐ด)) /
2)) |
33 | 5, 32 | syl 17 |
. . 3
โข (๐ด โ (-ฯ[,]ฯ) โ 0
โค ((1 + (cosโ๐ด)) /
2)) |
34 | 12, 33 | resqrtcld 15309 |
. 2
โข (๐ด โ (-ฯ[,]ฯ) โ
(โโ((1 + (cosโ๐ด)) / 2)) โ โ) |
35 | 2, 1 | elicc2i 13337 |
. . . 4
โข (๐ด โ (-ฯ[,]ฯ) โ
(๐ด โ โ โง
-ฯ โค ๐ด โง ๐ด โค ฯ)) |
36 | | 2re 12234 |
. . . . . . . . . . 11
โข 2 โ
โ |
37 | | 2pos 12263 |
. . . . . . . . . . 11
โข 0 <
2 |
38 | 36, 37 | pm3.2i 472 |
. . . . . . . . . 10
โข (2 โ
โ โง 0 < 2) |
39 | | lediv1 12027 |
. . . . . . . . . 10
โข ((-ฯ
โ โ โง ๐ด
โ โ โง (2 โ โ โง 0 < 2)) โ (-ฯ โค
๐ด โ (-ฯ / 2) โค
(๐ด / 2))) |
40 | 2, 38, 39 | mp3an13 1453 |
. . . . . . . . 9
โข (๐ด โ โ โ (-ฯ
โค ๐ด โ (-ฯ / 2)
โค (๐ด /
2))) |
41 | | picn 25832 |
. . . . . . . . . . 11
โข ฯ
โ โ |
42 | | 2cn 12235 |
. . . . . . . . . . 11
โข 2 โ
โ |
43 | | 2ne0 12264 |
. . . . . . . . . . 11
โข 2 โ
0 |
44 | | divneg 11854 |
. . . . . . . . . . 11
โข ((ฯ
โ โ โง 2 โ โ โง 2 โ 0) โ -(ฯ / 2) =
(-ฯ / 2)) |
45 | 41, 42, 43, 44 | mp3an 1462 |
. . . . . . . . . 10
โข -(ฯ /
2) = (-ฯ / 2) |
46 | 45 | breq1i 5117 |
. . . . . . . . 9
โข (-(ฯ /
2) โค (๐ด / 2) โ
(-ฯ / 2) โค (๐ด /
2)) |
47 | 40, 46 | bitr4di 289 |
. . . . . . . 8
โข (๐ด โ โ โ (-ฯ
โค ๐ด โ -(ฯ / 2)
โค (๐ด /
2))) |
48 | | lediv1 12027 |
. . . . . . . . 9
โข ((๐ด โ โ โง ฯ
โ โ โง (2 โ โ โง 0 < 2)) โ (๐ด โค ฯ โ (๐ด / 2) โค (ฯ /
2))) |
49 | 1, 38, 48 | mp3an23 1454 |
. . . . . . . 8
โข (๐ด โ โ โ (๐ด โค ฯ โ (๐ด / 2) โค (ฯ /
2))) |
50 | 47, 49 | anbi12d 632 |
. . . . . . 7
โข (๐ด โ โ โ ((-ฯ
โค ๐ด โง ๐ด โค ฯ) โ (-(ฯ / 2)
โค (๐ด / 2) โง (๐ด / 2) โค (ฯ /
2)))) |
51 | | rehalfcl 12386 |
. . . . . . . . 9
โข (๐ด โ โ โ (๐ด / 2) โ
โ) |
52 | 51 | rexrd 11212 |
. . . . . . . 8
โข (๐ด โ โ โ (๐ด / 2) โ
โ*) |
53 | | halfpire 25837 |
. . . . . . . . . . 11
โข (ฯ /
2) โ โ |
54 | 53 | renegcli 11469 |
. . . . . . . . . 10
โข -(ฯ /
2) โ โ |
55 | 54 | rexri 11220 |
. . . . . . . . 9
โข -(ฯ /
2) โ โ* |
56 | 53 | rexri 11220 |
. . . . . . . . 9
โข (ฯ /
2) โ โ* |
57 | | elicc4 13338 |
. . . . . . . . 9
โข ((-(ฯ
/ 2) โ โ* โง (ฯ / 2) โ โ*
โง (๐ด / 2) โ
โ*) โ ((๐ด / 2) โ (-(ฯ / 2)[,](ฯ / 2))
โ (-(ฯ / 2) โค (๐ด
/ 2) โง (๐ด / 2) โค
(ฯ / 2)))) |
58 | 55, 56, 57 | mp3an12 1452 |
. . . . . . . 8
โข ((๐ด / 2) โ โ*
โ ((๐ด / 2) โ
(-(ฯ / 2)[,](ฯ / 2)) โ (-(ฯ / 2) โค (๐ด / 2) โง (๐ด / 2) โค (ฯ / 2)))) |
59 | 52, 58 | syl 17 |
. . . . . . 7
โข (๐ด โ โ โ ((๐ด / 2) โ (-(ฯ /
2)[,](ฯ / 2)) โ (-(ฯ / 2) โค (๐ด / 2) โง (๐ด / 2) โค (ฯ / 2)))) |
60 | 50, 59 | bitr4d 282 |
. . . . . 6
โข (๐ด โ โ โ ((-ฯ
โค ๐ด โง ๐ด โค ฯ) โ (๐ด / 2) โ (-(ฯ /
2)[,](ฯ / 2)))) |
61 | 60 | biimpd 228 |
. . . . 5
โข (๐ด โ โ โ ((-ฯ
โค ๐ด โง ๐ด โค ฯ) โ (๐ด / 2) โ (-(ฯ /
2)[,](ฯ / 2)))) |
62 | 61 | 3impib 1117 |
. . . 4
โข ((๐ด โ โ โง -ฯ โค
๐ด โง ๐ด โค ฯ) โ (๐ด / 2) โ (-(ฯ / 2)[,](ฯ /
2))) |
63 | 35, 62 | sylbi 216 |
. . 3
โข (๐ด โ (-ฯ[,]ฯ) โ
(๐ด / 2) โ (-(ฯ /
2)[,](ฯ / 2))) |
64 | | cosq14ge0 25884 |
. . 3
โข ((๐ด / 2) โ (-(ฯ /
2)[,](ฯ / 2)) โ 0 โค (cosโ(๐ด / 2))) |
65 | 63, 64 | syl 17 |
. 2
โข (๐ด โ (-ฯ[,]ฯ) โ 0
โค (cosโ(๐ด /
2))) |
66 | 12, 33 | sqrtge0d 15312 |
. 2
โข (๐ด โ (-ฯ[,]ฯ) โ 0
โค (โโ((1 + (cosโ๐ด)) / 2))) |
67 | 5 | recnd 11190 |
. . 3
โข (๐ด โ (-ฯ[,]ฯ) โ
๐ด โ
โ) |
68 | | ax-1cn 11116 |
. . . . . . 7
โข 1 โ
โ |
69 | | coscl 16016 |
. . . . . . 7
โข (๐ด โ โ โ
(cosโ๐ด) โ
โ) |
70 | | addcl 11140 |
. . . . . . 7
โข ((1
โ โ โง (cosโ๐ด) โ โ) โ (1 +
(cosโ๐ด)) โ
โ) |
71 | 68, 69, 70 | sylancr 588 |
. . . . . 6
โข (๐ด โ โ โ (1 +
(cosโ๐ด)) โ
โ) |
72 | 71 | halfcld 12405 |
. . . . 5
โข (๐ด โ โ โ ((1 +
(cosโ๐ด)) / 2) โ
โ) |
73 | 72 | sqsqrtd 15331 |
. . . 4
โข (๐ด โ โ โ
((โโ((1 + (cosโ๐ด)) / 2))โ2) = ((1 + (cosโ๐ด)) / 2)) |
74 | | divcan2 11828 |
. . . . . . . . 9
โข ((๐ด โ โ โง 2 โ
โ โง 2 โ 0) โ (2 ยท (๐ด / 2)) = ๐ด) |
75 | 42, 43, 74 | mp3an23 1454 |
. . . . . . . 8
โข (๐ด โ โ โ (2
ยท (๐ด / 2)) = ๐ด) |
76 | 75 | fveq2d 6851 |
. . . . . . 7
โข (๐ด โ โ โ
(cosโ(2 ยท (๐ด /
2))) = (cosโ๐ด)) |
77 | | halfcl 12385 |
. . . . . . . 8
โข (๐ด โ โ โ (๐ด / 2) โ
โ) |
78 | | cos2t 16067 |
. . . . . . . 8
โข ((๐ด / 2) โ โ โ
(cosโ(2 ยท (๐ด /
2))) = ((2 ยท ((cosโ(๐ด / 2))โ2)) โ 1)) |
79 | 77, 78 | syl 17 |
. . . . . . 7
โข (๐ด โ โ โ
(cosโ(2 ยท (๐ด /
2))) = ((2 ยท ((cosโ(๐ด / 2))โ2)) โ 1)) |
80 | 76, 79 | eqtr3d 2779 |
. . . . . 6
โข (๐ด โ โ โ
(cosโ๐ด) = ((2
ยท ((cosโ(๐ด /
2))โ2)) โ 1)) |
81 | 80 | oveq2d 7378 |
. . . . 5
โข (๐ด โ โ โ (1 +
(cosโ๐ด)) = (1 + ((2
ยท ((cosโ(๐ด /
2))โ2)) โ 1))) |
82 | 81 | oveq1d 7377 |
. . . 4
โข (๐ด โ โ โ ((1 +
(cosโ๐ด)) / 2) = ((1 +
((2 ยท ((cosโ(๐ด
/ 2))โ2)) โ 1)) / 2)) |
83 | 77 | coscld 16020 |
. . . . . 6
โข (๐ด โ โ โ
(cosโ(๐ด / 2)) โ
โ) |
84 | 83 | sqcld 14056 |
. . . . 5
โข (๐ด โ โ โ
((cosโ(๐ด /
2))โ2) โ โ) |
85 | | mulcl 11142 |
. . . . . . . . 9
โข ((2
โ โ โง ((cosโ(๐ด / 2))โ2) โ โ) โ (2
ยท ((cosโ(๐ด /
2))โ2)) โ โ) |
86 | 42, 85 | mpan 689 |
. . . . . . . 8
โข
(((cosโ(๐ด /
2))โ2) โ โ โ (2 ยท ((cosโ(๐ด / 2))โ2)) โ
โ) |
87 | | pncan3 11416 |
. . . . . . . 8
โข ((1
โ โ โง (2 ยท ((cosโ(๐ด / 2))โ2)) โ โ) โ (1 +
((2 ยท ((cosโ(๐ด
/ 2))โ2)) โ 1)) = (2 ยท ((cosโ(๐ด / 2))โ2))) |
88 | 68, 86, 87 | sylancr 588 |
. . . . . . 7
โข
(((cosโ(๐ด /
2))โ2) โ โ โ (1 + ((2 ยท ((cosโ(๐ด / 2))โ2)) โ 1)) = (2
ยท ((cosโ(๐ด /
2))โ2))) |
89 | 88 | oveq1d 7377 |
. . . . . 6
โข
(((cosโ(๐ด /
2))โ2) โ โ โ ((1 + ((2 ยท ((cosโ(๐ด / 2))โ2)) โ 1)) / 2)
= ((2 ยท ((cosโ(๐ด / 2))โ2)) / 2)) |
90 | | divcan3 11846 |
. . . . . . 7
โข
((((cosโ(๐ด /
2))โ2) โ โ โง 2 โ โ โง 2 โ 0) โ ((2
ยท ((cosโ(๐ด /
2))โ2)) / 2) = ((cosโ(๐ด / 2))โ2)) |
91 | 42, 43, 90 | mp3an23 1454 |
. . . . . 6
โข
(((cosโ(๐ด /
2))โ2) โ โ โ ((2 ยท ((cosโ(๐ด / 2))โ2)) / 2) = ((cosโ(๐ด / 2))โ2)) |
92 | 89, 91 | eqtrd 2777 |
. . . . 5
โข
(((cosโ(๐ด /
2))โ2) โ โ โ ((1 + ((2 ยท ((cosโ(๐ด / 2))โ2)) โ 1)) / 2)
= ((cosโ(๐ด /
2))โ2)) |
93 | 84, 92 | syl 17 |
. . . 4
โข (๐ด โ โ โ ((1 + ((2
ยท ((cosโ(๐ด /
2))โ2)) โ 1)) / 2) = ((cosโ(๐ด / 2))โ2)) |
94 | 73, 82, 93 | 3eqtrrd 2782 |
. . 3
โข (๐ด โ โ โ
((cosโ(๐ด /
2))โ2) = ((โโ((1 + (cosโ๐ด)) / 2))โ2)) |
95 | 67, 94 | syl 17 |
. 2
โข (๐ด โ (-ฯ[,]ฯ) โ
((cosโ(๐ด /
2))โ2) = ((โโ((1 + (cosโ๐ด)) / 2))โ2)) |
96 | 7, 34, 65, 66, 95 | sq11d 14168 |
1
โข (๐ด โ (-ฯ[,]ฯ) โ
(cosโ(๐ด / 2)) =
(โโ((1 + (cosโ๐ด)) / 2))) |