Description: The sine of 2 _pi is 0. (Contributed by Paul Chapman, 23-Jan-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | sin2pi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | picn | |
|
2 | sin2t | |
|
3 | 1 2 | ax-mp | |
4 | sinpi | |
|
5 | cospi | |
|
6 | 4 5 | oveq12i | |
7 | neg1cn | |
|
8 | 7 | mul02i | |
9 | 6 8 | eqtri | |
10 | 9 | oveq2i | |
11 | 2t0e0 | |
|
12 | 10 11 | eqtri | |
13 | 3 12 | eqtri | |