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	mullidd	$⊢ 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	addridi	$⊢ (\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	mullidd	$⊢ φ \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	mulridd	$⊢ φ \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		2thalfe1	$⊢ 2 (\frac{1}{2}) = 1$
119	118	oveq2i	$⊢ K 2 (\frac{1}{2}) = K \cdot 1$
120	10	mulridd	$⊢ φ \to K \cdot 1 = K$
121	119 120	eqtrid	$⊢ φ \to K 2 (\frac{1}{2}) = K$
122	116 117 121	3eqtrd	$⊢ φ \to 2 K (\frac{1}{2}) = K$
123	114 122	oveq12d	$⊢ φ \to N \cdot 1 + 2 K (\frac{1}{2}) = N + K$
124	113 123	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$
125	49 10	mulcld	$⊢ φ \to N K \in ℂ$
126	50 125	mulcld	$⊢ φ \to 2 N K \in ℂ$
127	49 10	addcld	$⊢ φ \to N + K \in ℂ$
128	126 102 127	addassd	$⊢ φ \to 2 N K + (\frac{1}{2}) + N + K = 2 N K + (\frac{1}{2}) + (N + K)$
129	110 124 128	3eqtrd	$⊢ φ \to (N + (\frac{1}{2})) (2 K + 1) = 2 N K + (\frac{1}{2}) + (N + K)$
130	102 127	addcld	$⊢ φ \to (\frac{1}{2}) + N + K \in ℂ$
131	126 130	addcomd	$⊢ φ \to 2 N K + (\frac{1}{2}) + (N + K) = (\frac{1}{2}) + (N + K) + 2 N K$
132	50 125	mulcomd	$⊢ φ \to 2 N K = N K \cdot 2$
133	132	oveq2d	$⊢ φ \to (\frac{1}{2}) + (N + K) + 2 N K = (\frac{1}{2}) + (N + K) + N K \cdot 2$
134	129 131 133	3eqtrd	$⊢ φ \to (N + (\frac{1}{2})) (2 K + 1) = (\frac{1}{2}) + (N + K) + N K \cdot 2$
135	134	oveq1d	$⊢ φ \to (N + (\frac{1}{2})) (2 K + 1) π = ((\frac{1}{2}) + (N + K) + N K \cdot 2) π$
136	125 50	mulcld	$⊢ φ \to N K \cdot 2 \in ℂ$
137	130 136 107	adddird	$⊢ φ \to ((\frac{1}{2}) + (N + K) + N K \cdot 2) π = ((\frac{1}{2}) + N + K) π + N K \cdot 2 π$
138	125 50 107	mulassd	$⊢ φ \to N K \cdot 2 π = N K 2 π$
139	138	oveq2d	$⊢ φ \to ((\frac{1}{2}) + N + K) π + N K \cdot 2 π = ((\frac{1}{2}) + N + K) π + N K 2 π$
140	135 137 139	3eqtrd	$⊢ φ \to (N + (\frac{1}{2})) (2 K + 1) π = ((\frac{1}{2}) + N + K) π + N K 2 π$
141	101 108 140	3eqtr2d	$⊢ φ \to (N + (\frac{1}{2})) A = ((\frac{1}{2}) + N + K) π + N K 2 π$
142	141	fveq2d	$⊢ φ \to \sin (N + (\frac{1}{2})) A = \sin (((\frac{1}{2}) + N + K) π + N K 2 π)$
143	130 107	mulcld	$⊢ φ \to ((\frac{1}{2}) + N + K) π \in ℂ$
144	1	nnzd	$⊢ φ \to N \in ℤ$
145	144 2	zmulcld	$⊢ φ \to N K \in ℤ$
146		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) π$
147	143 145 146	syl2anc	$⊢ φ \to \sin (((\frac{1}{2}) + N + K) π + N K 2 π) = \sin ((\frac{1}{2}) + N + K) π$
148	102 127	addcomd	$⊢ φ \to (\frac{1}{2}) + N + K = N + K + (\frac{1}{2})$
149	49 10 102	addassd	$⊢ φ \to N + K + (\frac{1}{2}) = N + K + (\frac{1}{2})$
150	10 102	addcld	$⊢ φ \to K + (\frac{1}{2}) \in ℂ$
151	49 150	addcomd	$⊢ φ \to N + K + (\frac{1}{2}) = K + (\frac{1}{2}) + N$
152	148 149 151	3eqtrd	$⊢ φ \to (\frac{1}{2}) + N + K = K + (\frac{1}{2}) + N$
153	152	oveq1d	$⊢ φ \to ((\frac{1}{2}) + N + K) π = (K + (\frac{1}{2}) + N) π$
154	153	fveq2d	$⊢ φ \to \sin ((\frac{1}{2}) + N + K) π = \sin (K + (\frac{1}{2}) + N) π$
155	142 147 154	3eqtrd	$⊢ φ \to \sin (N + (\frac{1}{2})) A = \sin (K + (\frac{1}{2}) + N) π$
156	3	a1i	$⊢ φ \to A = (2 K + 1) π$
157	156	oveq1d	$⊢ φ \to \frac{A}{2} = \frac{(2 K + 1) π}{2}$
158	106 107 50 52	div23d	$⊢ φ \to \frac{(2 K + 1) π}{2} = (\frac{2 K + 1}{2}) π$
159	104 109 50 52	divdird	$⊢ φ \to \frac{2 K + 1}{2} = (\frac{2 K}{2}) + (\frac{1}{2})$
160	10 50 52	divcan3d	$⊢ φ \to \frac{2 K}{2} = K$
161	160	oveq1d	$⊢ φ \to (\frac{2 K}{2}) + (\frac{1}{2}) = K + (\frac{1}{2})$
162	159 161	eqtrd	$⊢ φ \to \frac{2 K + 1}{2} = K + (\frac{1}{2})$
163	162	oveq1d	$⊢ φ \to (\frac{2 K + 1}{2}) π = (K + (\frac{1}{2})) π$
164	157 158 163	3eqtrd	$⊢ φ \to \frac{A}{2} = (K + (\frac{1}{2})) π$
165	164	fveq2d	$⊢ φ \to \sin (\frac{A}{2}) = \sin (K + (\frac{1}{2})) π$
166	165	oveq2d	$⊢ φ \to 2 π \sin (\frac{A}{2}) = 2 π \sin (K + (\frac{1}{2})) π$
167	155 166	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})) π}$
168	167	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})) π}$
169	150 49 107	adddird	$⊢ φ \to (K + (\frac{1}{2}) + N) π = (K + (\frac{1}{2})) π + N π$
170	169	fveq2d	$⊢ φ \to \sin (K + (\frac{1}{2}) + N) π = \sin ((K + (\frac{1}{2})) π + N π)$
171	170	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})) π}$
172	171	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})) π}$
173	49	halfcld	$⊢ φ \to \frac{N}{2} \in ℂ$
174	50 173	mulcomd	$⊢ φ \to 2 (\frac{N}{2}) = (\frac{N}{2}) \cdot 2$
175	53 174	eqtr3d	$⊢ φ \to N = (\frac{N}{2}) \cdot 2$
176	175	oveq1d	$⊢ φ \to N π = (\frac{N}{2}) \cdot 2 π$
177	173 50 107	mulassd	$⊢ φ \to (\frac{N}{2}) \cdot 2 π = (\frac{N}{2}) 2 π$
178	176 177	eqtrd	$⊢ φ \to N π = (\frac{N}{2}) 2 π$
179	178	oveq2d	$⊢ φ \to (K + (\frac{1}{2})) π + N π = (K + (\frac{1}{2})) π + (\frac{N}{2}) 2 π$
180	179	fveq2d	$⊢ φ \to \sin ((K + (\frac{1}{2})) π + N π) = \sin ((K + (\frac{1}{2})) π + (\frac{N}{2}) 2 π)$
181	180	adantr	$⊢ (φ \land N \mod 2 = 0) \to \sin ((K + (\frac{1}{2})) π + N π) = \sin ((K + (\frac{1}{2})) π + (\frac{N}{2}) 2 π)$
182	10	adantr	$⊢ (φ \land N \mod 2 = 0) \to K \in ℂ$
183		1cnd	$⊢ (φ \land N \mod 2 = 0) \to 1 \in ℂ$
184	183	halfcld	$⊢ (φ \land N \mod 2 = 0) \to \frac{1}{2} \in ℂ$
185	182 184	addcld	$⊢ (φ \land N \mod 2 = 0) \to K + (\frac{1}{2}) \in ℂ$
186	15	a1i	$⊢ (φ \land N \mod 2 = 0) \to π \in ℂ$
187	185 186	mulcld	$⊢ (φ \land N \mod 2 = 0) \to (K + (\frac{1}{2})) π \in ℂ$
188		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})) π$
189	187 72 188	syl2anc	$⊢ (φ \land N \mod 2 = 0) \to \sin ((K + (\frac{1}{2})) π + (\frac{N}{2}) 2 π) = \sin (K + (\frac{1}{2})) π$
190	181 189	eqtrd	$⊢ (φ \land N \mod 2 = 0) \to \sin ((K + (\frac{1}{2})) π + N π) = \sin (K + (\frac{1}{2})) π$
191	50 107	mulcld	$⊢ φ \to 2 π \in ℂ$
192	150 107	mulcld	$⊢ φ \to (K + (\frac{1}{2})) π \in ℂ$
193	192	sincld	$⊢ φ \to \sin (K + (\frac{1}{2})) π \in ℂ$
194	191 193	mulcomd	$⊢ φ \to 2 π \sin (K + (\frac{1}{2})) π = \sin (K + (\frac{1}{2})) π 2 π$
195	194	adantr	$⊢ (φ \land N \mod 2 = 0) \to 2 π \sin (K + (\frac{1}{2})) π = \sin (K + (\frac{1}{2})) π 2 π$
196	190 195	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 π}$
197	94	a1i	$⊢ φ \to π \neq 0$
198	150 107 197	divcan4d	$⊢ φ \to \frac{(K + (\frac{1}{2})) π}{π} = K + (\frac{1}{2})$
199	2	zred	$⊢ φ \to K \in ℝ$
200	69	a1i	$⊢ φ \to 2 \in ℝ^{+}$
201	200	rpreccld	$⊢ φ \to \frac{1}{2} \in ℝ^{+}$
202	199 201	ltaddrpd	$⊢ φ \to K < K + (\frac{1}{2})$
203		1red	$⊢ φ \to 1 \in ℝ$
204	203	rehalfcld	$⊢ φ \to \frac{1}{2} \in ℝ$
205		halflt1	$⊢ \frac{1}{2} < 1$
206	205	a1i	$⊢ φ \to \frac{1}{2} < 1$
207	204 203 199 206	ltadd2dd	$⊢ φ \to K + (\frac{1}{2}) < K + 1$
208		btwnnz	$⊢ (K \in ℤ \land K < K + (\frac{1}{2}) \land K + (\frac{1}{2}) < K + 1) \to \neg K + (\frac{1}{2}) \in ℤ$
209	2 202 207 208	syl3anc	$⊢ φ \to \neg K + (\frac{1}{2}) \in ℤ$
210	198 209	eqneltrd	$⊢ φ \to \neg \frac{(K + (\frac{1}{2})) π}{π} \in ℤ$
211		sineq0	$⊢ (K + (\frac{1}{2})) π \in ℂ \to (\sin (K + (\frac{1}{2})) π = 0 \leftrightarrow \frac{(K + (\frac{1}{2})) π}{π} \in ℤ)$
212	192 211	syl	$⊢ φ \to (\sin (K + (\frac{1}{2})) π = 0 \leftrightarrow \frac{(K + (\frac{1}{2})) π}{π} \in ℤ)$
213	210 212	mtbird	$⊢ φ \to \neg \sin (K + (\frac{1}{2})) π = 0$
214	213	neqned	$⊢ φ \to \sin (K + (\frac{1}{2})) π \neq 0$
215	50 107 52 197	mulne0d	$⊢ φ \to 2 π \neq 0$
216	193 193 191 214 215	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 π}$
217	193 214	dividd	$⊢ φ \to \frac{\sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π} = 1$
218	217	oveq1d	$⊢ φ \to \frac{\frac{\sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π}}{2 π} = \frac{1}{2 π}$
219	216 218	eqtr3d	$⊢ φ \to \frac{\sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π 2 π} = \frac{1}{2 π}$
220	219	adantr	$⊢ (φ \land N \mod 2 = 0) \to \frac{\sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π 2 π} = \frac{1}{2 π}$
221	196 220	eqtrd	$⊢ (φ \land N \mod 2 = 0) \to \frac{\sin ((K + (\frac{1}{2})) π + N π)}{2 π \sin (K + (\frac{1}{2})) π} = \frac{1}{2 π}$
222	168 172 221	3eqtrrd	$⊢ (φ \land N \mod 2 = 0) \to \frac{1}{2 π} = \frac{\sin (N + (\frac{1}{2})) A}{2 π \sin (\frac{A}{2})}$
223	99 222	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})}$
224	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}{π}$
225	144	adantr	$⊢ (φ \land \neg N \mod 2 = 0) \to N \in ℤ$
226		simpr	$⊢ (φ \land \neg N \mod 2 = 0) \to \neg N \mod 2 = 0$
227	226	neqned	$⊢ (φ \land \neg N \mod 2 = 0) \to N \mod 2 \neq 0$
228		oddfl	$⊢ (N \in ℤ \land N \mod 2 \neq 0) \to N = 2 ⌊\frac{N}{2}⌋ + 1$
229	225 227 228	syl2anc	$⊢ (φ \land \neg N \mod 2 = 0) \to N = 2 ⌊\frac{N}{2}⌋ + 1$
230	229	oveq2d	$⊢ (φ \land \neg N \mod 2 = 0) \to (1 \dots N) = (1 \dots 2 ⌊\frac{N}{2}⌋ + 1)$
231	230	sumeq1d	$⊢ (φ \land \neg N \mod 2 = 0) \to \sum_{n = 1}^{N} \cos π n = \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋ + 1} \cos π n$
232		fvoveq1	$⊢ N = 1 \to ⌊\frac{N}{2}⌋ = ⌊\frac{1}{2}⌋$
233		halffl	$⊢ ⌊\frac{1}{2}⌋ = 0$
234	232 233	eqtrdi	$⊢ N = 1 \to ⌊\frac{N}{2}⌋ = 0$
235	234	oveq2d	$⊢ N = 1 \to 2 ⌊\frac{N}{2}⌋ = 2 \cdot 0$
236		2t0e0	$⊢ 2 \cdot 0 = 0$
237	235 236	eqtrdi	$⊢ N = 1 \to 2 ⌊\frac{N}{2}⌋ = 0$
238	237	oveq1d	$⊢ N = 1 \to 2 ⌊\frac{N}{2}⌋ + 1 = 0 + 1$
239	90	addlidi	$⊢ 0 + 1 = 1$
240	238 239	eqtrdi	$⊢ N = 1 \to 2 ⌊\frac{N}{2}⌋ + 1 = 1$
241	240	oveq2d	$⊢ N = 1 \to (1 \dots 2 ⌊\frac{N}{2}⌋ + 1) = (1 \dots 1)$
242	241	sumeq1d	$⊢ N = 1 \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋ + 1} \cos π n = \sum_{n = 1}^{1} \cos π n$
243		1z	$⊢ 1 \in ℤ$
244		coscl	$⊢ π \in ℂ \to \cos π \in ℂ$
245	15 244	ax-mp	$⊢ \cos π \in ℂ$
246		oveq2	$⊢ n = 1 \to π n = π \cdot 1$
247	15	mulridi	$⊢ π \cdot 1 = π$
248	246 247	eqtrdi	$⊢ n = 1 \to π n = π$
249	248	fveq2d	$⊢ n = 1 \to \cos π n = \cos π$
250	249	fsum1	$⊢ (1 \in ℤ \land \cos π \in ℂ) \to \sum_{n = 1}^{1} \cos π n = \cos π$
251	243 245 250	mp2an	$⊢ \sum_{n = 1}^{1} \cos π n = \cos π$
252	251	a1i	$⊢ N = 1 \to \sum_{n = 1}^{1} \cos π n = \cos π$
253		cospi	$⊢ \cos π = - 1$
254	253	a1i	$⊢ N = 1 \to \cos π = - 1$
255	242 252 254	3eqtrd	$⊢ N = 1 \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋ + 1} \cos π n = - 1$
256	255	adantl	$⊢ (φ \land N = 1) \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋ + 1} \cos π n = - 1$
257		2nn	$⊢ 2 \in ℕ$
258	257	a1i	$⊢ (φ \land \neg N = 1) \to 2 \in ℕ$
259	67	rehalfcld	$⊢ φ \to \frac{N}{2} \in ℝ$
260	259	flcld	$⊢ φ \to ⌊\frac{N}{2}⌋ \in ℤ$
261	260	adantr	$⊢ (φ \land \neg N = 1) \to ⌊\frac{N}{2}⌋ \in ℤ$
262		2div2e1	$⊢ \frac{2}{2} = 1$
263	73	a1i	$⊢ (φ \land \neg N = 1) \to 2 \in ℝ$
264	67	adantr	$⊢ (φ \land \neg N = 1) \to N \in ℝ$
265	69	a1i	$⊢ (φ \land \neg N = 1) \to 2 \in ℝ^{+}$
266		neqne	$⊢ \neg N = 1 \to N \neq 1$
267		nnne1ge2	$⊢ (N \in ℕ \land N \neq 1) \to 2 \leq N$
268	1 266 267	syl2an	$⊢ (φ \land \neg N = 1) \to 2 \leq N$
269	263 264 265 268	lediv1dd	$⊢ (φ \land \neg N = 1) \to \frac{2}{2} \leq \frac{N}{2}$
270	262 269	eqbrtrrid	$⊢ (φ \land \neg N = 1) \to 1 \leq \frac{N}{2}$
271	259	adantr	$⊢ (φ \land \neg N = 1) \to \frac{N}{2} \in ℝ$
272		flge	$⊢ (\frac{N}{2} \in ℝ \land 1 \in ℤ) \to (1 \leq \frac{N}{2} \leftrightarrow 1 \leq ⌊\frac{N}{2}⌋)$
273	271 243 272	sylancl	$⊢ (φ \land \neg N = 1) \to (1 \leq \frac{N}{2} \leftrightarrow 1 \leq ⌊\frac{N}{2}⌋)$
274	270 273	mpbid	$⊢ (φ \land \neg N = 1) \to 1 \leq ⌊\frac{N}{2}⌋$
275		elnnz1	$⊢ ⌊\frac{N}{2}⌋ \in ℕ \leftrightarrow (⌊\frac{N}{2}⌋ \in ℤ \land 1 \leq ⌊\frac{N}{2}⌋)$
276	261 274 275	sylanbrc	$⊢ (φ \land \neg N = 1) \to ⌊\frac{N}{2}⌋ \in ℕ$
277	258 276	nnmulcld	$⊢ (φ \land \neg N = 1) \to 2 ⌊\frac{N}{2}⌋ \in ℕ$
278		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
279	277 278	eleqtrdi	$⊢ (φ \land \neg N = 1) \to 2 ⌊\frac{N}{2}⌋ \in ℤ_{\geq 1}$
280	15	a1i	$⊢ ((φ \land \neg N = 1) \land n \in (1 \dots 2 ⌊\frac{N}{2}⌋ + 1)) \to π \in ℂ$
281		elfzelz	$⊢ n \in (1 \dots 2 ⌊\frac{N}{2}⌋ + 1) \to n \in ℤ$
282	281	zcnd	$⊢ n \in (1 \dots 2 ⌊\frac{N}{2}⌋ + 1) \to n \in ℂ$
283	282	adantl	$⊢ ((φ \land \neg N = 1) \land n \in (1 \dots 2 ⌊\frac{N}{2}⌋ + 1)) \to n \in ℂ$
284	280 283	mulcld	$⊢ ((φ \land \neg N = 1) \land n \in (1 \dots 2 ⌊\frac{N}{2}⌋ + 1)) \to π n \in ℂ$
285	284	coscld	$⊢ ((φ \land \neg N = 1) \land n \in (1 \dots 2 ⌊\frac{N}{2}⌋ + 1)) \to \cos π n \in ℂ$
286		oveq2	$⊢ n = 2 ⌊\frac{N}{2}⌋ + 1 \to π n = π (2 ⌊\frac{N}{2}⌋ + 1)$
287	286	fveq2d	$⊢ n = 2 ⌊\frac{N}{2}⌋ + 1 \to \cos π n = \cos π (2 ⌊\frac{N}{2}⌋ + 1)$
288	279 285 287	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)$
289	15	a1i	$⊢ n \in (1 \dots 2 ⌊\frac{N}{2}⌋) \to π \in ℂ$
290		elfzelz	$⊢ n \in (1 \dots 2 ⌊\frac{N}{2}⌋) \to n \in ℤ$
291	290	zcnd	$⊢ n \in (1 \dots 2 ⌊\frac{N}{2}⌋) \to n \in ℂ$
292	289 291	mulcomd	$⊢ n \in (1 \dots 2 ⌊\frac{N}{2}⌋) \to π n = n π$
293	292	fveq2d	$⊢ n \in (1 \dots 2 ⌊\frac{N}{2}⌋) \to \cos π n = \cos n π$
294	293	sumeq2i	$⊢ \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋} \cos π n = \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋} \cos n π$
295		dirkertrigeqlem1	$⊢ ⌊\frac{N}{2}⌋ \in ℕ \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋} \cos n π = 0$
296	276 295	syl	$⊢ (φ \land \neg N = 1) \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋} \cos n π = 0$
297	294 296	eqtrid	$⊢ (φ \land \neg N = 1) \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋} \cos π n = 0$
298	260	zcnd	$⊢ φ \to ⌊\frac{N}{2}⌋ \in ℂ$
299	50 298	mulcld	$⊢ φ \to 2 ⌊\frac{N}{2}⌋ \in ℂ$
300	107 299 109	adddid	$⊢ φ \to π (2 ⌊\frac{N}{2}⌋ + 1) = π 2 ⌊\frac{N}{2}⌋ + π \cdot 1$
301	107 50 298	mul13d	$⊢ φ \to π 2 ⌊\frac{N}{2}⌋ = ⌊\frac{N}{2}⌋ 2 π$
302	247	a1i	$⊢ φ \to π \cdot 1 = π$
303	301 302	oveq12d	$⊢ φ \to π 2 ⌊\frac{N}{2}⌋ + π \cdot 1 = ⌊\frac{N}{2}⌋ 2 π + π$
304	298 191	mulcld	$⊢ φ \to ⌊\frac{N}{2}⌋ 2 π \in ℂ$
305	304 107	addcomd	$⊢ φ \to ⌊\frac{N}{2}⌋ 2 π + π = π + ⌊\frac{N}{2}⌋ 2 π$
306	300 303 305	3eqtrd	$⊢ φ \to π (2 ⌊\frac{N}{2}⌋ + 1) = π + ⌊\frac{N}{2}⌋ 2 π$
307	306	fveq2d	$⊢ φ \to \cos π (2 ⌊\frac{N}{2}⌋ + 1) = \cos (π + ⌊\frac{N}{2}⌋ 2 π)$
308		cosper	$⊢ (π \in ℂ \land ⌊\frac{N}{2}⌋ \in ℤ) \to \cos (π + ⌊\frac{N}{2}⌋ 2 π) = \cos π$
309	107 260 308	syl2anc	$⊢ φ \to \cos (π + ⌊\frac{N}{2}⌋ 2 π) = \cos π$
310	253	a1i	$⊢ φ \to \cos π = - 1$
311	307 309 310	3eqtrd	$⊢ φ \to \cos π (2 ⌊\frac{N}{2}⌋ + 1) = - 1$
312	311	adantr	$⊢ (φ \land \neg N = 1) \to \cos π (2 ⌊\frac{N}{2}⌋ + 1) = - 1$
313	297 312	oveq12d	$⊢ (φ \land \neg N = 1) \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋} \cos π n + \cos π (2 ⌊\frac{N}{2}⌋ + 1) = 0 + -1$
314		neg1cn	$⊢ - 1 \in ℂ$
315	314	addlidi	$⊢ 0 + -1 = - 1$
316	315	a1i	$⊢ (φ \land \neg N = 1) \to 0 + -1 = - 1$
317	288 313 316	3eqtrd	$⊢ (φ \land \neg N = 1) \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋ + 1} \cos π n = - 1$
318	256 317	pm2.61dan	$⊢ φ \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋ + 1} \cos π n = - 1$
319	318	adantr	$⊢ (φ \land \neg N \mod 2 = 0) \to \sum_{n = 1}^{2 ⌊\frac{N}{2}⌋ + 1} \cos π n = - 1$
320	231 319	eqtrd	$⊢ (φ \land \neg N \mod 2 = 0) \to \sum_{n = 1}^{N} \cos π n = - 1$
321	320	oveq2d	$⊢ (φ \land \neg N \mod 2 = 0) \to (\frac{1}{2}) + \sum_{n = 1}^{N} \cos π n = (\frac{1}{2}) + -1$
322	321	oveq1d	$⊢ (φ \land \neg N \mod 2 = 0) \to \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos π n}{π} = \frac{(\frac{1}{2}) + -1}{π}$
323	167 171	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})) π}$
324	323	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})) π}$
325	229	oveq1d	$⊢ (φ \land \neg N \mod 2 = 0) \to N π = (2 ⌊\frac{N}{2}⌋ + 1) π$
326	299 109 107	adddird	$⊢ φ \to (2 ⌊\frac{N}{2}⌋ + 1) π = 2 ⌊\frac{N}{2}⌋ π + 1 π$
327	107	mullidd	$⊢ φ \to 1 π = π$
328	327	oveq2d	$⊢ φ \to 2 ⌊\frac{N}{2}⌋ π + 1 π = 2 ⌊\frac{N}{2}⌋ π + π$
329	299 107	mulcld	$⊢ φ \to 2 ⌊\frac{N}{2}⌋ π \in ℂ$
330	329 107	addcomd	$⊢ φ \to 2 ⌊\frac{N}{2}⌋ π + π = π + 2 ⌊\frac{N}{2}⌋ π$
331	326 328 330	3eqtrd	$⊢ φ \to (2 ⌊\frac{N}{2}⌋ + 1) π = π + 2 ⌊\frac{N}{2}⌋ π$
332	331	adantr	$⊢ (φ \land \neg N \mod 2 = 0) \to (2 ⌊\frac{N}{2}⌋ + 1) π = π + 2 ⌊\frac{N}{2}⌋ π$
333	50 298	mulcomd	$⊢ φ \to 2 ⌊\frac{N}{2}⌋ = ⌊\frac{N}{2}⌋ \cdot 2$
334	333	oveq1d	$⊢ φ \to 2 ⌊\frac{N}{2}⌋ π = ⌊\frac{N}{2}⌋ \cdot 2 π$
335	298 50 107	mulassd	$⊢ φ \to ⌊\frac{N}{2}⌋ \cdot 2 π = ⌊\frac{N}{2}⌋ 2 π$
336	334 335	eqtrd	$⊢ φ \to 2 ⌊\frac{N}{2}⌋ π = ⌊\frac{N}{2}⌋ 2 π$
337	336	oveq2d	$⊢ φ \to π + 2 ⌊\frac{N}{2}⌋ π = π + ⌊\frac{N}{2}⌋ 2 π$
338	337	adantr	$⊢ (φ \land \neg N \mod 2 = 0) \to π + 2 ⌊\frac{N}{2}⌋ π = π + ⌊\frac{N}{2}⌋ 2 π$
339	325 332 338	3eqtrd	$⊢ (φ \land \neg N \mod 2 = 0) \to N π = π + ⌊\frac{N}{2}⌋ 2 π$
340	339	oveq2d	$⊢ (φ \land \neg N \mod 2 = 0) \to (K + (\frac{1}{2})) π + N π = (K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π$
341	192	adantr	$⊢ (φ \land \neg N \mod 2 = 0) \to (K + (\frac{1}{2})) π \in ℂ$
342	15	a1i	$⊢ (φ \land \neg N \mod 2 = 0) \to π \in ℂ$
343	304	adantr	$⊢ (φ \land \neg N \mod 2 = 0) \to ⌊\frac{N}{2}⌋ 2 π \in ℂ$
344	341 342 343	addassd	$⊢ (φ \land \neg N \mod 2 = 0) \to (K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π = (K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π$
345	340 344	eqtr4d	$⊢ (φ \land \neg N \mod 2 = 0) \to (K + (\frac{1}{2})) π + N π = (K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π$
346	345	fveq2d	$⊢ (φ \land \neg N \mod 2 = 0) \to \sin ((K + (\frac{1}{2})) π + N π) = \sin ((K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π)$
347	346	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})) π}$
348	192 107	addcld	$⊢ φ \to (K + (\frac{1}{2})) π + π \in ℂ$
349		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})) π + π)$
350	348 260 349	syl2anc	$⊢ φ \to \sin ((K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π) = \sin ((K + (\frac{1}{2})) π + π)$
351		sinppi	$⊢ (K + (\frac{1}{2})) π \in ℂ \to \sin ((K + (\frac{1}{2})) π + π) = - \sin (K + (\frac{1}{2})) π$
352	192 351	syl	$⊢ φ \to \sin ((K + (\frac{1}{2})) π + π) = - \sin (K + (\frac{1}{2})) π$
353	350 352	eqtrd	$⊢ φ \to \sin ((K + (\frac{1}{2})) π + π + ⌊\frac{N}{2}⌋ 2 π) = - \sin (K + (\frac{1}{2})) π$
354	353	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})) π}$
355	194	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 π}$
356	193 193 214	divnegd	$⊢ φ \to - \frac{\sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π} = \frac{- \sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π}$
357	217	negeqd	$⊢ φ \to - \frac{\sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π} = - 1$
358	356 357	eqtr3d	$⊢ φ \to \frac{- \sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π} = - 1$
359	358	oveq1d	$⊢ φ \to \frac{\frac{- \sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π}}{2 π} = \frac{- 1}{2 π}$
360	193	negcld	$⊢ φ \to - \sin (K + (\frac{1}{2})) π \in ℂ$
361	360 193 191 214 215	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 π}$
362	86 90	negsubi	$⊢ (\frac{1}{2}) + -1 = (\frac{1}{2}) - 1$
363	90 86	negsubdi2i	$⊢ - (1 - (\frac{1}{2})) = (\frac{1}{2}) - 1$
364		1mhlfehlf	$⊢ 1 - (\frac{1}{2}) = \frac{1}{2}$
365	364	negeqi	$⊢ - (1 - (\frac{1}{2})) = - \frac{1}{2}$
366		2cn	$⊢ 2 \in ℂ$
367		divneg	$⊢ (1 \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to - \frac{1}{2} = \frac{- 1}{2}$
368	90 366 51 367	mp3an	$⊢ - \frac{1}{2} = \frac{- 1}{2}$
369	365 368	eqtri	$⊢ - (1 - (\frac{1}{2})) = \frac{- 1}{2}$
370	362 363 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	314 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	359 361 375	3eqtr3d	$⊢ φ \to \frac{- \sin (K + (\frac{1}{2})) π}{\sin (K + (\frac{1}{2})) π 2 π} = \frac{(\frac{1}{2}) + -1}{π}$
377	354 355 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	324 347 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	224 322 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	223 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