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	eqtrid	⊢ ( 𝜑 → ( 𝐶 / ( 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 (,) ) ) ‘ 𝑌 ) )