dirkercncf

Description: For any natural number N , the Dirichlet Kernel ( DN ) is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Hypothesis	dirkercncf.d	$⊢ 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})})))$
	Assertion	dirkercncf	$⊢ N \in ℕ \to D (N) : ℝ \underset{cn}{⟶} ℝ$

Proof

Step	Hyp	Ref	Expression
1		dirkercncf.d	$⊢ 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	1	dirkerf	$⊢ N \in ℕ \to D (N) : ℝ ⟶ ℝ$
3		ax-resscn	$⊢ ℝ \subseteq ℂ$
4	3	a1i	$⊢ N \in ℕ \to ℝ \subseteq ℂ$
5	2 4	fssd	$⊢ N \in ℕ \to D (N) : ℝ ⟶ ℂ$
6	5	ad2antrr	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to D (N) : ℝ ⟶ ℂ$
7		oveq1	$⊢ y = w \to y \mod 2 π = w \mod 2 π$
8	7	eqeq1d	$⊢ y = w \to (y \mod 2 π = 0 \leftrightarrow w \mod 2 π = 0)$
9		oveq2	$⊢ y = w \to (n + (\frac{1}{2})) y = (n + (\frac{1}{2})) w$
10	9	fveq2d	$⊢ y = w \to \sin (n + (\frac{1}{2})) y = \sin (n + (\frac{1}{2})) w$
11		oveq1	$⊢ y = w \to \frac{y}{2} = \frac{w}{2}$
12	11	fveq2d	$⊢ y = w \to \sin (\frac{y}{2}) = \sin (\frac{w}{2})$
13	12	oveq2d	$⊢ y = w \to 2 π \sin (\frac{y}{2}) = 2 π \sin (\frac{w}{2})$
14	10 13	oveq12d	$⊢ y = w \to \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})} = \frac{\sin (n + (\frac{1}{2})) w}{2 π \sin (\frac{w}{2})}$
15	8 14	ifbieq2d	$⊢ y = w \to if (y \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})}) = if (w \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) w}{2 π \sin (\frac{w}{2})})$
16	15	cbvmptv	$⊢ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})) = (w \in ℝ ⟼ if (w \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) w}{2 π \sin (\frac{w}{2})}))$
17	16	mpteq2i	$⊢ (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})}))) = (n \in ℕ ⟼ (w \in ℝ ⟼ if (w \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) w}{2 π \sin (\frac{w}{2})})))$
18	1 17	eqtri	$⊢ D = (n \in ℕ ⟼ (w \in ℝ ⟼ if (w \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) w}{2 π \sin (\frac{w}{2})})))$
19		eqid	$⊢ y - π = y - π$
20		eqid	$⊢ y + π = y + π$
21		eqid	$⊢ (w \in (y - π, y + π) ⟼ \frac{\sin (n + (\frac{1}{2})) w}{2 π \sin (\frac{w}{2})}) = (w \in (y - π, y + π) ⟼ \frac{\sin (n + (\frac{1}{2})) w}{2 π \sin (\frac{w}{2})})$
22		eqid	$⊢ (w \in (y - π, y + π) ⟼ 2 π \sin (\frac{w}{2})) = (w \in (y - π, y + π) ⟼ 2 π \sin (\frac{w}{2}))$
23		simpll	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to N \in ℕ$
24		simplr	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to y \in ℝ$
25		simpr	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to y \mod 2 π = 0$
26	18 19 20 21 22 23 24 25	dirkercncflem3	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to D (N) (y) \in (D (N) {lim}_{ℂ} y)$
27	3	jctl	$⊢ y \in ℝ \to (ℝ \subseteq ℂ \land y \in ℝ)$
28	27	ad2antlr	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to (ℝ \subseteq ℂ \land y \in ℝ)$
29		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
30	29	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
31	29 30	cnplimc	$⊢ (ℝ \subseteq ℂ \land y \in ℝ) \to (D (N) \in (topGen (ran (.)) CnP TopOpen (ℂ_{fld})) (y) \leftrightarrow (D (N) : ℝ ⟶ ℂ \land D (N) (y) \in (D (N) {lim}_{ℂ} y)))$
32	28 31	syl	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to (D (N) \in (topGen (ran (.)) CnP TopOpen (ℂ_{fld})) (y) \leftrightarrow (D (N) : ℝ ⟶ ℂ \land D (N) (y) \in (D (N) {lim}_{ℂ} y)))$
33	6 26 32	mpbir2and	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to D (N) \in (topGen (ran (.)) CnP TopOpen (ℂ_{fld})) (y)$
34	29	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
35	34	a1i	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to TopOpen (ℂ_{fld}) \in Top$
36	2	ad2antrr	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to D (N) : ℝ ⟶ ℝ$
37	3	a1i	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to ℝ \subseteq ℂ$
38		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
39	38	toponunii	$⊢ ℝ = ⋃ topGen (ran (.))$
40	29	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
41	40	toponunii	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
42	39 41	cnprest2	$⊢ (TopOpen (ℂ_{fld}) \in Top \land D (N) : ℝ ⟶ ℝ \land ℝ \subseteq ℂ) \to (D (N) \in (topGen (ran (.)) CnP TopOpen (ℂ_{fld})) (y) \leftrightarrow D (N) \in (topGen (ran (.)) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)) (y))$
43	35 36 37 42	syl3anc	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to (D (N) \in (topGen (ran (.)) CnP TopOpen (ℂ_{fld})) (y) \leftrightarrow D (N) \in (topGen (ran (.)) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)) (y))$
44	33 43	mpbid	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to D (N) \in (topGen (ran (.)) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)) (y)$
45	30	eqcomi	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ = topGen (ran (.))$
46	45	a1i	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ = topGen (ran (.))$
47	46	oveq2d	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to topGen (ran (.)) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) = topGen (ran (.)) CnP topGen (ran (.))$
48	47	fveq1d	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to (topGen (ran (.)) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)) (y) = (topGen (ran (.)) CnP topGen (ran (.))) (y)$
49	44 48	eleqtrd	$⊢ ((N \in ℕ \land y \in ℝ) \land y \mod 2 π = 0) \to D (N) \in (topGen (ran (.)) CnP topGen (ran (.))) (y)$
50		simpll	$⊢ ((N \in ℕ \land y \in ℝ) \land \neg y \mod 2 π = 0) \to N \in ℕ$
51		simplr	$⊢ ((N \in ℕ \land y \in ℝ) \land \neg y \mod 2 π = 0) \to y \in ℝ$
52		neqne	$⊢ \neg y \mod 2 π = 0 \to y \mod 2 π \neq 0$
53	52	adantl	$⊢ ((N \in ℕ \land y \in ℝ) \land \neg y \mod 2 π = 0) \to y \mod 2 π \neq 0$
54		eqid	$⊢ ⌊\frac{y}{2 π}⌋ = ⌊\frac{y}{2 π}⌋$
55		eqid	$⊢ ⌊\frac{y}{2 π}⌋ + 1 = ⌊\frac{y}{2 π}⌋ + 1$
56		eqid	$⊢ ⌊\frac{y}{2 π}⌋ 2 π = ⌊\frac{y}{2 π}⌋ 2 π$
57		eqid	$⊢ (⌊\frac{y}{2 π}⌋ + 1) 2 π = (⌊\frac{y}{2 π}⌋ + 1) 2 π$
58	18 50 51 53 54 55 56 57	dirkercncflem4	$⊢ ((N \in ℕ \land y \in ℝ) \land \neg y \mod 2 π = 0) \to D (N) \in (topGen (ran (.)) CnP topGen (ran (.))) (y)$
59	49 58	pm2.61dan	$⊢ (N \in ℕ \land y \in ℝ) \to D (N) \in (topGen (ran (.)) CnP topGen (ran (.))) (y)$
60	59	ralrimiva	$⊢ N \in ℕ \to \forall y \in ℝ D (N) \in (topGen (ran (.)) CnP topGen (ran (.))) (y)$
61		cncnp	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land topGen (ran (.)) \in TopOn (ℝ)) \to (D (N) \in (topGen (ran (.)) Cn topGen (ran (.))) \leftrightarrow (D (N) : ℝ ⟶ ℝ \land \forall y \in ℝ D (N) \in (topGen (ran (.)) CnP topGen (ran (.))) (y)))$
62	38 38 61	mp2an	$⊢ D (N) \in (topGen (ran (.)) Cn topGen (ran (.))) \leftrightarrow (D (N) : ℝ ⟶ ℝ \land \forall y \in ℝ D (N) \in (topGen (ran (.)) CnP topGen (ran (.))) (y))$
63	2 60 62	sylanbrc	$⊢ N \in ℕ \to D (N) \in (topGen (ran (.)) Cn topGen (ran (.)))$
64	29 30 30	cncfcn	$⊢ (ℝ \subseteq ℂ \land ℝ \subseteq ℂ) \to ℝ \underset{cn}{⟶} ℝ = topGen (ran (.)) Cn topGen (ran (.))$
65	3 3 64	mp2an	$⊢ ℝ \underset{cn}{⟶} ℝ = topGen (ran (.)) Cn topGen (ran (.))$
66	63 65	eleqtrrdi	$⊢ N \in ℕ \to D (N) : ℝ \underset{cn}{⟶} ℝ$

Metamath Proof Explorer

Theorem dirkercncf

Proof