Metamath Proof Explorer

Theorem 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 ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
Assertion dirkercncf ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) ∈ ( ℝ –cn→ ℝ ) )

Proof

Step Hyp Ref Expression
1 dirkercncf.d ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
2 1 dirkerf ⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
3 ax-resscn ⊢ ℝ ⊆ ℂ
4 3 a1i ⊢ ( 𝑁 ∈ ℕ → ℝ ⊆ ℂ )
5 2 4 fssd ⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℂ )
6 5 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℂ )
7 oveq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 mod ( 2 · π ) ) = ( 𝑤 mod ( 2 · π ) ) )
8 7 eqeq1d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 mod ( 2 · π ) ) = 0 ↔ ( 𝑤 mod ( 2 · π ) ) = 0 ) )
9 oveq2 ⊢ ( 𝑦 = 𝑤 → ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) = ( ( 𝑛 + ( 1 / 2 ) ) · 𝑤 ) )
10 9 fveq2d ⊢ ( 𝑦 = 𝑤 → ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) = ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑤 ) ) )
11 oveq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 / 2 ) = ( 𝑤 / 2 ) )
12 11 fveq2d ⊢ ( 𝑦 = 𝑤 → ( sin ‘ ( 𝑦 / 2 ) ) = ( sin ‘ ( 𝑤 / 2 ) ) )
13 12 oveq2d ⊢ ( 𝑦 = 𝑤 → ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) )
14 10 13 oveq12d ⊢ ( 𝑦 = 𝑤 → ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑤 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) )
15 8 14 ifbieq2d ⊢ ( 𝑦 = 𝑤 → if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) = if ( ( 𝑤 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑤 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ) )
16 15 cbvmptv ⊢ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) = ( 𝑤 ∈ ℝ ↦ if ( ( 𝑤 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑤 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ) )
17 16 mpteq2i ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑤 ∈ ℝ ↦ if ( ( 𝑤 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑤 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ) ) )
18 1 17 eqtri ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑤 ∈ ℝ ↦ if ( ( 𝑤 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑤 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ) ) )
19 eqid ⊢ ( 𝑦 − π ) = ( 𝑦 − π )
20 eqid ⊢ ( 𝑦 + π ) = ( 𝑦 + π )
21 eqid ⊢ ( 𝑤 ∈ ( ( 𝑦 − π ) (,) ( 𝑦 + π ) ) ↦ ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑤 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) ) = ( 𝑤 ∈ ( ( 𝑦 − π ) (,) ( 𝑦 + π ) ) ↦ ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑤 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) )
22 eqid ⊢ ( 𝑤 ∈ ( ( 𝑦 − π ) (,) ( 𝑦 + π ) ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) ) = ( 𝑤 ∈ ( ( 𝑦 − π ) (,) ( 𝑦 + π ) ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑤 / 2 ) ) ) )
23 simpll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → 𝑁 ∈ ℕ )
24 simplr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → 𝑦 ∈ ℝ )
25 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ( 𝑦 mod ( 2 · π ) ) = 0 )
26 18 19 20 21 22 23 24 25 dirkercncflem3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑦 ) ∈ ( ( 𝐷 ‘ 𝑁 ) limℂ 𝑦 ) )
27 3 jctl ⊢ ( 𝑦 ∈ ℝ → ( ℝ ⊆ ℂ ∧ 𝑦 ∈ ℝ ) )
28 27 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ( ℝ ⊆ ℂ ∧ 𝑦 ∈ ℝ ) )
29 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
30 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
31 29 30 cnplimc ⊢ ( ( ℝ ⊆ ℂ ∧ 𝑦 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ↔ ( ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℂ ∧ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑦 ) ∈ ( ( 𝐷 ‘ 𝑁 ) limℂ 𝑦 ) ) ) )
32 28 31 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ( ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ↔ ( ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℂ ∧ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑦 ) ∈ ( ( 𝐷 ‘ 𝑁 ) limℂ 𝑦 ) ) ) )
33 6 26 32 mpbir2and ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
34 29 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
35 34 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ( TopOpen ‘ ℂfld ) ∈ Top )
36 2 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
37 3 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ℝ ⊆ ℂ )
38 retopon ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
39 38 toponunii ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
40 29 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
41 40 toponunii ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
42 39 41 cnprest2 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ( ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ↔ ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ 𝑦 ) ) )
43 35 36 37 42 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ( ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ↔ ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ 𝑦 ) ) )
44 33 43 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ 𝑦 ) )
45 30 eqcomi ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) = ( topGen ‘ ran (,) )
46 45 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) = ( topGen ‘ ran (,) ) )
47 46 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ( ( topGen ‘ ran (,) ) CnP ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) = ( ( topGen ‘ ran (,) ) CnP ( topGen ‘ ran (,) ) ) )
48 47 fveq1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ( ( ( topGen ‘ ran (,) ) CnP ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ 𝑦 ) = ( ( ( topGen ‘ ran (,) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑦 ) )
49 44 48 eleqtrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑦 ) )
50 simpll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ¬ ( 𝑦 mod ( 2 · π ) ) = 0 ) → 𝑁 ∈ ℕ )
51 simplr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ¬ ( 𝑦 mod ( 2 · π ) ) = 0 ) → 𝑦 ∈ ℝ )
52 neqne ⊢ ( ¬ ( 𝑦 mod ( 2 · π ) ) = 0 → ( 𝑦 mod ( 2 · π ) ) ≠ 0 )
53 52 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ¬ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ( 𝑦 mod ( 2 · π ) ) ≠ 0 )
54 eqid ⊢ ( ⌊ ‘ ( 𝑦 / ( 2 · π ) ) ) = ( ⌊ ‘ ( 𝑦 / ( 2 · π ) ) )
55 eqid ⊢ ( ( ⌊ ‘ ( 𝑦 / ( 2 · π ) ) ) + 1 ) = ( ( ⌊ ‘ ( 𝑦 / ( 2 · π ) ) ) + 1 )
56 eqid ⊢ ( ( ⌊ ‘ ( 𝑦 / ( 2 · π ) ) ) · ( 2 · π ) ) = ( ( ⌊ ‘ ( 𝑦 / ( 2 · π ) ) ) · ( 2 · π ) )
57 eqid ⊢ ( ( ( ⌊ ‘ ( 𝑦 / ( 2 · π ) ) ) + 1 ) · ( 2 · π ) ) = ( ( ( ⌊ ‘ ( 𝑦 / ( 2 · π ) ) ) + 1 ) · ( 2 · π ) )
58 18 50 51 53 54 55 56 57 dirkercncflem4 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ∧ ¬ ( 𝑦 mod ( 2 · π ) ) = 0 ) → ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑦 ) )
59 49 58 pm2.61dan ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) → ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑦 ) )
60 59 ralrimiva ⊢ ( 𝑁 ∈ ℕ → ∀ 𝑦 ∈ ℝ ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑦 ) )
61 cncnp ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ) → ( ( 𝐷 ‘ 𝑁 ) ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) ↔ ( ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ ∧ ∀ 𝑦 ∈ ℝ ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑦 ) ) ) )
62 38 38 61 mp2an ⊢ ( ( 𝐷 ‘ 𝑁 ) ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) ↔ ( ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ ∧ ∀ 𝑦 ∈ ℝ ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑦 ) ) )
63 2 60 62 sylanbrc ⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) )
64 29 30 30 cncfcn ⊢ ( ( ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℝ –cn→ ℝ ) = ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) )
65 3 3 64 mp2an ⊢ ( ℝ –cn→ ℝ ) = ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) )
66 63 65 eleqtrrdi ⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) ∈ ( ℝ –cn→ ℝ ) )