Metamath Proof Explorer

Theorem cos2pi

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

Ref Expression
Assertion cos2pi ${⊢}\mathrm{cos}2\mathrm{\pi }=1$

Proof

Step Hyp Ref Expression
1 picn ${⊢}\mathrm{\pi }\in ℂ$
2 cos2t ${⊢}\mathrm{\pi }\in ℂ\to \mathrm{cos}2\mathrm{\pi }=2{\mathrm{cos}\mathrm{\pi }}^{2}-1$
3 1 2 ax-mp ${⊢}\mathrm{cos}2\mathrm{\pi }=2{\mathrm{cos}\mathrm{\pi }}^{2}-1$
4 cospi ${⊢}\mathrm{cos}\mathrm{\pi }=-1$
5 4 oveq1i ${⊢}{\mathrm{cos}\mathrm{\pi }}^{2}={\left(-1\right)}^{2}$
6 ax-1cn ${⊢}1\in ℂ$
7 sqneg ${⊢}1\in ℂ\to {\left(-1\right)}^{2}={1}^{2}$
8 6 7 ax-mp ${⊢}{\left(-1\right)}^{2}={1}^{2}$
9 sq1 ${⊢}{1}^{2}=1$
10 5 8 9 3eqtri ${⊢}{\mathrm{cos}\mathrm{\pi }}^{2}=1$
11 10 oveq2i ${⊢}2{\mathrm{cos}\mathrm{\pi }}^{2}=2\cdot 1$
12 2t1e2 ${⊢}2\cdot 1=2$
13 11 12 eqtri ${⊢}2{\mathrm{cos}\mathrm{\pi }}^{2}=2$
14 13 oveq1i ${⊢}2{\mathrm{cos}\mathrm{\pi }}^{2}-1=2-1$
15 2m1e1 ${⊢}2-1=1$
16 3 14 15 3eqtri ${⊢}\mathrm{cos}2\mathrm{\pi }=1$