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 46150

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 26382	. . . . . . . . . . 11 ⊢ sin ∈ (ℂ–cn→ℂ)
2	1	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → sin ∈ (ℂ–cn→ℂ))
3		ioosscn 13308	. . . . . . . . . . . . 13 ⊢ (𝐶(,)𝐸) ⊆ ℂ
4	3	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶(,)𝐸) ⊆ ℂ)
5		dirkercncflem4.n	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	nncnd 12141	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
7		1cnd 11107	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℂ)
8	7	halfcld 12366	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
9	6, 8	addcld 11131	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ)
10		ssid 3957	. . . . . . . . . . . . 13 ⊢ ℂ ⊆ ℂ
11	10	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ ⊆ ℂ)
12	4, 9, 11	constcncfg 45916	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑁 + (1 / 2))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
13	4, 11	idcncfg 45917	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ 𝑦) ∈ ((𝐶(,)𝐸)–cn→ℂ))
14	12, 13	mulcncf 25374	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
15	2, 14	cncfmpt1f 24835	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
16		2cnd 12203	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ∈ ℂ)
17		pirp 26398	. . . . . . . . . . . . . . . 16 ⊢ π ∈ ℝ⁺
18	17	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ∈ ℝ⁺)
19	18	rpcnd 12936	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ∈ ℂ)
20	16, 19	mulcld 11132	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℂ)
21		ioossre 13307	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶(,)𝐸) ⊆ ℝ
22	21	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐶(,)𝐸) ⊆ ℝ)
23	22	sselda 3934	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 ∈ ℝ)
24	23	recnd 11140	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 ∈ ℂ)
25	24	halfcld 12366	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / 2) ∈ ℂ)
26	25	sincld 16039	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘(𝑦 / 2)) ∈ ℂ)
27	20, 26	mulcld 11132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
28		2rp 12895	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ⁺
29	28	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ∈ ℝ⁺)
30	29	rpne0d 12939	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ≠ 0)
31	18	rpne0d 12939	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ≠ 0)
32	16, 19, 30, 31	mulne0d 11769	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ≠ 0)
33	24, 16, 19, 30, 31	divdiv1d 11928	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
34		dirkercncflem4.c	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐶 = (𝐴 · (2 · π))
35		dirkercncflem4.a	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐴 = (⌊‘(𝑌 / (2 · π)))
36	35	oveq1i 7356	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 · (2 · π)) = ((⌊‘(𝑌 / (2 · π))) · (2 · π))
37	34, 36	eqtri 2754	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐶 = ((⌊‘(𝑌 / (2 · π))) · (2 · π))
38	37	oveq1i 7356	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐶 / (2 · π)) = (((⌊‘(𝑌 / (2 · π))) · (2 · π)) / (2 · π))
39		dirkercncflem4.y	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑌 ∈ ℝ)
40		2re 12199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 2 ∈ ℝ
41		pire 26394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ π ∈ ℝ
42	40, 41	remulcli 11128	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (2 · π) ∈ ℝ
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (2 · π) ∈ ℝ)
44		0re 11114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 ∈ ℝ
45		2pos 12228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 < 2
46		pipos 26396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 < π
47	40, 41, 45, 46	mulgt0ii 11246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 < (2 · π)
48	44, 47	gtneii 11225	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (2 · π) ≠ 0
49	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (2 · π) ≠ 0)
50	39, 43, 49	redivcld 11949	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑌 / (2 · π)) ∈ ℝ)
51	50	flcld 13702	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) ∈ ℤ)
52	51	zred 12577	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) ∈ ℝ)
53	52	recnd 11140	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) ∈ ℂ)
54	43	recnd 11140	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (2 · π) ∈ ℂ)
55	53, 54, 49	divcan4d 11903	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((⌊‘(𝑌 / (2 · π))) · (2 · π)) / (2 · π)) = (⌊‘(𝑌 / (2 · π))))
56	38, 55	eqtrid 2778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐶 / (2 · π)) = (⌊‘(𝑌 / (2 · π))))
57	56, 51	eqeltrd 2831	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐶 / (2 · π)) ∈ ℤ)
58	57	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝐶 / (2 · π)) ∈ ℤ)
59	52, 43	remulcld 11142	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) · (2 · π)) ∈ ℝ)
60	37, 59	eqeltrid 2835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ ℝ)
61	60	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐶 ∈ ℝ)
62	29, 18	rpmulcld 12950	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℝ⁺)
63		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 ∈ (𝐶(,)𝐸))
64	60	rexrd 11162	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
65	64	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐶 ∈ ℝ^*)
66	35	eqcomi 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⌊‘(𝑌 / (2 · π))) = 𝐴
67	66	oveq1i 7356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((⌊‘(𝑌 / (2 · π))) + 1) = (𝐴 + 1)
68		dirkercncflem4.b	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 𝐵 = (𝐴 + 1)
69	67, 68	eqtr4i 2757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((⌊‘(𝑌 / (2 · π))) + 1) = 𝐵
70	69	oveq1i 7356	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) = (𝐵 · (2 · π))
71		dirkercncflem4.e	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝐸 = (𝐵 · (2 · π))
72	70, 71	eqtr4i 2757	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) = 𝐸
73	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) = 𝐸)
74		1red 11113	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 1 ∈ ℝ)
75	52, 74	readdcld 11141	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) + 1) ∈ ℝ)
76	75, 43	remulcld 11142	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) ∈ ℝ)
77	73, 76	eqeltrrd 2832	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐸 ∈ ℝ)
78	77	rexrd 11162	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐸 ∈ ℝ^*)
79	78	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐸 ∈ ℝ^*)
80		elioo2 13286	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐸 ∈ ℝ^*) → (𝑦 ∈ (𝐶(,)𝐸) ↔ (𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸)))
81	65, 79, 80	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 ∈ (𝐶(,)𝐸) ↔ (𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸)))
82	63, 81	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸))
83	82	simp2d 1143	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐶 < 𝑦)
84	61, 23, 62, 83	ltdiv1dd 12991	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝐶 / (2 · π)) < (𝑦 / (2 · π)))
85	77	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐸 ∈ ℝ)
86	82	simp3d 1144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 < 𝐸)
87	23, 85, 62, 86	ltdiv1dd 12991	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / (2 · π)) < (𝐸 / (2 · π)))
88	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐶 = (𝐴 · (2 · π)))
89	88	oveq1d 7361	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐶 / (2 · π)) = ((𝐴 · (2 · π)) / (2 · π)))
90	89	oveq1d 7361	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝐶 / (2 · π)) + 1) = (((𝐴 · (2 · π)) / (2 · π)) + 1))
91	35, 53	eqeltrid 2835	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐴 ∈ ℂ)
92	91, 54, 49	divcan4d 11903	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 · (2 · π)) / (2 · π)) = 𝐴)
93	92	oveq1d 7361	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝐴 · (2 · π)) / (2 · π)) + 1) = (𝐴 + 1))
94	68	oveq1i 7356	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐵 · (2 · π)) = ((𝐴 + 1) · (2 · π))
95	71, 94	eqtri 2754	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐸 = ((𝐴 + 1) · (2 · π))
96	95	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐸 = ((𝐴 + 1) · (2 · π)))
97	96	oveq1d 7361	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐸 / (2 · π)) = (((𝐴 + 1) · (2 · π)) / (2 · π)))
98	91, 7	addcld 11131	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 + 1) ∈ ℂ)
99	98, 54, 49	divcan4d 11903	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴 + 1) · (2 · π)) / (2 · π)) = (𝐴 + 1))
100	97, 99	eqtr2d 2767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴 + 1) = (𝐸 / (2 · π)))
101	90, 93, 100	3eqtrrd 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 / (2 · π)) = ((𝐶 / (2 · π)) + 1))
102	101	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝐸 / (2 · π)) = ((𝐶 / (2 · π)) + 1))
103	87, 102	breqtrd 5117	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / (2 · π)) < ((𝐶 / (2 · π)) + 1))
104		btwnnz 12549	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶 / (2 · π)) ∈ ℤ ∧ (𝐶 / (2 · π)) < (𝑦 / (2 · π)) ∧ (𝑦 / (2 · π)) < ((𝐶 / (2 · π)) + 1)) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
105	58, 84, 103, 104	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
106	33, 105	eqneltrd 2851	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ ((𝑦 / 2) / π) ∈ ℤ)
107		sineq0 26461	. . . . . . . . . . . . . . . . . 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 2935	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘(𝑦 / 2)) ≠ 0)
111	20, 26, 32, 110	mulne0d 11769	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ≠ 0)
112	111	neneqd 2933	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ ((2 · π) · (sin‘(𝑦 / 2))) = 0)
113	40	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ∈ ℝ)
114	41	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ∈ ℝ)
115	113, 114	remulcld 11142	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℝ)
116	23	rehalfcld 12368	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / 2) ∈ ℝ)
117	116	resincld 16052	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘(𝑦 / 2)) ∈ ℝ)
118	115, 117	remulcld 11142	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℝ)
119		elsng 4590	. . . . . . . . . . . . . 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 3913	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ (ℂ ∖ {0}))
123		eqidd 2732	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))))
124		eqidd 2732	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)))
125		oveq2 7354	. . . . . . . . . . 11 ⊢ (𝑥 = ((2 · π) · (sin‘(𝑦 / 2))) → (1 / 𝑥) = (1 / ((2 · π) · (sin‘(𝑦 / 2)))))
126	122, 123, 124, 125	fmptco 7062	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∘ (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ (𝐶(,)𝐸) ↦ (1 / ((2 · π) · (sin‘(𝑦 / 2))))))
127		eqid 2731	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
128		2cnd 12203	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℂ)
129	4, 128, 11	constcncfg 45916	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ 2) ∈ ((𝐶(,)𝐸)–cn→ℂ))
130	17	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → π ∈ ℝ⁺)
131	130	rpcnd 12936	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → π ∈ ℂ)
132	4, 131, 11	constcncfg 45916	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ π) ∈ ((𝐶(,)𝐸)–cn→ℂ))
133	129, 132	mulcncf 25374	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (2 · π)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
134	24, 16, 30	divrecd 11900	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / 2) = (𝑦 · (1 / 2)))
135	134	mpteq2dva 5184	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 / 2)) = (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 · (1 / 2))))
136	4, 8, 11	constcncfg 45916	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (1 / 2)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
137	13, 136	mulcncf 25374	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 · (1 / 2))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
138	135, 137	eqeltrd 2831	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 / 2)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
139	2, 138	cncfmpt1f 24835	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (sin‘(𝑦 / 2))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
140	133, 139	mulcncf 25374	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
141		ssid 3957	. . . . . . . . . . . . 13 ⊢ (𝐶(,)𝐸) ⊆ (𝐶(,)𝐸)
142	141	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶(,)𝐸) ⊆ (𝐶(,)𝐸))
143		difssd 4087	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
144	127, 140, 142, 143, 122	cncfmptssg 45915	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ∈ ((𝐶(,)𝐸)–cn→(ℂ ∖ {0})))
145		ax-1cn 11064	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
146		eqid 2731	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥))
147	146	cdivcncf 24842	. . . . . . . . . . . 12 ⊢ (1 ∈ ℂ → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∈ ((ℂ ∖ {0})–cn→ℂ))
148	145, 147	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∈ ((ℂ ∖ {0})–cn→ℂ))
149	144, 148	cncfco 24828	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∘ (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
150	126, 149	eqeltrrd 2832	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (1 / ((2 · π) · (sin‘(𝑦 / 2))))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
151	15, 150	mulcncf 25374	. . . . . . . 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 46135	. . . . . . . . . . 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 5927	. . . . . . . . 9 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) = ((𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) ↾ (𝐶(,)𝐸)))
156	22	resmptd 5989	. . . . . . . . 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 12950	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · π) ∈ ℝ⁺)
159	158	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℝ⁺)
160		mod0 13780	. . . . . . . . . . . . . 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 4486	. . . . . . . . . . 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 11107	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 1 ∈ ℂ)
166	165	halfcld 12366	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (1 / 2) ∈ ℂ)
167	164, 166	addcld 11131	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑁 + (1 / 2)) ∈ ℂ)
168	167, 24	mulcld 11132	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
169	168	sincld 16039	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
170	169, 27, 111	divrecd 11900	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2))))))
171	163, 170	eqtrd 2766	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2))))))
172	171	mpteq2dva 5184	. . . . . . . . 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 2771	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2)))))) = ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)))
174		eqid 2731	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
175		tgioo4 24721	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
176	175	oveq1i 7356	. . . . . . . . . . 11 ⊢ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) = (((TopOpen‘ℂ_fld) ↾_t ℝ) ↾_t (𝐶(,)𝐸))
177	174	cnfldtop 24699	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) ∈ Top
178		reex 11097	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
179		restabs 23081	. . . . . . . . . . . 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 2754	. . . . . . . . . 10 ⊢ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) = ((TopOpen‘ℂ_fld) ↾_t (𝐶(,)𝐸))
182		unicntop 24701	. . . . . . . . . . . . 13 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
183	182	restid 17337	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ∈ Top → ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld))
184	177, 183	ax-mp 5	. . . . . . . . . . 11 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld)
185	184	eqcomi 2740	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
186	174, 181, 185	cncfcn 24831	. . . . . . . . 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 2845	. . . . . . 7 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) Cn (TopOpen‘ℂ_fld)))
189		retopon 24679	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
190	189	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (topGen‘ran (,)) ∈ (TopOn‘ℝ))
191		resttopon 23077	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (𝐶(,)𝐸) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) ∈ (TopOn‘(𝐶(,)𝐸)))
192	190, 22, 191	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) ∈ (TopOn‘(𝐶(,)𝐸)))
193	174	cnfldtopon 24698	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
194	193	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
195		cncnp 23196	. . . . . . . 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 2933	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝑌 mod (2 · π)) = 0)
201		mod0 13780	. . . . . . . . . . . 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 13715	. . . . . . . . . 10 ⊢ (((𝑌 / (2 · π)) ∈ ℝ ∧ ¬ (𝑌 / (2 · π)) ∈ ℤ) → (⌊‘(𝑌 / (2 · π))) < (𝑌 / (2 · π)))
205	50, 203, 204	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) < (𝑌 / (2 · π)))
206	52, 50, 158, 205	ltmul1dd 12989	. . . . . . . 8 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) · (2 · π)) < ((𝑌 / (2 · π)) · (2 · π)))
207	39	recnd 11140	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ ℂ)
208	207, 54, 49	divcan1d 11898	. . . . . . . 8 ⊢ (𝜑 → ((𝑌 / (2 · π)) · (2 · π)) = 𝑌)
209	206, 208	breqtrd 5117	. . . . . . 7 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) · (2 · π)) < 𝑌)
210	37, 209	eqbrtrid 5126	. . . . . 6 ⊢ (𝜑 → 𝐶 < 𝑌)
211		fllelt 13701	. . . . . . . . . 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 12989	. . . . . . 7 ⊢ (𝜑 → ((𝑌 / (2 · π)) · (2 · π)) < (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)))
215	214, 208, 73	3brtr3d 5122	. . . . . 6 ⊢ (𝜑 → 𝑌 < 𝐸)
216	64, 78, 39, 210, 215	eliood 45544	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ (𝐶(,)𝐸))
217		fveq2 6822	. . . . . . 7 ⊢ (𝑦 = 𝑌 → ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦) = ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌))
218	217	eleq2d 2817	. . . . . 6 ⊢ (𝑦 = 𝑌 → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦) ↔ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌)))
219	218	rspccva 3576	. . . . 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 46141	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁):ℝ⟶ℝ)
223	5, 222	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐷‘𝑁):ℝ⟶ℝ)
224	223, 22	fssresd 6690	. . . . 5 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)):(𝐶(,)𝐸)⟶ℝ)
225		ax-resscn 11063	. . . . . 6 ⊢ ℝ ⊆ ℂ
226	225	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ⊆ ℂ)
227		retop 24677	. . . . . . 7 ⊢ (topGen‘ran (,)) ∈ Top
228		uniretop 24678	. . . . . . . 8 ⊢ ℝ = ∪ (topGen‘ran (,))
229	228	restuni 23078	. . . . . . 7 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐶(,)𝐸) ⊆ ℝ) → (𝐶(,)𝐸) = ∪ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)))
230	227, 21, 229	mp2an 692	. . . . . 6 ⊢ (𝐶(,)𝐸) = ∪ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸))
231	230, 182	cnprest2 23206	. . . . 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 2740	. . . . . 6 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℝ) = (topGen‘ran (,))
235	234	a1i 11	. . . . 5 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t ℝ) = (topGen‘ran (,)))
236	235	oveq2d 7362	. . . 4 ⊢ (𝜑 → (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ)) = (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,))))
237	236	fveq1d 6824	. . 3 ⊢ (𝜑 → ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ))‘𝑌) = ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,)))‘𝑌))
238	233, 237	eleqtrd 2833	. 2 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,)))‘𝑌))
239	227	a1i 11	. . 3 ⊢ (𝜑 → (topGen‘ran (,)) ∈ Top)
240		iooretop 24681	. . . . . . 7 ⊢ (𝐶(,)𝐸) ∈ (topGen‘ran (,))
241	228	isopn3 22982	. . . . . . 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 2737	. . . 4 ⊢ (𝜑 → (𝐶(,)𝐸) = ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)))
245	216, 244	eleqtrd 2833	. . 3 ⊢ (𝜑 → 𝑌 ∈ ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)))
246	228, 228	cnprest 23205	. . 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 838	. 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 1086 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 Vcvv 3436 ∖ cdif 3899 ⊆ wss 3902 ifcif 4475 {csn 4576 ∪ cuni 4859 class class class wbr 5091 ↦ cmpt 5172 ran crn 5617 ↾ cres 5618 ∘ ccom 5620 ⟶wf 6477 ‘cfv 6481 (class class class)co 7346 ℂcc 11004 ℝcr 11005 0cc0 11006 1c1 11007 + caddc 11009 · cmul 11011 ℝ^*cxr 11145 < clt 11146 ≤ cle 11147 / cdiv 11774 ℕcn 12125 2c2 12180 ℤcz 12468 ℝ⁺crp 12890 (,)cioo 13245 ⌊cfl 13694 mod cmo 13773 sincsin 15970 πcpi 15973 ↾_t crest 17324 TopOpenctopn 17325 topGenctg 17341 ℂ_fldccnfld 21292 Topctop 22809 TopOnctopon 22826 intcnt 22933 Cn ccn 23140 CnP ccnp 23141 –cn→ccncf 24797

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5217 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-inf2 9531 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084 ax-addf 11085

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-tp 4581 df-op 4583 df-uni 4860 df-int 4898 df-iun 4943 df-iin 4944 df-br 5092 df-opab 5154 df-mpt 5173 df-tr 5199 df-id 5511 df-eprel 5516 df-po 5524 df-so 5525 df-fr 5569 df-se 5570 df-we 5571 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-of 7610 df-om 7797 df-1st 7921 df-2nd 7922 df-supp 8091 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-2o 8386 df-er 8622 df-map 8752 df-pm 8753 df-ixp 8822 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-fsupp 9246 df-fi 9295 df-sup 9326 df-inf 9327 df-oi 9396 df-card 9832 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-4 12190 df-5 12191 df-6 12192 df-7 12193 df-8 12194 df-9 12195 df-n0 12382 df-z 12469 df-dec 12589 df-uz 12733 df-q 12847 df-rp 12891 df-xneg 13011 df-xadd 13012 df-xmul 13013 df-ioo 13249 df-ioc 13250 df-ico 13251 df-icc 13252 df-fz 13408 df-fzo 13555 df-fl 13696 df-mod 13774 df-seq 13909 df-exp 13969 df-fac 14181 df-bc 14210 df-hash 14238 df-shft 14974 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-limsup 15378 df-clim 15395 df-rlim 15396 df-sum 15594 df-ef 15974 df-sin 15976 df-cos 15977 df-pi 15979 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-starv 17176 df-sca 17177 df-vsca 17178 df-ip 17179 df-tset 17180 df-ple 17181 df-ds 17183 df-unif 17184 df-hom 17185 df-cco 17186 df-rest 17326 df-topn 17327 df-0g 17345 df-gsum 17346 df-topgen 17347 df-pt 17348 df-prds 17351 df-xrs 17406 df-qtop 17411 df-imas 17412 df-xps 17414 df-mre 17488 df-mrc 17489 df-acs 17491 df-mgm 18548 df-sgrp 18627 df-mnd 18643 df-submnd 18692 df-mulg 18981 df-cntz 19230 df-cmn 19695 df-psmet 21284 df-xmet 21285 df-met 21286 df-bl 21287 df-mopn 21288 df-fbas 21289 df-fg 21290 df-cnfld 21293 df-top 22810 df-topon 22827 df-topsp 22849 df-bases 22862 df-cld 22935 df-ntr 22936 df-cls 22937 df-nei 23014 df-lp 23052 df-perf 23053 df-cn 23143 df-cnp 23144 df-haus 23231 df-tx 23478 df-hmeo 23671 df-fil 23762 df-fm 23854 df-flim 23855 df-flf 23856 df-xms 24236 df-ms 24237 df-tms 24238 df-cncf 24799 df-limc 25795 df-dv 25796

This theorem is referenced by: dirkercncf 46151

W3C validator