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 46121

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 26488	. . . . . . . . . . 11 ⊢ sin ∈ (ℂ–cn→ℂ)
2	1	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → sin ∈ (ℂ–cn→ℂ))
3		ioosscn 13449	. . . . . . . . . . . . 13 ⊢ (𝐶(,)𝐸) ⊆ ℂ
4	3	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶(,)𝐸) ⊆ ℂ)
5		dirkercncflem4.n	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	nncnd 12282	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
7		1cnd 11256	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℂ)
8	7	halfcld 12511	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
9	6, 8	addcld 11280	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ)
10		ssid 4006	. . . . . . . . . . . . 13 ⊢ ℂ ⊆ ℂ
11	10	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ ⊆ ℂ)
12	4, 9, 11	constcncfg 45887	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑁 + (1 / 2))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
13	4, 11	idcncfg 45888	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ 𝑦) ∈ ((𝐶(,)𝐸)–cn→ℂ))
14	12, 13	mulcncf 25480	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
15	2, 14	cncfmpt1f 24940	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
16		2cnd 12344	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ∈ ℂ)
17		pirp 26503	. . . . . . . . . . . . . . . 16 ⊢ π ∈ ℝ⁺
18	17	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ∈ ℝ⁺)
19	18	rpcnd 13079	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ∈ ℂ)
20	16, 19	mulcld 11281	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℂ)
21		ioossre 13448	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶(,)𝐸) ⊆ ℝ
22	21	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐶(,)𝐸) ⊆ ℝ)
23	22	sselda 3983	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 ∈ ℝ)
24	23	recnd 11289	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 ∈ ℂ)
25	24	halfcld 12511	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / 2) ∈ ℂ)
26	25	sincld 16166	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘(𝑦 / 2)) ∈ ℂ)
27	20, 26	mulcld 11281	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
28		2rp 13039	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ⁺
29	28	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ∈ ℝ⁺)
30	29	rpne0d 13082	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ≠ 0)
31	18	rpne0d 13082	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ≠ 0)
32	16, 19, 30, 31	mulne0d 11915	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ≠ 0)
33	24, 16, 19, 30, 31	divdiv1d 12074	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
34		dirkercncflem4.c	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐶 = (𝐴 · (2 · π))
35		dirkercncflem4.a	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐴 = (⌊‘(𝑌 / (2 · π)))
36	35	oveq1i 7441	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 · (2 · π)) = ((⌊‘(𝑌 / (2 · π))) · (2 · π))
37	34, 36	eqtri 2765	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐶 = ((⌊‘(𝑌 / (2 · π))) · (2 · π))
38	37	oveq1i 7441	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐶 / (2 · π)) = (((⌊‘(𝑌 / (2 · π))) · (2 · π)) / (2 · π))
39		dirkercncflem4.y	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑌 ∈ ℝ)
40		2re 12340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 2 ∈ ℝ
41		pire 26500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ π ∈ ℝ
42	40, 41	remulcli 11277	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (2 · π) ∈ ℝ
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (2 · π) ∈ ℝ)
44		0re 11263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 ∈ ℝ
45		2pos 12369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 < 2
46		pipos 26502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 < π
47	40, 41, 45, 46	mulgt0ii 11394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 < (2 · π)
48	44, 47	gtneii 11373	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (2 · π) ≠ 0
49	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (2 · π) ≠ 0)
50	39, 43, 49	redivcld 12095	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑌 / (2 · π)) ∈ ℝ)
51	50	flcld 13838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) ∈ ℤ)
52	51	zred 12722	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) ∈ ℝ)
53	52	recnd 11289	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) ∈ ℂ)
54	43	recnd 11289	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (2 · π) ∈ ℂ)
55	53, 54, 49	divcan4d 12049	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((⌊‘(𝑌 / (2 · π))) · (2 · π)) / (2 · π)) = (⌊‘(𝑌 / (2 · π))))
56	38, 55	eqtrid 2789	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐶 / (2 · π)) = (⌊‘(𝑌 / (2 · π))))
57	56, 51	eqeltrd 2841	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐶 / (2 · π)) ∈ ℤ)
58	57	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝐶 / (2 · π)) ∈ ℤ)
59	52, 43	remulcld 11291	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) · (2 · π)) ∈ ℝ)
60	37, 59	eqeltrid 2845	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ ℝ)
61	60	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐶 ∈ ℝ)
62	29, 18	rpmulcld 13093	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℝ⁺)
63		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 ∈ (𝐶(,)𝐸))
64	60	rexrd 11311	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
65	64	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐶 ∈ ℝ^*)
66	35	eqcomi 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⌊‘(𝑌 / (2 · π))) = 𝐴
67	66	oveq1i 7441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((⌊‘(𝑌 / (2 · π))) + 1) = (𝐴 + 1)
68		dirkercncflem4.b	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 𝐵 = (𝐴 + 1)
69	67, 68	eqtr4i 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((⌊‘(𝑌 / (2 · π))) + 1) = 𝐵
70	69	oveq1i 7441	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) = (𝐵 · (2 · π))
71		dirkercncflem4.e	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝐸 = (𝐵 · (2 · π))
72	70, 71	eqtr4i 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) = 𝐸
73	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) = 𝐸)
74		1red 11262	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 1 ∈ ℝ)
75	52, 74	readdcld 11290	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) + 1) ∈ ℝ)
76	75, 43	remulcld 11291	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) ∈ ℝ)
77	73, 76	eqeltrrd 2842	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐸 ∈ ℝ)
78	77	rexrd 11311	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐸 ∈ ℝ^*)
79	78	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐸 ∈ ℝ^*)
80		elioo2 13428	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐸 ∈ ℝ^*) → (𝑦 ∈ (𝐶(,)𝐸) ↔ (𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸)))
81	65, 79, 80	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 ∈ (𝐶(,)𝐸) ↔ (𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸)))
82	63, 81	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸))
83	82	simp2d 1144	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐶 < 𝑦)
84	61, 23, 62, 83	ltdiv1dd 13134	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝐶 / (2 · π)) < (𝑦 / (2 · π)))
85	77	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐸 ∈ ℝ)
86	82	simp3d 1145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 < 𝐸)
87	23, 85, 62, 86	ltdiv1dd 13134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / (2 · π)) < (𝐸 / (2 · π)))
88	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐶 = (𝐴 · (2 · π)))
89	88	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐶 / (2 · π)) = ((𝐴 · (2 · π)) / (2 · π)))
90	89	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝐶 / (2 · π)) + 1) = (((𝐴 · (2 · π)) / (2 · π)) + 1))
91	35, 53	eqeltrid 2845	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐴 ∈ ℂ)
92	91, 54, 49	divcan4d 12049	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 · (2 · π)) / (2 · π)) = 𝐴)
93	92	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝐴 · (2 · π)) / (2 · π)) + 1) = (𝐴 + 1))
94	68	oveq1i 7441	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐵 · (2 · π)) = ((𝐴 + 1) · (2 · π))
95	71, 94	eqtri 2765	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐸 = ((𝐴 + 1) · (2 · π))
96	95	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐸 = ((𝐴 + 1) · (2 · π)))
97	96	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐸 / (2 · π)) = (((𝐴 + 1) · (2 · π)) / (2 · π)))
98	91, 7	addcld 11280	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 + 1) ∈ ℂ)
99	98, 54, 49	divcan4d 12049	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴 + 1) · (2 · π)) / (2 · π)) = (𝐴 + 1))
100	97, 99	eqtr2d 2778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴 + 1) = (𝐸 / (2 · π)))
101	90, 93, 100	3eqtrrd 2782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 / (2 · π)) = ((𝐶 / (2 · π)) + 1))
102	101	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝐸 / (2 · π)) = ((𝐶 / (2 · π)) + 1))
103	87, 102	breqtrd 5169	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / (2 · π)) < ((𝐶 / (2 · π)) + 1))
104		btwnnz 12694	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶 / (2 · π)) ∈ ℤ ∧ (𝐶 / (2 · π)) < (𝑦 / (2 · π)) ∧ (𝑦 / (2 · π)) < ((𝐶 / (2 · π)) + 1)) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
105	58, 84, 103, 104	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
106	33, 105	eqneltrd 2861	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ ((𝑦 / 2) / π) ∈ ℤ)
107		sineq0 26566	. . . . . . . . . . . . . . . . . 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 2947	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘(𝑦 / 2)) ≠ 0)
111	20, 26, 32, 110	mulne0d 11915	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ≠ 0)
112	111	neneqd 2945	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ ((2 · π) · (sin‘(𝑦 / 2))) = 0)
113	40	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ∈ ℝ)
114	41	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ∈ ℝ)
115	113, 114	remulcld 11291	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℝ)
116	23	rehalfcld 12513	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / 2) ∈ ℝ)
117	116	resincld 16179	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘(𝑦 / 2)) ∈ ℝ)
118	115, 117	remulcld 11291	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℝ)
119		elsng 4640	. . . . . . . . . . . . . 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 3962	. . . . . . . . . . 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 7439	. . . . . . . . . . 11 ⊢ (𝑥 = ((2 · π) · (sin‘(𝑦 / 2))) → (1 / 𝑥) = (1 / ((2 · π) · (sin‘(𝑦 / 2)))))
126	122, 123, 124, 125	fmptco 7149	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∘ (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ (𝐶(,)𝐸) ↦ (1 / ((2 · π) · (sin‘(𝑦 / 2))))))
127		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
128		2cnd 12344	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℂ)
129	4, 128, 11	constcncfg 45887	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ 2) ∈ ((𝐶(,)𝐸)–cn→ℂ))
130	17	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → π ∈ ℝ⁺)
131	130	rpcnd 13079	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → π ∈ ℂ)
132	4, 131, 11	constcncfg 45887	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ π) ∈ ((𝐶(,)𝐸)–cn→ℂ))
133	129, 132	mulcncf 25480	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (2 · π)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
134	24, 16, 30	divrecd 12046	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / 2) = (𝑦 · (1 / 2)))
135	134	mpteq2dva 5242	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 / 2)) = (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 · (1 / 2))))
136	4, 8, 11	constcncfg 45887	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (1 / 2)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
137	13, 136	mulcncf 25480	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 · (1 / 2))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
138	135, 137	eqeltrd 2841	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 / 2)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
139	2, 138	cncfmpt1f 24940	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (sin‘(𝑦 / 2))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
140	133, 139	mulcncf 25480	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
141		ssid 4006	. . . . . . . . . . . . 13 ⊢ (𝐶(,)𝐸) ⊆ (𝐶(,)𝐸)
142	141	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶(,)𝐸) ⊆ (𝐶(,)𝐸))
143		difssd 4137	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
144	127, 140, 142, 143, 122	cncfmptssg 45886	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ∈ ((𝐶(,)𝐸)–cn→(ℂ ∖ {0})))
145		ax-1cn 11213	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
146		eqid 2737	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥))
147	146	cdivcncf 24947	. . . . . . . . . . . 12 ⊢ (1 ∈ ℂ → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∈ ((ℂ ∖ {0})–cn→ℂ))
148	145, 147	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∈ ((ℂ ∖ {0})–cn→ℂ))
149	144, 148	cncfco 24933	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∘ (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
150	126, 149	eqeltrrd 2842	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (1 / ((2 · π) · (sin‘(𝑦 / 2))))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
151	15, 150	mulcncf 25480	. . . . . . . 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 46106	. . . . . . . . . . 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 5996	. . . . . . . . 9 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) = ((𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) ↾ (𝐶(,)𝐸)))
156	22	resmptd 6058	. . . . . . . . 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 13093	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · π) ∈ ℝ⁺)
159	158	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℝ⁺)
160		mod0 13916	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℝ ∧ (2 · π) ∈ ℝ⁺) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
161	23, 159, 160	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
162	105, 161	mtbird 325	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ (𝑦 mod (2 · π)) = 0)
163	162	iffalsed 4536	. . . . . . . . . . 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 11256	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 1 ∈ ℂ)
166	165	halfcld 12511	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (1 / 2) ∈ ℂ)
167	164, 166	addcld 11280	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑁 + (1 / 2)) ∈ ℂ)
168	167, 24	mulcld 11281	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
169	168	sincld 16166	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
170	169, 27, 111	divrecd 12046	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2))))))
171	163, 170	eqtrd 2777	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2))))))
172	171	mpteq2dva 5242	. . . . . . . . 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 2782	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2)))))) = ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)))
174		eqid 2737	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
175		tgioo4 24826	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
176	175	oveq1i 7441	. . . . . . . . . . 11 ⊢ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) = (((TopOpen‘ℂ_fld) ↾_t ℝ) ↾_t (𝐶(,)𝐸))
177	174	cnfldtop 24804	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) ∈ Top
178		reex 11246	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
179		restabs 23173	. . . . . . . . . . . 12 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ (𝐶(,)𝐸) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂ_fld) ↾_t ℝ) ↾_t (𝐶(,)𝐸)) = ((TopOpen‘ℂ_fld) ↾_t (𝐶(,)𝐸)))
180	177, 21, 178, 179	mp3an 1463	. . . . . . . . . . 11 ⊢ (((TopOpen‘ℂ_fld) ↾_t ℝ) ↾_t (𝐶(,)𝐸)) = ((TopOpen‘ℂ_fld) ↾_t (𝐶(,)𝐸))
181	176, 180	eqtri 2765	. . . . . . . . . 10 ⊢ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) = ((TopOpen‘ℂ_fld) ↾_t (𝐶(,)𝐸))
182		unicntop 24806	. . . . . . . . . . . . 13 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
183	182	restid 17478	. . . . . . . . . . . 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 24936	. . . . . . . . 9 ⊢ (((𝐶(,)𝐸) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐶(,)𝐸)–cn→ℂ) = (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) Cn (TopOpen‘ℂ_fld)))
187	4, 11, 186	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → ((𝐶(,)𝐸)–cn→ℂ) = (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) Cn (TopOpen‘ℂ_fld)))
188	151, 173, 187	3eltr3d 2855	. . . . . . 7 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) Cn (TopOpen‘ℂ_fld)))
189		retopon 24784	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
190	189	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (topGen‘ran (,)) ∈ (TopOn‘ℝ))
191		resttopon 23169	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (𝐶(,)𝐸) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) ∈ (TopOn‘(𝐶(,)𝐸)))
192	190, 22, 191	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) ∈ (TopOn‘(𝐶(,)𝐸)))
193	174	cnfldtopon 24803	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
194	193	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
195		cncnp 23288	. . . . . . . 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 584	. . . . . . 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 2945	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝑌 mod (2 · π)) = 0)
201		mod0 13916	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ ℝ ∧ (2 · π) ∈ ℝ⁺) → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
202	39, 158, 201	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
203	200, 202	mtbid 324	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝑌 / (2 · π)) ∈ ℤ)
204		flltnz 13851	. . . . . . . . . 10 ⊢ (((𝑌 / (2 · π)) ∈ ℝ ∧ ¬ (𝑌 / (2 · π)) ∈ ℤ) → (⌊‘(𝑌 / (2 · π))) < (𝑌 / (2 · π)))
205	50, 203, 204	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) < (𝑌 / (2 · π)))
206	52, 50, 158, 205	ltmul1dd 13132	. . . . . . . 8 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) · (2 · π)) < ((𝑌 / (2 · π)) · (2 · π)))
207	39	recnd 11289	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ ℂ)
208	207, 54, 49	divcan1d 12044	. . . . . . . 8 ⊢ (𝜑 → ((𝑌 / (2 · π)) · (2 · π)) = 𝑌)
209	206, 208	breqtrd 5169	. . . . . . 7 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) · (2 · π)) < 𝑌)
210	37, 209	eqbrtrid 5178	. . . . . 6 ⊢ (𝜑 → 𝐶 < 𝑌)
211		fllelt 13837	. . . . . . . . . 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 13132	. . . . . . 7 ⊢ (𝜑 → ((𝑌 / (2 · π)) · (2 · π)) < (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)))
215	214, 208, 73	3brtr3d 5174	. . . . . 6 ⊢ (𝜑 → 𝑌 < 𝐸)
216	64, 78, 39, 210, 215	eliood 45511	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ (𝐶(,)𝐸))
217		fveq2 6906	. . . . . . 7 ⊢ (𝑦 = 𝑌 → ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦) = ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌))
218	217	eleq2d 2827	. . . . . 6 ⊢ (𝑦 = 𝑌 → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦) ↔ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌)))
219	218	rspccva 3621	. . . . 5 ⊢ ((∀𝑦 ∈ (𝐶(,)𝐸)((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦) ∧ 𝑌 ∈ (𝐶(,)𝐸)) → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌))
220	198, 216, 219	syl2anc 584	. . . 4 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌))
221	177	a1i 11	. . . . 5 ⊢ (𝜑 → (TopOpen‘ℂ_fld) ∈ Top)
222	152	dirkerf 46112	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁):ℝ⟶ℝ)
223	5, 222	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐷‘𝑁):ℝ⟶ℝ)
224	223, 22	fssresd 6775	. . . . 5 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)):(𝐶(,)𝐸)⟶ℝ)
225		ax-resscn 11212	. . . . . 6 ⊢ ℝ ⊆ ℂ
226	225	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ⊆ ℂ)
227		retop 24782	. . . . . . 7 ⊢ (topGen‘ran (,)) ∈ Top
228		uniretop 24783	. . . . . . . 8 ⊢ ℝ = ∪ (topGen‘ran (,))
229	228	restuni 23170	. . . . . . 7 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐶(,)𝐸) ⊆ ℝ) → (𝐶(,)𝐸) = ∪ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)))
230	227, 21, 229	mp2an 692	. . . . . 6 ⊢ (𝐶(,)𝐸) = ∪ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸))
231	230, 182	cnprest2 23298	. . . . 5 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)):(𝐶(,)𝐸)⟶ℝ ∧ ℝ ⊆ ℂ) → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌) ↔ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ))‘𝑌)))
232	221, 224, 226, 231	syl3anc 1373	. . . 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 7447	. . . 4 ⊢ (𝜑 → (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ)) = (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,))))
237	236	fveq1d 6908	. . 3 ⊢ (𝜑 → ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ))‘𝑌) = ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,)))‘𝑌))
238	233, 237	eleqtrd 2843	. 2 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,)))‘𝑌))
239	227	a1i 11	. . 3 ⊢ (𝜑 → (topGen‘ran (,)) ∈ Top)
240		iooretop 24786	. . . . . . 7 ⊢ (𝐶(,)𝐸) ∈ (topGen‘ran (,))
241	228	isopn3 23074	. . . . . . 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 584	. . . . 5 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)) = (𝐶(,)𝐸))
244	243	eqcomd 2743	. . . 4 ⊢ (𝜑 → (𝐶(,)𝐸) = ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)))
245	216, 244	eleqtrd 2843	. . 3 ⊢ (𝜑 → 𝑌 ∈ ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)))
246	228, 228	cnprest 23297	. . 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 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 Vcvv 3480 ∖ cdif 3948 ⊆ wss 3951 ifcif 4525 {csn 4626 ∪ cuni 4907 class class class wbr 5143 ↦ cmpt 5225 ran crn 5686 ↾ cres 5687 ∘ ccom 5689 ⟶wf 6557 ‘cfv 6561 (class class class)co 7431 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 · cmul 11160 ℝ^*cxr 11294 < clt 11295 ≤ cle 11296 / cdiv 11920 ℕcn 12266 2c2 12321 ℤcz 12613 ℝ⁺crp 13034 (,)cioo 13387 ⌊cfl 13830 mod cmo 13909 sincsin 16099 πcpi 16102 ↾_t crest 17465 TopOpenctopn 17466 topGenctg 17482 ℂ_fldccnfld 21364 Topctop 22899 TopOnctopon 22916 intcnt 23025 Cn ccn 23232 CnP ccnp 23233 –cn→ccncf 24902

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233 ax-addf 11234

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-iin 4994 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-om 7888 df-1st 8014 df-2nd 8015 df-supp 8186 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-er 8745 df-map 8868 df-pm 8869 df-ixp 8938 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-fsupp 9402 df-fi 9451 df-sup 9482 df-inf 9483 df-oi 9550 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-9 12336 df-n0 12527 df-z 12614 df-dec 12734 df-uz 12879 df-q 12991 df-rp 13035 df-xneg 13154 df-xadd 13155 df-xmul 13156 df-ioo 13391 df-ioc 13392 df-ico 13393 df-icc 13394 df-fz 13548 df-fzo 13695 df-fl 13832 df-mod 13910 df-seq 14043 df-exp 14103 df-fac 14313 df-bc 14342 df-hash 14370 df-shft 15106 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-limsup 15507 df-clim 15524 df-rlim 15525 df-sum 15723 df-ef 16103 df-sin 16105 df-cos 16106 df-pi 16108 df-struct 17184 df-sets 17201 df-slot 17219 df-ndx 17231 df-base 17248 df-ress 17275 df-plusg 17310 df-mulr 17311 df-starv 17312 df-sca 17313 df-vsca 17314 df-ip 17315 df-tset 17316 df-ple 17317 df-ds 17319 df-unif 17320 df-hom 17321 df-cco 17322 df-rest 17467 df-topn 17468 df-0g 17486 df-gsum 17487 df-topgen 17488 df-pt 17489 df-prds 17492 df-xrs 17547 df-qtop 17552 df-imas 17553 df-xps 17555 df-mre 17629 df-mrc 17630 df-acs 17632 df-mgm 18653 df-sgrp 18732 df-mnd 18748 df-submnd 18797 df-mulg 19086 df-cntz 19335 df-cmn 19800 df-psmet 21356 df-xmet 21357 df-met 21358 df-bl 21359 df-mopn 21360 df-fbas 21361 df-fg 21362 df-cnfld 21365 df-top 22900 df-topon 22917 df-topsp 22939 df-bases 22953 df-cld 23027 df-ntr 23028 df-cls 23029 df-nei 23106 df-lp 23144 df-perf 23145 df-cn 23235 df-cnp 23236 df-haus 23323 df-tx 23570 df-hmeo 23763 df-fil 23854 df-fm 23946 df-flim 23947 df-flf 23948 df-xms 24330 df-ms 24331 df-tms 24332 df-cncf 24904 df-limc 25901 df-dv 25902

This theorem is referenced by: dirkercncf 46122

W3C validator