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	$⊢ D = (n \in ℕ ⟼ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})))$
	dirkercncflem4.n	$⊢ φ \to N \in ℕ$
	dirkercncflem4.y	$⊢ φ \to Y \in ℝ$
	dirkercncflem4.ymod0	$⊢ φ \to Y \mod 2 π \neq 0$
	dirkercncflem4.a	$⊢ A = ⌊\frac{Y}{2 π}⌋$
	dirkercncflem4.b	$⊢ B = A + 1$
	dirkercncflem4.c	$⊢ C = A 2 π$
	dirkercncflem4.e	$⊢ E = B 2 π$
Assertion	dirkercncflem4	$⊢ φ \to D (N) \in (topGen (ran (.)) CnP topGen (ran (.))) (Y)$

Proof

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

Metamath Proof Explorer

Theorem dirkercncflem4

Proof