Theorem 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	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
	dirkercncflem3.a	⊢ 𝐴 = ( 𝑌 − π )
	dirkercncflem3.b	⊢ 𝐵 = ( 𝑌 + π )
	dirkercncflem3.f	⊢ 𝐹 = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) )
	dirkercncflem3.g	⊢ 𝐺 = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) )
	dirkercncflem3.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	dirkercncflem3.yr	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
	dirkercncflem3.yod	⊢ ( 𝜑 → ( 𝑌 mod ( 2 · π ) ) = 0 )
Assertion	dirkercncflem3	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑌 ) ∈ ( ( 𝐷 ‘ 𝑁 ) limℂ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		dirkercncflem3.d	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
2		dirkercncflem3.a	⊢ 𝐴 = ( 𝑌 − π )
3		dirkercncflem3.b	⊢ 𝐵 = ( 𝑌 + π )
4		dirkercncflem3.f	⊢ 𝐹 = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) )
5		dirkercncflem3.g	⊢ 𝐺 = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) )
6		dirkercncflem3.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7		dirkercncflem3.yr	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
8		dirkercncflem3.yod	⊢ ( 𝜑 → ( 𝑌 mod ( 2 · π ) ) = 0 )
9		oveq2	⊢ ( 𝑤 = 𝑦 → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) )
10	9	fveq2d	⊢ ( 𝑤 = 𝑦 → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) )
11	10	cbvmptv	⊢ ( 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) )
12		fvoveq1	⊢ ( 𝑤 = 𝑦 → ( sin ‘ ( 𝑤 / 2 ) ) = ( sin ‘ ( 𝑦 / 2 ) ) )
13	12	oveq2d	⊢ ( 𝑤 = 𝑦 → ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) )
14	13	cbvmptv	⊢ ( 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) )
15	2 3 7 8	dirkercncflem1	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐴 (,) 𝐵 ) ∧ ∀ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( ( sin ‘ ( 𝑦 / 2 ) ) ≠ 0 ∧ ( cos ‘ ( 𝑦 / 2 ) ) ≠ 0 ) ) )
16	15	simprd	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( ( sin ‘ ( 𝑦 / 2 ) ) ≠ 0 ∧ ( cos ‘ ( 𝑦 / 2 ) ) ≠ 0 ) )
17		r19.26	⊢ ( ∀ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( ( sin ‘ ( 𝑦 / 2 ) ) ≠ 0 ∧ ( cos ‘ ( 𝑦 / 2 ) ) ≠ 0 ) ↔ ( ∀ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( sin ‘ ( 𝑦 / 2 ) ) ≠ 0 ∧ ∀ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( cos ‘ ( 𝑦 / 2 ) ) ≠ 0 ) )
18	16 17	sylib	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( sin ‘ ( 𝑦 / 2 ) ) ≠ 0 ∧ ∀ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( cos ‘ ( 𝑦 / 2 ) ) ≠ 0 ) )
19	18	simpld	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( sin ‘ ( 𝑦 / 2 ) ) ≠ 0 )
20	19	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( sin ‘ ( 𝑦 / 2 ) ) ≠ 0 )
21	9	fveq2d	⊢ ( 𝑤 = 𝑦 → ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) = ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) )
22	21	oveq2d	⊢ ( 𝑤 = 𝑦 → ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) = ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) )
23	22	cbvmptv	⊢ ( 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) )
24		fvoveq1	⊢ ( 𝑤 = 𝑦 → ( cos ‘ ( 𝑤 / 2 ) ) = ( cos ‘ ( 𝑦 / 2 ) ) )
25	24	oveq2d	⊢ ( 𝑤 = 𝑦 → ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) = ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) )
26	25	cbvmptv	⊢ ( 𝑤 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) )
27		eqid	⊢ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑧 ) ) ) / ( π · ( cos ‘ ( 𝑧 / 2 ) ) ) ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑧 ) ) ) / ( π · ( cos ‘ ( 𝑧 / 2 ) ) ) ) )
28	15	simpld	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 (,) 𝐵 ) )
29	18	simprd	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ( cos ‘ ( 𝑦 / 2 ) ) ≠ 0 )
30	29	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( cos ‘ ( 𝑦 / 2 ) ) ≠ 0 )
31	1 11 14 20 23 26 27 6 28 8 30	dirkercncflem2	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑌 ) ∈ ( ( ( 𝐷 ‘ 𝑁 ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) limℂ 𝑌 ) )
32	1	dirkerf	⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
33	6 32	syl	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
34		ax-resscn	⊢ ℝ ⊆ ℂ
35	34	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
36	33 35	fssd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℂ )
37		ioossre	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
38	37	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
39	38	ssdifssd	⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ⊆ ℝ )
40		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
41		eqid	⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ℝ ∪ { 𝑌 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ℝ ∪ { 𝑌 } ) )
42		iooretop	⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
43		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
44		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
45	44	isopn3	⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) → ( ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ↔ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) ) )
46	43 38 45	sylancr	⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ↔ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) ) )
47	42 46	mpbii	⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
48	28 47	eleqtrrd	⊢ ( 𝜑 → 𝑌 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) )
49	40	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
50	49	a1i	⊢ ( 𝜑 → ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
51	50	fveq2d	⊢ ( 𝜑 → ( int ‘ ( topGen ‘ ran (,) ) ) = ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) )
52	51	fveq1d	⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ ( 𝐴 (,) 𝐵 ) ) )
53	48 52	eleqtrd	⊢ ( 𝜑 → 𝑌 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ ( 𝐴 (,) 𝐵 ) ) )
54	7	snssd	⊢ ( 𝜑 → { 𝑌 } ⊆ ℝ )
55		ssequn2	⊢ ( { 𝑌 } ⊆ ℝ ↔ ( ℝ ∪ { 𝑌 } ) = ℝ )
56	54 55	sylib	⊢ ( 𝜑 → ( ℝ ∪ { 𝑌 } ) = ℝ )
57	56	oveq2d	⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( ℝ ∪ { 𝑌 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
58	57	fveq2d	⊢ ( 𝜑 → ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ℝ ∪ { 𝑌 } ) ) ) = ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) )
59		uncom	⊢ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) = ( { 𝑌 } ∪ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) )
60	28	snssd	⊢ ( 𝜑 → { 𝑌 } ⊆ ( 𝐴 (,) 𝐵 ) )
61		undif	⊢ ( { 𝑌 } ⊆ ( 𝐴 (,) 𝐵 ) ↔ ( { 𝑌 } ∪ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( 𝐴 (,) 𝐵 ) )
62	60 61	sylib	⊢ ( 𝜑 → ( { 𝑌 } ∪ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) = ( 𝐴 (,) 𝐵 ) )
63	59 62	eqtrid	⊢ ( 𝜑 → ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) = ( 𝐴 (,) 𝐵 ) )
64	58 63	fveq12d	⊢ ( 𝜑 → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ℝ ∪ { 𝑌 } ) ) ) ‘ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ ( 𝐴 (,) 𝐵 ) ) )
65	53 64	eleqtrrd	⊢ ( 𝜑 → 𝑌 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ℝ ∪ { 𝑌 } ) ) ) ‘ ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) ) )
66	36 39 35 40 41 65	limcres	⊢ ( 𝜑 → ( ( ( 𝐷 ‘ 𝑁 ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) limℂ 𝑌 ) = ( ( 𝐷 ‘ 𝑁 ) limℂ 𝑌 ) )
67	31 66	eleqtrd	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑌 ) ∈ ( ( 𝐷 ‘ 𝑁 ) limℂ 𝑌 ) )