Metamath Proof Explorer

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 syl5eq ⊢ ( 𝜑 → ( ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ∪ { 𝑌 } ) = ( 𝐴 (,) 𝐵 ) )
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ℂ 𝑌 ) )