dirkercncflem3

Description: The Dirichlet Kernel is continuous at Y points that are multiples of ( 2 x. _pi ) . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	dirkercncflem3.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})})))$
	dirkercncflem3.a	$⊢ A = Y - π$
	dirkercncflem3.b	$⊢ B = Y + π$
	dirkercncflem3.f	$⊢ F = (y \in (A, B) ⟼ \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})$
	dirkercncflem3.g	$⊢ G = (y \in (A, B) ⟼ 2 π \sin (\frac{y}{2}))$
	dirkercncflem3.n	$⊢ φ \to N \in ℕ$
	dirkercncflem3.yr	$⊢ φ \to Y \in ℝ$
	dirkercncflem3.yod	$⊢ φ \to Y \mod 2 π = 0$
Assertion	dirkercncflem3	$⊢ φ \to D (N) (Y) \in (D (N) {lim}_{ℂ} Y)$

Proof

Step	Hyp	Ref	Expression
1		dirkercncflem3.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		dirkercncflem3.a	$⊢ A = Y - π$
3		dirkercncflem3.b	$⊢ B = Y + π$
4		dirkercncflem3.f	$⊢ F = (y \in (A, B) ⟼ \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})$
5		dirkercncflem3.g	$⊢ G = (y \in (A, B) ⟼ 2 π \sin (\frac{y}{2}))$
6		dirkercncflem3.n	$⊢ φ \to N \in ℕ$
7		dirkercncflem3.yr	$⊢ φ \to Y \in ℝ$
8		dirkercncflem3.yod	$⊢ φ \to Y \mod 2 π = 0$
9		oveq2	$⊢ w = y \to (N + (\frac{1}{2})) w = (N + (\frac{1}{2})) y$
10	9	fveq2d	$⊢ w = y \to \sin (N + (\frac{1}{2})) w = \sin (N + (\frac{1}{2})) y$
11	10	cbvmptv	$⊢ (w \in ((A, B) ∖ \{Y\}) ⟼ \sin (N + (\frac{1}{2})) w) = (y \in ((A, B) ∖ \{Y\}) ⟼ \sin (N + (\frac{1}{2})) y)$
12		fvoveq1	$⊢ w = y \to \sin (\frac{w}{2}) = \sin (\frac{y}{2})$
13	12	oveq2d	$⊢ w = y \to 2 π \sin (\frac{w}{2}) = 2 π \sin (\frac{y}{2})$
14	13	cbvmptv	$⊢ (w \in ((A, B) ∖ \{Y\}) ⟼ 2 π \sin (\frac{w}{2})) = (y \in ((A, B) ∖ \{Y\}) ⟼ 2 π \sin (\frac{y}{2}))$
15	2 3 7 8	dirkercncflem1	$⊢ φ \to (Y \in (A, B) \land \forall y \in ((A, B) ∖ \{Y\}) (\sin (\frac{y}{2}) \neq 0 \land \cos (\frac{y}{2}) \neq 0))$
16	15	simprd	$⊢ φ \to \forall y \in ((A, B) ∖ \{Y\}) (\sin (\frac{y}{2}) \neq 0 \land \cos (\frac{y}{2}) \neq 0)$
17		r19.26	$⊢ \forall y \in ((A, B) ∖ \{Y\}) (\sin (\frac{y}{2}) \neq 0 \land \cos (\frac{y}{2}) \neq 0) \leftrightarrow (\forall y \in ((A, B) ∖ \{Y\}) \sin (\frac{y}{2}) \neq 0 \land \forall y \in ((A, B) ∖ \{Y\}) \cos (\frac{y}{2}) \neq 0)$
18	16 17	sylib	$⊢ φ \to (\forall y \in ((A, B) ∖ \{Y\}) \sin (\frac{y}{2}) \neq 0 \land \forall y \in ((A, B) ∖ \{Y\}) \cos (\frac{y}{2}) \neq 0)$
19	18	simpld	$⊢ φ \to \forall y \in ((A, B) ∖ \{Y\}) \sin (\frac{y}{2}) \neq 0$
20	19	r19.21bi	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \sin (\frac{y}{2}) \neq 0$
21	9	fveq2d	$⊢ w = y \to \cos (N + (\frac{1}{2})) w = \cos (N + (\frac{1}{2})) y$
22	21	oveq2d	$⊢ w = y \to (N + (\frac{1}{2})) \cos (N + (\frac{1}{2})) w = (N + (\frac{1}{2})) \cos (N + (\frac{1}{2})) y$
23	22	cbvmptv	$⊢ (w \in ((A, B) ∖ \{Y\}) ⟼ (N + (\frac{1}{2})) \cos (N + (\frac{1}{2})) w) = (y \in ((A, B) ∖ \{Y\}) ⟼ (N + (\frac{1}{2})) \cos (N + (\frac{1}{2})) y)$
24		fvoveq1	$⊢ w = y \to \cos (\frac{w}{2}) = \cos (\frac{y}{2})$
25	24	oveq2d	$⊢ w = y \to π \cos (\frac{w}{2}) = π \cos (\frac{y}{2})$
26	25	cbvmptv	$⊢ (w \in ((A, B) ∖ \{Y\}) ⟼ π \cos (\frac{w}{2})) = (y \in ((A, B) ∖ \{Y\}) ⟼ π \cos (\frac{y}{2}))$
27		eqid	$⊢ (z \in (A, B) ⟼ \frac{(N + (\frac{1}{2})) \cos (N + (\frac{1}{2})) z}{π \cos (\frac{z}{2})}) = (z \in (A, B) ⟼ \frac{(N + (\frac{1}{2})) \cos (N + (\frac{1}{2})) z}{π \cos (\frac{z}{2})})$
28	15	simpld	$⊢ φ \to Y \in (A, B)$
29	18	simprd	$⊢ φ \to \forall y \in ((A, B) ∖ \{Y\}) \cos (\frac{y}{2}) \neq 0$
30	29	r19.21bi	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \cos (\frac{y}{2}) \neq 0$
31	1 11 14 20 23 26 27 6 28 8 30	dirkercncflem2	$⊢ φ \to D (N) (Y) \in (({D (N) ↾}_{((A, B) ∖ \{Y\})}) {lim}_{ℂ} Y)$
32	1	dirkerf	$⊢ N \in ℕ \to D (N) : ℝ ⟶ ℝ$
33	6 32	syl	$⊢ φ \to D (N) : ℝ ⟶ ℝ$
34		ax-resscn	$⊢ ℝ \subseteq ℂ$
35	34	a1i	$⊢ φ \to ℝ \subseteq ℂ$
36	33 35	fssd	$⊢ φ \to D (N) : ℝ ⟶ ℂ$
37		ioossre	$⊢ (A, B) \subseteq ℝ$
38	37	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
39	38	ssdifssd	$⊢ φ \to (A, B) ∖ \{Y\} \subseteq ℝ$
40		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
41		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (ℝ \cup \{Y\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} (ℝ \cup \{Y\})$
42		iooretop	$⊢ (A, B) \in topGen (ran (.))$
43		retop	$⊢ topGen (ran (.)) \in Top$
44		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
45	44	isopn3	$⊢ (topGen (ran (.)) \in Top \land (A, B) \subseteq ℝ) \to ((A, B) \in topGen (ran (.)) \leftrightarrow int (topGen (ran (.))) ((A, B)) = (A, B))$
46	43 38 45	sylancr	$⊢ φ \to ((A, B) \in topGen (ran (.)) \leftrightarrow int (topGen (ran (.))) ((A, B)) = (A, B))$
47	42 46	mpbii	$⊢ φ \to int (topGen (ran (.))) ((A, B)) = (A, B)$
48	28 47	eleqtrrd	$⊢ φ \to Y \in int (topGen (ran (.))) ((A, B))$
49	40	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
50	49	a1i	$⊢ φ \to topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
51	50	fveq2d	$⊢ φ \to int (topGen (ran (.))) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
52	51	fveq1d	$⊢ φ \to int (topGen (ran (.))) ((A, B)) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ((A, B))$
53	48 52	eleqtrd	$⊢ φ \to Y \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ((A, B))$
54	7	snssd	$⊢ φ \to \{Y\} \subseteq ℝ$
55		ssequn2	$⊢ \{Y\} \subseteq ℝ \leftrightarrow ℝ \cup \{Y\} = ℝ$
56	54 55	sylib	$⊢ φ \to ℝ \cup \{Y\} = ℝ$
57	56	oveq2d	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} (ℝ \cup \{Y\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
58	57	fveq2d	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} (ℝ \cup \{Y\})) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
59		uncom	$⊢ ((A, B) ∖ \{Y\}) \cup \{Y\} = \{Y\} \cup ((A, B) ∖ \{Y\})$
60	28	snssd	$⊢ φ \to \{Y\} \subseteq (A, B)$
61		undif	$⊢ \{Y\} \subseteq (A, B) \leftrightarrow \{Y\} \cup ((A, B) ∖ \{Y\}) = (A, B)$
62	60 61	sylib	$⊢ φ \to \{Y\} \cup ((A, B) ∖ \{Y\}) = (A, B)$
63	59 62	eqtrid	$⊢ φ \to ((A, B) ∖ \{Y\}) \cup \{Y\} = (A, B)$
64	58 63	fveq12d	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} (ℝ \cup \{Y\})) (((A, B) ∖ \{Y\}) \cup \{Y\}) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ((A, B))$
65	53 64	eleqtrrd	$⊢ φ \to Y \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} (ℝ \cup \{Y\})) (((A, B) ∖ \{Y\}) \cup \{Y\})$
66	36 39 35 40 41 65	limcres	$⊢ φ \to ({D (N) ↾}_{((A, B) ∖ \{Y\})}) {lim}_{ℂ} Y = D (N) {lim}_{ℂ} Y$
67	31 66	eleqtrd	$⊢ φ \to D (N) (Y) \in (D (N) {lim}_{ℂ} Y)$

Metamath Proof Explorer

Theorem dirkercncflem3

Proof