# Metamath Proof Explorer

## Theorem cospi

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

Ref Expression
Assertion cospi ${⊢}\mathrm{cos}\mathrm{\pi }=-1$

### Proof

Step Hyp Ref Expression
1 picn ${⊢}\mathrm{\pi }\in ℂ$
2 2cn ${⊢}2\in ℂ$
3 2ne0 ${⊢}2\ne 0$
4 1 2 3 divcli ${⊢}\frac{\mathrm{\pi }}{2}\in ℂ$
5 cos2t ${⊢}\frac{\mathrm{\pi }}{2}\in ℂ\to \mathrm{cos}2\left(\frac{\mathrm{\pi }}{2}\right)=2{\mathrm{cos}\left(\frac{\mathrm{\pi }}{2}\right)}^{2}-1$
6 4 5 ax-mp ${⊢}\mathrm{cos}2\left(\frac{\mathrm{\pi }}{2}\right)=2{\mathrm{cos}\left(\frac{\mathrm{\pi }}{2}\right)}^{2}-1$
7 1 2 3 divcan2i ${⊢}2\left(\frac{\mathrm{\pi }}{2}\right)=\mathrm{\pi }$
8 7 fveq2i ${⊢}\mathrm{cos}2\left(\frac{\mathrm{\pi }}{2}\right)=\mathrm{cos}\mathrm{\pi }$
9 coshalfpi ${⊢}\mathrm{cos}\left(\frac{\mathrm{\pi }}{2}\right)=0$
10 9 oveq1i ${⊢}{\mathrm{cos}\left(\frac{\mathrm{\pi }}{2}\right)}^{2}={0}^{2}$
11 sq0 ${⊢}{0}^{2}=0$
12 10 11 eqtri ${⊢}{\mathrm{cos}\left(\frac{\mathrm{\pi }}{2}\right)}^{2}=0$
13 12 oveq2i ${⊢}2{\mathrm{cos}\left(\frac{\mathrm{\pi }}{2}\right)}^{2}=2\cdot 0$
14 2t0e0 ${⊢}2\cdot 0=0$
15 13 14 eqtri ${⊢}2{\mathrm{cos}\left(\frac{\mathrm{\pi }}{2}\right)}^{2}=0$
16 15 oveq1i ${⊢}2{\mathrm{cos}\left(\frac{\mathrm{\pi }}{2}\right)}^{2}-1=0-1$
17 df-neg ${⊢}-1=0-1$
18 16 17 eqtr4i ${⊢}2{\mathrm{cos}\left(\frac{\mathrm{\pi }}{2}\right)}^{2}-1=-1$
19 6 8 18 3eqtr3i ${⊢}\mathrm{cos}\mathrm{\pi }=-1$