Metamath Proof Explorer

Theorem coskpi2

Description: The cosine of an integer multiple of negative _pi is either 1 or negative 1 . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion coskpi2 
|- ( K e. ZZ -> ( cos ` ( K x. _pi ) ) = if ( 2 || K , 1 , -u 1 ) )

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 divides 
 |-  ( ( 2 e. ZZ /\ K e. ZZ ) -> ( 2 || K <-> E. n e. ZZ ( n x. 2 ) = K ) )
3 1 2 mpan 
 |-  ( K e. ZZ -> ( 2 || K <-> E. n e. ZZ ( n x. 2 ) = K ) )
4 3 biimpa 
 |-  ( ( K e. ZZ /\ 2 || K ) -> E. n e. ZZ ( n x. 2 ) = K )
5 zcn 
 |-  ( n e. ZZ -> n e. CC )
6 2cnd 
 |-  ( n e. ZZ -> 2 e. CC )
7 picn 
 |-  _pi e. CC
8 7 a1i 
 |-  ( n e. ZZ -> _pi e. CC )
9 5 6 8 mulassd 
 |-  ( n e. ZZ -> ( ( n x. 2 ) x. _pi ) = ( n x. ( 2 x. _pi ) ) )
10 9 eqcomd 
 |-  ( n e. ZZ -> ( n x. ( 2 x. _pi ) ) = ( ( n x. 2 ) x. _pi ) )
11 10 adantr 
 |-  ( ( n e. ZZ /\ ( n x. 2 ) = K ) -> ( n x. ( 2 x. _pi ) ) = ( ( n x. 2 ) x. _pi ) )
12 oveq1 
 |-  ( ( n x. 2 ) = K -> ( ( n x. 2 ) x. _pi ) = ( K x. _pi ) )
13 12 adantl 
 |-  ( ( n e. ZZ /\ ( n x. 2 ) = K ) -> ( ( n x. 2 ) x. _pi ) = ( K x. _pi ) )
14 11 13 eqtr2d 
 |-  ( ( n e. ZZ /\ ( n x. 2 ) = K ) -> ( K x. _pi ) = ( n x. ( 2 x. _pi ) ) )
15 14 fveq2d 
 |-  ( ( n e. ZZ /\ ( n x. 2 ) = K ) -> ( cos ` ( K x. _pi ) ) = ( cos ` ( n x. ( 2 x. _pi ) ) ) )
16 cos2kpi 
 |-  ( n e. ZZ -> ( cos ` ( n x. ( 2 x. _pi ) ) ) = 1 )
17 16 adantr 
 |-  ( ( n e. ZZ /\ ( n x. 2 ) = K ) -> ( cos ` ( n x. ( 2 x. _pi ) ) ) = 1 )
18 15 17 eqtrd 
 |-  ( ( n e. ZZ /\ ( n x. 2 ) = K ) -> ( cos ` ( K x. _pi ) ) = 1 )
19 18 3adant1 
 |-  ( ( 2 || K /\ n e. ZZ /\ ( n x. 2 ) = K ) -> ( cos ` ( K x. _pi ) ) = 1 )
20 iftrue 
 |-  ( 2 || K -> if ( 2 || K , 1 , -u 1 ) = 1 )
21 20 eqcomd 
 |-  ( 2 || K -> 1 = if ( 2 || K , 1 , -u 1 ) )
22 21 3ad2ant1 
 |-  ( ( 2 || K /\ n e. ZZ /\ ( n x. 2 ) = K ) -> 1 = if ( 2 || K , 1 , -u 1 ) )
23 19 22 eqtrd 
 |-  ( ( 2 || K /\ n e. ZZ /\ ( n x. 2 ) = K ) -> ( cos ` ( K x. _pi ) ) = if ( 2 || K , 1 , -u 1 ) )
24 23 3exp 
 |-  ( 2 || K -> ( n e. ZZ -> ( ( n x. 2 ) = K -> ( cos ` ( K x. _pi ) ) = if ( 2 || K , 1 , -u 1 ) ) ) )
25 24 adantl 
 |-  ( ( K e. ZZ /\ 2 || K ) -> ( n e. ZZ -> ( ( n x. 2 ) = K -> ( cos ` ( K x. _pi ) ) = if ( 2 || K , 1 , -u 1 ) ) ) )
26 25 rexlimdv 
 |-  ( ( K e. ZZ /\ 2 || K ) -> ( E. n e. ZZ ( n x. 2 ) = K -> ( cos ` ( K x. _pi ) ) = if ( 2 || K , 1 , -u 1 ) ) )
27 4 26 mpd 
 |-  ( ( K e. ZZ /\ 2 || K ) -> ( cos ` ( K x. _pi ) ) = if ( 2 || K , 1 , -u 1 ) )
28 odd2np1 
 |-  ( K e. ZZ -> ( -. 2 || K <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = K ) )
29 28 biimpa 
 |-  ( ( K e. ZZ /\ -. 2 || K ) -> E. n e. ZZ ( ( 2 x. n ) + 1 ) = K )
30 6 5 mulcld 
 |-  ( n e. ZZ -> ( 2 x. n ) e. CC )
31 1cnd 
 |-  ( n e. ZZ -> 1 e. CC )
32 30 31 8 adddird 
 |-  ( n e. ZZ -> ( ( ( 2 x. n ) + 1 ) x. _pi ) = ( ( ( 2 x. n ) x. _pi ) + ( 1 x. _pi ) ) )
33 6 5 mulcomd 
 |-  ( n e. ZZ -> ( 2 x. n ) = ( n x. 2 ) )
34 33 oveq1d 
 |-  ( n e. ZZ -> ( ( 2 x. n ) x. _pi ) = ( ( n x. 2 ) x. _pi ) )
35 34 9 eqtrd 
 |-  ( n e. ZZ -> ( ( 2 x. n ) x. _pi ) = ( n x. ( 2 x. _pi ) ) )
36 7 mulid2i 
 |-  ( 1 x. _pi ) = _pi
37 36 a1i 
 |-  ( n e. ZZ -> ( 1 x. _pi ) = _pi )
38 35 37 oveq12d 
 |-  ( n e. ZZ -> ( ( ( 2 x. n ) x. _pi ) + ( 1 x. _pi ) ) = ( ( n x. ( 2 x. _pi ) ) + _pi ) )
39 2cn 
 |-  2 e. CC
40 39 7 mulcli 
 |-  ( 2 x. _pi ) e. CC
41 40 a1i 
 |-  ( n e. ZZ -> ( 2 x. _pi ) e. CC )
42 5 41 mulcld 
 |-  ( n e. ZZ -> ( n x. ( 2 x. _pi ) ) e. CC )
43 42 8 addcomd 
 |-  ( n e. ZZ -> ( ( n x. ( 2 x. _pi ) ) + _pi ) = ( _pi + ( n x. ( 2 x. _pi ) ) ) )
44 32 38 43 3eqtrrd 
 |-  ( n e. ZZ -> ( _pi + ( n x. ( 2 x. _pi ) ) ) = ( ( ( 2 x. n ) + 1 ) x. _pi ) )
45 44 adantr 
 |-  ( ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( _pi + ( n x. ( 2 x. _pi ) ) ) = ( ( ( 2 x. n ) + 1 ) x. _pi ) )
46 oveq1 
 |-  ( ( ( 2 x. n ) + 1 ) = K -> ( ( ( 2 x. n ) + 1 ) x. _pi ) = ( K x. _pi ) )
47 46 adantl 
 |-  ( ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( ( ( 2 x. n ) + 1 ) x. _pi ) = ( K x. _pi ) )
48 45 47 eqtr2d 
 |-  ( ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( K x. _pi ) = ( _pi + ( n x. ( 2 x. _pi ) ) ) )
49 48 fveq2d 
 |-  ( ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( cos ` ( K x. _pi ) ) = ( cos ` ( _pi + ( n x. ( 2 x. _pi ) ) ) ) )
50 cosper 
 |-  ( ( _pi e. CC /\ n e. ZZ ) -> ( cos ` ( _pi + ( n x. ( 2 x. _pi ) ) ) ) = ( cos ` _pi ) )
51 7 50 mpan 
 |-  ( n e. ZZ -> ( cos ` ( _pi + ( n x. ( 2 x. _pi ) ) ) ) = ( cos ` _pi ) )
52 51 adantr 
 |-  ( ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( cos ` ( _pi + ( n x. ( 2 x. _pi ) ) ) ) = ( cos ` _pi ) )
53 cospi 
 |-  ( cos ` _pi ) = -u 1
54 53 a1i 
 |-  ( ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( cos ` _pi ) = -u 1 )
55 49 52 54 3eqtrd 
 |-  ( ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( cos ` ( K x. _pi ) ) = -u 1 )
56 55 3adant1 
 |-  ( ( -. 2 || K /\ n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( cos ` ( K x. _pi ) ) = -u 1 )
57 iffalse 
 |-  ( -. 2 || K -> if ( 2 || K , 1 , -u 1 ) = -u 1 )
58 57 eqcomd 
 |-  ( -. 2 || K -> -u 1 = if ( 2 || K , 1 , -u 1 ) )
59 58 3ad2ant1 
 |-  ( ( -. 2 || K /\ n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> -u 1 = if ( 2 || K , 1 , -u 1 ) )
60 56 59 eqtrd 
 |-  ( ( -. 2 || K /\ n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( cos ` ( K x. _pi ) ) = if ( 2 || K , 1 , -u 1 ) )
61 60 3exp 
 |-  ( -. 2 || K -> ( n e. ZZ -> ( ( ( 2 x. n ) + 1 ) = K -> ( cos ` ( K x. _pi ) ) = if ( 2 || K , 1 , -u 1 ) ) ) )
62 61 adantl 
 |-  ( ( K e. ZZ /\ -. 2 || K ) -> ( n e. ZZ -> ( ( ( 2 x. n ) + 1 ) = K -> ( cos ` ( K x. _pi ) ) = if ( 2 || K , 1 , -u 1 ) ) ) )
63 62 rexlimdv 
 |-  ( ( K e. ZZ /\ -. 2 || K ) -> ( E. n e. ZZ ( ( 2 x. n ) + 1 ) = K -> ( cos ` ( K x. _pi ) ) = if ( 2 || K , 1 , -u 1 ) ) )
64 29 63 mpd 
 |-  ( ( K e. ZZ /\ -. 2 || K ) -> ( cos ` ( K x. _pi ) ) = if ( 2 || K , 1 , -u 1 ) )
65 27 64 pm2.61dan 
 |-  ( K e. ZZ -> ( cos ` ( K x. _pi ) ) = if ( 2 || K , 1 , -u 1 ) )