Metamath Proof Explorer

Theorem coskpi

Description: The absolute value of the cosine of an integer multiple of _pi is 1. (Contributed by NM, 19-Aug-2008)

Ref Expression
Assertion coskpi 
|- ( K e. ZZ -> ( abs ` ( cos ` ( K x. _pi ) ) ) = 1 )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( K e. ZZ -> K e. CC )
2 2cn 
 |-  2 e. CC
3 picn 
 |-  _pi e. CC
4 mul12 
 |-  ( ( K e. CC /\ 2 e. CC /\ _pi e. CC ) -> ( K x. ( 2 x. _pi ) ) = ( 2 x. ( K x. _pi ) ) )
5 2 3 4 mp3an23 
 |-  ( K e. CC -> ( K x. ( 2 x. _pi ) ) = ( 2 x. ( K x. _pi ) ) )
6 1 5 syl 
 |-  ( K e. ZZ -> ( K x. ( 2 x. _pi ) ) = ( 2 x. ( K x. _pi ) ) )
7 6 fveq2d 
 |-  ( K e. ZZ -> ( cos ` ( K x. ( 2 x. _pi ) ) ) = ( cos ` ( 2 x. ( K x. _pi ) ) ) )
8 cos2kpi 
 |-  ( K e. ZZ -> ( cos ` ( K x. ( 2 x. _pi ) ) ) = 1 )
9 zre 
 |-  ( K e. ZZ -> K e. RR )
10 pire 
 |-  _pi e. RR
11 remulcl 
 |-  ( ( K e. RR /\ _pi e. RR ) -> ( K x. _pi ) e. RR )
12 9 10 11 sylancl 
 |-  ( K e. ZZ -> ( K x. _pi ) e. RR )
13 12 recnd 
 |-  ( K e. ZZ -> ( K x. _pi ) e. CC )
14 cos2t 
 |-  ( ( K x. _pi ) e. CC -> ( cos ` ( 2 x. ( K x. _pi ) ) ) = ( ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) - 1 ) )
15 13 14 syl 
 |-  ( K e. ZZ -> ( cos ` ( 2 x. ( K x. _pi ) ) ) = ( ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) - 1 ) )
16 7 8 15 3eqtr3rd 
 |-  ( K e. ZZ -> ( ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) - 1 ) = 1 )
17 12 recoscld 
 |-  ( K e. ZZ -> ( cos ` ( K x. _pi ) ) e. RR )
18 17 recnd 
 |-  ( K e. ZZ -> ( cos ` ( K x. _pi ) ) e. CC )
19 18 sqcld 
 |-  ( K e. ZZ -> ( ( cos ` ( K x. _pi ) ) ^ 2 ) e. CC )
20 mulcl 
 |-  ( ( 2 e. CC /\ ( ( cos ` ( K x. _pi ) ) ^ 2 ) e. CC ) -> ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) e. CC )
21 2 19 20 sylancr 
 |-  ( K e. ZZ -> ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) e. CC )
22 ax-1cn 
 |-  1 e. CC
23 subadd 
 |-  ( ( ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) - 1 ) = 1 <-> ( 1 + 1 ) = ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) ) )
24 22 22 23 mp3an23 
 |-  ( ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) e. CC -> ( ( ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) - 1 ) = 1 <-> ( 1 + 1 ) = ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) ) )
25 21 24 syl 
 |-  ( K e. ZZ -> ( ( ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) - 1 ) = 1 <-> ( 1 + 1 ) = ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) ) )
26 16 25 mpbid 
 |-  ( K e. ZZ -> ( 1 + 1 ) = ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) )
27 2t1e2 
 |-  ( 2 x. 1 ) = 2
28 df-2 
 |-  2 = ( 1 + 1 )
29 27 28 eqtr2i 
 |-  ( 1 + 1 ) = ( 2 x. 1 )
30 26 29 eqtr3di 
 |-  ( K e. ZZ -> ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) = ( 2 x. 1 ) )
31 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
32 mulcan 
 |-  ( ( ( ( cos ` ( K x. _pi ) ) ^ 2 ) e. CC /\ 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) = ( 2 x. 1 ) <-> ( ( cos ` ( K x. _pi ) ) ^ 2 ) = 1 ) )
33 22 31 32 mp3an23 
 |-  ( ( ( cos ` ( K x. _pi ) ) ^ 2 ) e. CC -> ( ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) = ( 2 x. 1 ) <-> ( ( cos ` ( K x. _pi ) ) ^ 2 ) = 1 ) )
34 19 33 syl 
 |-  ( K e. ZZ -> ( ( 2 x. ( ( cos ` ( K x. _pi ) ) ^ 2 ) ) = ( 2 x. 1 ) <-> ( ( cos ` ( K x. _pi ) ) ^ 2 ) = 1 ) )
35 30 34 mpbid 
 |-  ( K e. ZZ -> ( ( cos ` ( K x. _pi ) ) ^ 2 ) = 1 )
36 sq1 
 |-  ( 1 ^ 2 ) = 1
37 35 36 eqtr4di 
 |-  ( K e. ZZ -> ( ( cos ` ( K x. _pi ) ) ^ 2 ) = ( 1 ^ 2 ) )
38 1re 
 |-  1 e. RR
39 sqabs 
 |-  ( ( ( cos ` ( K x. _pi ) ) e. RR /\ 1 e. RR ) -> ( ( ( cos ` ( K x. _pi ) ) ^ 2 ) = ( 1 ^ 2 ) <-> ( abs ` ( cos ` ( K x. _pi ) ) ) = ( abs ` 1 ) ) )
40 17 38 39 sylancl 
 |-  ( K e. ZZ -> ( ( ( cos ` ( K x. _pi ) ) ^ 2 ) = ( 1 ^ 2 ) <-> ( abs ` ( cos ` ( K x. _pi ) ) ) = ( abs ` 1 ) ) )
41 37 40 mpbid 
 |-  ( K e. ZZ -> ( abs ` ( cos ` ( K x. _pi ) ) ) = ( abs ` 1 ) )
42 abs1 
 |-  ( abs ` 1 ) = 1
43 41 42 eqtrdi 
 |-  ( K e. ZZ -> ( abs ` ( cos ` ( K x. _pi ) ) ) = 1 )