This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cos2pi

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

Ref Expression
Assertion cos2pi ⊢ cos ⁡ 2 ⁢ π = 1

Proof

Step Hyp Ref Expression
1 picn ⊢ π ∈ ℂ
2 cos2t ⊢ π ∈ ℂ → cos ⁡ 2 ⁢ π = 2 ⁢ cos ⁡ π 2 − 1
3 1 2 ax-mp ⊢ cos ⁡ 2 ⁢ π = 2 ⁢ cos ⁡ π 2 − 1
4 cospi ⊢ cos ⁡ π = − 1
5 4 oveq1i ⊢ cos ⁡ π 2 = − 1 2
6 ax-1cn ⊢ 1 ∈ ℂ
7 sqneg ⊢ 1 ∈ ℂ → − 1 2 = 1 2
8 6 7 ax-mp ⊢ − 1 2 = 1 2
9 sq1 ⊢ 1 2 = 1
10 5 8 9 3eqtri ⊢ cos ⁡ π 2 = 1
11 10 oveq2i ⊢ 2 ⁢ cos ⁡ π 2 = 2 ⋅ 1
12 2t1e2 ⊢ 2 ⋅ 1 = 2
13 11 12 eqtri ⊢ 2 ⁢ cos ⁡ π 2 = 2
14 13 oveq1i ⊢ 2 ⁢ cos ⁡ π 2 − 1 = 2 − 1
15 2m1e1 ⊢ 2 − 1 = 1
16 3 14 15 3eqtri ⊢ cos ⁡ 2 ⁢ π = 1