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 ⊢ D = n ∈ ℕ ⟼ y ∈ ℝ ⟼ if y mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ y 2 ⁢ π ⁢ sin ⁡ y 2
Assertion dirkercncf ⊢ N ∈ ℕ → D ⁡ N : ℝ ⟶cn ℝ

Proof

Step Hyp Ref Expression
1 dirkercncf.d ⊢ D = n ∈ ℕ ⟼ y ∈ ℝ ⟼ if y mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ y 2 ⁢ π ⁢ sin ⁡ y 2
2 1 dirkerf ⊢ N ∈ ℕ → D ⁡ N : ℝ ⟶ ℝ
3 ax-resscn ⊢ ℝ ⊆ ℂ
4 3 a1i ⊢ N ∈ ℕ → ℝ ⊆ ℂ
5 2 4 fssd ⊢ N ∈ ℕ → D ⁡ N : ℝ ⟶ ℂ
6 5 ad2antrr ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y mod 2 ⁢ π = 0 → D ⁡ N : ℝ ⟶ ℂ
7 oveq1 ⊢ y = w → y mod 2 ⁢ π = w mod 2 ⁢ π
8 7 eqeq1d ⊢ y = w → y mod 2 ⁢ π = 0 ↔ w mod 2 ⁢ π = 0
9 oveq2 ⊢ y = w → n + 1 2 ⁢ y = n + 1 2 ⁢ w
10 9 fveq2d ⊢ y = w → sin ⁡ n + 1 2 ⁢ y = sin ⁡ n + 1 2 ⁢ w
11 oveq1 ⊢ y = w → y 2 = w 2
12 11 fveq2d ⊢ y = w → sin ⁡ y 2 = sin ⁡ w 2
13 12 oveq2d ⊢ y = w → 2 ⁢ π ⁢ sin ⁡ y 2 = 2 ⁢ π ⁢ sin ⁡ w 2
14 10 13 oveq12d ⊢ y = w → sin ⁡ n + 1 2 ⁢ y 2 ⁢ π ⁢ sin ⁡ y 2 = sin ⁡ n + 1 2 ⁢ w 2 ⁢ π ⁢ sin ⁡ w 2
15 8 14 ifbieq2d ⊢ y = w → if y mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ y 2 ⁢ π ⁢ sin ⁡ y 2 = if w mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ w 2 ⁢ π ⁢ sin ⁡ w 2
16 15 cbvmptv ⊢ y ∈ ℝ ⟼ if y mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ y 2 ⁢ π ⁢ sin ⁡ y 2 = w ∈ ℝ ⟼ if w mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ w 2 ⁢ π ⁢ sin ⁡ w 2
17 16 mpteq2i ⊢ n ∈ ℕ ⟼ y ∈ ℝ ⟼ if y mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ y 2 ⁢ π ⁢ sin ⁡ y 2 = n ∈ ℕ ⟼ w ∈ ℝ ⟼ if w mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ w 2 ⁢ π ⁢ sin ⁡ w 2
18 1 17 eqtri ⊢ D = n ∈ ℕ ⟼ w ∈ ℝ ⟼ if w mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ w 2 ⁢ π ⁢ sin ⁡ w 2
19 eqid ⊢ y − π = y − π
20 eqid ⊢ y + π = y + π
21 eqid ⊢ w ∈ y − π y + π ⟼ sin ⁡ n + 1 2 ⁢ w 2 ⁢ π ⁢ sin ⁡ w 2 = w ∈ y − π y + π ⟼ sin ⁡ n + 1 2 ⁢ w 2 ⁢ π ⁢ sin ⁡ w 2
22 eqid ⊢ w ∈ y − π y + π ⟼ 2 ⁢ π ⁢ sin ⁡ w 2 = w ∈ y − π y + π ⟼ 2 ⁢ π ⁢ sin ⁡ w 2
23 simpll ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y mod 2 ⁢ π = 0 → N ∈ ℕ
24 simplr ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y mod 2 ⁢ π = 0 → y ∈ ℝ
25 simpr ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y mod 2 ⁢ π = 0 → y mod 2 ⁢ π = 0
26 18 19 20 21 22 23 24 25 dirkercncflem3 ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y mod 2 ⁢ π = 0 → D ⁡ N ⁡ y ∈ D ⁡ N lim ℂ y
27 3 jctl ⊢ y ∈ ℝ → ℝ ⊆ ℂ ∧ y ∈ ℝ
28 27 ad2antlr ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y mod 2 ⁢ π = 0 → ℝ ⊆ ℂ ∧ y ∈ ℝ
29 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
30 29 tgioo2 ⊢ topGen ⁡ ran ⁡ . = TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
31 29 30 cnplimc ⊢ ℝ ⊆ ℂ ∧ y ∈ ℝ → D ⁡ N ∈ topGen ⁡ ran ⁡ . CnP TopOpen ⁡ ℂ fld ⁡ y ↔ D ⁡ N : ℝ ⟶ ℂ ∧ D ⁡ N ⁡ y ∈ D ⁡ N lim ℂ y
32 28 31 syl ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y mod 2 ⁢ π = 0 → D ⁡ N ∈ topGen ⁡ ran ⁡ . CnP TopOpen ⁡ ℂ fld ⁡ y ↔ D ⁡ N : ℝ ⟶ ℂ ∧ D ⁡ N ⁡ y ∈ D ⁡ N lim ℂ y
33 6 26 32 mpbir2and ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y mod 2 ⁢ π = 0 → D ⁡ N ∈ topGen ⁡ ran ⁡ . CnP TopOpen ⁡ ℂ fld ⁡ y
34 29 cnfldtop ⊢ TopOpen ⁡ ℂ fld ∈ Top
35 34 a1i ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y mod 2 ⁢ π = 0 → TopOpen ⁡ ℂ fld ∈ Top
36 2 ad2antrr ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y mod 2 ⁢ π = 0 → D ⁡ N : ℝ ⟶ ℝ
37 3 a1i ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y 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 ∧ D ⁡ N : ℝ ⟶ ℝ ∧ ℝ ⊆ ℂ → D ⁡ N ∈ topGen ⁡ ran ⁡ . CnP TopOpen ⁡ ℂ fld ⁡ y ↔ D ⁡ N ∈ topGen ⁡ ran ⁡ . CnP TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ ⁡ y
43 35 36 37 42 syl3anc ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y mod 2 ⁢ π = 0 → D ⁡ N ∈ topGen ⁡ ran ⁡ . CnP TopOpen ⁡ ℂ fld ⁡ y ↔ D ⁡ N ∈ topGen ⁡ ran ⁡ . CnP TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ ⁡ y
44 33 43 mpbid ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y mod 2 ⁢ π = 0 → D ⁡ N ∈ topGen ⁡ ran ⁡ . CnP TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ ⁡ y
45 30 eqcomi ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ = topGen ⁡ ran ⁡ .
46 45 a1i ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y mod 2 ⁢ π = 0 → TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ = topGen ⁡ ran ⁡ .
47 46 oveq2d ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y mod 2 ⁢ π = 0 → topGen ⁡ ran ⁡ . CnP TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ = topGen ⁡ ran ⁡ . CnP topGen ⁡ ran ⁡ .
48 47 fveq1d ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y mod 2 ⁢ π = 0 → topGen ⁡ ran ⁡ . CnP TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ ⁡ y = topGen ⁡ ran ⁡ . CnP topGen ⁡ ran ⁡ . ⁡ y
49 44 48 eleqtrd ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ y mod 2 ⁢ π = 0 → D ⁡ N ∈ topGen ⁡ ran ⁡ . CnP topGen ⁡ ran ⁡ . ⁡ y
50 simpll ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ ¬ y mod 2 ⁢ π = 0 → N ∈ ℕ
51 simplr ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ ¬ y mod 2 ⁢ π = 0 → y ∈ ℝ
52 neqne ⊢ ¬ y mod 2 ⁢ π = 0 → y mod 2 ⁢ π ≠ 0
53 52 adantl ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ ¬ y mod 2 ⁢ π = 0 → y mod 2 ⁢ π ≠ 0
54 eqid ⊢ y 2 ⁢ π = y 2 ⁢ π
55 eqid ⊢ y 2 ⁢ π + 1 = y 2 ⁢ π + 1
56 eqid ⊢ y 2 ⁢ π ⁢ 2 ⁢ π = y 2 ⁢ π ⁢ 2 ⁢ π
57 eqid ⊢ y 2 ⁢ π + 1 ⁢ 2 ⁢ π = y 2 ⁢ π + 1 ⁢ 2 ⁢ π
58 18 50 51 53 54 55 56 57 dirkercncflem4 ⊢ N ∈ ℕ ∧ y ∈ ℝ ∧ ¬ y mod 2 ⁢ π = 0 → D ⁡ N ∈ topGen ⁡ ran ⁡ . CnP topGen ⁡ ran ⁡ . ⁡ y
59 49 58 pm2.61dan ⊢ N ∈ ℕ ∧ y ∈ ℝ → D ⁡ N ∈ topGen ⁡ ran ⁡ . CnP topGen ⁡ ran ⁡ . ⁡ y
60 59 ralrimiva ⊢ N ∈ ℕ → ∀ y ∈ ℝ D ⁡ N ∈ topGen ⁡ ran ⁡ . CnP topGen ⁡ ran ⁡ . ⁡ y
61 cncnp ⊢ topGen ⁡ ran ⁡ . ∈ TopOn ⁡ ℝ ∧ topGen ⁡ ran ⁡ . ∈ TopOn ⁡ ℝ → D ⁡ N ∈ topGen ⁡ ran ⁡ . Cn topGen ⁡ ran ⁡ . ↔ D ⁡ N : ℝ ⟶ ℝ ∧ ∀ y ∈ ℝ D ⁡ N ∈ topGen ⁡ ran ⁡ . CnP topGen ⁡ ran ⁡ . ⁡ y
62 38 38 61 mp2an ⊢ D ⁡ N ∈ topGen ⁡ ran ⁡ . Cn topGen ⁡ ran ⁡ . ↔ D ⁡ N : ℝ ⟶ ℝ ∧ ∀ y ∈ ℝ D ⁡ N ∈ topGen ⁡ ran ⁡ . CnP topGen ⁡ ran ⁡ . ⁡ y
63 2 60 62 sylanbrc ⊢ N ∈ ℕ → D ⁡ N ∈ 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 ⊢ N ∈ ℕ → D ⁡ N : ℝ ⟶cn ℝ