dirkertrigeqlem1

Description: Sum of an even number of alternating cos values. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	dirkertrigeqlem1	$⊢ K \in ℕ \to \sum_{n = 1}^{2 K} \cos n π = 0$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = 1 \to 2 x = 2 \cdot 1$
2	1	oveq2d	$⊢ x = 1 \to (1 \dots 2 x) = (1 \dots 2 \cdot 1)$
3	2	sumeq1d	$⊢ x = 1 \to \sum_{n = 1}^{2 x} \cos n π = \sum_{n = 1}^{2 \cdot 1} \cos n π$
4	3	eqeq1d	$⊢ x = 1 \to (\sum_{n = 1}^{2 x} \cos n π = 0 \leftrightarrow \sum_{n = 1}^{2 \cdot 1} \cos n π = 0)$
5		oveq2	$⊢ x = y \to 2 x = 2 y$
6	5	oveq2d	$⊢ x = y \to (1 \dots 2 x) = (1 \dots 2 y)$
7	6	sumeq1d	$⊢ x = y \to \sum_{n = 1}^{2 x} \cos n π = \sum_{n = 1}^{2 y} \cos n π$
8	7	eqeq1d	$⊢ x = y \to (\sum_{n = 1}^{2 x} \cos n π = 0 \leftrightarrow \sum_{n = 1}^{2 y} \cos n π = 0)$
9		oveq2	$⊢ x = y + 1 \to 2 x = 2 (y + 1)$
10	9	oveq2d	$⊢ x = y + 1 \to (1 \dots 2 x) = (1 \dots 2 (y + 1))$
11	10	sumeq1d	$⊢ x = y + 1 \to \sum_{n = 1}^{2 x} \cos n π = \sum_{n = 1}^{2 (y + 1)} \cos n π$
12	11	eqeq1d	$⊢ x = y + 1 \to (\sum_{n = 1}^{2 x} \cos n π = 0 \leftrightarrow \sum_{n = 1}^{2 (y + 1)} \cos n π = 0)$
13		oveq2	$⊢ x = K \to 2 x = 2 K$
14	13	oveq2d	$⊢ x = K \to (1 \dots 2 x) = (1 \dots 2 K)$
15	14	sumeq1d	$⊢ x = K \to \sum_{n = 1}^{2 x} \cos n π = \sum_{n = 1}^{2 K} \cos n π$
16	15	eqeq1d	$⊢ x = K \to (\sum_{n = 1}^{2 x} \cos n π = 0 \leftrightarrow \sum_{n = 1}^{2 K} \cos n π = 0)$
17		ax-1cn	$⊢ 1 \in ℂ$
18	17	2timesi	$⊢ 2 \cdot 1 = 1 + 1$
19	18	oveq2i	$⊢ (1 \dots 2 \cdot 1) = (1 \dots 1 + 1)$
20	19	sumeq1i	$⊢ \sum_{n = 1}^{2 \cdot 1} \cos n π = \sum_{n = 1}^{1 + 1} \cos n π$
21		1z	$⊢ 1 \in ℤ$
22		uzid	$⊢ 1 \in ℤ \to 1 \in ℤ_{\geq 1}$
23	21 22	ax-mp	$⊢ 1 \in ℤ_{\geq 1}$
24	23	a1i	$⊢ ⊤ \to 1 \in ℤ_{\geq 1}$
25		elfzelz	$⊢ n \in (1 \dots 1 + 1) \to n \in ℤ$
26	25	zcnd	$⊢ n \in (1 \dots 1 + 1) \to n \in ℂ$
27	26	adantl	$⊢ (⊤ \land n \in (1 \dots 1 + 1)) \to n \in ℂ$
28		picn	$⊢ π \in ℂ$
29	28	a1i	$⊢ (⊤ \land n \in (1 \dots 1 + 1)) \to π \in ℂ$
30	27 29	mulcld	$⊢ (⊤ \land n \in (1 \dots 1 + 1)) \to n π \in ℂ$
31	30	coscld	$⊢ (⊤ \land n \in (1 \dots 1 + 1)) \to \cos n π \in ℂ$
32		id	$⊢ n = 1 + 1 \to n = 1 + 1$
33		1p1e2	$⊢ 1 + 1 = 2$
34	32 33	eqtrdi	$⊢ n = 1 + 1 \to n = 2$
35	34	fvoveq1d	$⊢ n = 1 + 1 \to \cos n π = \cos 2 π$
36	24 31 35	fsump1	$⊢ ⊤ \to \sum_{n = 1}^{1 + 1} \cos n π = \sum_{n = 1}^{1} \cos n π + \cos 2 π$
37	36	mptru	$⊢ \sum_{n = 1}^{1 + 1} \cos n π = \sum_{n = 1}^{1} \cos n π + \cos 2 π$
38		coscl	$⊢ π \in ℂ \to \cos π \in ℂ$
39	28 38	ax-mp	$⊢ \cos π \in ℂ$
40		oveq1	$⊢ n = 1 \to n π = 1 π$
41	28	mulid2i	$⊢ 1 π = π$
42	40 41	eqtrdi	$⊢ n = 1 \to n π = π$
43	42	fveq2d	$⊢ n = 1 \to \cos n π = \cos π$
44	43	fsum1	$⊢ (1 \in ℤ \land \cos π \in ℂ) \to \sum_{n = 1}^{1} \cos n π = \cos π$
45	21 39 44	mp2an	$⊢ \sum_{n = 1}^{1} \cos n π = \cos π$
46		cospi	$⊢ \cos π = - 1$
47	45 46	eqtri	$⊢ \sum_{n = 1}^{1} \cos n π = - 1$
48		cos2pi	$⊢ \cos 2 π = 1$
49	47 48	oveq12i	$⊢ \sum_{n = 1}^{1} \cos n π + \cos 2 π = - 1 + 1$
50		neg1cn	$⊢ - 1 \in ℂ$
51		1pneg1e0	$⊢ 1 + -1 = 0$
52	17 50 51	addcomli	$⊢ - 1 + 1 = 0$
53	37 49 52	3eqtri	$⊢ \sum_{n = 1}^{1 + 1} \cos n π = 0$
54	20 53	eqtri	$⊢ \sum_{n = 1}^{2 \cdot 1} \cos n π = 0$
55	18	oveq2i	$⊢ 2 y + 2 \cdot 1 = 2 y + 1 + 1$
56		2cnd	$⊢ y \in ℕ \to 2 \in ℂ$
57		nncn	$⊢ y \in ℕ \to y \in ℂ$
58	17	a1i	$⊢ y \in ℕ \to 1 \in ℂ$
59	56 57 58	adddid	$⊢ y \in ℕ \to 2 (y + 1) = 2 y + 2 \cdot 1$
60	56 57	mulcld	$⊢ y \in ℕ \to 2 y \in ℂ$
61	60 58 58	addassd	$⊢ y \in ℕ \to 2 y + 1 + 1 = 2 y + 1 + 1$
62	55 59 61	3eqtr4a	$⊢ y \in ℕ \to 2 (y + 1) = 2 y + 1 + 1$
63	62	oveq2d	$⊢ y \in ℕ \to (1 \dots 2 (y + 1)) = (1 \dots 2 y + 1 + 1)$
64	63	sumeq1d	$⊢ y \in ℕ \to \sum_{n = 1}^{2 (y + 1)} \cos n π = \sum_{n = 1}^{2 y + 1 + 1} \cos n π$
65	64	adantr	$⊢ (y \in ℕ \land \sum_{n = 1}^{2 y} \cos n π = 0) \to \sum_{n = 1}^{2 (y + 1)} \cos n π = \sum_{n = 1}^{2 y + 1 + 1} \cos n π$
66		1red	$⊢ y \in ℕ \to 1 \in ℝ$
67		2re	$⊢ 2 \in ℝ$
68	67	a1i	$⊢ y \in ℕ \to 2 \in ℝ$
69		nnre	$⊢ y \in ℕ \to y \in ℝ$
70	68 69	remulcld	$⊢ y \in ℕ \to 2 y \in ℝ$
71	70 66	readdcld	$⊢ y \in ℕ \to 2 y + 1 \in ℝ$
72		2rp	$⊢ 2 \in ℝ^{+}$
73	72	a1i	$⊢ y \in ℕ \to 2 \in ℝ^{+}$
74		nnrp	$⊢ y \in ℕ \to y \in ℝ^{+}$
75	73 74	rpmulcld	$⊢ y \in ℕ \to 2 y \in ℝ^{+}$
76	66 75	ltaddrp2d	$⊢ y \in ℕ \to 1 < 2 y + 1$
77	66 71 76	ltled	$⊢ y \in ℕ \to 1 \leq 2 y + 1$
78		2z	$⊢ 2 \in ℤ$
79	78	a1i	$⊢ y \in ℕ \to 2 \in ℤ$
80		nnz	$⊢ y \in ℕ \to y \in ℤ$
81	79 80	zmulcld	$⊢ y \in ℕ \to 2 y \in ℤ$
82	81	peano2zd	$⊢ y \in ℕ \to 2 y + 1 \in ℤ$
83		eluz	$⊢ (1 \in ℤ \land 2 y + 1 \in ℤ) \to (2 y + 1 \in ℤ_{\geq 1} \leftrightarrow 1 \leq 2 y + 1)$
84	21 82 83	sylancr	$⊢ y \in ℕ \to (2 y + 1 \in ℤ_{\geq 1} \leftrightarrow 1 \leq 2 y + 1)$
85	77 84	mpbird	$⊢ y \in ℕ \to 2 y + 1 \in ℤ_{\geq 1}$
86		elfzelz	$⊢ n \in (1 \dots 2 y + 1 + 1) \to n \in ℤ$
87	86	zcnd	$⊢ n \in (1 \dots 2 y + 1 + 1) \to n \in ℂ$
88	28	a1i	$⊢ n \in (1 \dots 2 y + 1 + 1) \to π \in ℂ$
89	87 88	mulcld	$⊢ n \in (1 \dots 2 y + 1 + 1) \to n π \in ℂ$
90	89	coscld	$⊢ n \in (1 \dots 2 y + 1 + 1) \to \cos n π \in ℂ$
91	90	adantl	$⊢ (y \in ℕ \land n \in (1 \dots 2 y + 1 + 1)) \to \cos n π \in ℂ$
92		fvoveq1	$⊢ n = 2 y + 1 + 1 \to \cos n π = \cos (2 y + 1 + 1) π$
93	85 91 92	fsump1	$⊢ y \in ℕ \to \sum_{n = 1}^{2 y + 1 + 1} \cos n π = \sum_{n = 1}^{2 y + 1} \cos n π + \cos (2 y + 1 + 1) π$
94	93	adantr	$⊢ (y \in ℕ \land \sum_{n = 1}^{2 y} \cos n π = 0) \to \sum_{n = 1}^{2 y + 1 + 1} \cos n π = \sum_{n = 1}^{2 y + 1} \cos n π + \cos (2 y + 1 + 1) π$
95		1lt2	$⊢ 1 < 2$
96	95	a1i	$⊢ y \in ℕ \to 1 < 2$
97		2t1e2	$⊢ 2 \cdot 1 = 2$
98		nnge1	$⊢ y \in ℕ \to 1 \leq y$
99	66 69 73	lemul2d	$⊢ y \in ℕ \to (1 \leq y \leftrightarrow 2 \cdot 1 \leq 2 y)$
100	98 99	mpbid	$⊢ y \in ℕ \to 2 \cdot 1 \leq 2 y$
101	97 100	eqbrtrrid	$⊢ y \in ℕ \to 2 \leq 2 y$
102	66 68 70 96 101	ltletrd	$⊢ y \in ℕ \to 1 < 2 y$
103	66 70 102	ltled	$⊢ y \in ℕ \to 1 \leq 2 y$
104		eluz	$⊢ (1 \in ℤ \land 2 y \in ℤ) \to (2 y \in ℤ_{\geq 1} \leftrightarrow 1 \leq 2 y)$
105	21 81 104	sylancr	$⊢ y \in ℕ \to (2 y \in ℤ_{\geq 1} \leftrightarrow 1 \leq 2 y)$
106	103 105	mpbird	$⊢ y \in ℕ \to 2 y \in ℤ_{\geq 1}$
107		elfzelz	$⊢ n \in (1 \dots 2 y + 1) \to n \in ℤ$
108	107	zcnd	$⊢ n \in (1 \dots 2 y + 1) \to n \in ℂ$
109	28	a1i	$⊢ n \in (1 \dots 2 y + 1) \to π \in ℂ$
110	108 109	mulcld	$⊢ n \in (1 \dots 2 y + 1) \to n π \in ℂ$
111	110	coscld	$⊢ n \in (1 \dots 2 y + 1) \to \cos n π \in ℂ$
112	111	adantl	$⊢ (y \in ℕ \land n \in (1 \dots 2 y + 1)) \to \cos n π \in ℂ$
113		fvoveq1	$⊢ n = 2 y + 1 \to \cos n π = \cos (2 y + 1) π$
114	106 112 113	fsump1	$⊢ y \in ℕ \to \sum_{n = 1}^{2 y + 1} \cos n π = \sum_{n = 1}^{2 y} \cos n π + \cos (2 y + 1) π$
115	33 97	eqtr4i	$⊢ 1 + 1 = 2 \cdot 1$
116	115	a1i	$⊢ y \in ℕ \to 1 + 1 = 2 \cdot 1$
117	116	oveq2d	$⊢ y \in ℕ \to 2 y + 1 + 1 = 2 y + 2 \cdot 1$
118	117 61 59	3eqtr4d	$⊢ y \in ℕ \to 2 y + 1 + 1 = 2 (y + 1)$
119	118	fvoveq1d	$⊢ y \in ℕ \to \cos (2 y + 1 + 1) π = \cos 2 (y + 1) π$
120	57 58	addcld	$⊢ y \in ℕ \to y + 1 \in ℂ$
121	28	a1i	$⊢ y \in ℕ \to π \in ℂ$
122	56 120 121	mulassd	$⊢ y \in ℕ \to 2 (y + 1) π = 2 (y + 1) π$
123	122	oveq1d	$⊢ y \in ℕ \to \frac{2 (y + 1) π}{2 π} = \frac{2 (y + 1) π}{2 π}$
124	120 121	mulcld	$⊢ y \in ℕ \to (y + 1) π \in ℂ$
125		0re	$⊢ 0 \in ℝ$
126		pipos	$⊢ 0 < π$
127	125 126	gtneii	$⊢ π \neq 0$
128	127	a1i	$⊢ y \in ℕ \to π \neq 0$
129	73	rpne0d	$⊢ y \in ℕ \to 2 \neq 0$
130	124 121 56 128 129	divcan5d	$⊢ y \in ℕ \to \frac{2 (y + 1) π}{2 π} = \frac{(y + 1) π}{π}$
131	120 121 128	divcan4d	$⊢ y \in ℕ \to \frac{(y + 1) π}{π} = y + 1$
132	123 130 131	3eqtrd	$⊢ y \in ℕ \to \frac{2 (y + 1) π}{2 π} = y + 1$
133	80	peano2zd	$⊢ y \in ℕ \to y + 1 \in ℤ$
134	132 133	eqeltrd	$⊢ y \in ℕ \to \frac{2 (y + 1) π}{2 π} \in ℤ$
135		peano2cn	$⊢ y \in ℂ \to y + 1 \in ℂ$
136	57 135	syl	$⊢ y \in ℕ \to y + 1 \in ℂ$
137	56 136	mulcld	$⊢ y \in ℕ \to 2 (y + 1) \in ℂ$
138	137 121	mulcld	$⊢ y \in ℕ \to 2 (y + 1) π \in ℂ$
139		coseq1	$⊢ 2 (y + 1) π \in ℂ \to (\cos 2 (y + 1) π = 1 \leftrightarrow \frac{2 (y + 1) π}{2 π} \in ℤ)$
140	138 139	syl	$⊢ y \in ℕ \to (\cos 2 (y + 1) π = 1 \leftrightarrow \frac{2 (y + 1) π}{2 π} \in ℤ)$
141	134 140	mpbird	$⊢ y \in ℕ \to \cos 2 (y + 1) π = 1$
142	119 141	eqtrd	$⊢ y \in ℕ \to \cos (2 y + 1 + 1) π = 1$
143	114 142	oveq12d	$⊢ y \in ℕ \to \sum_{n = 1}^{2 y + 1} \cos n π + \cos (2 y + 1 + 1) π = \sum_{n = 1}^{2 y} \cos n π + \cos (2 y + 1) π + 1$
144	143	adantr	$⊢ (y \in ℕ \land \sum_{n = 1}^{2 y} \cos n π = 0) \to \sum_{n = 1}^{2 y + 1} \cos n π + \cos (2 y + 1 + 1) π = \sum_{n = 1}^{2 y} \cos n π + \cos (2 y + 1) π + 1$
145		simpr	$⊢ (y \in ℕ \land \sum_{n = 1}^{2 y} \cos n π = 0) \to \sum_{n = 1}^{2 y} \cos n π = 0$
146	60 58 121	adddird	$⊢ y \in ℕ \to (2 y + 1) π = 2 y π + 1 π$
147	60 121	mulcld	$⊢ y \in ℕ \to 2 y π \in ℂ$
148	41 121	eqeltrid	$⊢ y \in ℕ \to 1 π \in ℂ$
149	147 148	addcomd	$⊢ y \in ℕ \to 2 y π + 1 π = 1 π + 2 y π$
150	41	a1i	$⊢ y \in ℕ \to 1 π = π$
151	56 57	mulcomd	$⊢ y \in ℕ \to 2 y = y \cdot 2$
152	151	oveq1d	$⊢ y \in ℕ \to 2 y π = y \cdot 2 π$
153	57 56 121	mulassd	$⊢ y \in ℕ \to y \cdot 2 π = y 2 π$
154	152 153	eqtrd	$⊢ y \in ℕ \to 2 y π = y 2 π$
155	150 154	oveq12d	$⊢ y \in ℕ \to 1 π + 2 y π = π + y 2 π$
156	146 149 155	3eqtrd	$⊢ y \in ℕ \to (2 y + 1) π = π + y 2 π$
157	156	fveq2d	$⊢ y \in ℕ \to \cos (2 y + 1) π = \cos (π + y 2 π)$
158		cosper	$⊢ (π \in ℂ \land y \in ℤ) \to \cos (π + y 2 π) = \cos π$
159	28 80 158	sylancr	$⊢ y \in ℕ \to \cos (π + y 2 π) = \cos π$
160	46	a1i	$⊢ y \in ℕ \to \cos π = - 1$
161	157 159 160	3eqtrd	$⊢ y \in ℕ \to \cos (2 y + 1) π = - 1$
162	161	adantr	$⊢ (y \in ℕ \land \sum_{n = 1}^{2 y} \cos n π = 0) \to \cos (2 y + 1) π = - 1$
163	145 162	oveq12d	$⊢ (y \in ℕ \land \sum_{n = 1}^{2 y} \cos n π = 0) \to \sum_{n = 1}^{2 y} \cos n π + \cos (2 y + 1) π = 0 + -1$
164	163	oveq1d	$⊢ (y \in ℕ \land \sum_{n = 1}^{2 y} \cos n π = 0) \to \sum_{n = 1}^{2 y} \cos n π + \cos (2 y + 1) π + 1 = 0 + -1 + 1$
165	50	addid2i	$⊢ 0 + -1 = - 1$
166	165	oveq1i	$⊢ 0 + -1 + 1 = - 1 + 1$
167	166 52	eqtri	$⊢ 0 + -1 + 1 = 0$
168	164 167	eqtrdi	$⊢ (y \in ℕ \land \sum_{n = 1}^{2 y} \cos n π = 0) \to \sum_{n = 1}^{2 y} \cos n π + \cos (2 y + 1) π + 1 = 0$
169	144 168	eqtrd	$⊢ (y \in ℕ \land \sum_{n = 1}^{2 y} \cos n π = 0) \to \sum_{n = 1}^{2 y + 1} \cos n π + \cos (2 y + 1 + 1) π = 0$
170	65 94 169	3eqtrd	$⊢ (y \in ℕ \land \sum_{n = 1}^{2 y} \cos n π = 0) \to \sum_{n = 1}^{2 (y + 1)} \cos n π = 0$
171	170	ex	$⊢ y \in ℕ \to (\sum_{n = 1}^{2 y} \cos n π = 0 \to \sum_{n = 1}^{2 (y + 1)} \cos n π = 0)$
172	4 8 12 16 54 171	nnind	$⊢ K \in ℕ \to \sum_{n = 1}^{2 K} \cos n π = 0$

Metamath Proof Explorer

Theorem dirkertrigeqlem1

Proof