Step | Hyp | Ref
| Expression |
1 | | coscl 16014 |
. . . 4
β’ (π΄ β β β
(cosβπ΄) β
β) |
2 | 1 | sqcld 14055 |
. . 3
β’ (π΄ β β β
((cosβπ΄)β2)
β β) |
3 | | ax-1cn 11114 |
. . . 4
β’ 1 β
β |
4 | | subsub3 11438 |
. . . 4
β’
((((cosβπ΄)β2) β β β§ 1 β
β β§ ((cosβπ΄)β2) β β) β
(((cosβπ΄)β2)
β (1 β ((cosβπ΄)β2))) = ((((cosβπ΄)β2) + ((cosβπ΄)β2)) β
1)) |
5 | 3, 4 | mp3an2 1450 |
. . 3
β’
((((cosβπ΄)β2) β β β§
((cosβπ΄)β2)
β β) β (((cosβπ΄)β2) β (1 β
((cosβπ΄)β2))) =
((((cosβπ΄)β2) +
((cosβπ΄)β2))
β 1)) |
6 | 2, 2, 5 | syl2anc 585 |
. 2
β’ (π΄ β β β
(((cosβπ΄)β2)
β (1 β ((cosβπ΄)β2))) = ((((cosβπ΄)β2) + ((cosβπ΄)β2)) β
1)) |
7 | | cosadd 16052 |
. . . . 5
β’ ((π΄ β β β§ π΄ β β) β
(cosβ(π΄ + π΄)) = (((cosβπ΄) Β· (cosβπ΄)) β ((sinβπ΄) Β· (sinβπ΄)))) |
8 | 7 | anidms 568 |
. . . 4
β’ (π΄ β β β
(cosβ(π΄ + π΄)) = (((cosβπ΄) Β· (cosβπ΄)) β ((sinβπ΄) Β· (sinβπ΄)))) |
9 | | 2times 12294 |
. . . . 5
β’ (π΄ β β β (2
Β· π΄) = (π΄ + π΄)) |
10 | 9 | fveq2d 6847 |
. . . 4
β’ (π΄ β β β
(cosβ(2 Β· π΄))
= (cosβ(π΄ + π΄))) |
11 | 1 | sqvald 14054 |
. . . . 5
β’ (π΄ β β β
((cosβπ΄)β2) =
((cosβπ΄) Β·
(cosβπ΄))) |
12 | | sincl 16013 |
. . . . . 6
β’ (π΄ β β β
(sinβπ΄) β
β) |
13 | 12 | sqvald 14054 |
. . . . 5
β’ (π΄ β β β
((sinβπ΄)β2) =
((sinβπ΄) Β·
(sinβπ΄))) |
14 | 11, 13 | oveq12d 7376 |
. . . 4
β’ (π΄ β β β
(((cosβπ΄)β2)
β ((sinβπ΄)β2)) = (((cosβπ΄) Β· (cosβπ΄)) β ((sinβπ΄) Β· (sinβπ΄)))) |
15 | 8, 10, 14 | 3eqtr4d 2783 |
. . 3
β’ (π΄ β β β
(cosβ(2 Β· π΄))
= (((cosβπ΄)β2)
β ((sinβπ΄)β2))) |
16 | 12 | sqcld 14055 |
. . . . . . 7
β’ (π΄ β β β
((sinβπ΄)β2)
β β) |
17 | 16, 2 | addcomd 11362 |
. . . . . 6
β’ (π΄ β β β
(((sinβπ΄)β2) +
((cosβπ΄)β2)) =
(((cosβπ΄)β2) +
((sinβπ΄)β2))) |
18 | | sincossq 16063 |
. . . . . 6
β’ (π΄ β β β
(((sinβπ΄)β2) +
((cosβπ΄)β2)) =
1) |
19 | 17, 18 | eqtr3d 2775 |
. . . . 5
β’ (π΄ β β β
(((cosβπ΄)β2) +
((sinβπ΄)β2)) =
1) |
20 | | subadd 11409 |
. . . . . 6
β’ ((1
β β β§ ((cosβπ΄)β2) β β β§
((sinβπ΄)β2)
β β) β ((1 β ((cosβπ΄)β2)) = ((sinβπ΄)β2) β (((cosβπ΄)β2) + ((sinβπ΄)β2)) =
1)) |
21 | 3, 2, 16, 20 | mp3an2i 1467 |
. . . . 5
β’ (π΄ β β β ((1
β ((cosβπ΄)β2)) = ((sinβπ΄)β2) β (((cosβπ΄)β2) + ((sinβπ΄)β2)) =
1)) |
22 | 19, 21 | mpbird 257 |
. . . 4
β’ (π΄ β β β (1
β ((cosβπ΄)β2)) = ((sinβπ΄)β2)) |
23 | 22 | oveq2d 7374 |
. . 3
β’ (π΄ β β β
(((cosβπ΄)β2)
β (1 β ((cosβπ΄)β2))) = (((cosβπ΄)β2) β ((sinβπ΄)β2))) |
24 | 15, 23 | eqtr4d 2776 |
. 2
β’ (π΄ β β β
(cosβ(2 Β· π΄))
= (((cosβπ΄)β2)
β (1 β ((cosβπ΄)β2)))) |
25 | 2 | 2timesd 12401 |
. . 3
β’ (π΄ β β β (2
Β· ((cosβπ΄)β2)) = (((cosβπ΄)β2) + ((cosβπ΄)β2))) |
26 | 25 | oveq1d 7373 |
. 2
β’ (π΄ β β β ((2
Β· ((cosβπ΄)β2)) β 1) = ((((cosβπ΄)β2) + ((cosβπ΄)β2)) β
1)) |
27 | 6, 24, 26 | 3eqtr4d 2783 |
1
β’ (π΄ β β β
(cosβ(2 Β· π΄))
= ((2 Β· ((cosβπ΄)β2)) β 1)) |