Metamath Proof Explorer


Theorem cospi

Description: The cosine of _pi is -u 1 . (Contributed by Paul Chapman, 23-Jan-2008)

Ref Expression
Assertion cospi cosπ=1

Proof

Step Hyp Ref Expression
1 picn π
2 2cn 2
3 2ne0 20
4 1 2 3 divcli π2
5 cos2t π2cos2π2=2cosπ221
6 4 5 ax-mp cos2π2=2cosπ221
7 1 2 3 divcan2i 2π2=π
8 7 fveq2i cos2π2=cosπ
9 coshalfpi cosπ2=0
10 9 oveq1i cosπ22=02
11 sq0 02=0
12 10 11 eqtri cosπ22=0
13 12 oveq2i 2cosπ22=20
14 2t0e0 20=0
15 13 14 eqtri 2cosπ22=0
16 15 oveq1i 2cosπ221=01
17 df-neg 1=01
18 16 17 eqtr4i 2cosπ221=1
19 6 8 18 3eqtr3i cosπ=1