Step | Hyp | Ref
| Expression |
1 | | coscl 16073 |
. . . 4
β’ (π΄ β β β
(cosβπ΄) β
β) |
2 | 1 | sqcld 14110 |
. . 3
β’ (π΄ β β β
((cosβπ΄)β2)
β β) |
3 | | ax-1cn 11165 |
. . . 4
β’ 1 β
β |
4 | | subsub3 11491 |
. . . 4
β’
((((cosβπ΄)β2) β β β§ 1 β
β β§ ((cosβπ΄)β2) β β) β
(((cosβπ΄)β2)
β (1 β ((cosβπ΄)β2))) = ((((cosβπ΄)β2) + ((cosβπ΄)β2)) β
1)) |
5 | 3, 4 | mp3an2 1445 |
. . 3
β’
((((cosβπ΄)β2) β β β§
((cosβπ΄)β2)
β β) β (((cosβπ΄)β2) β (1 β
((cosβπ΄)β2))) =
((((cosβπ΄)β2) +
((cosβπ΄)β2))
β 1)) |
6 | 2, 2, 5 | syl2anc 583 |
. 2
β’ (π΄ β β β
(((cosβπ΄)β2)
β (1 β ((cosβπ΄)β2))) = ((((cosβπ΄)β2) + ((cosβπ΄)β2)) β
1)) |
7 | | cosadd 16111 |
. . . . 5
β’ ((π΄ β β β§ π΄ β β) β
(cosβ(π΄ + π΄)) = (((cosβπ΄) Β· (cosβπ΄)) β ((sinβπ΄) Β· (sinβπ΄)))) |
8 | 7 | anidms 566 |
. . . 4
β’ (π΄ β β β
(cosβ(π΄ + π΄)) = (((cosβπ΄) Β· (cosβπ΄)) β ((sinβπ΄) Β· (sinβπ΄)))) |
9 | | 2times 12347 |
. . . . 5
β’ (π΄ β β β (2
Β· π΄) = (π΄ + π΄)) |
10 | 9 | fveq2d 6886 |
. . . 4
β’ (π΄ β β β
(cosβ(2 Β· π΄))
= (cosβ(π΄ + π΄))) |
11 | 1 | sqvald 14109 |
. . . . 5
β’ (π΄ β β β
((cosβπ΄)β2) =
((cosβπ΄) Β·
(cosβπ΄))) |
12 | | sincl 16072 |
. . . . . 6
β’ (π΄ β β β
(sinβπ΄) β
β) |
13 | 12 | sqvald 14109 |
. . . . 5
β’ (π΄ β β β
((sinβπ΄)β2) =
((sinβπ΄) Β·
(sinβπ΄))) |
14 | 11, 13 | oveq12d 7420 |
. . . 4
β’ (π΄ β β β
(((cosβπ΄)β2)
β ((sinβπ΄)β2)) = (((cosβπ΄) Β· (cosβπ΄)) β ((sinβπ΄) Β· (sinβπ΄)))) |
15 | 8, 10, 14 | 3eqtr4d 2774 |
. . 3
β’ (π΄ β β β
(cosβ(2 Β· π΄))
= (((cosβπ΄)β2)
β ((sinβπ΄)β2))) |
16 | 12 | sqcld 14110 |
. . . . . . 7
β’ (π΄ β β β
((sinβπ΄)β2)
β β) |
17 | 16, 2 | addcomd 11415 |
. . . . . 6
β’ (π΄ β β β
(((sinβπ΄)β2) +
((cosβπ΄)β2)) =
(((cosβπ΄)β2) +
((sinβπ΄)β2))) |
18 | | sincossq 16122 |
. . . . . 6
β’ (π΄ β β β
(((sinβπ΄)β2) +
((cosβπ΄)β2)) =
1) |
19 | 17, 18 | eqtr3d 2766 |
. . . . 5
β’ (π΄ β β β
(((cosβπ΄)β2) +
((sinβπ΄)β2)) =
1) |
20 | | subadd 11462 |
. . . . . 6
β’ ((1
β β β§ ((cosβπ΄)β2) β β β§
((sinβπ΄)β2)
β β) β ((1 β ((cosβπ΄)β2)) = ((sinβπ΄)β2) β (((cosβπ΄)β2) + ((sinβπ΄)β2)) =
1)) |
21 | 3, 2, 16, 20 | mp3an2i 1462 |
. . . . 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 7418 |
. . 3
β’ (π΄ β β β
(((cosβπ΄)β2)
β (1 β ((cosβπ΄)β2))) = (((cosβπ΄)β2) β ((sinβπ΄)β2))) |
24 | 15, 23 | eqtr4d 2767 |
. 2
β’ (π΄ β β β
(cosβ(2 Β· π΄))
= (((cosβπ΄)β2)
β (1 β ((cosβπ΄)β2)))) |
25 | 2 | 2timesd 12454 |
. . 3
β’ (π΄ β β β (2
Β· ((cosβπ΄)β2)) = (((cosβπ΄)β2) + ((cosβπ΄)β2))) |
26 | 25 | oveq1d 7417 |
. 2
β’ (π΄ β β β ((2
Β· ((cosβπ΄)β2)) β 1) = ((((cosβπ΄)β2) + ((cosβπ΄)β2)) β
1)) |
27 | 6, 24, 26 | 3eqtr4d 2774 |
1
β’ (π΄ β β β
(cosβ(2 Β· π΄))
= ((2 Β· ((cosβπ΄)β2)) β 1)) |