dirkertrigeqlem3

Description: Trigonometric equality lemma for the Dirichlet Kernel trigonometric equality. Here we handle the case for an angle that's an odd multiple of _pi . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	dirkertrigeqlem3.n	$⊢ φ \to N \in ℕ$
	dirkertrigeqlem3.k	$⊢ φ \to K \in ℤ$
	dirkertrigeqlem3.a	$⊢ A = (2 K + 1) π$
Assertion	dirkertrigeqlem3	$⊢ φ \to \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n A}{π} = \frac{\sin (N + (\frac{1}{2})) A}{2 π \sin (\frac{A}{2})}$

Proof

Step	Hyp	Ref	Expression
1		dirkertrigeqlem3.n	$⊢ φ \to N \in ℕ$
2		dirkertrigeqlem3.k	$⊢ φ \to K \in ℤ$
3		dirkertrigeqlem3.a	$⊢ A = (2 K + 1) π$
4	3	a1i	$⊢ (φ \land n \in (1 \dots N)) \to A = (2 K + 1) π$
5	4	oveq2d	$⊢ (φ \land n \in (1 \dots N)) \to n A = n (2 K + 1) π$
6		elfzelz	$⊢ n \in (1 \dots N) \to n \in ℤ$
7	6	zcnd	$⊢ n \in (1 \dots N) \to n \in ℂ$
8	7	adantl	$⊢ (φ \land n \in (1 \dots N)) \to n \in ℂ$
9		2cnd	$⊢ (φ \land n \in (1 \dots N)) \to 2 \in ℂ$
10	2	zcnd	$⊢ φ \to K \in ℂ$
11	10	adantr	$⊢ (φ \land n \in (1 \dots N)) \to K \in ℂ$
12	9 11	mulcld	$⊢ (φ \land n \in (1 \dots N)) \to 2 K \in ℂ$
13		1cnd	$⊢ (φ \land n \in (1 \dots N)) \to 1 \in ℂ$
14	12 13	addcld	$⊢ (φ \land n \in (1 \dots N)) \to 2 K + 1 \in ℂ$
15		picn	$⊢ π \in ℂ$
16	15	a1i	$⊢ (φ \land n \in (1 \dots N)) \to π \in ℂ$
17	14 16	mulcld	$⊢ (φ \land n \in (1 \dots N)) \to (2 K + 1) π \in ℂ$
18	8 17	mulcomd	$⊢ (φ \land n \in (1 \dots N)) \to n (2 K + 1) π = (2 K + 1) π n$
19	14 16 8	mulassd	$⊢ (φ \land n \in (1 \dots N)) \to (2 K + 1) π n = (2 K + 1) π n$
20	16 8	mulcld	$⊢ (φ \land n \in (1 \dots N)) \to π n \in ℂ$
21	12 13 20	adddird	$⊢ (φ \land n \in (1 \dots N)) \to (2 K + 1) π n = 2 K π n + 1 π n$
22	12 20	mulcld	$⊢ (φ \land n \in (1 \dots N)) \to 2 K π n \in ℂ$
23	13 20	mulcld	$⊢ (φ \land n \in (1 \dots N)) \to 1 π n \in ℂ$
24	22 23	addcomd	$⊢ (φ \land n \in (1 \dots N)) \to 2 K π n + 1 π n = 1 π n + 2 K π n$
25	15	a1i	$⊢ n \in (1 \dots N) \to π \in ℂ$
26	25 7	mulcld	$⊢ n \in (1 \dots N) \to π n \in ℂ$
27	26	mulid2d	$⊢ n \in (1 \dots N) \to 1 π n = π n$
28	27	adantl	$⊢ (φ \land n \in (1 \dots N)) \to 1 π n = π n$
29	9 11 16 8	mul4d	$⊢ (φ \land n \in (1 \dots N)) \to 2 K π n = 2 π K n$
30	9 16	mulcld	$⊢ (φ \land n \in (1 \dots N)) \to 2 π \in ℂ$
31	11 8	mulcld	$⊢ (φ \land n \in (1 \dots N)) \to K n \in ℂ$
32	30 31	mulcomd	$⊢ (φ \land n \in (1 \dots N)) \to 2 π K n = K n 2 π$
33	29 32	eqtrd	$⊢ (φ \land n \in (1 \dots N)) \to 2 K π n = K n 2 π$
34	28 33	oveq12d	$⊢ (φ \land n \in (1 \dots N)) \to 1 π n + 2 K π n = π n + K n 2 π$
35	24 34	eqtrd	$⊢ (φ \land n \in (1 \dots N)) \to 2 K π n + 1 π n = π n + K n 2 π$
36	19 21 35	3eqtrd	$⊢ (φ \land n \in (1 \dots N)) \to (2 K + 1) π n = π n + K n 2 π$
37	5 18 36	3eqtrd	$⊢ (φ \land n \in (1 \dots N)) \to n A = π n + K n 2 π$
38	37	fveq2d	$⊢ (φ \land n \in (1 \dots N)) \to \cos n A = \cos (π n + K n 2 π)$
39	2	adantr	$⊢ (φ \land n \in (1 \dots N)) \to K \in ℤ$
40	6	adantl	$⊢ (φ \land n \in (1 \dots N)) \to n \in ℤ$
41	39 40	zmulcld	$⊢ (φ \land n \in (1 \dots N)) \to K n \in ℤ$
42		cosper	$⊢ (π n \in ℂ \land K n \in ℤ) \to \cos (π n + K n 2 π) = \cos π n$
43	20 41 42	syl2anc	$⊢ (φ \land n \in (1 \dots N)) \to \cos (π n + K n 2 π) = \cos π n$
44	38 43	eqtrd	$⊢ (φ \land n \in (1 \dots N)) \to \cos n A = \cos π n$
45	44	sumeq2dv	$⊢ φ \to \sum_{n = 1}^{N} \cos n A = \sum_{n = 1}^{N} \cos π n$
46	45	oveq2d	$⊢ φ \to (\frac{1}{2}) + \sum_{n = 1}^{N} \cos n A = (\frac{1}{2}) + \sum_{n = 1}^{N} \cos π n$
47	46	oveq1d	$⊢ φ \to \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n A}{π} = \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos π n}{π}$
48	47	adantr	$⊢ (φ \land N \mod 2 = 0) \to \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n A}{π} = \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos π n}{π}$
49	1	nncnd	$⊢ φ \to N \in ℂ$
50		2cnd	$⊢ φ \to 2 \in ℂ$
51		2ne0	$⊢ 2 \neq 0$
52	51	a1i	$⊢ φ \to 2 \neq 0$
53	49 50 52	divcan2d	$⊢ φ \to 2 (\frac{N}{2}) = N$
54	53	eqcomd	$⊢ φ \to N = 2 (\frac{N}{2})$
55	54	oveq2d	$⊢ φ \to (1 \dots N) = (1 \dots 2 (\frac{N}{2}))$
56	55	sumeq1d	$⊢ φ \to \sum_{n = 1}^{N} \cos π n = \sum_{n = 1}^{2 (\frac{N}{2})} \cos π n$
57	56	adantr	$⊢ (φ \land N \mod 2 = 0) \to \sum_{n = 1}^{N} \cos π n = \sum_{n = 1}^{2 (\frac{N}{2})} \cos π n$
58	15	a1i	$⊢ n \in (1 \dots 2 (\frac{N}{2})) \to π \in ℂ$
59		elfzelz	$⊢ n \in (1 \dots 2 (\frac{N}{2})) \to n \in ℤ$
60	59	zcnd	$⊢ n \in (1 \dots 2 (\frac{N}{2})) \to n \in ℂ$
61	58 60	mulcomd	$⊢ n \in (1 \dots 2 (\frac{N}{2})) \to π n = n π$
62	61	fveq2d	$⊢ n \in (1 \dots 2 (\frac{N}{2})) \to \cos π n = \cos n π$
63	62	rgen	$⊢ \forall n \in (1 \dots 2 (\frac{N}{2})) \cos π n = \cos n π$
64	63	a1i	$⊢ (φ \land N \mod 2 = 0) \to \forall n \in (1 \dots 2 (\frac{N}{2})) \cos π n = \cos n π$
65	64	sumeq2d	$⊢ (φ \land N \mod 2 = 0) \to \sum_{n = 1}^{2 (\frac{N}{2})} \cos π n = \sum_{n = 1}^{2 (\frac{N}{2})} \cos n π$
66		simpr	$⊢ (φ \land N \mod 2 = 0) \to N \mod 2 = 0$
67	1	nnred	$⊢ φ \to N \in ℝ$
68	67	adantr	$⊢ (φ \land N \mod 2 = 0) \to N \in ℝ$
69		2rp	$⊢ 2 \in ℝ^{+}$
70		mod0	$⊢ (N \in ℝ \land 2 \in ℝ^{+}) \to (N \mod 2 = 0 \leftrightarrow \frac{N}{2} \in ℤ)$
71	68 69 70	sylancl	$⊢ (φ \land N \mod 2 = 0) \to (N \mod 2 = 0 \leftrightarrow \frac{N}{2} \in ℤ)$
72	66 71	mpbid	$⊢ (φ \land N \mod 2 = 0) \to \frac{N}{2} \in ℤ$
73		2re	$⊢ 2 \in ℝ$
74	73	a1i	$⊢ φ \to 2 \in ℝ$
75	1	nngt0d	$⊢ φ \to 0 < N$
76		2pos	$⊢ 0 < 2$
77	76	a1i	$⊢ φ \to 0 < 2$
78	67 74 75 77	divgt0d	$⊢ φ \to 0 < \frac{N}{2}$
79	78	adantr	$⊢ (φ \land N \mod 2 = 0) \to 0 < \frac{N}{2}$
80		elnnz	$⊢ \frac{N}{2} \in ℕ \leftrightarrow (\frac{N}{2} \in ℤ \land 0 < \frac{N}{2})$
81	72 79 80	sylanbrc	$⊢ (φ \land N \mod 2 = 0) \to \frac{N}{2} \in ℕ$
82		dirkertrigeqlem1	$⊢ \frac{N}{2} \in ℕ \to \sum_{n = 1}^{2 (\frac{N}{2})} \cos n π = 0$
83	81 82	syl	$⊢ (φ \land N \mod 2 = 0) \to \sum_{n = 1}^{2 (\frac{N}{2})} \cos n π = 0$
84	57 65 83	3eqtrd	$⊢ (φ \land N \mod 2 = 0) \to \sum_{n = 1}^{N} \cos π n = 0$
85	84	oveq2d	$⊢ (φ \land N \mod 2 = 0) \to (\frac{1}{2}) + \sum_{n = 1}^{N} \cos π n = (\frac{1}{2}) + 0$
86		halfcn	$⊢ \frac{1}{2} \in ℂ$
87	86	addid1i	$⊢ (\frac{1}{2}) + 0 = \frac{1}{2}$
88	85 87	eqtrdi	$⊢ (φ \land N \mod 2 = 0) \to (\frac{1}{2}) + \sum_{n = 1}^{N} \cos π n = \frac{1}{2}$
89	88	oveq1d	$⊢ (φ \land N \mod 2 = 0) \to \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos π n}{π} = \frac{\frac{1}{2}}{π}$
90		ax-1cn	$⊢ 1 \in ℂ$
91		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
92		pire	$⊢ π \in ℝ$
93		pipos	$⊢ 0 < π$
94	92 93	gt0ne0ii	$⊢ π \neq 0$
95	15 94	pm3.2i	$⊢ (π \in ℂ \land π \neq 0)$
96		divdiv1	$⊢ (1 \in ℂ \land (2 \in ℂ \land 2 \neq 0) \land (π \in ℂ \land π \neq 0)) \to \frac{\frac{1}{2}}{π} = \frac{1}{2 π}$
97	90 91 95 96	mp3an	$⊢ \frac{\frac{1}{2}}{π} = \frac{1}{2 π}$
98	97	a1i	$⊢ (φ \land N \mod 2 = 0) \to \frac{\frac{1}{2}}{π} = \frac{1}{2 π}$
99	48 89 98	3eqtrd	$⊢ (φ \land N \mod 2 = 0) \to \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n A}{π} = \frac{1}{2 π}$
100	3	oveq2i	$⊢ (N + (\frac{1}{2})) A = (N + (\frac{1}{2})) (2 K + 1) π$
101	100	a1i	$⊢ φ \to (N + (\frac{1}{2})) A = (N + (\frac{1}{2})) (2 K + 1) π$
102	86	a1i	$⊢ φ \to \frac{1}{2} \in ℂ$
103	49 102	addcld	$⊢ φ \to N + (\frac{1}{2}) \in ℂ$
104	50 10	mulcld	$⊢ φ \to 2 K \in ℂ$
105		peano2cn	$⊢ 2 K \in ℂ \to 2 K + 1 \in ℂ$
106	104 105	syl	$⊢ φ \to 2 K + 1 \in ℂ$
107	15	a1i	$⊢ φ \to π \in ℂ$
108	103 106 107	mulassd	$⊢ φ \to (N + (\frac{1}{2})) (2 K + 1) π = (N + (\frac{1}{2})) (2 K + 1) π$
109		1cnd	$⊢ φ \to 1 \in ℂ$
110	49 102 104 109	muladdd	$⊢ φ \to (N + (\frac{1}{2})) (2 K + 1) = N 2 K + 1 (\frac{1}{2}) + N \cdot 1 + 2 K (\frac{1}{2})$
111	49 50 10	mul12d	$⊢ φ \to N 2 K = 2 N K$
112	102	mulid2d	$⊢ φ \to 1 (\frac{1}{2}) = \frac{1}{2}$
113	111 112	oveq12d	$⊢ φ \to N 2 K + 1 (\frac{1}{2}) = 2 N K + (\frac{1}{2})$
114	49	mulid1d	$⊢ φ \to N \cdot 1 = N$
115	50 10	mulcomd	$⊢ φ \to 2 K = K \cdot 2$
116	115	oveq1d	$⊢ φ \to 2 K (\frac{1}{2}) = K \cdot 2 (\frac{1}{2})$
117	10 50 102	mulassd	$⊢ φ \to K \cdot 2 (\frac{1}{2}) = K 2 (\frac{1}{2})$
118		2cn	$⊢ 2 \in ℂ$
119	118 51	recidi	$⊢ 2 (\frac{1}{2}) = 1$
120	119	oveq2i	$⊢ K 2 (\frac{1}{2}) = K \cdot 1$
121	10	mulid1d	$⊢ φ \to K \cdot 1 = K$
122	120 121	syl5eq	$⊢ φ \to K 2 (\frac{1}{2}) = K$
123	116 117 122	3eqtrd	$⊢ φ \to 2 K (\frac{1}{2}) = K$
124	114 123	oveq12d	$⊢ φ \to N \cdot 1 + 2 K (\frac{1}{2}) = N + K$
125	113 124	oveq12d	$⊢ φ \to N 2 K + 1 (\frac{1}{2}) + N \cdot 1 + 2 K (\frac{1}{2}) = 2 N K + (\frac{1}{2}) + N + K$
126	49 10	mulcld	$⊢ φ \to N K \in ℂ$
127	50 126	mulcld	$⊢ φ \to 2 N K \in ℂ$
128	49 10	addcld	$⊢ φ \to N + K \in ℂ$
129	127 102 128	addassd	$⊢ φ \to 2 N K + (\frac{1}{2}) + N + K = 2 N K + (\frac{1}{2}) + (N + K)$
130	110 125 129	3eqtrd	$⊢ φ \to (N + (\frac{1}{2})) (2 K + 1) = 2 N K + (\frac{1}{2}) + (N + K)$
131	102 128	addcld	$⊢ φ \to (\frac{1}{2}) + N + K \in ℂ$
132	127 131	addcomd	$⊢ φ \to 2 N K + (\frac{1}{2}) + (N + K) = (\frac{1}{2}) + (N + K) + 2 N K$
133	50 126	mulcomd	$⊢ φ \to 2 N K = N K \cdot 2$
134	133	oveq2d	$⊢ φ \to (\frac{1}{2}) + (N + K) + 2 N K = (\frac{1}{2}) + (N + K) + N K \cdot 2$
135	130 132 134	3eqtrd	$⊢ φ \to (N + (\frac{1}{2})) (2 K + 1) = (\frac{1}{2}) + (N + K) + N K \cdot 2$
136	135	oveq1d	$⊢ φ \to (N + (\frac{1}{2})) (2 K + 1) π = ((\frac{1}{2}) + (N + K) + N K \cdot 2) π$
137	126 50	mulcld	$⊢ φ \to N K \cdot 2 \in ℂ$
138	131 137 107	adddird	$⊢ φ \to ((\frac{1}{2}) + (N + K) + N K \cdot 2) π = ((\frac{1}{2}) + N + K) π + N K \cdot 2 π$
139	126 50 107	mulassd	$⊢ φ \to N K \cdot 2 π = N K 2 π$
140	139	oveq2d	$⊢ φ \to ((\frac{1}{2}) + N + K) π + N K \cdot 2 π = ((\frac{1}{2}) + N + K) π + N K 2 π$
141	136 138 140	3eqtrd	$⊢ φ \to (N + (\frac{1}{2})) (2 K + 1) π = ((\frac{1}{2}) + N + K) π + N K 2 π$
142	101 108 141	3eqtr2d	$⊢ φ \to (N + (\frac{1}{2})) A = ((\frac{1}{2}) + N + K) π + N K 2 π$
143	142	fveq2d	$⊢ φ \to \sin (N + (\frac{1}{2})) A = \sin (((\frac{1}{2}) + N + K) π + N K 2 π)$
144	131 107	mulcld	$⊢ φ \to ((\frac{1}{2}) + N + K) π \in ℂ$
145	1	nnzd	$⊢ φ \to N \in ℤ$
146	145 2	zmulcld	$⊢ φ \to N K \in ℤ$
147		sinper	$⊢ (((\frac{1}{2}) + N + K) π \in ℂ \land N K \in ℤ) \to \sin (((\frac{1}{2}) + N + K) π + N K 2 π) = \sin ((\frac{1}{2}) + N + K) π$
148	144 146 147	syl2anc	$⊢ φ \to \sin (((\frac{1}{2}) + N + K) π + N K 2 π) = \sin ((\frac{1}{2}) + N + K) π$
149	102 128	addcomd	$⊢ φ \to (\frac{1}{2}) + N + K = N + K + (\frac{1}{2})$
150	49 10 102	addassd	$⊢ φ \to N + K + (\frac{1}{2}) = N + K + (\frac{1}{2})$
151	10 102	addcld	$⊢ φ \to K + (\frac{1}{2}) \in ℂ$
152	49 151	addcomd	$⊢ φ \to N + K + (\frac{1}{2}) = K + (\frac{1}{2}) + N$
153	149 150 152	3eqtrd	$⊢ φ \to (\frac{1}{2}) + N + K = K + (\frac{1}{2}) + N$
154	153	oveq1d	$⊢ φ \to ((\frac{1}{2}) + N + K) π = (K + (\frac{1}{2}) + N) π$
155	154	fveq2d	$⊢ φ \to \sin ((\frac{1}{2}) + N + K) π = \sin (K + (\frac{1}{2}) + N) π$
156	143 148 155	3eqtrd	$⊢ φ \to \sin (N + (\frac{1}{2})) A = \sin (K + (\frac{1}{2}) + N) π$
157	3	a1i	$⊢ φ \to A = (2 K + 1) π$
158	157	oveq1d	$⊢ φ \to \frac{A}{2} = \frac{(2 K + 1) π}{2}$
159	106 107 50 52	div23d	$⊢ φ \to \frac{(2 K + 1) π}{2} = (\frac{2 K + 1}{2}) π$
160	104 109 50 52	divdird	$⊢ φ \to \frac{2 K + 1}{2} = (\frac{2 K}{2}) + (\frac{1}{2})$
161	10 50 52	divcan3d	$⊢ φ \to \frac{2 K}{2} = K$
162	161	oveq1d	$⊢ φ \to (\frac{2 K}{2}) + (\frac{1}{2}) = K + (\frac{1}{2})$
163	160 162	eqtrd	$⊢ φ \to \frac{2 K + 1}{2} = K + (\frac{1}{2})$
164	163	oveq1d	$⊢ φ \to (\frac{2 K + 1}{2}) π = (K + (\frac{1}{2})) π$
165	158 159 164	3eqtrd	$⊢ φ \to \frac{A}{2} = (K + (\frac{1}{2})) π$
166	165	fveq2d	$⊢ φ \to \sin (\frac{A}{2}) = \sin (K + (\frac{1}{2})) π$
167	166	oveq2d	$⊢ φ \to 2 π \sin (\frac{A}{2}) = 2 π \sin (K + (\frac{1}{2})) π$
168	156 167	oveq12d	$⊢ φ \to \frac{\sin (N + (\frac{1}{2})) A}{2 π \sin (\frac{A}{2})} = \frac{\sin (K + (\frac{1}{2}) + N) π}{2 π \sin (K + (\frac{1}{2})) π}$
169	168	adantr	$⊢ (φ \land N \mod 2 = 0) \to \frac{\sin (N + (\frac{1}{2})) A}{2 π \sin (\frac{A}{2})} = \frac{\sin (K + (\frac{1}{2}) + N) π}{2 π \sin (K + (\frac{1}{2})) π}$
170	151 49 107	adddird	$⊢ φ \to (K + (\frac{1}{2}) + N) π = (K + (\frac{1}{2})) π + N π$
171	170	fveq2d	$⊢ φ \to \sin (K + (\frac{1}{2}) + N) π = \sin ((K + (\frac{1}{2})) π + N π)$
172	171	oveq1d	$⊢ φ \to \frac{\sin (K + (\frac{1}{2}) + N) π}{2 π \sin (K + (\frac{1}{2})) π} = \frac{\sin ((K + (\frac{1}{2})) π + N π)}{2 π \sin (K + (\frac{1}{2})) π}$
173	172	adantr	$⊢ (φ \land N \mod 2 = 0) \to \frac{\sin (K + (\frac{1}{2}) + N) π}{2 π \sin (K + (\frac{1}{2})) π} = \frac{\sin ((K + (\frac{1}{2})) π + N π)}{2 π \sin (K + (\frac{1}{2})) π}$
174	49	halfcld	$⊢ φ \to \frac{N}{2} \in ℂ$
175	50 174	mulcomd	$⊢ φ \to 2 (\frac{N}{2}) = (\frac{N}{2}) \cdot 2$
176	53 175	eqtr3d	$⊢ φ \to N = (\frac{N}{2}) \cdot 2$
177	176	oveq1d	$⊢ φ \to N π = (\frac{N}{2}) \cdot 2 π$
178	174 50 107	mulassd	$⊢ φ \to (\frac{N}{2}) \cdot 2 π = (\frac{N}{2}) 2 π$
179	177 178	eqtrd	$⊢ φ \to N π = (\frac{N}{2}) 2 π$
180	179	oveq2d	$⊢ φ \to (K + (\frac{1}{2})) π + N π = (K + (\frac{1}{2})) π + (\frac{N}{2}) 2 π$
181	180	fveq2d	$⊢ φ \to \sin ((K + (\frac{1}{2})) π + N π) = \sin ((K + (\frac{1}{2})) π + (\frac{N}{2}) 2 π)$
182	181	adantr	$⊢ (φ \land N \mod 2 = 0) \to \sin ((K + (\frac{1}{2})) π + N π) = \sin ((K + (\frac{1}{2})) π + (\frac{N}{2}) 2 π)$
183	10	adantr	$⊢ (φ \land N \mod 2 = 0) \to K \in ℂ$
184		1cnd	$⊢ (φ \land N \mod 2 = 0) \to 1 \in ℂ$
185	184	halfcld	$⊢ (φ \land N \mod 2 = 0) \to \frac{1}{2} \in ℂ$
186	183 185	addcld	$⊢ (φ \land N \mod 2 = 0) \to K + (\frac{1}{2}) \in ℂ$
187	15	a1i	$⊢ (φ \land N \mod 2 = 0) \to π \in ℂ$
188	186 187	mulcld	$⊢ (φ \land N \mod 2 = 0) \to (K + (\frac{1}{2})) π \in ℂ$
189		sinper	$⊢ ((K + (\frac{1}{2})) π \in ℂ \land \frac{N}{2} \in ℤ) \to \sin ((K + (\frac{1}{2})) π + (\frac{N}{2}) 2 π) = \sin (K + (\frac{1}{2})) π$
190	188 72 189	syl2anc	$⊢ (φ \land N \mod 2 = 0) \to \sin ((K + (\frac{1}{2})) π + (\frac{N}{2}) 2 π) = \sin (K + (\frac{1}{2})) π$
191	182 190	eqtrd	$⊢ (φ \land N \mod 2 = 0) \to \sin ((K + (\frac{1}{2})) π + N π) = \sin (K + (\frac{1}{2})) π$
192	50 107	mulcld	$⊢ φ \to 2 π \in ℂ$
193	151 107	mulcld	$⊢ φ \to (K + (\frac{1}{2})) π \in ℂ$
194	193	sincld	$⊢ φ \to \sin (K + (\frac{1}{2})) π \in ℂ$
195	192 194	mulcomd	$⊢ φ \to 2 π \sin (K + (\frac{1}{2})) π = \sin (K + (\frac{1}{2})) π 2 π$
196	195	adantr	$⊢ (φ \land N \mod 2 = 0) \to 2 π \sin (K + (\frac{1}{2})) π = \sin (K + (\frac{1}{2})) π 2 π$
197	191 196	oveq12d	$⊢ (φ \land N \mod 2 = 0) \to \frac{\sin ((K + (\frac{1}{2})) π + N π)}{2 π \sin (K + (\frac{1}{2})) π} = \frac{\sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π 2 π}$
198	94	a1i	$⊢ φ \to π \neq 0$
199	151 107 198	divcan4d	$⊢ φ \to \frac{(K + (\frac{1}{2})) π}{π} = K + (\frac{1}{2})$
200	2	zred	$⊢ φ \to K \in ℝ$
201	69	a1i	$⊢ φ \to 2 \in ℝ^{+}$
202	201	rpreccld	$⊢ φ \to \frac{1}{2} \in ℝ^{+}$
203	200 202	ltaddrpd	$⊢ φ \to K < K + (\frac{1}{2})$
204		1red	$⊢ φ \to 1 \in ℝ$
205	204	rehalfcld	$⊢ φ \to \frac{1}{2} \in ℝ$
206		halflt1	$⊢ \frac{1}{2} < 1$
207	206	a1i	$⊢ φ \to \frac{1}{2} < 1$
208	205 204 200 207	ltadd2dd	$⊢ φ \to K + (\frac{1}{2}) < K + 1$
209		btwnnz	$⊢ (K \in ℤ \land K < K + (\frac{1}{2}) \land K + (\frac{1}{2}) < K + 1) \to \neg K + (\frac{1}{2}) \in ℤ$
210	2 203 208 209	syl3anc	$⊢ φ \to \neg K + (\frac{1}{2}) \in ℤ$
211	199 210	eqneltrd	$⊢ φ \to \neg \frac{(K + (\frac{1}{2})) π}{π} \in ℤ$
212		sineq0	$⊢ (K + (\frac{1}{2})) π \in ℂ \to (\sin (K + (\frac{1}{2})) π = 0 \leftrightarrow \frac{(K + (\frac{1}{2})) π}{π} \in ℤ)$
213	193 212	syl	$⊢ φ \to (\sin (K + (\frac{1}{2})) π = 0 \leftrightarrow \frac{(K + (\frac{1}{2})) π}{π} \in ℤ)$
214	211 213	mtbird	$⊢ φ \to \neg \sin (K + (\frac{1}{2})) π = 0$
215	214	neqned	$⊢ φ \to \sin (K + (\frac{1}{2})) π \neq 0$
216	50 107 52 198	mulne0d	$⊢ φ \to 2 π \neq 0$
217	194 194 192 215 216	divdiv1d	$⊢ φ \to \frac{\frac{\sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π}}{2 π} = \frac{\sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π 2 π}$
218	194 215	dividd	$⊢ φ \to \frac{\sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π} = 1$
219	218	oveq1d	$⊢ φ \to \frac{\frac{\sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π}}{2 π} = \frac{1}{2 π}$
220	217 219	eqtr3d	$⊢ φ \to \frac{\sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π 2 π} = \frac{1}{2 π}$
221	220	adantr	$⊢ (φ \land N \mod 2 = 0) \to \frac{\sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π 2 π} = \frac{1}{2 π}$
222	197 221	eqtrd	$⊢ (φ \land N \mod 2 = 0) \to \frac{\sin ((K + (\frac{1}{2})) π + N π)}{2 π \sin (K + (\frac{1}{2})) π} = \frac{1}{2 π}$
223	169 173 222	3eqtrrd	$⊢ (φ \land N \mod 2 = 0) \to \frac{1}{2 π} = \frac{\sin (N + (\frac{1}{2})) A}{2 π \sin (\frac{A}{2})}$
224	99 223	eqtrd	$⊢ (φ \land N \mod 2 = 0) \to \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n A}{π} = \frac{\sin (N + (\frac{1}{2})) A}{2 π \sin (\frac{A}{2})}$
225	47	adantr	$⊢ (φ \land \neg N \mod 2 = 0) \to \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n A}{π} = \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos π n}{π}$
226	145	adantr	$⊢ (φ \land \neg N \mod 2 = 0) \to N \in ℤ$
227		simpr	$⊢ (φ \land \neg N \mod 2 = 0) \to \neg N \mod 2 = 0$
228	227	neqned	$⊢ (φ \land \neg N \mod 2 = 0) \to N \mod 2 \neq 0$
229		oddfl	$⊢ (N \in ℤ \land N \mod 2 \neq 0) \to N = 2 ⌊\frac{N}{2}⌋ + 1$
230	226 228 229	syl2anc	$⊢ (φ \land \neg N \mod 2 = 0) \to N = 2 ⌊\frac{N}{2}⌋ + 1$
231	230	oveq2d	$⊢ (φ \land \neg N \mod 2 = 0) \to (1 \dots N) = (1 \dots 2 ⌊\frac{N}{2}⌋ + 1)$
232	231	sumeq1d	$⊢ (φ \land \neg N \mod 2 = 0) \to \sum_{n = 1}^{N} \cos π n = \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋ + 1} \cos π n$
233		fvoveq1	$⊢ N = 1 \to ⌊\frac{N}{2}⌋ = ⌊\frac{1}{2}⌋$
234		halffl	$⊢ ⌊\frac{1}{2}⌋ = 0$
235	233 234	eqtrdi	$⊢ N = 1 \to ⌊\frac{N}{2}⌋ = 0$
236	235	oveq2d	$⊢ N = 1 \to 2 ⌊\frac{N}{2}⌋ = 2 \cdot 0$
237		2t0e0	$⊢ 2 \cdot 0 = 0$
238	236 237	eqtrdi	$⊢ N = 1 \to 2 ⌊\frac{N}{2}⌋ = 0$
239	238	oveq1d	$⊢ N = 1 \to 2 ⌊\frac{N}{2}⌋ + 1 = 0 + 1$
240	90	addid2i	$⊢ 0 + 1 = 1$
241	239 240	eqtrdi	$⊢ N = 1 \to 2 ⌊\frac{N}{2}⌋ + 1 = 1$
242	241	oveq2d	$⊢ N = 1 \to (1 \dots 2 ⌊\frac{N}{2}⌋ + 1) = (1 \dots 1)$
243	242	sumeq1d	$⊢ N = 1 \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋ + 1} \cos π n = \sum_{n = 1}^{1} \cos π n$
244		1z	$⊢ 1 \in ℤ$
245		coscl	$⊢ π \in ℂ \to \cos π \in ℂ$
246	15 245	ax-mp	$⊢ \cos π \in ℂ$
247		oveq2	$⊢ n = 1 \to π n = π \cdot 1$
248	15	mulid1i	$⊢ π \cdot 1 = π$
249	247 248	eqtrdi	$⊢ n = 1 \to π n = π$
250	249	fveq2d	$⊢ n = 1 \to \cos π n = \cos π$
251	250	fsum1	$⊢ (1 \in ℤ \land \cos π \in ℂ) \to \sum_{n = 1}^{1} \cos π n = \cos π$
252	244 246 251	mp2an	$⊢ \sum_{n = 1}^{1} \cos π n = \cos π$
253	252	a1i	$⊢ N = 1 \to \sum_{n = 1}^{1} \cos π n = \cos π$
254		cospi	$⊢ \cos π = - 1$
255	254	a1i	$⊢ N = 1 \to \cos π = - 1$
256	243 253 255	3eqtrd	$⊢ N = 1 \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋ + 1} \cos π n = - 1$
257	256	adantl	$⊢ (φ \land N = 1) \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋ + 1} \cos π n = - 1$
258		2nn	$⊢ 2 \in ℕ$
259	258	a1i	$⊢ (φ \land \neg N = 1) \to 2 \in ℕ$
260	67	rehalfcld	$⊢ φ \to \frac{N}{2} \in ℝ$
261	260	flcld	$⊢ φ \to ⌊\frac{N}{2}⌋ \in ℤ$
262	261	adantr	$⊢ (φ \land \neg N = 1) \to ⌊\frac{N}{2}⌋ \in ℤ$
263		2div2e1	$⊢ \frac{2}{2} = 1$
264	73	a1i	$⊢ (φ \land \neg N = 1) \to 2 \in ℝ$
265	67	adantr	$⊢ (φ \land \neg N = 1) \to N \in ℝ$
266	69	a1i	$⊢ (φ \land \neg N = 1) \to 2 \in ℝ^{+}$
267		neqne	$⊢ \neg N = 1 \to N \neq 1$
268		nnne1ge2	$⊢ (N \in ℕ \land N \neq 1) \to 2 \leq N$
269	1 267 268	syl2an	$⊢ (φ \land \neg N = 1) \to 2 \leq N$
270	264 265 266 269	lediv1dd	$⊢ (φ \land \neg N = 1) \to \frac{2}{2} \leq \frac{N}{2}$
271	263 270	eqbrtrrid	$⊢ (φ \land \neg N = 1) \to 1 \leq \frac{N}{2}$
272	260	adantr	$⊢ (φ \land \neg N = 1) \to \frac{N}{2} \in ℝ$
273		flge	$⊢ (\frac{N}{2} \in ℝ \land 1 \in ℤ) \to (1 \leq \frac{N}{2} \leftrightarrow 1 \leq ⌊\frac{N}{2}⌋)$
274	272 244 273	sylancl	$⊢ (φ \land \neg N = 1) \to (1 \leq \frac{N}{2} \leftrightarrow 1 \leq ⌊\frac{N}{2}⌋)$
275	271 274	mpbid	$⊢ (φ \land \neg N = 1) \to 1 \leq ⌊\frac{N}{2}⌋$
276		elnnz1	$⊢ ⌊\frac{N}{2}⌋ \in ℕ \leftrightarrow (⌊\frac{N}{2}⌋ \in ℤ \land 1 \leq ⌊\frac{N}{2}⌋)$
277	262 275 276	sylanbrc	$⊢ (φ \land \neg N = 1) \to ⌊\frac{N}{2}⌋ \in ℕ$
278	259 277	nnmulcld	$⊢ (φ \land \neg N = 1) \to 2 ⌊\frac{N}{2}⌋ \in ℕ$
279		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
280	278 279	eleqtrdi	$⊢ (φ \land \neg N = 1) \to 2 ⌊\frac{N}{2}⌋ \in ℤ_{\geq 1}$
281	15	a1i	$⊢ ((φ \land \neg N = 1) \land n \in (1 \dots 2 ⌊\frac{N}{2}⌋ + 1)) \to π \in ℂ$
282		elfzelz	$⊢ n \in (1 \dots 2 ⌊\frac{N}{2}⌋ + 1) \to n \in ℤ$
283	282	zcnd	$⊢ n \in (1 \dots 2 ⌊\frac{N}{2}⌋ + 1) \to n \in ℂ$
284	283	adantl	$⊢ ((φ \land \neg N = 1) \land n \in (1 \dots 2 ⌊\frac{N}{2}⌋ + 1)) \to n \in ℂ$
285	281 284	mulcld	$⊢ ((φ \land \neg N = 1) \land n \in (1 \dots 2 ⌊\frac{N}{2}⌋ + 1)) \to π n \in ℂ$
286	285	coscld	$⊢ ((φ \land \neg N = 1) \land n \in (1 \dots 2 ⌊\frac{N}{2}⌋ + 1)) \to \cos π n \in ℂ$
287		oveq2	$⊢ n = 2 ⌊\frac{N}{2}⌋ + 1 \to π n = π (2 ⌊\frac{N}{2}⌋ + 1)$
288	287	fveq2d	$⊢ n = 2 ⌊\frac{N}{2}⌋ + 1 \to \cos π n = \cos π (2 ⌊\frac{N}{2}⌋ + 1)$
289	280 286 288	fsump1	$⊢ (φ \land \neg N = 1) \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋ + 1} \cos π n = \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋} \cos π n + \cos π (2 ⌊\frac{N}{2}⌋ + 1)$
290	15	a1i	$⊢ n \in (1 \dots 2 ⌊\frac{N}{2}⌋) \to π \in ℂ$
291		elfzelz	$⊢ n \in (1 \dots 2 ⌊\frac{N}{2}⌋) \to n \in ℤ$
292	291	zcnd	$⊢ n \in (1 \dots 2 ⌊\frac{N}{2}⌋) \to n \in ℂ$
293	290 292	mulcomd	$⊢ n \in (1 \dots 2 ⌊\frac{N}{2}⌋) \to π n = n π$
294	293	fveq2d	$⊢ n \in (1 \dots 2 ⌊\frac{N}{2}⌋) \to \cos π n = \cos n π$
295	294	sumeq2i	$⊢ \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋} \cos π n = \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋} \cos n π$
296		dirkertrigeqlem1	$⊢ ⌊\frac{N}{2}⌋ \in ℕ \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋} \cos n π = 0$
297	277 296	syl	$⊢ (φ \land \neg N = 1) \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋} \cos n π = 0$
298	295 297	syl5eq	$⊢ (φ \land \neg N = 1) \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋} \cos π n = 0$
299	261	zcnd	$⊢ φ \to ⌊\frac{N}{2}⌋ \in ℂ$
300	50 299	mulcld	$⊢ φ \to 2 ⌊\frac{N}{2}⌋ \in ℂ$
301	107 300 109	adddid	$⊢ φ \to π (2 ⌊\frac{N}{2}⌋ + 1) = π 2 ⌊\frac{N}{2}⌋ + π \cdot 1$
302	107 50 299	mul13d	$⊢ φ \to π 2 ⌊\frac{N}{2}⌋ = ⌊\frac{N}{2}⌋ 2 π$
303	248	a1i	$⊢ φ \to π \cdot 1 = π$
304	302 303	oveq12d	$⊢ φ \to π 2 ⌊\frac{N}{2}⌋ + π \cdot 1 = ⌊\frac{N}{2}⌋ 2 π + π$
305	299 192	mulcld	$⊢ φ \to ⌊\frac{N}{2}⌋ 2 π \in ℂ$
306	305 107	addcomd	$⊢ φ \to ⌊\frac{N}{2}⌋ 2 π + π = π + ⌊\frac{N}{2}⌋ 2 π$
307	301 304 306	3eqtrd	$⊢ φ \to π (2 ⌊\frac{N}{2}⌋ + 1) = π + ⌊\frac{N}{2}⌋ 2 π$
308	307	fveq2d	$⊢ φ \to \cos π (2 ⌊\frac{N}{2}⌋ + 1) = \cos (π + ⌊\frac{N}{2}⌋ 2 π)$
309		cosper	$⊢ (π \in ℂ \land ⌊\frac{N}{2}⌋ \in ℤ) \to \cos (π + ⌊\frac{N}{2}⌋ 2 π) = \cos π$
310	107 261 309	syl2anc	$⊢ φ \to \cos (π + ⌊\frac{N}{2}⌋ 2 π) = \cos π$
311	254	a1i	$⊢ φ \to \cos π = - 1$
312	308 310 311	3eqtrd	$⊢ φ \to \cos π (2 ⌊\frac{N}{2}⌋ + 1) = - 1$
313	312	adantr	$⊢ (φ \land \neg N = 1) \to \cos π (2 ⌊\frac{N}{2}⌋ + 1) = - 1$
314	298 313	oveq12d	$⊢ (φ \land \neg N = 1) \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋} \cos π n + \cos π (2 ⌊\frac{N}{2}⌋ + 1) = 0 + -1$
315		neg1cn	$⊢ - 1 \in ℂ$
316	315	addid2i	$⊢ 0 + -1 = - 1$
317	316	a1i	$⊢ (φ \land \neg N = 1) \to 0 + -1 = - 1$
318	289 314 317	3eqtrd	$⊢ (φ \land \neg N = 1) \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋ + 1} \cos π n = - 1$
319	257 318	pm2.61dan	$⊢ φ \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋ + 1} \cos π n = - 1$
320	319	adantr	$⊢ (φ \land \neg N \mod 2 = 0) \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋ + 1} \cos π n = - 1$
321	232 320	eqtrd	$⊢ (φ \land \neg N \mod 2 = 0) \to \sum_{n = 1}^{N} \cos π n = - 1$
322	321	oveq2d	$⊢ (φ \land \neg N \mod 2 = 0) \to (\frac{1}{2}) + \sum_{n = 1}^{N} \cos π n = (\frac{1}{2}) + -1$
323	322	oveq1d	$⊢ (φ \land \neg N \mod 2 = 0) \to \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos π n}{π} = \frac{(\frac{1}{2}) + -1}{π}$
324	168 172	eqtrd	$⊢ φ \to \frac{\sin (N + (\frac{1}{2})) A}{2 π \sin (\frac{A}{2})} = \frac{\sin ((K + (\frac{1}{2})) π + N π)}{2 π \sin (K + (\frac{1}{2})) π}$
325	324	adantr	$⊢ (φ \land \neg N \mod 2 = 0) \to \frac{\sin (N + (\frac{1}{2})) A}{2 π \sin (\frac{A}{2})} = \frac{\sin ((K + (\frac{1}{2})) π + N π)}{2 π \sin (K + (\frac{1}{2})) π}$
326	230	oveq1d	$⊢ (φ \land \neg N \mod 2 = 0) \to N π = (2 ⌊\frac{N}{2}⌋ + 1) π$
327	300 109 107	adddird	$⊢ φ \to (2 ⌊\frac{N}{2}⌋ + 1) π = 2 ⌊\frac{N}{2}⌋ π + 1 π$
328	107	mulid2d	$⊢ φ \to 1 π = π$
329	328	oveq2d	$⊢ φ \to 2 ⌊\frac{N}{2}⌋ π + 1 π = 2 ⌊\frac{N}{2}⌋ π + π$
330	300 107	mulcld	$⊢ φ \to 2 ⌊\frac{N}{2}⌋ π \in ℂ$
331	330 107	addcomd	$⊢ φ \to 2 ⌊\frac{N}{2}⌋ π + π = π + 2 ⌊\frac{N}{2}⌋ π$
332	327 329 331	3eqtrd	$⊢ φ \to (2 ⌊\frac{N}{2}⌋ + 1) π = π + 2 ⌊\frac{N}{2}⌋ π$
333	332	adantr	$⊢ (φ \land \neg N \mod 2 = 0) \to (2 ⌊\frac{N}{2}⌋ + 1) π = π + 2 ⌊\frac{N}{2}⌋ π$
334	50 299	mulcomd	$⊢ φ \to 2 ⌊\frac{N}{2}⌋ = ⌊\frac{N}{2}⌋ \cdot 2$
335	334	oveq1d	$⊢ φ \to 2 ⌊\frac{N}{2}⌋ π = ⌊\frac{N}{2}⌋ \cdot 2 π$
336	299 50 107	mulassd	$⊢ φ \to ⌊\frac{N}{2}⌋ \cdot 2 π = ⌊\frac{N}{2}⌋ 2 π$
337	335 336	eqtrd	$⊢ φ \to 2 ⌊\frac{N}{2}⌋ π = ⌊\frac{N}{2}⌋ 2 π$
338	337	oveq2d	$⊢ φ \to π + 2 ⌊\frac{N}{2}⌋ π = π + ⌊\frac{N}{2}⌋ 2 π$
339	338	adantr	$⊢ (φ \land \neg N \mod 2 = 0) \to π + 2 ⌊\frac{N}{2}⌋ π = π + ⌊\frac{N}{2}⌋ 2 π$
340	326 333 339	3eqtrd	$⊢ (φ \land \neg N \mod 2 = 0) \to N π = π + ⌊\frac{N}{2}⌋ 2 π$
341	340	oveq2d	$⊢ (φ \land \neg N \mod 2 = 0) \to (K + (\frac{1}{2})) π + N π = (K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π$
342	193	adantr	$⊢ (φ \land \neg N \mod 2 = 0) \to (K + (\frac{1}{2})) π \in ℂ$
343	15	a1i	$⊢ (φ \land \neg N \mod 2 = 0) \to π \in ℂ$
344	305	adantr	$⊢ (φ \land \neg N \mod 2 = 0) \to ⌊\frac{N}{2}⌋ 2 π \in ℂ$
345	342 343 344	addassd	$⊢ (φ \land \neg N \mod 2 = 0) \to (K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π = (K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π$
346	341 345	eqtr4d	$⊢ (φ \land \neg N \mod 2 = 0) \to (K + (\frac{1}{2})) π + N π = (K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π$
347	346	fveq2d	$⊢ (φ \land \neg N \mod 2 = 0) \to \sin ((K + (\frac{1}{2})) π + N π) = \sin ((K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π)$
348	347	oveq1d	$⊢ (φ \land \neg N \mod 2 = 0) \to \frac{\sin ((K + (\frac{1}{2})) π + N π)}{2 π \sin (K + (\frac{1}{2})) π} = \frac{\sin ((K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π)}{2 π \sin (K + (\frac{1}{2})) π}$
349	193 107	addcld	$⊢ φ \to (K + (\frac{1}{2})) π + π \in ℂ$
350		sinper	$⊢ ((K + (\frac{1}{2})) π + π \in ℂ \land ⌊\frac{N}{2}⌋ \in ℤ) \to \sin ((K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π) = \sin ((K + (\frac{1}{2})) π + π)$
351	349 261 350	syl2anc	$⊢ φ \to \sin ((K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π) = \sin ((K + (\frac{1}{2})) π + π)$
352		sinppi	$⊢ (K + (\frac{1}{2})) π \in ℂ \to \sin ((K + (\frac{1}{2})) π + π) = - \sin (K + (\frac{1}{2})) π$
353	193 352	syl	$⊢ φ \to \sin ((K + (\frac{1}{2})) π + π) = - \sin (K + (\frac{1}{2})) π$
354	351 353	eqtrd	$⊢ φ \to \sin ((K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π) = - \sin (K + (\frac{1}{2})) π$
355	354	oveq1d	$⊢ φ \to \frac{\sin ((K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π)}{2 π \sin (K + (\frac{1}{2})) π} = \frac{- \sin (K + (\frac{1}{2})) π}{2 π \sin (K + (\frac{1}{2})) π}$
356	195	oveq2d	$⊢ φ \to \frac{- \sin (K + (\frac{1}{2})) π}{2 π \sin (K + (\frac{1}{2})) π} = \frac{- \sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π 2 π}$
357	194 194 215	divnegd	$⊢ φ \to - \frac{\sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π} = \frac{- \sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π}$
358	218	negeqd	$⊢ φ \to - \frac{\sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π} = - 1$
359	357 358	eqtr3d	$⊢ φ \to \frac{- \sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π} = - 1$
360	359	oveq1d	$⊢ φ \to \frac{\frac{- \sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π}}{2 π} = \frac{- 1}{2 π}$
361	194	negcld	$⊢ φ \to - \sin (K + (\frac{1}{2})) π \in ℂ$
362	361 194 192 215 216	divdiv1d	$⊢ φ \to \frac{\frac{- \sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π}}{2 π} = \frac{- \sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π 2 π}$
363	86 90	negsubi	$⊢ (\frac{1}{2}) + -1 = (\frac{1}{2}) - 1$
364	90 86	negsubdi2i	$⊢ - (1 - (\frac{1}{2})) = (\frac{1}{2}) - 1$
365		1mhlfehlf	$⊢ 1 - (\frac{1}{2}) = \frac{1}{2}$
366	365	negeqi	$⊢ - (1 - (\frac{1}{2})) = - \frac{1}{2}$
367		divneg	$⊢ (1 \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to - \frac{1}{2} = \frac{- 1}{2}$
368	90 118 51 367	mp3an	$⊢ - \frac{1}{2} = \frac{- 1}{2}$
369	366 368	eqtri	$⊢ - (1 - (\frac{1}{2})) = \frac{- 1}{2}$
370	363 364 369	3eqtr2i	$⊢ (\frac{1}{2}) + -1 = \frac{- 1}{2}$
371	370	oveq1i	$⊢ \frac{(\frac{1}{2}) + -1}{π} = \frac{\frac{- 1}{2}}{π}$
372		divdiv1	$⊢ (- 1 \in ℂ \land (2 \in ℂ \land 2 \neq 0) \land (π \in ℂ \land π \neq 0)) \to \frac{\frac{- 1}{2}}{π} = \frac{- 1}{2 π}$
373	315 91 95 372	mp3an	$⊢ \frac{\frac{- 1}{2}}{π} = \frac{- 1}{2 π}$
374	371 373	eqtr2i	$⊢ \frac{- 1}{2 π} = \frac{(\frac{1}{2}) + -1}{π}$
375	374	a1i	$⊢ φ \to \frac{- 1}{2 π} = \frac{(\frac{1}{2}) + -1}{π}$
376	360 362 375	3eqtr3d	$⊢ φ \to \frac{- \sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π 2 π} = \frac{(\frac{1}{2}) + -1}{π}$
377	355 356 376	3eqtrd	$⊢ φ \to \frac{\sin ((K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π)}{2 π \sin (K + (\frac{1}{2})) π} = \frac{(\frac{1}{2}) + -1}{π}$
378	377	adantr	$⊢ (φ \land \neg N \mod 2 = 0) \to \frac{\sin ((K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π)}{2 π \sin (K + (\frac{1}{2})) π} = \frac{(\frac{1}{2}) + -1}{π}$
379	325 348 378	3eqtrrd	$⊢ (φ \land \neg N \mod 2 = 0) \to \frac{(\frac{1}{2}) + -1}{π} = \frac{\sin (N + (\frac{1}{2})) A}{2 π \sin (\frac{A}{2})}$
380	225 323 379	3eqtrd	$⊢ (φ \land \neg N \mod 2 = 0) \to \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n A}{π} = \frac{\sin (N + (\frac{1}{2})) A}{2 π \sin (\frac{A}{2})}$
381	224 380	pm2.61dan	$⊢ φ \to \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n A}{π} = \frac{\sin (N + (\frac{1}{2})) A}{2 π \sin (\frac{A}{2})}$

Metamath Proof Explorer

Theorem dirkertrigeqlem3

Proof