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	⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 𝐾 · - π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )

Proof

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