dirkerper

Description: the Dirichlet kernel has period 2 _pi . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	dirkerper.1	$⊢ D = (n \in ℕ ⟼ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})))$
	dirkerper.2	$⊢ T = 2 π$
Assertion	dirkerper	$⊢ (N \in ℕ \land x \in ℝ) \to D (N) (x + T) = D (N) (x)$

Proof

Step	Hyp	Ref	Expression
1		dirkerper.1	$⊢ D = (n \in ℕ ⟼ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})))$
2		dirkerper.2	$⊢ T = 2 π$
3	2	eqcomi	$⊢ 2 π = T$
4	3	oveq2i	$⊢ 1 2 π = 1 T$
5		2pire	$⊢ 2 π \in ℝ$
6	2 5	eqeltri	$⊢ T \in ℝ$
7	6	recni	$⊢ T \in ℂ$
8	7	mullidi	$⊢ 1 T = T$
9	4 8	eqtri	$⊢ 1 2 π = T$
10	9	oveq2i	$⊢ x + 1 2 π = x + T$
11	10	eqcomi	$⊢ x + T = x + 1 2 π$
12	11	oveq1i	$⊢ (x + T) \mod 2 π = (x + 1 2 π) \mod 2 π$
13	12	a1i	$⊢ ((N \in ℕ \land x \in ℝ) \land x \mod 2 π = 0) \to (x + T) \mod 2 π = (x + 1 2 π) \mod 2 π$
14		id	$⊢ x \in ℝ \to x \in ℝ$
15	14	ad2antlr	$⊢ ((N \in ℕ \land x \in ℝ) \land x \mod 2 π = 0) \to x \in ℝ$
16		2rp	$⊢ 2 \in ℝ^{+}$
17		pirp	$⊢ π \in ℝ^{+}$
18		rpmulcl	$⊢ (2 \in ℝ^{+} \land π \in ℝ^{+}) \to 2 π \in ℝ^{+}$
19	16 17 18	mp2an	$⊢ 2 π \in ℝ^{+}$
20	19	a1i	$⊢ ((N \in ℕ \land x \in ℝ) \land x \mod 2 π = 0) \to 2 π \in ℝ^{+}$
21		1z	$⊢ 1 \in ℤ$
22	21	a1i	$⊢ ((N \in ℕ \land x \in ℝ) \land x \mod 2 π = 0) \to 1 \in ℤ$
23		modcyc	$⊢ (x \in ℝ \land 2 π \in ℝ^{+} \land 1 \in ℤ) \to (x + 1 2 π) \mod 2 π = x \mod 2 π$
24	15 20 22 23	syl3anc	$⊢ ((N \in ℕ \land x \in ℝ) \land x \mod 2 π = 0) \to (x + 1 2 π) \mod 2 π = x \mod 2 π$
25		simpr	$⊢ ((N \in ℕ \land x \in ℝ) \land x \mod 2 π = 0) \to x \mod 2 π = 0$
26	13 24 25	3eqtrd	$⊢ ((N \in ℕ \land x \in ℝ) \land x \mod 2 π = 0) \to (x + T) \mod 2 π = 0$
27	26	iftrued	$⊢ ((N \in ℕ \land x \in ℝ) \land x \mod 2 π = 0) \to if ((x + T) \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) (x + T)}{2 π \sin (\frac{x + T}{2})}) = \frac{2 \cdot N + 1}{2 π}$
28		iftrue	$⊢ x \mod 2 π = 0 \to if (x \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})}) = \frac{2 \cdot N + 1}{2 π}$
29	28	adantl	$⊢ ((N \in ℕ \land x \in ℝ) \land x \mod 2 π = 0) \to if (x \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})}) = \frac{2 \cdot N + 1}{2 π}$
30	27 29	eqtr4d	$⊢ ((N \in ℕ \land x \in ℝ) \land x \mod 2 π = 0) \to if ((x + T) \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) (x + T)}{2 π \sin (\frac{x + T}{2})}) = if (x \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})})$
31		iffalse	$⊢ \neg x \mod 2 π = 0 \to if (x \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})}) = \frac{\sin (N + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})}$
32	31	adantl	$⊢ ((N \in ℕ \land x \in ℝ) \land \neg x \mod 2 π = 0) \to if (x \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})}) = \frac{\sin (N + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})}$
33		nncn	$⊢ N \in ℕ \to N \in ℂ$
34		halfcn	$⊢ \frac{1}{2} \in ℂ$
35	34	a1i	$⊢ N \in ℕ \to \frac{1}{2} \in ℂ$
36	33 35	addcld	$⊢ N \in ℕ \to N + (\frac{1}{2}) \in ℂ$
37	36	adantr	$⊢ (N \in ℕ \land x \in ℝ) \to N + (\frac{1}{2}) \in ℂ$
38		recn	$⊢ x \in ℝ \to x \in ℂ$
39	38	adantl	$⊢ (N \in ℕ \land x \in ℝ) \to x \in ℂ$
40	37 39	mulcld	$⊢ (N \in ℕ \land x \in ℝ) \to (N + (\frac{1}{2})) x \in ℂ$
41	40	sincld	$⊢ (N \in ℕ \land x \in ℝ) \to \sin (N + (\frac{1}{2})) x \in ℂ$
42	41	adantr	$⊢ ((N \in ℕ \land x \in ℝ) \land \neg x \mod 2 π = 0) \to \sin (N + (\frac{1}{2})) x \in ℂ$
43		2picn	$⊢ 2 π \in ℂ$
44	43	a1i	$⊢ (N \in ℕ \land x \in ℝ) \to 2 π \in ℂ$
45	39	halfcld	$⊢ (N \in ℕ \land x \in ℝ) \to \frac{x}{2} \in ℂ$
46	45	sincld	$⊢ (N \in ℕ \land x \in ℝ) \to \sin (\frac{x}{2}) \in ℂ$
47	44 46	mulcld	$⊢ (N \in ℕ \land x \in ℝ) \to 2 π \sin (\frac{x}{2}) \in ℂ$
48	47	adantr	$⊢ ((N \in ℕ \land x \in ℝ) \land \neg x \mod 2 π = 0) \to 2 π \sin (\frac{x}{2}) \in ℂ$
49		dirkerdenne0	$⊢ (x \in ℝ \land \neg x \mod 2 π = 0) \to 2 π \sin (\frac{x}{2}) \neq 0$
50	49	adantll	$⊢ ((N \in ℕ \land x \in ℝ) \land \neg x \mod 2 π = 0) \to 2 π \sin (\frac{x}{2}) \neq 0$
51	42 48 50	div2negd	$⊢ ((N \in ℕ \land x \in ℝ) \land \neg x \mod 2 π = 0) \to \frac{- \sin (N + (\frac{1}{2})) x}{- 2 π \sin (\frac{x}{2})} = \frac{\sin (N + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})}$
52	12	a1i	$⊢ x \in ℝ \to (x + T) \mod 2 π = (x + 1 2 π) \mod 2 π$
53	19 21 23	mp3an23	$⊢ x \in ℝ \to (x + 1 2 π) \mod 2 π = x \mod 2 π$
54	52 53	eqtrd	$⊢ x \in ℝ \to (x + T) \mod 2 π = x \mod 2 π$
55	54	adantr	$⊢ (x \in ℝ \land \neg x \mod 2 π = 0) \to (x + T) \mod 2 π = x \mod 2 π$
56		simpr	$⊢ (x \in ℝ \land \neg x \mod 2 π = 0) \to \neg x \mod 2 π = 0$
57	56	neqned	$⊢ (x \in ℝ \land \neg x \mod 2 π = 0) \to x \mod 2 π \neq 0$
58	55 57	eqnetrd	$⊢ (x \in ℝ \land \neg x \mod 2 π = 0) \to (x + T) \mod 2 π \neq 0$
59	58	neneqd	$⊢ (x \in ℝ \land \neg x \mod 2 π = 0) \to \neg (x + T) \mod 2 π = 0$
60		iffalse	$⊢ \neg (x + T) \mod 2 π = 0 \to if ((x + T) \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) (x + T)}{2 π \sin (\frac{x + T}{2})}) = \frac{\sin (N + (\frac{1}{2})) (x + T)}{2 π \sin (\frac{x + T}{2})}$
61	2	oveq2i	$⊢ x + T = x + 2 π$
62	61	oveq2i	$⊢ (N + (\frac{1}{2})) (x + T) = (N + (\frac{1}{2})) (x + 2 π)$
63	62	fveq2i	$⊢ \sin (N + (\frac{1}{2})) (x + T) = \sin (N + (\frac{1}{2})) (x + 2 π)$
64	61	oveq1i	$⊢ \frac{x + T}{2} = \frac{x + 2 π}{2}$
65	64	fveq2i	$⊢ \sin (\frac{x + T}{2}) = \sin (\frac{x + 2 π}{2})$
66	65	oveq2i	$⊢ 2 π \sin (\frac{x + T}{2}) = 2 π \sin (\frac{x + 2 π}{2})$
67	63 66	oveq12i	$⊢ \frac{\sin (N + (\frac{1}{2})) (x + T)}{2 π \sin (\frac{x + T}{2})} = \frac{\sin (N + (\frac{1}{2})) (x + 2 π)}{2 π \sin (\frac{x + 2 π}{2})}$
68	60 67	eqtrdi	$⊢ \neg (x + T) \mod 2 π = 0 \to if ((x + T) \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) (x + T)}{2 π \sin (\frac{x + T}{2})}) = \frac{\sin (N + (\frac{1}{2})) (x + 2 π)}{2 π \sin (\frac{x + 2 π}{2})}$
69	59 68	syl	$⊢ (x \in ℝ \land \neg x \mod 2 π = 0) \to if ((x + T) \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) (x + T)}{2 π \sin (\frac{x + T}{2})}) = \frac{\sin (N + (\frac{1}{2})) (x + 2 π)}{2 π \sin (\frac{x + 2 π}{2})}$
70	69	adantll	$⊢ ((N \in ℕ \land x \in ℝ) \land \neg x \mod 2 π = 0) \to if ((x + T) \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) (x + T)}{2 π \sin (\frac{x + T}{2})}) = \frac{\sin (N + (\frac{1}{2})) (x + 2 π)}{2 π \sin (\frac{x + 2 π}{2})}$
71	43	a1i	$⊢ N \in ℕ \to 2 π \in ℂ$
72	33 35 71	adddird	$⊢ N \in ℕ \to (N + (\frac{1}{2})) 2 π = N 2 π + (\frac{1}{2}) 2 π$
73		ax-1cn	$⊢ 1 \in ℂ$
74		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
75		div32	$⊢ (1 \in ℂ \land (2 \in ℂ \land 2 \neq 0) \land 2 π \in ℂ) \to (\frac{1}{2}) 2 π = 1 (\frac{2 π}{2})$
76	73 74 43 75	mp3an	$⊢ (\frac{1}{2}) 2 π = 1 (\frac{2 π}{2})$
77		2cn	$⊢ 2 \in ℂ$
78		2ne0	$⊢ 2 \neq 0$
79	43 77 78	divcli	$⊢ \frac{2 π}{2} \in ℂ$
80	79	mullidi	$⊢ 1 (\frac{2 π}{2}) = \frac{2 π}{2}$
81		picn	$⊢ π \in ℂ$
82	81 77 78	divcan3i	$⊢ \frac{2 π}{2} = π$
83	80 82	eqtri	$⊢ 1 (\frac{2 π}{2}) = π$
84	76 83	eqtri	$⊢ (\frac{1}{2}) 2 π = π$
85	84	oveq2i	$⊢ N 2 π + (\frac{1}{2}) 2 π = N 2 π + π$
86	72 85	eqtrdi	$⊢ N \in ℕ \to (N + (\frac{1}{2})) 2 π = N 2 π + π$
87	86	oveq2d	$⊢ N \in ℕ \to (N + (\frac{1}{2})) x + (N + (\frac{1}{2})) 2 π = (N + (\frac{1}{2})) x + N 2 π + π$
88	87	adantr	$⊢ (N \in ℕ \land x \in ℝ) \to (N + (\frac{1}{2})) x + (N + (\frac{1}{2})) 2 π = (N + (\frac{1}{2})) x + N 2 π + π$
89	37 39 44	adddid	$⊢ (N \in ℕ \land x \in ℝ) \to (N + (\frac{1}{2})) (x + 2 π) = (N + (\frac{1}{2})) x + (N + (\frac{1}{2})) 2 π$
90	33 71	mulcld	$⊢ N \in ℕ \to N 2 π \in ℂ$
91	90	adantr	$⊢ (N \in ℕ \land x \in ℝ) \to N 2 π \in ℂ$
92	81	a1i	$⊢ (N \in ℕ \land x \in ℝ) \to π \in ℂ$
93	40 91 92	addassd	$⊢ (N \in ℕ \land x \in ℝ) \to (N + (\frac{1}{2})) x + N 2 π + π = (N + (\frac{1}{2})) x + N 2 π + π$
94	88 89 93	3eqtr4d	$⊢ (N \in ℕ \land x \in ℝ) \to (N + (\frac{1}{2})) (x + 2 π) = (N + (\frac{1}{2})) x + N 2 π + π$
95	94	fveq2d	$⊢ (N \in ℕ \land x \in ℝ) \to \sin (N + (\frac{1}{2})) (x + 2 π) = \sin ((N + (\frac{1}{2})) x + N 2 π + π)$
96	40 91	addcld	$⊢ (N \in ℕ \land x \in ℝ) \to (N + (\frac{1}{2})) x + N 2 π \in ℂ$
97		sinppi	$⊢ (N + (\frac{1}{2})) x + N 2 π \in ℂ \to \sin ((N + (\frac{1}{2})) x + N 2 π + π) = - \sin ((N + (\frac{1}{2})) x + N 2 π)$
98	96 97	syl	$⊢ (N \in ℕ \land x \in ℝ) \to \sin ((N + (\frac{1}{2})) x + N 2 π + π) = - \sin ((N + (\frac{1}{2})) x + N 2 π)$
99		simpl	$⊢ (N \in ℕ \land x \in ℝ) \to N \in ℕ$
100	99	nnzd	$⊢ (N \in ℕ \land x \in ℝ) \to N \in ℤ$
101		sinper	$⊢ ((N + (\frac{1}{2})) x \in ℂ \land N \in ℤ) \to \sin ((N + (\frac{1}{2})) x + N 2 π) = \sin (N + (\frac{1}{2})) x$
102	40 100 101	syl2anc	$⊢ (N \in ℕ \land x \in ℝ) \to \sin ((N + (\frac{1}{2})) x + N 2 π) = \sin (N + (\frac{1}{2})) x$
103	102	negeqd	$⊢ (N \in ℕ \land x \in ℝ) \to - \sin ((N + (\frac{1}{2})) x + N 2 π) = - \sin (N + (\frac{1}{2})) x$
104	95 98 103	3eqtrd	$⊢ (N \in ℕ \land x \in ℝ) \to \sin (N + (\frac{1}{2})) (x + 2 π) = - \sin (N + (\frac{1}{2})) x$
105	43	a1i	$⊢ x \in ℝ \to 2 π \in ℂ$
106	77	a1i	$⊢ x \in ℝ \to 2 \in ℂ$
107	78	a1i	$⊢ x \in ℝ \to 2 \neq 0$
108	38 105 106 107	divdird	$⊢ x \in ℝ \to \frac{x + 2 π}{2} = (\frac{x}{2}) + (\frac{2 π}{2})$
109	82	a1i	$⊢ x \in ℝ \to \frac{2 π}{2} = π$
110	109	oveq2d	$⊢ x \in ℝ \to (\frac{x}{2}) + (\frac{2 π}{2}) = (\frac{x}{2}) + π$
111	108 110	eqtrd	$⊢ x \in ℝ \to \frac{x + 2 π}{2} = (\frac{x}{2}) + π$
112	111	fveq2d	$⊢ x \in ℝ \to \sin (\frac{x + 2 π}{2}) = \sin ((\frac{x}{2}) + π)$
113	38	halfcld	$⊢ x \in ℝ \to \frac{x}{2} \in ℂ$
114		sinppi	$⊢ \frac{x}{2} \in ℂ \to \sin ((\frac{x}{2}) + π) = - \sin (\frac{x}{2})$
115	113 114	syl	$⊢ x \in ℝ \to \sin ((\frac{x}{2}) + π) = - \sin (\frac{x}{2})$
116	112 115	eqtrd	$⊢ x \in ℝ \to \sin (\frac{x + 2 π}{2}) = - \sin (\frac{x}{2})$
117	116	oveq2d	$⊢ x \in ℝ \to 2 π \sin (\frac{x + 2 π}{2}) = 2 π (- \sin (\frac{x}{2}))$
118	117	adantl	$⊢ (N \in ℕ \land x \in ℝ) \to 2 π \sin (\frac{x + 2 π}{2}) = 2 π (- \sin (\frac{x}{2}))$
119	104 118	oveq12d	$⊢ (N \in ℕ \land x \in ℝ) \to \frac{\sin (N + (\frac{1}{2})) (x + 2 π)}{2 π \sin (\frac{x + 2 π}{2})} = \frac{- \sin (N + (\frac{1}{2})) x}{2 π (- \sin (\frac{x}{2}))}$
120	119	adantr	$⊢ ((N \in ℕ \land x \in ℝ) \land \neg x \mod 2 π = 0) \to \frac{\sin (N + (\frac{1}{2})) (x + 2 π)}{2 π \sin (\frac{x + 2 π}{2})} = \frac{- \sin (N + (\frac{1}{2})) x}{2 π (- \sin (\frac{x}{2}))}$
121	113	sincld	$⊢ x \in ℝ \to \sin (\frac{x}{2}) \in ℂ$
122	105 121	mulneg2d	$⊢ x \in ℝ \to 2 π (- \sin (\frac{x}{2})) = - 2 π \sin (\frac{x}{2})$
123	122	oveq2d	$⊢ x \in ℝ \to \frac{- \sin (N + (\frac{1}{2})) x}{2 π (- \sin (\frac{x}{2}))} = \frac{- \sin (N + (\frac{1}{2})) x}{- 2 π \sin (\frac{x}{2})}$
124	123	ad2antlr	$⊢ ((N \in ℕ \land x \in ℝ) \land \neg x \mod 2 π = 0) \to \frac{- \sin (N + (\frac{1}{2})) x}{2 π (- \sin (\frac{x}{2}))} = \frac{- \sin (N + (\frac{1}{2})) x}{- 2 π \sin (\frac{x}{2})}$
125	70 120 124	3eqtrrd	$⊢ ((N \in ℕ \land x \in ℝ) \land \neg x \mod 2 π = 0) \to \frac{- \sin (N + (\frac{1}{2})) x}{- 2 π \sin (\frac{x}{2})} = if ((x + T) \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) (x + T)}{2 π \sin (\frac{x + T}{2})})$
126	32 51 125	3eqtr2rd	$⊢ ((N \in ℕ \land x \in ℝ) \land \neg x \mod 2 π = 0) \to if ((x + T) \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) (x + T)}{2 π \sin (\frac{x + T}{2})}) = if (x \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})})$
127	30 126	pm2.61dan	$⊢ (N \in ℕ \land x \in ℝ) \to if ((x + T) \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) (x + T)}{2 π \sin (\frac{x + T}{2})}) = if (x \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})})$
128	6	a1i	$⊢ x \in ℝ \to T \in ℝ$
129	14 128	readdcld	$⊢ x \in ℝ \to x + T \in ℝ$
130	1	dirkerval2	$⊢ (N \in ℕ \land x + T \in ℝ) \to D (N) (x + T) = if ((x + T) \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) (x + T)}{2 π \sin (\frac{x + T}{2})})$
131	129 130	sylan2	$⊢ (N \in ℕ \land x \in ℝ) \to D (N) (x + T) = if ((x + T) \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) (x + T)}{2 π \sin (\frac{x + T}{2})})$
132	1	dirkerval2	$⊢ (N \in ℕ \land x \in ℝ) \to D (N) (x) = if (x \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})})$
133	127 131 132	3eqtr4d	$⊢ (N \in ℕ \land x \in ℝ) \to D (N) (x + T) = D (N) (x)$

Metamath Proof Explorer

Theorem dirkerper

Proof