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

Metamath Proof Explorer

Theorem dirkerper

Proof