Step | Hyp | Ref
| Expression |
1 | | cos2t 16065 |
. 2
β’ (π΄ β β β
(cosβ(2 Β· π΄))
= ((2 Β· ((cosβπ΄)β2)) β 1)) |
2 | | 2cn 12233 |
. . . . . . 7
β’ 2 β
β |
3 | | sincl 16013 |
. . . . . . . 8
β’ (π΄ β β β
(sinβπ΄) β
β) |
4 | 3 | sqcld 14055 |
. . . . . . 7
β’ (π΄ β β β
((sinβπ΄)β2)
β β) |
5 | | coscl 16014 |
. . . . . . . 8
β’ (π΄ β β β
(cosβπ΄) β
β) |
6 | 5 | sqcld 14055 |
. . . . . . 7
β’ (π΄ β β β
((cosβπ΄)β2)
β β) |
7 | | adddi 11145 |
. . . . . . 7
β’ ((2
β β β§ ((sinβπ΄)β2) β β β§
((cosβπ΄)β2)
β β) β (2 Β· (((sinβπ΄)β2) + ((cosβπ΄)β2))) = ((2 Β· ((sinβπ΄)β2)) + (2 Β·
((cosβπ΄)β2)))) |
8 | 2, 4, 6, 7 | mp3an2i 1467 |
. . . . . 6
β’ (π΄ β β β (2
Β· (((sinβπ΄)β2) + ((cosβπ΄)β2))) = ((2 Β· ((sinβπ΄)β2)) + (2 Β·
((cosβπ΄)β2)))) |
9 | | sincossq 16063 |
. . . . . . 7
β’ (π΄ β β β
(((sinβπ΄)β2) +
((cosβπ΄)β2)) =
1) |
10 | 9 | oveq2d 7374 |
. . . . . 6
β’ (π΄ β β β (2
Β· (((sinβπ΄)β2) + ((cosβπ΄)β2))) = (2 Β·
1)) |
11 | 8, 10 | eqtr3d 2775 |
. . . . 5
β’ (π΄ β β β ((2
Β· ((sinβπ΄)β2)) + (2 Β· ((cosβπ΄)β2))) = (2 Β·
1)) |
12 | | 2t1e2 12321 |
. . . . 5
β’ (2
Β· 1) = 2 |
13 | 11, 12 | eqtrdi 2789 |
. . . 4
β’ (π΄ β β β ((2
Β· ((sinβπ΄)β2)) + (2 Β· ((cosβπ΄)β2))) =
2) |
14 | | mulcl 11140 |
. . . . . 6
β’ ((2
β β β§ ((sinβπ΄)β2) β β) β (2 Β·
((sinβπ΄)β2))
β β) |
15 | 2, 4, 14 | sylancr 588 |
. . . . 5
β’ (π΄ β β β (2
Β· ((sinβπ΄)β2)) β β) |
16 | | mulcl 11140 |
. . . . . 6
β’ ((2
β β β§ ((cosβπ΄)β2) β β) β (2 Β·
((cosβπ΄)β2))
β β) |
17 | 2, 6, 16 | sylancr 588 |
. . . . 5
β’ (π΄ β β β (2
Β· ((cosβπ΄)β2)) β β) |
18 | | subadd 11409 |
. . . . 5
β’ ((2
β β β§ (2 Β· ((sinβπ΄)β2)) β β β§ (2 Β·
((cosβπ΄)β2))
β β) β ((2 β (2 Β· ((sinβπ΄)β2))) = (2 Β· ((cosβπ΄)β2)) β ((2 Β·
((sinβπ΄)β2)) +
(2 Β· ((cosβπ΄)β2))) = 2)) |
19 | 2, 15, 17, 18 | mp3an2i 1467 |
. . . 4
β’ (π΄ β β β ((2
β (2 Β· ((sinβπ΄)β2))) = (2 Β· ((cosβπ΄)β2)) β ((2 Β·
((sinβπ΄)β2)) +
(2 Β· ((cosβπ΄)β2))) = 2)) |
20 | 13, 19 | mpbird 257 |
. . 3
β’ (π΄ β β β (2
β (2 Β· ((sinβπ΄)β2))) = (2 Β· ((cosβπ΄)β2))) |
21 | 20 | oveq1d 7373 |
. 2
β’ (π΄ β β β ((2
β (2 Β· ((sinβπ΄)β2))) β 1) = ((2 Β·
((cosβπ΄)β2))
β 1)) |
22 | | ax-1cn 11114 |
. . . . 5
β’ 1 β
β |
23 | | sub32 11440 |
. . . . 5
β’ ((2
β β β§ (2 Β· ((sinβπ΄)β2)) β β β§ 1 β
β) β ((2 β (2 Β· ((sinβπ΄)β2))) β 1) = ((2 β 1)
β (2 Β· ((sinβπ΄)β2)))) |
24 | 2, 22, 23 | mp3an13 1453 |
. . . 4
β’ ((2
Β· ((sinβπ΄)β2)) β β β ((2 β
(2 Β· ((sinβπ΄)β2))) β 1) = ((2 β 1)
β (2 Β· ((sinβπ΄)β2)))) |
25 | 15, 24 | syl 17 |
. . 3
β’ (π΄ β β β ((2
β (2 Β· ((sinβπ΄)β2))) β 1) = ((2 β 1)
β (2 Β· ((sinβπ΄)β2)))) |
26 | | 2m1e1 12284 |
. . . 4
β’ (2
β 1) = 1 |
27 | 26 | oveq1i 7368 |
. . 3
β’ ((2
β 1) β (2 Β· ((sinβπ΄)β2))) = (1 β (2 Β·
((sinβπ΄)β2))) |
28 | 25, 27 | eqtrdi 2789 |
. 2
β’ (π΄ β β β ((2
β (2 Β· ((sinβπ΄)β2))) β 1) = (1 β (2
Β· ((sinβπ΄)β2)))) |
29 | 1, 21, 28 | 3eqtr2d 2779 |
1
β’ (π΄ β β β
(cosβ(2 Β· π΄))
= (1 β (2 Β· ((sinβπ΄)β2)))) |