dirkercncflem4 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dirkercncflem4		Structured version Visualization version GIF version

Theorem dirkercncflem4 46461

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.)

**Hypotheses**
Ref	Expression
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**
Ref	Expression
dirkercncflem4	⊢ (𝜑 → (𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP (topGen‘ran (,)))‘𝑌))

Distinct variable groups: 𝑦,𝐶 𝑦,𝐷 𝑦,𝐸 𝑦,𝑁 𝑦,𝑌 𝑦,𝑛 𝜑,𝑦 Allowed substitution hints: 𝜑(𝑛) 𝐴(𝑦,𝑛) 𝐵(𝑦,𝑛) 𝐶(𝑛) 𝐷(𝑛) 𝐸(𝑛) 𝑁(𝑛) 𝑌(𝑛)

Proof of Theorem dirkercncflem4 Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sincn 26422	. . . . . . . . . . 11 ⊢ sin ∈ (ℂ–cn→ℂ)
2	1	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → sin ∈ (ℂ–cn→ℂ))
3		ioosscn 13336	. . . . . . . . . . . . 13 ⊢ (𝐶(,)𝐸) ⊆ ℂ
4	3	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶(,)𝐸) ⊆ ℂ)
5		dirkercncflem4.n	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	nncnd 12173	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
7		1cnd 11139	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℂ)
8	7	halfcld 12398	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
9	6, 8	addcld 11163	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ)
10		ssid 3958	. . . . . . . . . . . . 13 ⊢ ℂ ⊆ ℂ
11	10	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ ⊆ ℂ)
12	4, 9, 11	constcncfg 46227	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑁 + (1 / 2))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
13	4, 11	idcncfg 46228	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ 𝑦) ∈ ((𝐶(,)𝐸)–cn→ℂ))
14	12, 13	mulcncf 25414	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
15	2, 14	cncfmpt1f 24875	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
16		2cnd 12235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ∈ ℂ)
17		pirp 26438	. . . . . . . . . . . . . . . 16 ⊢ π ∈ ℝ⁺
18	17	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ∈ ℝ⁺)
19	18	rpcnd 12963	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ∈ ℂ)
20	16, 19	mulcld 11164	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℂ)
21		ioossre 13335	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶(,)𝐸) ⊆ ℝ
22	21	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐶(,)𝐸) ⊆ ℝ)
23	22	sselda 3935	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 ∈ ℝ)
24	23	recnd 11172	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 ∈ ℂ)
25	24	halfcld 12398	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / 2) ∈ ℂ)
26	25	sincld 16067	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘(𝑦 / 2)) ∈ ℂ)
27	20, 26	mulcld 11164	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
28		2rp 12922	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ⁺
29	28	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ∈ ℝ⁺)
30	29	rpne0d 12966	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ≠ 0)
31	18	rpne0d 12966	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ≠ 0)
32	16, 19, 30, 31	mulne0d 11801	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ≠ 0)
33	24, 16, 19, 30, 31	divdiv1d 11960	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
34		dirkercncflem4.c	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐶 = (𝐴 · (2 · π))
35		dirkercncflem4.a	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐴 = (⌊‘(𝑌 / (2 · π)))
36	35	oveq1i 7378	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 · (2 · π)) = ((⌊‘(𝑌 / (2 · π))) · (2 · π))
37	34, 36	eqtri 2760	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐶 = ((⌊‘(𝑌 / (2 · π))) · (2 · π))
38	37	oveq1i 7378	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐶 / (2 · π)) = (((⌊‘(𝑌 / (2 · π))) · (2 · π)) / (2 · π))
39		dirkercncflem4.y	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑌 ∈ ℝ)
40		2re 12231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 2 ∈ ℝ
41		pire 26434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ π ∈ ℝ
42	40, 41	remulcli 11160	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (2 · π) ∈ ℝ
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (2 · π) ∈ ℝ)
44		0re 11146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 ∈ ℝ
45		2pos 12260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 < 2
46		pipos 26436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 < π
47	40, 41, 45, 46	mulgt0ii 11278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 < (2 · π)
48	44, 47	gtneii 11257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (2 · π) ≠ 0
49	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (2 · π) ≠ 0)
50	39, 43, 49	redivcld 11981	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑌 / (2 · π)) ∈ ℝ)
51	50	flcld 13730	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) ∈ ℤ)
52	51	zred 12608	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) ∈ ℝ)
53	52	recnd 11172	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) ∈ ℂ)
54	43	recnd 11172	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (2 · π) ∈ ℂ)
55	53, 54, 49	divcan4d 11935	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((⌊‘(𝑌 / (2 · π))) · (2 · π)) / (2 · π)) = (⌊‘(𝑌 / (2 · π))))
56	38, 55	eqtrid 2784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐶 / (2 · π)) = (⌊‘(𝑌 / (2 · π))))
57	56, 51	eqeltrd 2837	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐶 / (2 · π)) ∈ ℤ)
58	57	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝐶 / (2 · π)) ∈ ℤ)
59	52, 43	remulcld 11174	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) · (2 · π)) ∈ ℝ)
60	37, 59	eqeltrid 2841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ ℝ)
61	60	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐶 ∈ ℝ)
62	29, 18	rpmulcld 12977	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℝ⁺)
63		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 ∈ (𝐶(,)𝐸))
64	60	rexrd 11194	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
65	64	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐶 ∈ ℝ^*)
66	35	eqcomi 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⌊‘(𝑌 / (2 · π))) = 𝐴
67	66	oveq1i 7378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((⌊‘(𝑌 / (2 · π))) + 1) = (𝐴 + 1)
68		dirkercncflem4.b	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 𝐵 = (𝐴 + 1)
69	67, 68	eqtr4i 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((⌊‘(𝑌 / (2 · π))) + 1) = 𝐵
70	69	oveq1i 7378	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) = (𝐵 · (2 · π))
71		dirkercncflem4.e	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝐸 = (𝐵 · (2 · π))
72	70, 71	eqtr4i 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) = 𝐸
73	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) = 𝐸)
74		1red 11145	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 1 ∈ ℝ)
75	52, 74	readdcld 11173	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) + 1) ∈ ℝ)
76	75, 43	remulcld 11174	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) ∈ ℝ)
77	73, 76	eqeltrrd 2838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐸 ∈ ℝ)
78	77	rexrd 11194	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐸 ∈ ℝ^*)
79	78	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐸 ∈ ℝ^*)
80		elioo2 13314	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐸 ∈ ℝ^*) → (𝑦 ∈ (𝐶(,)𝐸) ↔ (𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸)))
81	65, 79, 80	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 ∈ (𝐶(,)𝐸) ↔ (𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸)))
82	63, 81	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸))
83	82	simp2d 1144	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐶 < 𝑦)
84	61, 23, 62, 83	ltdiv1dd 13018	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝐶 / (2 · π)) < (𝑦 / (2 · π)))
85	77	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐸 ∈ ℝ)
86	82	simp3d 1145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 < 𝐸)
87	23, 85, 62, 86	ltdiv1dd 13018	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / (2 · π)) < (𝐸 / (2 · π)))
88	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐶 = (𝐴 · (2 · π)))
89	88	oveq1d 7383	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐶 / (2 · π)) = ((𝐴 · (2 · π)) / (2 · π)))
90	89	oveq1d 7383	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝐶 / (2 · π)) + 1) = (((𝐴 · (2 · π)) / (2 · π)) + 1))
91	35, 53	eqeltrid 2841	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐴 ∈ ℂ)
92	91, 54, 49	divcan4d 11935	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 · (2 · π)) / (2 · π)) = 𝐴)
93	92	oveq1d 7383	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝐴 · (2 · π)) / (2 · π)) + 1) = (𝐴 + 1))
94	68	oveq1i 7378	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐵 · (2 · π)) = ((𝐴 + 1) · (2 · π))
95	71, 94	eqtri 2760	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐸 = ((𝐴 + 1) · (2 · π))
96	95	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐸 = ((𝐴 + 1) · (2 · π)))
97	96	oveq1d 7383	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐸 / (2 · π)) = (((𝐴 + 1) · (2 · π)) / (2 · π)))
98	91, 7	addcld 11163	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 + 1) ∈ ℂ)
99	98, 54, 49	divcan4d 11935	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴 + 1) · (2 · π)) / (2 · π)) = (𝐴 + 1))
100	97, 99	eqtr2d 2773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴 + 1) = (𝐸 / (2 · π)))
101	90, 93, 100	3eqtrrd 2777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 / (2 · π)) = ((𝐶 / (2 · π)) + 1))
102	101	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝐸 / (2 · π)) = ((𝐶 / (2 · π)) + 1))
103	87, 102	breqtrd 5126	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / (2 · π)) < ((𝐶 / (2 · π)) + 1))
104		btwnnz 12580	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶 / (2 · π)) ∈ ℤ ∧ (𝐶 / (2 · π)) < (𝑦 / (2 · π)) ∧ (𝑦 / (2 · π)) < ((𝐶 / (2 · π)) + 1)) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
105	58, 84, 103, 104	syl3anc 1374	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
106	33, 105	eqneltrd 2857	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ ((𝑦 / 2) / π) ∈ ℤ)
107		sineq0 26501	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 / 2) ∈ ℂ → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
108	25, 107	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
109	106, 108	mtbird 325	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ (sin‘(𝑦 / 2)) = 0)
110	109	neqned 2940	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘(𝑦 / 2)) ≠ 0)
111	20, 26, 32, 110	mulne0d 11801	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ≠ 0)
112	111	neneqd 2938	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ ((2 · π) · (sin‘(𝑦 / 2))) = 0)
113	40	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ∈ ℝ)
114	41	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ∈ ℝ)
115	113, 114	remulcld 11174	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℝ)
116	23	rehalfcld 12400	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / 2) ∈ ℝ)
117	116	resincld 16080	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘(𝑦 / 2)) ∈ ℝ)
118	115, 117	remulcld 11174	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℝ)
119		elsng 4596	. . . . . . . . . . . . . 14 ⊢ (((2 · π) · (sin‘(𝑦 / 2))) ∈ ℝ → (((2 · π) · (sin‘(𝑦 / 2))) ∈ {0} ↔ ((2 · π) · (sin‘(𝑦 / 2))) = 0))
120	118, 119	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (((2 · π) · (sin‘(𝑦 / 2))) ∈ {0} ↔ ((2 · π) · (sin‘(𝑦 / 2))) = 0))
121	112, 120	mtbird 325	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ ((2 · π) · (sin‘(𝑦 / 2))) ∈ {0})
122	27, 121	eldifd 3914	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ (ℂ ∖ {0}))
123		eqidd 2738	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))))
124		eqidd 2738	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)))
125		oveq2 7376	. . . . . . . . . . 11 ⊢ (𝑥 = ((2 · π) · (sin‘(𝑦 / 2))) → (1 / 𝑥) = (1 / ((2 · π) · (sin‘(𝑦 / 2)))))
126	122, 123, 124, 125	fmptco 7084	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∘ (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ (𝐶(,)𝐸) ↦ (1 / ((2 · π) · (sin‘(𝑦 / 2))))))
127		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
128		2cnd 12235	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℂ)
129	4, 128, 11	constcncfg 46227	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ 2) ∈ ((𝐶(,)𝐸)–cn→ℂ))
130	17	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → π ∈ ℝ⁺)
131	130	rpcnd 12963	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → π ∈ ℂ)
132	4, 131, 11	constcncfg 46227	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ π) ∈ ((𝐶(,)𝐸)–cn→ℂ))
133	129, 132	mulcncf 25414	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (2 · π)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
134	24, 16, 30	divrecd 11932	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / 2) = (𝑦 · (1 / 2)))
135	134	mpteq2dva 5193	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 / 2)) = (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 · (1 / 2))))
136	4, 8, 11	constcncfg 46227	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (1 / 2)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
137	13, 136	mulcncf 25414	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 · (1 / 2))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
138	135, 137	eqeltrd 2837	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 / 2)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
139	2, 138	cncfmpt1f 24875	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (sin‘(𝑦 / 2))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
140	133, 139	mulcncf 25414	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
141		ssid 3958	. . . . . . . . . . . . 13 ⊢ (𝐶(,)𝐸) ⊆ (𝐶(,)𝐸)
142	141	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶(,)𝐸) ⊆ (𝐶(,)𝐸))
143		difssd 4091	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
144	127, 140, 142, 143, 122	cncfmptssg 46226	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ∈ ((𝐶(,)𝐸)–cn→(ℂ ∖ {0})))
145		ax-1cn 11096	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
146		eqid 2737	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥))
147	146	cdivcncf 24882	. . . . . . . . . . . 12 ⊢ (1 ∈ ℂ → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∈ ((ℂ ∖ {0})–cn→ℂ))
148	145, 147	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∈ ((ℂ ∖ {0})–cn→ℂ))
149	144, 148	cncfco 24868	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∘ (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
150	126, 149	eqeltrrd 2838	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (1 / ((2 · π) · (sin‘(𝑦 / 2))))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
151	15, 150	mulcncf 25414	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2)))))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
152		dirkercncflem4.d	. . . . . . . . . . . 12 ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
153	152	dirkerval 46446	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) = (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
154	5, 153	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷‘𝑁) = (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
155	154	reseq1d 5945	. . . . . . . . 9 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) = ((𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) ↾ (𝐶(,)𝐸)))
156	22	resmptd 6007	. . . . . . . . 9 ⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ 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)))))))
157	28	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 2 ∈ ℝ⁺)
158	157, 130	rpmulcld 12977	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · π) ∈ ℝ⁺)
159	158	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℝ⁺)
160		mod0 13808	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℝ ∧ (2 · π) ∈ ℝ⁺) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
161	23, 159, 160	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
162	105, 161	mtbird 325	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ (𝑦 mod (2 · π)) = 0)
163	162	iffalsed 4492	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
164	6	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑁 ∈ ℂ)
165		1cnd 11139	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 1 ∈ ℂ)
166	165	halfcld 12398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (1 / 2) ∈ ℂ)
167	164, 166	addcld 11163	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑁 + (1 / 2)) ∈ ℂ)
168	167, 24	mulcld 11164	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
169	168	sincld 16067	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
170	169, 27, 111	divrecd 11932	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2))))))
171	163, 170	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2))))))
172	171	mpteq2dva 5193	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) = (𝑦 ∈ (𝐶(,)𝐸) ↦ ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2)))))))
173	155, 156, 172	3eqtrrd 2777	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2)))))) = ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)))
174		eqid 2737	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
175		tgioo4 24761	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
176	175	oveq1i 7378	. . . . . . . . . . 11 ⊢ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) = (((TopOpen‘ℂ_fld) ↾_t ℝ) ↾_t (𝐶(,)𝐸))
177	174	cnfldtop 24739	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) ∈ Top
178		reex 11129	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
179		restabs 23121	. . . . . . . . . . . 12 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ (𝐶(,)𝐸) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂ_fld) ↾_t ℝ) ↾_t (𝐶(,)𝐸)) = ((TopOpen‘ℂ_fld) ↾_t (𝐶(,)𝐸)))
180	177, 21, 178, 179	mp3an 1464	. . . . . . . . . . 11 ⊢ (((TopOpen‘ℂ_fld) ↾_t ℝ) ↾_t (𝐶(,)𝐸)) = ((TopOpen‘ℂ_fld) ↾_t (𝐶(,)𝐸))
181	176, 180	eqtri 2760	. . . . . . . . . 10 ⊢ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) = ((TopOpen‘ℂ_fld) ↾_t (𝐶(,)𝐸))
182		unicntop 24741	. . . . . . . . . . . . 13 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
183	182	restid 17365	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ∈ Top → ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld))
184	177, 183	ax-mp 5	. . . . . . . . . . 11 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld)
185	184	eqcomi 2746	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
186	174, 181, 185	cncfcn 24871	. . . . . . . . 9 ⊢ (((𝐶(,)𝐸) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐶(,)𝐸)–cn→ℂ) = (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) Cn (TopOpen‘ℂ_fld)))
187	4, 11, 186	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → ((𝐶(,)𝐸)–cn→ℂ) = (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) Cn (TopOpen‘ℂ_fld)))
188	151, 173, 187	3eltr3d 2851	. . . . . . 7 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) Cn (TopOpen‘ℂ_fld)))
189		retopon 24719	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
190	189	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (topGen‘ran (,)) ∈ (TopOn‘ℝ))
191		resttopon 23117	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (𝐶(,)𝐸) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) ∈ (TopOn‘(𝐶(,)𝐸)))
192	190, 22, 191	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) ∈ (TopOn‘(𝐶(,)𝐸)))
193	174	cnfldtopon 24738	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
194	193	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
195		cncnp 23236	. . . . . . . 8 ⊢ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) ∈ (TopOn‘(𝐶(,)𝐸)) ∧ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)) → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) Cn (TopOpen‘ℂ_fld)) ↔ (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)):(𝐶(,)𝐸)⟶ℂ ∧ ∀𝑦 ∈ (𝐶(,)𝐸)((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦))))
196	192, 194, 195	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) Cn (TopOpen‘ℂ_fld)) ↔ (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)):(𝐶(,)𝐸)⟶ℂ ∧ ∀𝑦 ∈ (𝐶(,)𝐸)((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦))))
197	188, 196	mpbid 232	. . . . . 6 ⊢ (𝜑 → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)):(𝐶(,)𝐸)⟶ℂ ∧ ∀𝑦 ∈ (𝐶(,)𝐸)((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦)))
198	197	simprd 495	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ (𝐶(,)𝐸)((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦))
199		dirkercncflem4.ymod0	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 mod (2 · π)) ≠ 0)
200	199	neneqd 2938	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝑌 mod (2 · π)) = 0)
201		mod0 13808	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ ℝ ∧ (2 · π) ∈ ℝ⁺) → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
202	39, 158, 201	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
203	200, 202	mtbid 324	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝑌 / (2 · π)) ∈ ℤ)
204		flltnz 13743	. . . . . . . . . 10 ⊢ (((𝑌 / (2 · π)) ∈ ℝ ∧ ¬ (𝑌 / (2 · π)) ∈ ℤ) → (⌊‘(𝑌 / (2 · π))) < (𝑌 / (2 · π)))
205	50, 203, 204	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) < (𝑌 / (2 · π)))
206	52, 50, 158, 205	ltmul1dd 13016	. . . . . . . 8 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) · (2 · π)) < ((𝑌 / (2 · π)) · (2 · π)))
207	39	recnd 11172	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ ℂ)
208	207, 54, 49	divcan1d 11930	. . . . . . . 8 ⊢ (𝜑 → ((𝑌 / (2 · π)) · (2 · π)) = 𝑌)
209	206, 208	breqtrd 5126	. . . . . . 7 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) · (2 · π)) < 𝑌)
210	37, 209	eqbrtrid 5135	. . . . . 6 ⊢ (𝜑 → 𝐶 < 𝑌)
211		fllelt 13729	. . . . . . . . . 10 ⊢ ((𝑌 / (2 · π)) ∈ ℝ → ((⌊‘(𝑌 / (2 · π))) ≤ (𝑌 / (2 · π)) ∧ (𝑌 / (2 · π)) < ((⌊‘(𝑌 / (2 · π))) + 1)))
212	50, 211	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) ≤ (𝑌 / (2 · π)) ∧ (𝑌 / (2 · π)) < ((⌊‘(𝑌 / (2 · π))) + 1)))
213	212	simprd 495	. . . . . . . 8 ⊢ (𝜑 → (𝑌 / (2 · π)) < ((⌊‘(𝑌 / (2 · π))) + 1))
214	50, 75, 158, 213	ltmul1dd 13016	. . . . . . 7 ⊢ (𝜑 → ((𝑌 / (2 · π)) · (2 · π)) < (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)))
215	214, 208, 73	3brtr3d 5131	. . . . . 6 ⊢ (𝜑 → 𝑌 < 𝐸)
216	64, 78, 39, 210, 215	eliood 45855	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ (𝐶(,)𝐸))
217		fveq2 6842	. . . . . . 7 ⊢ (𝑦 = 𝑌 → ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦) = ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌))
218	217	eleq2d 2823	. . . . . 6 ⊢ (𝑦 = 𝑌 → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦) ↔ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌)))
219	218	rspccva 3577	. . . . 5 ⊢ ((∀𝑦 ∈ (𝐶(,)𝐸)((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦) ∧ 𝑌 ∈ (𝐶(,)𝐸)) → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌))
220	198, 216, 219	syl2anc 585	. . . 4 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌))
221	177	a1i 11	. . . . 5 ⊢ (𝜑 → (TopOpen‘ℂ_fld) ∈ Top)
222	152	dirkerf 46452	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁):ℝ⟶ℝ)
223	5, 222	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐷‘𝑁):ℝ⟶ℝ)
224	223, 22	fssresd 6709	. . . . 5 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)):(𝐶(,)𝐸)⟶ℝ)
225		ax-resscn 11095	. . . . . 6 ⊢ ℝ ⊆ ℂ
226	225	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ⊆ ℂ)
227		retop 24717	. . . . . . 7 ⊢ (topGen‘ran (,)) ∈ Top
228		uniretop 24718	. . . . . . . 8 ⊢ ℝ = ∪ (topGen‘ran (,))
229	228	restuni 23118	. . . . . . 7 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐶(,)𝐸) ⊆ ℝ) → (𝐶(,)𝐸) = ∪ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)))
230	227, 21, 229	mp2an 693	. . . . . 6 ⊢ (𝐶(,)𝐸) = ∪ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸))
231	230, 182	cnprest2 23246	. . . . 5 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)):(𝐶(,)𝐸)⟶ℝ ∧ ℝ ⊆ ℂ) → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌) ↔ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ))‘𝑌)))
232	221, 224, 226, 231	syl3anc 1374	. . . 4 ⊢ (𝜑 → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌) ↔ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ))‘𝑌)))
233	220, 232	mpbid 232	. . 3 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ))‘𝑌))
234	175	eqcomi 2746	. . . . . 6 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℝ) = (topGen‘ran (,))
235	234	a1i 11	. . . . 5 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t ℝ) = (topGen‘ran (,)))
236	235	oveq2d 7384	. . . 4 ⊢ (𝜑 → (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ)) = (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,))))
237	236	fveq1d 6844	. . 3 ⊢ (𝜑 → ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ))‘𝑌) = ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,)))‘𝑌))
238	233, 237	eleqtrd 2839	. 2 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,)))‘𝑌))
239	227	a1i 11	. . 3 ⊢ (𝜑 → (topGen‘ran (,)) ∈ Top)
240		iooretop 24721	. . . . . . 7 ⊢ (𝐶(,)𝐸) ∈ (topGen‘ran (,))
241	228	isopn3 23022	. . . . . . 7 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐶(,)𝐸) ⊆ ℝ) → ((𝐶(,)𝐸) ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)) = (𝐶(,)𝐸)))
242	240, 241	mpbii 233	. . . . . 6 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐶(,)𝐸) ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)) = (𝐶(,)𝐸))
243	239, 22, 242	syl2anc 585	. . . . 5 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)) = (𝐶(,)𝐸))
244	243	eqcomd 2743	. . . 4 ⊢ (𝜑 → (𝐶(,)𝐸) = ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)))
245	216, 244	eleqtrd 2839	. . 3 ⊢ (𝜑 → 𝑌 ∈ ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)))
246	228, 228	cnprest 23245	. . 3 ⊢ ((((topGen‘ran (,)) ∈ Top ∧ (𝐶(,)𝐸) ⊆ ℝ) ∧ (𝑌 ∈ ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)) ∧ (𝐷‘𝑁):ℝ⟶ℝ)) → ((𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP (topGen‘ran (,)))‘𝑌) ↔ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,)))‘𝑌)))
247	239, 22, 245, 223, 246	syl22anc 839	. 2 ⊢ (𝜑 → ((𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP (topGen‘ran (,)))‘𝑌) ↔ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,)))‘𝑌)))
248	238, 247	mpbird 257	1 ⊢ (𝜑 → (𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP (topGen‘ran (,)))‘𝑌))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 Vcvv 3442 ∖ cdif 3900 ⊆ wss 3903 ifcif 4481 {csn 4582 ∪ cuni 4865 class class class wbr 5100 ↦ cmpt 5181 ran crn 5633 ↾ cres 5634 ∘ ccom 5636 ⟶wf 6496 ‘cfv 6500 (class class class)co 7368 ℂcc 11036 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 ℝ^*cxr 11177 < clt 11178 ≤ cle 11179 / cdiv 11806 ℕcn 12157 2c2 12212 ℤcz 12500 ℝ⁺crp 12917 (,)cioo 13273 ⌊cfl 13722 mod cmo 13801 sincsin 15998 πcpi 16001 ↾_t crest 17352 TopOpenctopn 17353 topGenctg 17369 ℂ_fldccnfld 21321 Topctop 22849 TopOnctopon 22866 intcnt 22973 Cn ccn 23180 CnP ccnp 23181 –cn→ccncf 24837

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-inf2 9562 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116 ax-addf 11117

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-iin 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-se 5586 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-isom 6509 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-of 7632 df-om 7819 df-1st 7943 df-2nd 7944 df-supp 8113 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-2o 8408 df-er 8645 df-map 8777 df-pm 8778 df-ixp 8848 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9277 df-fi 9326 df-sup 9357 df-inf 9358 df-oi 9427 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-4 12222 df-5 12223 df-6 12224 df-7 12225 df-8 12226 df-9 12227 df-n0 12414 df-z 12501 df-dec 12620 df-uz 12764 df-q 12874 df-rp 12918 df-xneg 13038 df-xadd 13039 df-xmul 13040 df-ioo 13277 df-ioc 13278 df-ico 13279 df-icc 13280 df-fz 13436 df-fzo 13583 df-fl 13724 df-mod 13802 df-seq 13937 df-exp 13997 df-fac 14209 df-bc 14238 df-hash 14266 df-shft 15002 df-cj 15034 df-re 15035 df-im 15036 df-sqrt 15170 df-abs 15171 df-limsup 15406 df-clim 15423 df-rlim 15424 df-sum 15622 df-ef 16002 df-sin 16004 df-cos 16005 df-pi 16007 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17149 df-ress 17170 df-plusg 17202 df-mulr 17203 df-starv 17204 df-sca 17205 df-vsca 17206 df-ip 17207 df-tset 17208 df-ple 17209 df-ds 17211 df-unif 17212 df-hom 17213 df-cco 17214 df-rest 17354 df-topn 17355 df-0g 17373 df-gsum 17374 df-topgen 17375 df-pt 17376 df-prds 17379 df-xrs 17435 df-qtop 17440 df-imas 17441 df-xps 17443 df-mre 17517 df-mrc 17518 df-acs 17520 df-mgm 18577 df-sgrp 18656 df-mnd 18672 df-submnd 18721 df-mulg 19010 df-cntz 19258 df-cmn 19723 df-psmet 21313 df-xmet 21314 df-met 21315 df-bl 21316 df-mopn 21317 df-fbas 21318 df-fg 21319 df-cnfld 21322 df-top 22850 df-topon 22867 df-topsp 22889 df-bases 22902 df-cld 22975 df-ntr 22976 df-cls 22977 df-nei 23054 df-lp 23092 df-perf 23093 df-cn 23183 df-cnp 23184 df-haus 23271 df-tx 23518 df-hmeo 23711 df-fil 23802 df-fm 23894 df-flim 23895 df-flf 23896 df-xms 24276 df-ms 24277 df-tms 24278 df-cncf 24839 df-limc 25835 df-dv 25836

This theorem is referenced by: dirkercncf 46462

W3C validator