Metamath Proof Explorer

Theorem cosknegpi

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 cosknegpi 
|- ( K e. ZZ -> ( cos ` ( K x. -u _pi ) ) = if ( 2 || K , 1 , -u 1 ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( K e. ZZ /\ 2 || K ) -> 2 || K )
2 2z 
 |-  2 e. ZZ
3 simpl 
 |-  ( ( K e. ZZ /\ 2 || K ) -> K e. ZZ )
4 divides 
 |-  ( ( 2 e. ZZ /\ K e. ZZ ) -> ( 2 || K <-> E. n e. ZZ ( n x. 2 ) = K ) )
5 2 3 4 sylancr 
 |-  ( ( K e. ZZ /\ 2 || K ) -> ( 2 || K <-> E. n e. ZZ ( n x. 2 ) = K ) )
6 1 5 mpbid 
 |-  ( ( K e. ZZ /\ 2 || K ) -> E. n e. ZZ ( n x. 2 ) = K )
7 zcn 
 |-  ( n e. ZZ -> n e. CC )
8 negcl 
 |-  ( n e. CC -> -u n e. CC )
9 2cn 
 |-  2 e. CC
10 picn 
 |-  _pi e. CC
11 9 10 mulcli 
 |-  ( 2 x. _pi ) e. CC
12 11 a1i 
 |-  ( n e. CC -> ( 2 x. _pi ) e. CC )
13 8 12 mulcld 
 |-  ( n e. CC -> ( -u n x. ( 2 x. _pi ) ) e. CC )
14 13 addid2d 
 |-  ( n e. CC -> ( 0 + ( -u n x. ( 2 x. _pi ) ) ) = ( -u n x. ( 2 x. _pi ) ) )
15 2cnd 
 |-  ( n e. CC -> 2 e. CC )
16 10 a1i 
 |-  ( n e. CC -> _pi e. CC )
17 8 15 16 mulassd 
 |-  ( n e. CC -> ( ( -u n x. 2 ) x. _pi ) = ( -u n x. ( 2 x. _pi ) ) )
18 17 eqcomd 
 |-  ( n e. CC -> ( -u n x. ( 2 x. _pi ) ) = ( ( -u n x. 2 ) x. _pi ) )
19 id 
 |-  ( n e. CC -> n e. CC )
20 19 15 mulneg1d 
 |-  ( n e. CC -> ( -u n x. 2 ) = -u ( n x. 2 ) )
21 20 oveq1d 
 |-  ( n e. CC -> ( ( -u n x. 2 ) x. _pi ) = ( -u ( n x. 2 ) x. _pi ) )
22 14 18 21 3eqtrd 
 |-  ( n e. CC -> ( 0 + ( -u n x. ( 2 x. _pi ) ) ) = ( -u ( n x. 2 ) x. _pi ) )
23 7 22 syl 
 |-  ( n e. ZZ -> ( 0 + ( -u n x. ( 2 x. _pi ) ) ) = ( -u ( n x. 2 ) x. _pi ) )
24 23 adantr 
 |-  ( ( n e. ZZ /\ ( n x. 2 ) = K ) -> ( 0 + ( -u n x. ( 2 x. _pi ) ) ) = ( -u ( n x. 2 ) x. _pi ) )
25 19 15 mulcld 
 |-  ( n e. CC -> ( n x. 2 ) e. CC )
26 mulneg12 
 |-  ( ( ( n x. 2 ) e. CC /\ _pi e. CC ) -> ( -u ( n x. 2 ) x. _pi ) = ( ( n x. 2 ) x. -u _pi ) )
27 25 16 26 syl2anc 
 |-  ( n e. CC -> ( -u ( n x. 2 ) x. _pi ) = ( ( n x. 2 ) x. -u _pi ) )
28 7 27 syl 
 |-  ( n e. ZZ -> ( -u ( n x. 2 ) x. _pi ) = ( ( n x. 2 ) x. -u _pi ) )
29 28 adantr 
 |-  ( ( n e. ZZ /\ ( n x. 2 ) = K ) -> ( -u ( n x. 2 ) x. _pi ) = ( ( n x. 2 ) x. -u _pi ) )
30 oveq1 
 |-  ( ( n x. 2 ) = K -> ( ( n x. 2 ) x. -u _pi ) = ( K x. -u _pi ) )
31 30 adantl 
 |-  ( ( n e. ZZ /\ ( n x. 2 ) = K ) -> ( ( n x. 2 ) x. -u _pi ) = ( K x. -u _pi ) )
32 24 29 31 3eqtrrd 
 |-  ( ( n e. ZZ /\ ( n x. 2 ) = K ) -> ( K x. -u _pi ) = ( 0 + ( -u n x. ( 2 x. _pi ) ) ) )
33 32 fveq2d 
 |-  ( ( n e. ZZ /\ ( n x. 2 ) = K ) -> ( cos ` ( K x. -u _pi ) ) = ( cos ` ( 0 + ( -u n x. ( 2 x. _pi ) ) ) ) )
34 33 3adant1 
 |-  ( ( 2 || K /\ n e. ZZ /\ ( n x. 2 ) = K ) -> ( cos ` ( K x. -u _pi ) ) = ( cos ` ( 0 + ( -u n x. ( 2 x. _pi ) ) ) ) )
35 0cnd 
 |-  ( n e. ZZ -> 0 e. CC )
36 znegcl 
 |-  ( n e. ZZ -> -u n e. ZZ )
37 cosper 
 |-  ( ( 0 e. CC /\ -u n e. ZZ ) -> ( cos ` ( 0 + ( -u n x. ( 2 x. _pi ) ) ) ) = ( cos ` 0 ) )
38 35 36 37 syl2anc 
 |-  ( n e. ZZ -> ( cos ` ( 0 + ( -u n x. ( 2 x. _pi ) ) ) ) = ( cos ` 0 ) )
39 38 3ad2ant2 
 |-  ( ( 2 || K /\ n e. ZZ /\ ( n x. 2 ) = K ) -> ( cos ` ( 0 + ( -u n x. ( 2 x. _pi ) ) ) ) = ( cos ` 0 ) )
40 cos0 
 |-  ( cos ` 0 ) = 1
41 iftrue 
 |-  ( 2 || K -> if ( 2 || K , 1 , -u 1 ) = 1 )
42 40 41 eqtr4id 
 |-  ( 2 || K -> ( cos ` 0 ) = if ( 2 || K , 1 , -u 1 ) )
43 42 3ad2ant1 
 |-  ( ( 2 || K /\ n e. ZZ /\ ( n x. 2 ) = K ) -> ( cos ` 0 ) = if ( 2 || K , 1 , -u 1 ) )
44 34 39 43 3eqtrd 
 |-  ( ( 2 || K /\ n e. ZZ /\ ( n x. 2 ) = K ) -> ( cos ` ( K x. -u _pi ) ) = if ( 2 || K , 1 , -u 1 ) )
45 44 3exp 
 |-  ( 2 || K -> ( n e. ZZ -> ( ( n x. 2 ) = K -> ( cos ` ( K x. -u _pi ) ) = if ( 2 || K , 1 , -u 1 ) ) ) )
46 45 adantl 
 |-  ( ( K e. ZZ /\ 2 || K ) -> ( n e. ZZ -> ( ( n x. 2 ) = K -> ( cos ` ( K x. -u _pi ) ) = if ( 2 || K , 1 , -u 1 ) ) ) )
47 46 rexlimdv 
 |-  ( ( K e. ZZ /\ 2 || K ) -> ( E. n e. ZZ ( n x. 2 ) = K -> ( cos ` ( K x. -u _pi ) ) = if ( 2 || K , 1 , -u 1 ) ) )
48 6 47 mpd 
 |-  ( ( K e. ZZ /\ 2 || K ) -> ( cos ` ( K x. -u _pi ) ) = if ( 2 || K , 1 , -u 1 ) )
49 odd2np1 
 |-  ( K e. ZZ -> ( -. 2 || K <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = K ) )
50 49 biimpa 
 |-  ( ( K e. ZZ /\ -. 2 || K ) -> E. n e. ZZ ( ( 2 x. n ) + 1 ) = K )
51 oveq1 
 |-  ( ( ( 2 x. n ) + 1 ) = K -> ( ( ( 2 x. n ) + 1 ) x. -u _pi ) = ( K x. -u _pi ) )
52 51 eqcomd 
 |-  ( ( ( 2 x. n ) + 1 ) = K -> ( K x. -u _pi ) = ( ( ( 2 x. n ) + 1 ) x. -u _pi ) )
53 52 adantl 
 |-  ( ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( K x. -u _pi ) = ( ( ( 2 x. n ) + 1 ) x. -u _pi ) )
54 15 19 mulcld 
 |-  ( n e. CC -> ( 2 x. n ) e. CC )
55 1cnd 
 |-  ( n e. CC -> 1 e. CC )
56 negpicn 
 |-  -u _pi e. CC
57 56 a1i 
 |-  ( n e. CC -> -u _pi e. CC )
58 54 55 57 adddird 
 |-  ( n e. CC -> ( ( ( 2 x. n ) + 1 ) x. -u _pi ) = ( ( ( 2 x. n ) x. -u _pi ) + ( 1 x. -u _pi ) ) )
59 7 58 syl 
 |-  ( n e. ZZ -> ( ( ( 2 x. n ) + 1 ) x. -u _pi ) = ( ( ( 2 x. n ) x. -u _pi ) + ( 1 x. -u _pi ) ) )
60 59 adantr 
 |-  ( ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( ( ( 2 x. n ) + 1 ) x. -u _pi ) = ( ( ( 2 x. n ) x. -u _pi ) + ( 1 x. -u _pi ) ) )
61 mulneg12 
 |-  ( ( ( 2 x. n ) e. CC /\ _pi e. CC ) -> ( -u ( 2 x. n ) x. _pi ) = ( ( 2 x. n ) x. -u _pi ) )
62 54 16 61 syl2anc 
 |-  ( n e. CC -> ( -u ( 2 x. n ) x. _pi ) = ( ( 2 x. n ) x. -u _pi ) )
63 62 eqcomd 
 |-  ( n e. CC -> ( ( 2 x. n ) x. -u _pi ) = ( -u ( 2 x. n ) x. _pi ) )
64 15 19 mulneg2d 
 |-  ( n e. CC -> ( 2 x. -u n ) = -u ( 2 x. n ) )
65 15 8 mulcomd 
 |-  ( n e. CC -> ( 2 x. -u n ) = ( -u n x. 2 ) )
66 64 65 eqtr3d 
 |-  ( n e. CC -> -u ( 2 x. n ) = ( -u n x. 2 ) )
67 66 oveq1d 
 |-  ( n e. CC -> ( -u ( 2 x. n ) x. _pi ) = ( ( -u n x. 2 ) x. _pi ) )
68 63 67 17 3eqtrd 
 |-  ( n e. CC -> ( ( 2 x. n ) x. -u _pi ) = ( -u n x. ( 2 x. _pi ) ) )
69 57 mulid2d 
 |-  ( n e. CC -> ( 1 x. -u _pi ) = -u _pi )
70 68 69 oveq12d 
 |-  ( n e. CC -> ( ( ( 2 x. n ) x. -u _pi ) + ( 1 x. -u _pi ) ) = ( ( -u n x. ( 2 x. _pi ) ) + -u _pi ) )
71 13 57 addcomd 
 |-  ( n e. CC -> ( ( -u n x. ( 2 x. _pi ) ) + -u _pi ) = ( -u _pi + ( -u n x. ( 2 x. _pi ) ) ) )
72 70 71 eqtrd 
 |-  ( n e. CC -> ( ( ( 2 x. n ) x. -u _pi ) + ( 1 x. -u _pi ) ) = ( -u _pi + ( -u n x. ( 2 x. _pi ) ) ) )
73 7 72 syl 
 |-  ( n e. ZZ -> ( ( ( 2 x. n ) x. -u _pi ) + ( 1 x. -u _pi ) ) = ( -u _pi + ( -u n x. ( 2 x. _pi ) ) ) )
74 73 adantr 
 |-  ( ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( ( ( 2 x. n ) x. -u _pi ) + ( 1 x. -u _pi ) ) = ( -u _pi + ( -u n x. ( 2 x. _pi ) ) ) )
75 53 60 74 3eqtrd 
 |-  ( ( n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( K x. -u _pi ) = ( -u _pi + ( -u n x. ( 2 x. _pi ) ) ) )
76 75 3adant1 
 |-  ( ( K e. ZZ /\ n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( K x. -u _pi ) = ( -u _pi + ( -u n x. ( 2 x. _pi ) ) ) )
77 76 fveq2d 
 |-  ( ( K e. ZZ /\ n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( cos ` ( K x. -u _pi ) ) = ( cos ` ( -u _pi + ( -u n x. ( 2 x. _pi ) ) ) ) )
78 77 3adant1r 
 |-  ( ( ( K e. ZZ /\ -. 2 || K ) /\ n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( cos ` ( K x. -u _pi ) ) = ( cos ` ( -u _pi + ( -u n x. ( 2 x. _pi ) ) ) ) )
79 cosper 
 |-  ( ( -u _pi e. CC /\ -u n e. ZZ ) -> ( cos ` ( -u _pi + ( -u n x. ( 2 x. _pi ) ) ) ) = ( cos ` -u _pi ) )
80 56 36 79 sylancr 
 |-  ( n e. ZZ -> ( cos ` ( -u _pi + ( -u n x. ( 2 x. _pi ) ) ) ) = ( cos ` -u _pi ) )
81 80 3ad2ant2 
 |-  ( ( ( K e. ZZ /\ -. 2 || K ) /\ n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( cos ` ( -u _pi + ( -u n x. ( 2 x. _pi ) ) ) ) = ( cos ` -u _pi ) )
82 cosnegpi 
 |-  ( cos ` -u _pi ) = -u 1
83 iffalse 
 |-  ( -. 2 || K -> if ( 2 || K , 1 , -u 1 ) = -u 1 )
84 82 83 eqtr4id 
 |-  ( -. 2 || K -> ( cos ` -u _pi ) = if ( 2 || K , 1 , -u 1 ) )
85 84 adantl 
 |-  ( ( K e. ZZ /\ -. 2 || K ) -> ( cos ` -u _pi ) = if ( 2 || K , 1 , -u 1 ) )
86 85 3ad2ant1 
 |-  ( ( ( K e. ZZ /\ -. 2 || K ) /\ n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( cos ` -u _pi ) = if ( 2 || K , 1 , -u 1 ) )
87 78 81 86 3eqtrd 
 |-  ( ( ( K e. ZZ /\ -. 2 || K ) /\ n e. ZZ /\ ( ( 2 x. n ) + 1 ) = K ) -> ( cos ` ( K x. -u _pi ) ) = if ( 2 || K , 1 , -u 1 ) )
88 87 rexlimdv3a 
 |-  ( ( K e. ZZ /\ -. 2 || K ) -> ( E. n e. ZZ ( ( 2 x. n ) + 1 ) = K -> ( cos ` ( K x. -u _pi ) ) = if ( 2 || K , 1 , -u 1 ) ) )
89 50 88 mpd 
 |-  ( ( K e. ZZ /\ -. 2 || K ) -> ( cos ` ( K x. -u _pi ) ) = if ( 2 || K , 1 , -u 1 ) )
90 48 89 pm2.61dan 
 |-  ( K e. ZZ -> ( cos ` ( K x. -u _pi ) ) = if ( 2 || K , 1 , -u 1 ) )