dirkertrigeq

Description: Trigonometric equality for the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	dirkertrigeq.d	$⊢ D = (n \in ℕ ⟼ (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})))$
	dirkertrigeq.n	$⊢ φ \to N \in ℕ$
	dirkertrigeq.f	$⊢ F = D (N)$
	dirkertrigeq.h	$⊢ H = (s \in ℝ ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π})$
Assertion	dirkertrigeq	$⊢ φ \to F = H$

Proof

Step	Hyp	Ref	Expression
1		dirkertrigeq.d	$⊢ D = (n \in ℕ ⟼ (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})))$
2		dirkertrigeq.n	$⊢ φ \to N \in ℕ$
3		dirkertrigeq.f	$⊢ F = D (N)$
4		dirkertrigeq.h	$⊢ H = (s \in ℝ ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π})$
5	3	a1i	$⊢ φ \to F = D (N)$
6	1	dirkerval	$⊢ N \in ℕ \to D (N) = (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}))$
7	2 6	syl	$⊢ φ \to D (N) = (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}))$
8		2cnd	$⊢ φ \to 2 \in ℂ$
9	2	nncnd	$⊢ φ \to N \in ℂ$
10	8 9	mulcld	$⊢ φ \to 2 \cdot N \in ℂ$
11		peano2cn	$⊢ 2 \cdot N \in ℂ \to 2 \cdot N + 1 \in ℂ$
12	10 11	syl	$⊢ φ \to 2 \cdot N + 1 \in ℂ$
13		picn	$⊢ π \in ℂ$
14	13	a1i	$⊢ φ \to π \in ℂ$
15		2ne0	$⊢ 2 \neq 0$
16	15	a1i	$⊢ φ \to 2 \neq 0$
17		pire	$⊢ π \in ℝ$
18		pipos	$⊢ 0 < π$
19	17 18	gt0ne0ii	$⊢ π \neq 0$
20	19	a1i	$⊢ φ \to π \neq 0$
21	12 8 14 16 20	divdiv1d	$⊢ φ \to \frac{\frac{2 \cdot N + 1}{2}}{π} = \frac{2 \cdot N + 1}{2 π}$
22	21	eqcomd	$⊢ φ \to \frac{2 \cdot N + 1}{2 π} = \frac{\frac{2 \cdot N + 1}{2}}{π}$
23	22	ad2antrr	$⊢ ((φ \land s \in ℝ) \land s \mod 2 π = 0) \to \frac{2 \cdot N + 1}{2 π} = \frac{\frac{2 \cdot N + 1}{2}}{π}$
24		iftrue	$⊢ s \mod 2 π = 0 \to if (s \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}) = \frac{2 \cdot N + 1}{2 π}$
25	24	adantl	$⊢ ((φ \land s \in ℝ) \land s \mod 2 π = 0) \to if (s \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}) = \frac{2 \cdot N + 1}{2 π}$
26		elfzelz	$⊢ k \in (1 \dots N) \to k \in ℤ$
27	26	zcnd	$⊢ k \in (1 \dots N) \to k \in ℂ$
28	27	adantl	$⊢ ((s \in ℝ \land s \mod 2 π = 0) \land k \in (1 \dots N)) \to k \in ℂ$
29		recn	$⊢ s \in ℝ \to s \in ℂ$
30	29	ad2antrr	$⊢ ((s \in ℝ \land s \mod 2 π = 0) \land k \in (1 \dots N)) \to s \in ℂ$
31		2cn	$⊢ 2 \in ℂ$
32	31 13	mulcli	$⊢ 2 π \in ℂ$
33	32	a1i	$⊢ ((s \in ℝ \land s \mod 2 π = 0) \land k \in (1 \dots N)) \to 2 π \in ℂ$
34	31 13 15 19	mulne0i	$⊢ 2 π \neq 0$
35	34	a1i	$⊢ ((s \in ℝ \land s \mod 2 π = 0) \land k \in (1 \dots N)) \to 2 π \neq 0$
36	28 30 33 35	divassd	$⊢ ((s \in ℝ \land s \mod 2 π = 0) \land k \in (1 \dots N)) \to \frac{k s}{2 π} = k (\frac{s}{2 π})$
37	26	adantl	$⊢ ((s \in ℝ \land s \mod 2 π = 0) \land k \in (1 \dots N)) \to k \in ℤ$
38		simpr	$⊢ (s \in ℝ \land s \mod 2 π = 0) \to s \mod 2 π = 0$
39		simpl	$⊢ (s \in ℝ \land s \mod 2 π = 0) \to s \in ℝ$
40		2rp	$⊢ 2 \in ℝ^{+}$
41		pirp	$⊢ π \in ℝ^{+}$
42		rpmulcl	$⊢ (2 \in ℝ^{+} \land π \in ℝ^{+}) \to 2 π \in ℝ^{+}$
43	40 41 42	mp2an	$⊢ 2 π \in ℝ^{+}$
44		mod0	$⊢ (s \in ℝ \land 2 π \in ℝ^{+}) \to (s \mod 2 π = 0 \leftrightarrow \frac{s}{2 π} \in ℤ)$
45	39 43 44	sylancl	$⊢ (s \in ℝ \land s \mod 2 π = 0) \to (s \mod 2 π = 0 \leftrightarrow \frac{s}{2 π} \in ℤ)$
46	38 45	mpbid	$⊢ (s \in ℝ \land s \mod 2 π = 0) \to \frac{s}{2 π} \in ℤ$
47	46	adantr	$⊢ ((s \in ℝ \land s \mod 2 π = 0) \land k \in (1 \dots N)) \to \frac{s}{2 π} \in ℤ$
48	37 47	zmulcld	$⊢ ((s \in ℝ \land s \mod 2 π = 0) \land k \in (1 \dots N)) \to k (\frac{s}{2 π}) \in ℤ$
49	36 48	eqeltrd	$⊢ ((s \in ℝ \land s \mod 2 π = 0) \land k \in (1 \dots N)) \to \frac{k s}{2 π} \in ℤ$
50	27	adantl	$⊢ (s \in ℝ \land k \in (1 \dots N)) \to k \in ℂ$
51	29	adantr	$⊢ (s \in ℝ \land k \in (1 \dots N)) \to s \in ℂ$
52	50 51	mulcld	$⊢ (s \in ℝ \land k \in (1 \dots N)) \to k s \in ℂ$
53		coseq1	$⊢ k s \in ℂ \to (\cos k s = 1 \leftrightarrow \frac{k s}{2 π} \in ℤ)$
54	52 53	syl	$⊢ (s \in ℝ \land k \in (1 \dots N)) \to (\cos k s = 1 \leftrightarrow \frac{k s}{2 π} \in ℤ)$
55	54	adantlr	$⊢ ((s \in ℝ \land s \mod 2 π = 0) \land k \in (1 \dots N)) \to (\cos k s = 1 \leftrightarrow \frac{k s}{2 π} \in ℤ)$
56	49 55	mpbird	$⊢ ((s \in ℝ \land s \mod 2 π = 0) \land k \in (1 \dots N)) \to \cos k s = 1$
57	56	ralrimiva	$⊢ (s \in ℝ \land s \mod 2 π = 0) \to \forall k \in (1 \dots N) \cos k s = 1$
58	57	adantll	$⊢ ((φ \land s \in ℝ) \land s \mod 2 π = 0) \to \forall k \in (1 \dots N) \cos k s = 1$
59	58	sumeq2d	$⊢ ((φ \land s \in ℝ) \land s \mod 2 π = 0) \to \sum_{k = 1}^{N} \cos k s = \sum_{k = 1}^{N} 1$
60		fzfid	$⊢ ((φ \land s \in ℝ) \land s \mod 2 π = 0) \to (1 \dots N) \in Fin$
61		1cnd	$⊢ ((φ \land s \in ℝ) \land s \mod 2 π = 0) \to 1 \in ℂ$
62		fsumconst	$⊢ ((1 \dots N) \in Fin \land 1 \in ℂ) \to \sum_{k = 1}^{N} 1 = \|(1 \dots N)\| \cdot 1$
63	60 61 62	syl2anc	$⊢ ((φ \land s \in ℝ) \land s \mod 2 π = 0) \to \sum_{k = 1}^{N} 1 = \|(1 \dots N)\| \cdot 1$
64	2	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
65		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
66	64 65	syl	$⊢ φ \to \|(1 \dots N)\| = N$
67	66	oveq1d	$⊢ φ \to \|(1 \dots N)\| \cdot 1 = N \cdot 1$
68	9	mulid1d	$⊢ φ \to N \cdot 1 = N$
69	67 68	eqtrd	$⊢ φ \to \|(1 \dots N)\| \cdot 1 = N$
70	69	ad2antrr	$⊢ ((φ \land s \in ℝ) \land s \mod 2 π = 0) \to \|(1 \dots N)\| \cdot 1 = N$
71	59 63 70	3eqtrd	$⊢ ((φ \land s \in ℝ) \land s \mod 2 π = 0) \to \sum_{k = 1}^{N} \cos k s = N$
72	71	oveq2d	$⊢ ((φ \land s \in ℝ) \land s \mod 2 π = 0) \to (\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s = (\frac{1}{2}) + N$
73	9	div1d	$⊢ φ \to \frac{N}{1} = N$
74	73	eqcomd	$⊢ φ \to N = \frac{N}{1}$
75	74	oveq2d	$⊢ φ \to (\frac{1}{2}) + N = (\frac{1}{2}) + (\frac{N}{1})$
76		1cnd	$⊢ φ \to 1 \in ℂ$
77		ax-1ne0	$⊢ 1 \neq 0$
78	77	a1i	$⊢ φ \to 1 \neq 0$
79	76 8 9 76 16 78	divadddivd	$⊢ φ \to (\frac{1}{2}) + (\frac{N}{1}) = \frac{1 \cdot 1 + N \cdot 2}{2 \cdot 1}$
80	76 76	mulcld	$⊢ φ \to 1 \cdot 1 \in ℂ$
81	9 8	mulcld	$⊢ φ \to N \cdot 2 \in ℂ$
82	80 81	addcomd	$⊢ φ \to 1 \cdot 1 + N \cdot 2 = N \cdot 2 + 1 \cdot 1$
83	9 8	mulcomd	$⊢ φ \to N \cdot 2 = 2 \cdot N$
84	76	mulid1d	$⊢ φ \to 1 \cdot 1 = 1$
85	83 84	oveq12d	$⊢ φ \to N \cdot 2 + 1 \cdot 1 = 2 \cdot N + 1$
86	82 85	eqtrd	$⊢ φ \to 1 \cdot 1 + N \cdot 2 = 2 \cdot N + 1$
87	8	mulid1d	$⊢ φ \to 2 \cdot 1 = 2$
88	86 87	oveq12d	$⊢ φ \to \frac{1 \cdot 1 + N \cdot 2}{2 \cdot 1} = \frac{2 \cdot N + 1}{2}$
89	75 79 88	3eqtrd	$⊢ φ \to (\frac{1}{2}) + N = \frac{2 \cdot N + 1}{2}$
90	89	ad2antrr	$⊢ ((φ \land s \in ℝ) \land s \mod 2 π = 0) \to (\frac{1}{2}) + N = \frac{2 \cdot N + 1}{2}$
91	72 90	eqtrd	$⊢ ((φ \land s \in ℝ) \land s \mod 2 π = 0) \to (\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s = \frac{2 \cdot N + 1}{2}$
92	91	oveq1d	$⊢ ((φ \land s \in ℝ) \land s \mod 2 π = 0) \to \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π} = \frac{\frac{2 \cdot N + 1}{2}}{π}$
93	23 25 92	3eqtr4rd	$⊢ ((φ \land s \in ℝ) \land s \mod 2 π = 0) \to \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π} = if (s \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})$
94		iffalse	$⊢ \neg s \mod 2 π = 0 \to if (s \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}) = \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}$
95	94	adantl	$⊢ ((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \to if (s \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}) = \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}$
96	13	a1i	$⊢ s \in ℝ \to π \in ℂ$
97	19	a1i	$⊢ s \in ℝ \to π \neq 0$
98	29 96 97	divcan1d	$⊢ s \in ℝ \to (\frac{s}{π}) π = s$
99	98	eqcomd	$⊢ s \in ℝ \to s = (\frac{s}{π}) π$
100	99	ad2antrr	$⊢ ((s \in ℝ \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to s = (\frac{s}{π}) π$
101		simpr	$⊢ (s \in ℝ \land s \mod π = 0) \to s \mod π = 0$
102		simpl	$⊢ (s \in ℝ \land s \mod π = 0) \to s \in ℝ$
103		mod0	$⊢ (s \in ℝ \land π \in ℝ^{+}) \to (s \mod π = 0 \leftrightarrow \frac{s}{π} \in ℤ)$
104	102 41 103	sylancl	$⊢ (s \in ℝ \land s \mod π = 0) \to (s \mod π = 0 \leftrightarrow \frac{s}{π} \in ℤ)$
105	101 104	mpbid	$⊢ (s \in ℝ \land s \mod π = 0) \to \frac{s}{π} \in ℤ$
106	105	adantlr	$⊢ ((s \in ℝ \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to \frac{s}{π} \in ℤ$
107		rpreccl	$⊢ π \in ℝ^{+} \to \frac{1}{π} \in ℝ^{+}$
108	41 107	ax-mp	$⊢ \frac{1}{π} \in ℝ^{+}$
109		moddi	$⊢ (\frac{1}{π} \in ℝ^{+} \land s \in ℝ \land 2 π \in ℝ^{+}) \to (\frac{1}{π}) (s \mod 2 π) = (\frac{1}{π}) s \mod (\frac{1}{π}) 2 π$
110	108 43 109	mp3an13	$⊢ s \in ℝ \to (\frac{1}{π}) (s \mod 2 π) = (\frac{1}{π}) s \mod (\frac{1}{π}) 2 π$
111	29 96 97	divrec2d	$⊢ s \in ℝ \to \frac{s}{π} = (\frac{1}{π}) s$
112	111	eqcomd	$⊢ s \in ℝ \to (\frac{1}{π}) s = \frac{s}{π}$
113	96 97	reccld	$⊢ s \in ℝ \to \frac{1}{π} \in ℂ$
114	32	a1i	$⊢ s \in ℝ \to 2 π \in ℂ$
115	113 114	mulcomd	$⊢ s \in ℝ \to (\frac{1}{π}) 2 π = 2 π (\frac{1}{π})$
116		2cnd	$⊢ s \in ℝ \to 2 \in ℂ$
117	116 96 113	mulassd	$⊢ s \in ℝ \to 2 π (\frac{1}{π}) = 2 π (\frac{1}{π})$
118	13 19	recidi	$⊢ π (\frac{1}{π}) = 1$
119	118	oveq2i	$⊢ 2 π (\frac{1}{π}) = 2 \cdot 1$
120	116	mulid1d	$⊢ s \in ℝ \to 2 \cdot 1 = 2$
121	119 120	eqtrid	$⊢ s \in ℝ \to 2 π (\frac{1}{π}) = 2$
122	115 117 121	3eqtrd	$⊢ s \in ℝ \to (\frac{1}{π}) 2 π = 2$
123	112 122	oveq12d	$⊢ s \in ℝ \to (\frac{1}{π}) s \mod (\frac{1}{π}) 2 π = (\frac{s}{π}) \mod 2$
124	110 123	eqtr2d	$⊢ s \in ℝ \to (\frac{s}{π}) \mod 2 = (\frac{1}{π}) (s \mod 2 π)$
125	124	adantr	$⊢ (s \in ℝ \land \neg s \mod 2 π = 0) \to (\frac{s}{π}) \mod 2 = (\frac{1}{π}) (s \mod 2 π)$
126	113	adantr	$⊢ (s \in ℝ \land \neg s \mod 2 π = 0) \to \frac{1}{π} \in ℂ$
127		id	$⊢ s \in ℝ \to s \in ℝ$
128	43	a1i	$⊢ s \in ℝ \to 2 π \in ℝ^{+}$
129	127 128	modcld	$⊢ s \in ℝ \to s \mod 2 π \in ℝ$
130	129	recnd	$⊢ s \in ℝ \to s \mod 2 π \in ℂ$
131	130	adantr	$⊢ (s \in ℝ \land \neg s \mod 2 π = 0) \to s \mod 2 π \in ℂ$
132		ax-1cn	$⊢ 1 \in ℂ$
133	132 13 77 19	divne0i	$⊢ \frac{1}{π} \neq 0$
134	133	a1i	$⊢ (s \in ℝ \land \neg s \mod 2 π = 0) \to \frac{1}{π} \neq 0$
135		neqne	$⊢ \neg s \mod 2 π = 0 \to s \mod 2 π \neq 0$
136	135	adantl	$⊢ (s \in ℝ \land \neg s \mod 2 π = 0) \to s \mod 2 π \neq 0$
137	126 131 134 136	mulne0d	$⊢ (s \in ℝ \land \neg s \mod 2 π = 0) \to (\frac{1}{π}) (s \mod 2 π) \neq 0$
138	125 137	eqnetrd	$⊢ (s \in ℝ \land \neg s \mod 2 π = 0) \to (\frac{s}{π}) \mod 2 \neq 0$
139	138	adantr	$⊢ ((s \in ℝ \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to (\frac{s}{π}) \mod 2 \neq 0$
140		oddfl	$⊢ (\frac{s}{π} \in ℤ \land (\frac{s}{π}) \mod 2 \neq 0) \to \frac{s}{π} = 2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1$
141	106 139 140	syl2anc	$⊢ ((s \in ℝ \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to \frac{s}{π} = 2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1$
142	141	oveq1d	$⊢ ((s \in ℝ \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to (\frac{s}{π}) π = (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π$
143	100 142	eqtrd	$⊢ ((s \in ℝ \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to s = (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π$
144	143	oveq2d	$⊢ ((s \in ℝ \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to k s = k (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π$
145	144	fveq2d	$⊢ ((s \in ℝ \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to \cos k s = \cos k (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π$
146	145	sumeq2sdv	$⊢ ((s \in ℝ \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to \sum_{k = 1}^{N} \cos k s = \sum_{k = 1}^{N} \cos k (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π$
147	146	oveq2d	$⊢ ((s \in ℝ \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to (\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s = (\frac{1}{2}) + \sum_{k = 1}^{N} \cos k (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π$
148	147	oveq1d	$⊢ ((s \in ℝ \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π} = \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π}{π}$
149	148	adantlll	$⊢ (((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π} = \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π}{π}$
150	2	ad2antrr	$⊢ ((φ \land s \in ℝ) \land s \mod π = 0) \to N \in ℕ$
151	17	a1i	$⊢ s \in ℝ \to π \in ℝ$
152	127 151 97	redivcld	$⊢ s \in ℝ \to \frac{s}{π} \in ℝ$
153	152	rehalfcld	$⊢ s \in ℝ \to \frac{\frac{s}{π}}{2} \in ℝ$
154	153	flcld	$⊢ s \in ℝ \to ⌊\frac{\frac{s}{π}}{2}⌋ \in ℤ$
155	154	ad2antlr	$⊢ ((φ \land s \in ℝ) \land s \mod π = 0) \to ⌊\frac{\frac{s}{π}}{2}⌋ \in ℤ$
156		eqid	$⊢ (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π = (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π$
157	150 155 156	dirkertrigeqlem3	$⊢ ((φ \land s \in ℝ) \land s \mod π = 0) \to \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π}{π} = \frac{\sin (N + (\frac{1}{2})) (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π}{2 π \sin (\frac{(2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π}{2})}$
158	157	adantlr	$⊢ (((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π}{π} = \frac{\sin (N + (\frac{1}{2})) (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π}{2 π \sin (\frac{(2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π}{2})}$
159	141	adantlll	$⊢ (((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to \frac{s}{π} = 2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1$
160	159	eqcomd	$⊢ (((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to 2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1 = \frac{s}{π}$
161	160	oveq1d	$⊢ (((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π = (\frac{s}{π}) π$
162	161	oveq2d	$⊢ (((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to (N + (\frac{1}{2})) (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π = (N + (\frac{1}{2})) (\frac{s}{π}) π$
163	162	fveq2d	$⊢ (((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to \sin (N + (\frac{1}{2})) (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π = \sin (N + (\frac{1}{2})) (\frac{s}{π}) π$
164	161	fvoveq1d	$⊢ (((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to \sin (\frac{(2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π}{2}) = \sin (\frac{(\frac{s}{π}) π}{2})$
165	164	oveq2d	$⊢ (((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to 2 π \sin (\frac{(2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π}{2}) = 2 π \sin (\frac{(\frac{s}{π}) π}{2})$
166	163 165	oveq12d	$⊢ (((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to \frac{\sin (N + (\frac{1}{2})) (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π}{2 π \sin (\frac{(2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π}{2})} = \frac{\sin (N + (\frac{1}{2})) (\frac{s}{π}) π}{2 π \sin (\frac{(\frac{s}{π}) π}{2})}$
167	98	oveq2d	$⊢ s \in ℝ \to (N + (\frac{1}{2})) (\frac{s}{π}) π = (N + (\frac{1}{2})) s$
168	167	fveq2d	$⊢ s \in ℝ \to \sin (N + (\frac{1}{2})) (\frac{s}{π}) π = \sin (N + (\frac{1}{2})) s$
169	98	fvoveq1d	$⊢ s \in ℝ \to \sin (\frac{(\frac{s}{π}) π}{2}) = \sin (\frac{s}{2})$
170	169	oveq2d	$⊢ s \in ℝ \to 2 π \sin (\frac{(\frac{s}{π}) π}{2}) = 2 π \sin (\frac{s}{2})$
171	168 170	oveq12d	$⊢ s \in ℝ \to \frac{\sin (N + (\frac{1}{2})) (\frac{s}{π}) π}{2 π \sin (\frac{(\frac{s}{π}) π}{2})} = \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}$
172	171	adantl	$⊢ (φ \land s \in ℝ) \to \frac{\sin (N + (\frac{1}{2})) (\frac{s}{π}) π}{2 π \sin (\frac{(\frac{s}{π}) π}{2})} = \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}$
173	172	ad2antrr	$⊢ (((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to \frac{\sin (N + (\frac{1}{2})) (\frac{s}{π}) π}{2 π \sin (\frac{(\frac{s}{π}) π}{2})} = \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}$
174	166 173	eqtrd	$⊢ (((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to \frac{\sin (N + (\frac{1}{2})) (2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π}{2 π \sin (\frac{(2 ⌊\frac{\frac{s}{π}}{2}⌋ + 1) π}{2})} = \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}$
175	149 158 174	3eqtrrd	$⊢ (((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \land s \mod π = 0) \to \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})} = \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}$
176		simplr	$⊢ ((φ \land s \in ℝ) \land \neg s \mod π = 0) \to s \in ℝ$
177		simpr	$⊢ ((φ \land s \in ℝ) \land \neg s \mod π = 0) \to \neg s \mod π = 0$
178	176 41 103	sylancl	$⊢ ((φ \land s \in ℝ) \land \neg s \mod π = 0) \to (s \mod π = 0 \leftrightarrow \frac{s}{π} \in ℤ)$
179	177 178	mtbid	$⊢ ((φ \land s \in ℝ) \land \neg s \mod π = 0) \to \neg \frac{s}{π} \in ℤ$
180	176	recnd	$⊢ ((φ \land s \in ℝ) \land \neg s \mod π = 0) \to s \in ℂ$
181		sineq0	$⊢ s \in ℂ \to (\sin s = 0 \leftrightarrow \frac{s}{π} \in ℤ)$
182	180 181	syl	$⊢ ((φ \land s \in ℝ) \land \neg s \mod π = 0) \to (\sin s = 0 \leftrightarrow \frac{s}{π} \in ℤ)$
183	179 182	mtbird	$⊢ ((φ \land s \in ℝ) \land \neg s \mod π = 0) \to \neg \sin s = 0$
184	183	neqned	$⊢ ((φ \land s \in ℝ) \land \neg s \mod π = 0) \to \sin s \neq 0$
185	2	ad2antrr	$⊢ ((φ \land s \in ℝ) \land \neg s \mod π = 0) \to N \in ℕ$
186	176 184 185	dirkertrigeqlem2	$⊢ ((φ \land s \in ℝ) \land \neg s \mod π = 0) \to \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π} = \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}$
187	186	eqcomd	$⊢ ((φ \land s \in ℝ) \land \neg s \mod π = 0) \to \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})} = \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}$
188	187	adantlr	$⊢ (((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \land \neg s \mod π = 0) \to \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})} = \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}$
189	175 188	pm2.61dan	$⊢ ((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \to \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})} = \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}$
190	95 189	eqtr2d	$⊢ ((φ \land s \in ℝ) \land \neg s \mod 2 π = 0) \to \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π} = if (s \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})$
191	93 190	pm2.61dan	$⊢ (φ \land s \in ℝ) \to \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π} = if (s \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})$
192	191	mpteq2dva	$⊢ φ \to (s \in ℝ ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}) = (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}))$
193	4 192	eqtr2id	$⊢ φ \to (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})) = H$
194	5 7 193	3eqtrd	$⊢ φ \to F = H$

Metamath Proof Explorer

Theorem dirkertrigeq

Proof