Description: The cosine of _pi is -u 1 . (Contributed by Paul Chapman, 23-Jan-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | cospi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | picn | |
|
2 | 2cn | |
|
3 | 2ne0 | |
|
4 | 1 2 3 | divcli | |
5 | cos2t | |
|
6 | 4 5 | ax-mp | |
7 | 1 2 3 | divcan2i | |
8 | 7 | fveq2i | |
9 | coshalfpi | |
|
10 | 9 | oveq1i | |
11 | sq0 | |
|
12 | 10 11 | eqtri | |
13 | 12 | oveq2i | |
14 | 2t0e0 | |
|
15 | 13 14 | eqtri | |
16 | 15 | oveq1i | |
17 | df-neg | |
|
18 | 16 17 | eqtr4i | |
19 | 6 8 18 | 3eqtr3i | |