Metamath Proof Explorer

Theorem dirkercncflem4

Description: The Dirichlet Kernel is continuos at points that are not multiple of 2 π . This is the easier condition, for the proof of the continuity of the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dirkercncflem4.d ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
dirkercncflem4.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
dirkercncflem4.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
dirkercncflem4.ymod0 ⊢ ( 𝜑 → ( 𝑌 mod ( 2 · π ) ) ≠ 0 )
dirkercncflem4.a ⊢ 𝐴 = ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) )
dirkercncflem4.b ⊢ 𝐵 = ( 𝐴 + 1 )
dirkercncflem4.c ⊢ 𝐶 = ( 𝐴 · ( 2 · π ) )
dirkercncflem4.e ⊢ 𝐸 = ( 𝐵 · ( 2 · π ) )
Assertion dirkercncflem4 ( 𝜑 → ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 dirkercncflem4.d ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
2 dirkercncflem4.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 dirkercncflem4.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
4 dirkercncflem4.ymod0 ⊢ ( 𝜑 → ( 𝑌 mod ( 2 · π ) ) ≠ 0 )
5 dirkercncflem4.a ⊢ 𝐴 = ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) )
6 dirkercncflem4.b ⊢ 𝐵 = ( 𝐴 + 1 )
7 dirkercncflem4.c ⊢ 𝐶 = ( 𝐴 · ( 2 · π ) )
8 dirkercncflem4.e ⊢ 𝐸 = ( 𝐵 · ( 2 · π ) )
9 sincn ⊢ sin ∈ ( ℂ –cn→ ℂ )
10 9 a1i ⊢ ( 𝜑 → sin ∈ ( ℂ –cn→ ℂ ) )
11 ioosscn ⊢ ( 𝐶 (,) 𝐸 ) ⊆ ℂ
12 11 a1i ⊢ ( 𝜑 → ( 𝐶 (,) 𝐸 ) ⊆ ℂ )
13 2 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
14 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
15 14 halfcld ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
16 13 15 addcld ⊢ ( 𝜑 → ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ )
17 ssid ⊢ ℂ ⊆ ℂ
18 17 a1i ⊢ ( 𝜑 → ℂ ⊆ ℂ )
19 12 16 18 constcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( 𝑁 + ( 1 / 2 ) ) ) ∈ ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) )
20 12 18 idcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ 𝑦 ) ∈ ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) )
21 19 20 mulcncf ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ∈ ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) )
22 10 21 cncfmpt1f ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) ∈ ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) )
23 2cnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → 2 ∈ ℂ )
24 pirp ⊢ π ∈ ℝ+
25 24 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → π ∈ ℝ+ )
26 25 rpcnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → π ∈ ℂ )
27 23 26 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 2 · π ) ∈ ℂ )
28 ioossre ⊢ ( 𝐶 (,) 𝐸 ) ⊆ ℝ
29 28 a1i ⊢ ( 𝜑 → ( 𝐶 (,) 𝐸 ) ⊆ ℝ )
30 29 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → 𝑦 ∈ ℝ )
31 30 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → 𝑦 ∈ ℂ )
32 31 halfcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 𝑦 / 2 ) ∈ ℂ )
33 32 sincld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( sin ‘ ( 𝑦 / 2 ) ) ∈ ℂ )
34 27 33 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ∈ ℂ )
35 2rp ⊢ 2 ∈ ℝ+
36 35 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → 2 ∈ ℝ+ )
37 36 rpne0d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → 2 ≠ 0 )
38 25 rpne0d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → π ≠ 0 )
39 23 26 37 38 mulne0d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 2 · π ) ≠ 0 )
40 31 23 26 37 38 divdiv1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( ( 𝑦 / 2 ) / π ) = ( 𝑦 / ( 2 · π ) ) )
41 5 oveq1i ⊢ ( 𝐴 · ( 2 · π ) ) = ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) · ( 2 · π ) )
42 7 41 eqtri ⊢ 𝐶 = ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) · ( 2 · π ) )
43 42 oveq1i ⊢ ( 𝐶 / ( 2 · π ) ) = ( ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) · ( 2 · π ) ) / ( 2 · π ) )
44 2re ⊢ 2 ∈ ℝ
45 pire ⊢ π ∈ ℝ
46 44 45 remulcli ⊢ ( 2 · π ) ∈ ℝ
47 46 a1i ⊢ ( 𝜑 → ( 2 · π ) ∈ ℝ )
48 0re ⊢ 0 ∈ ℝ
49 2pos ⊢ 0 < 2
50 pipos ⊢ 0 < π
51 44 45 49 50 mulgt0ii ⊢ 0 < ( 2 · π )
52 48 51 gtneii ⊢ ( 2 · π ) ≠ 0
53 52 a1i ⊢ ( 𝜑 → ( 2 · π ) ≠ 0 )
54 3 47 53 redivcld ⊢ ( 𝜑 → ( 𝑌 / ( 2 · π ) ) ∈ ℝ )
55 54 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) ∈ ℤ )
56 55 zred ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) ∈ ℝ )
57 56 recnd ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) ∈ ℂ )
58 47 recnd ⊢ ( 𝜑 → ( 2 · π ) ∈ ℂ )
59 57 58 53 divcan4d ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) · ( 2 · π ) ) / ( 2 · π ) ) = ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) )
60 43 59 syl5eq ⊢ ( 𝜑 → ( 𝐶 / ( 2 · π ) ) = ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) )
61 60 55 eqeltrd ⊢ ( 𝜑 → ( 𝐶 / ( 2 · π ) ) ∈ ℤ )
62 61 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 𝐶 / ( 2 · π ) ) ∈ ℤ )
63 56 47 remulcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) · ( 2 · π ) ) ∈ ℝ )
64 42 63 eqeltrid ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
65 64 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → 𝐶 ∈ ℝ )
66 36 25 rpmulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 2 · π ) ∈ ℝ+ )
67 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → 𝑦 ∈ ( 𝐶 (,) 𝐸 ) )
68 64 rexrd ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → 𝐶 ∈ ℝ* )
70 5 eqcomi ⊢ ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) = 𝐴
71 70 oveq1i ⊢ ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) + 1 ) = ( 𝐴 + 1 )
72 71 6 eqtr4i ⊢ ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) + 1 ) = 𝐵
73 72 oveq1i ⊢ ( ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) + 1 ) · ( 2 · π ) ) = ( 𝐵 · ( 2 · π ) )
74 73 8 eqtr4i ⊢ ( ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) + 1 ) · ( 2 · π ) ) = 𝐸
75 74 a1i ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) + 1 ) · ( 2 · π ) ) = 𝐸 )
76 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
77 56 76 readdcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) + 1 ) ∈ ℝ )
78 77 47 remulcld ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) + 1 ) · ( 2 · π ) ) ∈ ℝ )
79 75 78 eqeltrrd ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
80 79 rexrd ⊢ ( 𝜑 → 𝐸 ∈ ℝ* )
81 80 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → 𝐸 ∈ ℝ* )
82 elioo2 ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐸 ∈ ℝ* ) → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸 ) ) )
83 69 81 82 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸 ) ) )
84 67 83 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸 ) )
85 84 simp2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → 𝐶 < 𝑦 )
86 65 30 66 85 ltdiv1dd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 𝐶 / ( 2 · π ) ) < ( 𝑦 / ( 2 · π ) ) )
87 79 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → 𝐸 ∈ ℝ )
88 84 simp3d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → 𝑦 < 𝐸 )
89 30 87 66 88 ltdiv1dd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 𝑦 / ( 2 · π ) ) < ( 𝐸 / ( 2 · π ) ) )
90 7 a1i ⊢ ( 𝜑 → 𝐶 = ( 𝐴 · ( 2 · π ) ) )
91 90 oveq1d ⊢ ( 𝜑 → ( 𝐶 / ( 2 · π ) ) = ( ( 𝐴 · ( 2 · π ) ) / ( 2 · π ) ) )
92 91 oveq1d ⊢ ( 𝜑 → ( ( 𝐶 / ( 2 · π ) ) + 1 ) = ( ( ( 𝐴 · ( 2 · π ) ) / ( 2 · π ) ) + 1 ) )
93 5 57 eqeltrid ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
94 93 58 53 divcan4d ⊢ ( 𝜑 → ( ( 𝐴 · ( 2 · π ) ) / ( 2 · π ) ) = 𝐴 )
95 94 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐴 · ( 2 · π ) ) / ( 2 · π ) ) + 1 ) = ( 𝐴 + 1 ) )
96 6 oveq1i ⊢ ( 𝐵 · ( 2 · π ) ) = ( ( 𝐴 + 1 ) · ( 2 · π ) )
97 8 96 eqtri ⊢ 𝐸 = ( ( 𝐴 + 1 ) · ( 2 · π ) )
98 97 a1i ⊢ ( 𝜑 → 𝐸 = ( ( 𝐴 + 1 ) · ( 2 · π ) ) )
99 98 oveq1d ⊢ ( 𝜑 → ( 𝐸 / ( 2 · π ) ) = ( ( ( 𝐴 + 1 ) · ( 2 · π ) ) / ( 2 · π ) ) )
100 93 14 addcld ⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℂ )
101 100 58 53 divcan4d ⊢ ( 𝜑 → ( ( ( 𝐴 + 1 ) · ( 2 · π ) ) / ( 2 · π ) ) = ( 𝐴 + 1 ) )
102 99 101 eqtr2d ⊢ ( 𝜑 → ( 𝐴 + 1 ) = ( 𝐸 / ( 2 · π ) ) )
103 92 95 102 3eqtrrd ⊢ ( 𝜑 → ( 𝐸 / ( 2 · π ) ) = ( ( 𝐶 / ( 2 · π ) ) + 1 ) )
104 103 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 𝐸 / ( 2 · π ) ) = ( ( 𝐶 / ( 2 · π ) ) + 1 ) )
105 89 104 breqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 𝑦 / ( 2 · π ) ) < ( ( 𝐶 / ( 2 · π ) ) + 1 ) )
106 btwnnz ⊢ ( ( ( 𝐶 / ( 2 · π ) ) ∈ ℤ ∧ ( 𝐶 / ( 2 · π ) ) < ( 𝑦 / ( 2 · π ) ) ∧ ( 𝑦 / ( 2 · π ) ) < ( ( 𝐶 / ( 2 · π ) ) + 1 ) ) → ¬ ( 𝑦 / ( 2 · π ) ) ∈ ℤ )
107 62 86 105 106 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ¬ ( 𝑦 / ( 2 · π ) ) ∈ ℤ )
108 40 107 eqneltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ¬ ( ( 𝑦 / 2 ) / π ) ∈ ℤ )
109 sineq0 ⊢ ( ( 𝑦 / 2 ) ∈ ℂ → ( ( sin ‘ ( 𝑦 / 2 ) ) = 0 ↔ ( ( 𝑦 / 2 ) / π ) ∈ ℤ ) )
110 32 109 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( ( sin ‘ ( 𝑦 / 2 ) ) = 0 ↔ ( ( 𝑦 / 2 ) / π ) ∈ ℤ ) )
111 108 110 mtbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ¬ ( sin ‘ ( 𝑦 / 2 ) ) = 0 )
112 111 neqned ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( sin ‘ ( 𝑦 / 2 ) ) ≠ 0 )
113 27 33 39 112 mulne0d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ≠ 0 )
114 113 neneqd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ¬ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) = 0 )
115 44 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → 2 ∈ ℝ )
116 45 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → π ∈ ℝ )
117 115 116 remulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 2 · π ) ∈ ℝ )
118 30 rehalfcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 𝑦 / 2 ) ∈ ℝ )
119 118 resincld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( sin ‘ ( 𝑦 / 2 ) ) ∈ ℝ )
120 117 119 remulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ∈ ℝ )
121 elsng ⊢ ( ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ∈ ℝ → ( ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ∈ { 0 } ↔ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) = 0 ) )
122 120 121 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ∈ { 0 } ↔ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) = 0 ) )
123 114 122 mtbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ¬ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ∈ { 0 } )
124 34 123 eldifd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ∈ ( ℂ ∖ { 0 } ) )
125 eqidd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) = ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) )
126 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) )
127 oveq2 ⊢ ( 𝑥 = ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) → ( 1 / 𝑥 ) = ( 1 / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) )
128 124 125 126 127 fmptco ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) ∘ ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) = ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( 1 / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) )
129 eqid ⊢ ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) = ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) )
130 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
131 12 130 18 constcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ 2 ) ∈ ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) )
132 24 a1i ⊢ ( 𝜑 → π ∈ ℝ+ )
133 132 rpcnd ⊢ ( 𝜑 → π ∈ ℂ )
134 12 133 18 constcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ π ) ∈ ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) )
135 131 134 mulcncf ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( 2 · π ) ) ∈ ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) )
136 31 23 37 divrecd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 𝑦 / 2 ) = ( 𝑦 · ( 1 / 2 ) ) )
137 136 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( 𝑦 / 2 ) ) = ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( 𝑦 · ( 1 / 2 ) ) ) )
138 12 15 18 constcncfg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( 1 / 2 ) ) ∈ ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) )
139 20 138 mulcncf ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( 𝑦 · ( 1 / 2 ) ) ) ∈ ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) )
140 137 139 eqeltrd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( 𝑦 / 2 ) ) ∈ ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) )
141 10 140 cncfmpt1f ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( sin ‘ ( 𝑦 / 2 ) ) ) ∈ ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) )
142 135 141 mulcncf ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ∈ ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) )
143 ssid ⊢ ( 𝐶 (,) 𝐸 ) ⊆ ( 𝐶 (,) 𝐸 )
144 143 a1i ⊢ ( 𝜑 → ( 𝐶 (,) 𝐸 ) ⊆ ( 𝐶 (,) 𝐸 ) )
145 difssd ⊢ ( 𝜑 → ( ℂ ∖ { 0 } ) ⊆ ℂ )
146 129 142 144 145 124 cncfmptssg ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ∈ ( ( 𝐶 (,) 𝐸 ) –cn→ ( ℂ ∖ { 0 } ) ) )
147 ax-1cn ⊢ 1 ∈ ℂ
148 eqid ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) )
149 148 cdivcncf ⊢ ( 1 ∈ ℂ → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) ∈ ( ( ℂ ∖ { 0 } ) –cn→ ℂ ) )
150 147 149 mp1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) ∈ ( ( ℂ ∖ { 0 } ) –cn→ ℂ ) )
151 146 150 cncfco ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) ∘ ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ∈ ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) )
152 128 151 eqeltrrd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( 1 / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ∈ ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) )
153 22 152 mulcncf ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) · ( 1 / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) ∈ ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) )
154 1 dirkerval ⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) = ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
155 2 154 syl ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) = ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
156 155 reseq1d ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) = ( ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) ↾ ( 𝐶 (,) 𝐸 ) ) )
157 29 resmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ 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 ) ) ) ) ) ) )
158 35 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
159 158 132 rpmulcld ⊢ ( 𝜑 → ( 2 · π ) ∈ ℝ+ )
160 159 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 2 · π ) ∈ ℝ+ )
161 mod0 ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 2 · π ) ∈ ℝ+ ) → ( ( 𝑦 mod ( 2 · π ) ) = 0 ↔ ( 𝑦 / ( 2 · π ) ) ∈ ℤ ) )
162 30 160 161 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( ( 𝑦 mod ( 2 · π ) ) = 0 ↔ ( 𝑦 / ( 2 · π ) ) ∈ ℤ ) )
163 107 162 mtbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ¬ ( 𝑦 mod ( 2 · π ) ) = 0 )
164 163 iffalsed ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) )
165 13 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → 𝑁 ∈ ℂ )
166 1cnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → 1 ∈ ℂ )
167 166 halfcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 1 / 2 ) ∈ ℂ )
168 165 167 addcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ )
169 168 31 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ∈ ℂ )
170 169 sincld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ∈ ℂ )
171 170 34 113 divrecd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) · ( 1 / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) )
172 164 171 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ) → if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) · ( 1 / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) )
173 172 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) = ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) · ( 1 / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
174 156 157 173 3eqtrrd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ↦ ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) · ( 1 / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) = ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) )
175 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
176 175 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
177 176 oveq1i ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( 𝐶 (,) 𝐸 ) )
178 175 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
179 reex ⊢ ℝ ∈ V
180 restabs ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( 𝐶 (,) 𝐸 ) ⊆ ℝ ∧ ℝ ∈ V ) → ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( 𝐶 (,) 𝐸 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐶 (,) 𝐸 ) ) )
181 178 28 179 180 mp3an ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( 𝐶 (,) 𝐸 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐶 (,) 𝐸 ) )
182 177 181 eqtri ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐶 (,) 𝐸 ) )
183 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
184 183 restid ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
185 178 184 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
186 185 eqcomi ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
187 175 182 186 cncfcn ⊢ ( ( ( 𝐶 (,) 𝐸 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) = ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
188 12 18 187 syl2anc ⊢ ( 𝜑 → ( ( 𝐶 (,) 𝐸 ) –cn→ ℂ ) = ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
189 153 174 188 3eltr3d ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
190 retopon ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
191 190 a1i ⊢ ( 𝜑 → ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) )
192 resttopon ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( 𝐶 (,) 𝐸 ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) ∈ ( TopOn ‘ ( 𝐶 (,) 𝐸 ) ) )
193 191 29 192 syl2anc ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) ∈ ( TopOn ‘ ( 𝐶 (,) 𝐸 ) ) )
194 175 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
195 194 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
196 cncnp ⊢ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) ∈ ( TopOn ‘ ( 𝐶 (,) 𝐸 ) ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) : ( 𝐶 (,) 𝐸 ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) ) )
197 193 195 196 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) : ( 𝐶 (,) 𝐸 ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) ) )
198 189 197 mpbid ⊢ ( 𝜑 → ( ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) : ( 𝐶 (,) 𝐸 ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) )
199 198 simprd ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
200 4 neneqd ⊢ ( 𝜑 → ¬ ( 𝑌 mod ( 2 · π ) ) = 0 )
201 mod0 ⊢ ( ( 𝑌 ∈ ℝ ∧ ( 2 · π ) ∈ ℝ+ ) → ( ( 𝑌 mod ( 2 · π ) ) = 0 ↔ ( 𝑌 / ( 2 · π ) ) ∈ ℤ ) )
202 3 159 201 syl2anc ⊢ ( 𝜑 → ( ( 𝑌 mod ( 2 · π ) ) = 0 ↔ ( 𝑌 / ( 2 · π ) ) ∈ ℤ ) )
203 200 202 mtbid ⊢ ( 𝜑 → ¬ ( 𝑌 / ( 2 · π ) ) ∈ ℤ )
204 flltnz ⊢ ( ( ( 𝑌 / ( 2 · π ) ) ∈ ℝ ∧ ¬ ( 𝑌 / ( 2 · π ) ) ∈ ℤ ) → ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) < ( 𝑌 / ( 2 · π ) ) )
205 54 203 204 syl2anc ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) < ( 𝑌 / ( 2 · π ) ) )
206 56 54 159 205 ltmul1dd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) · ( 2 · π ) ) < ( ( 𝑌 / ( 2 · π ) ) · ( 2 · π ) ) )
207 3 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
208 207 58 53 divcan1d ⊢ ( 𝜑 → ( ( 𝑌 / ( 2 · π ) ) · ( 2 · π ) ) = 𝑌 )
209 206 208 breqtrd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) · ( 2 · π ) ) < 𝑌 )
210 42 209 eqbrtrid ⊢ ( 𝜑 → 𝐶 < 𝑌 )
211 fllelt ⊢ ( ( 𝑌 / ( 2 · π ) ) ∈ ℝ → ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) ≤ ( 𝑌 / ( 2 · π ) ) ∧ ( 𝑌 / ( 2 · π ) ) < ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) + 1 ) ) )
212 54 211 syl ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) ≤ ( 𝑌 / ( 2 · π ) ) ∧ ( 𝑌 / ( 2 · π ) ) < ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) + 1 ) ) )
213 212 simprd ⊢ ( 𝜑 → ( 𝑌 / ( 2 · π ) ) < ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) + 1 ) )
214 54 77 159 213 ltmul1dd ⊢ ( 𝜑 → ( ( 𝑌 / ( 2 · π ) ) · ( 2 · π ) ) < ( ( ( ⌊ ‘ ( 𝑌 / ( 2 · π ) ) ) + 1 ) · ( 2 · π ) ) )
215 214 208 75 3brtr3d ⊢ ( 𝜑 → 𝑌 < 𝐸 )
216 68 80 3 210 215 eliood ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 (,) 𝐸 ) )
217 fveq2 ⊢ ( 𝑦 = 𝑌 → ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) = ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
218 217 eleq2d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ↔ ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) ) )
219 218 rspccva ⊢ ( ( ∀ 𝑦 ∈ ( 𝐶 (,) 𝐸 ) ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ∧ 𝑌 ∈ ( 𝐶 (,) 𝐸 ) ) → ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
220 199 216 219 syl2anc ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) )
221 178 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ Top )
222 1 dirkerf ⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
223 2 222 syl ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
224 223 29 fssresd ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) : ( 𝐶 (,) 𝐸 ) ⟶ ℝ )
225 ax-resscn ⊢ ℝ ⊆ ℂ
226 225 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
227 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
228 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
229 228 restuni ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐶 (,) 𝐸 ) ⊆ ℝ ) → ( 𝐶 (,) 𝐸 ) = ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) )
230 227 28 229 mp2an ⊢ ( 𝐶 (,) 𝐸 ) = ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) )
231 230 183 cnprest2 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) : ( 𝐶 (,) 𝐸 ) ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ( ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) ↔ ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ 𝑌 ) ) )
232 221 224 226 231 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑌 ) ↔ ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ 𝑌 ) ) )
233 220 232 mpbid ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ 𝑌 ) )
234 176 eqcomi ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) = ( topGen ‘ ran (,) )
235 234 a1i ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) = ( topGen ‘ ran (,) ) )
236 235 oveq2d ⊢ ( 𝜑 → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) = ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( topGen ‘ ran (,) ) ) )
237 236 fveq1d ⊢ ( 𝜑 → ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ‘ 𝑌 ) = ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) )
238 233 237 eleqtrd ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) )
239 227 a1i ⊢ ( 𝜑 → ( topGen ‘ ran (,) ) ∈ Top )
240 iooretop ⊢ ( 𝐶 (,) 𝐸 ) ∈ ( topGen ‘ ran (,) )
241 228 isopn3 ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐶 (,) 𝐸 ) ⊆ ℝ ) → ( ( 𝐶 (,) 𝐸 ) ∈ ( topGen ‘ ran (,) ) ↔ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐶 (,) 𝐸 ) ) = ( 𝐶 (,) 𝐸 ) ) )
242 240 241 mpbii ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐶 (,) 𝐸 ) ⊆ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐶 (,) 𝐸 ) ) = ( 𝐶 (,) 𝐸 ) )
243 239 29 242 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐶 (,) 𝐸 ) ) = ( 𝐶 (,) 𝐸 ) )
244 243 eqcomd ⊢ ( 𝜑 → ( 𝐶 (,) 𝐸 ) = ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐶 (,) 𝐸 ) ) )
245 216 244 eleqtrd ⊢ ( 𝜑 → 𝑌 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐶 (,) 𝐸 ) ) )
246 228 228 cnprest ⊢ ( ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐶 (,) 𝐸 ) ⊆ ℝ ) ∧ ( 𝑌 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐶 (,) 𝐸 ) ) ∧ ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ ) ) → ( ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) ↔ ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) ) )
247 239 29 245 223 246 syl22anc ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) ↔ ( ( 𝐷 ‘ 𝑁 ) ↾ ( 𝐶 (,) 𝐸 ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐶 (,) 𝐸 ) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) ) )
248 238 247 mpbird ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) ∈ ( ( ( topGen ‘ ran (,) ) CnP ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) )