# 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 x. _pi ) ) = 1`

### Proof

Step Hyp Ref Expression
1 picn
` |-  _pi e. CC`
2 cos2t
` |-  ( _pi e. CC -> ( cos ` ( 2 x. _pi ) ) = ( ( 2 x. ( ( cos ` _pi ) ^ 2 ) ) - 1 ) )`
3 1 2 ax-mp
` |-  ( cos ` ( 2 x. _pi ) ) = ( ( 2 x. ( ( cos ` _pi ) ^ 2 ) ) - 1 )`
4 cospi
` |-  ( cos ` _pi ) = -u 1`
5 4 oveq1i
` |-  ( ( cos ` _pi ) ^ 2 ) = ( -u 1 ^ 2 )`
6 ax-1cn
` |-  1 e. CC`
7 sqneg
` |-  ( 1 e. CC -> ( -u 1 ^ 2 ) = ( 1 ^ 2 ) )`
8 6 7 ax-mp
` |-  ( -u 1 ^ 2 ) = ( 1 ^ 2 )`
9 sq1
` |-  ( 1 ^ 2 ) = 1`
10 5 8 9 3eqtri
` |-  ( ( cos ` _pi ) ^ 2 ) = 1`
11 10 oveq2i
` |-  ( 2 x. ( ( cos ` _pi ) ^ 2 ) ) = ( 2 x. 1 )`
12 2t1e2
` |-  ( 2 x. 1 ) = 2`
13 11 12 eqtri
` |-  ( 2 x. ( ( cos ` _pi ) ^ 2 ) ) = 2`
14 13 oveq1i
` |-  ( ( 2 x. ( ( cos ` _pi ) ^ 2 ) ) - 1 ) = ( 2 - 1 )`
15 2m1e1
` |-  ( 2 - 1 ) = 1`
16 3 14 15 3eqtri
` |-  ( cos ` ( 2 x. _pi ) ) = 1`