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 46935

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 26681	. . . . . . . . . . 11 ⊢ sin ∈ (ℂ–cn→ℂ)
2	1	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → sin ∈ (ℂ–cn→ℂ))
3		ioosscn 13462	. . . . . . . . . . . . 13 ⊢ (𝐶(,)𝐸) ⊆ ℂ
4	3	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶(,)𝐸) ⊆ ℂ)
5		dirkercncflem4.n	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	nncnd 12274	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
7		1cnd 11227	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℂ)
8	7	halfcld 12514	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
9	6, 8	addcld 11253	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ)
10		ssid 3953	. . . . . . . . . . . . 13 ⊢ ℂ ⊆ ℂ
11	10	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ ⊆ ℂ)
12	4, 9, 11	constcncfg 46701	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑁 + (1 / 2))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
13	4, 11	idcncfg 46702	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ 𝑦) ∈ ((𝐶(,)𝐸)–cn→ℂ))
14	12, 13	mulcncf 25675	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
15	2, 14	cncfmpt1f 25143	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
16		2cnd 12344	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ∈ ℂ)
17		pirp 26700	. . . . . . . . . . . . . . . 16 ⊢ π ∈ ℝ⁺
18	17	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ∈ ℝ⁺)
19	18	rpcnd 13089	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ∈ ℂ)
20	16, 19	mulcld 11254	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℂ)
21		ioossre 13461	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶(,)𝐸) ⊆ ℝ
22	21	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐶(,)𝐸) ⊆ ℝ)
23	22	sselda 3931	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 ∈ ℝ)
24	23	recnd 11262	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 ∈ ℂ)
25	24	halfcld 12514	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / 2) ∈ ℂ)
26	25	sincld 16219	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘(𝑦 / 2)) ∈ ℂ)
27	20, 26	mulcld 11254	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
28		2rp 13048	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ⁺
29	28	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ∈ ℝ⁺)
30	29	rpne0d 13092	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ≠ 0)
31	18	rpne0d 13092	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ≠ 0)
32	16, 19, 30, 31	mulne0d 11891	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ≠ 0)
33	24, 16, 19, 30, 31	divdiv1d 12047	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
34		dirkercncflem4.c	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐶 = (𝐴 · (2 · π))
35		dirkercncflem4.a	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐴 = (⌊‘(𝑌 / (2 · π)))
36	35	oveq1i 7424	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 · (2 · π)) = ((⌊‘(𝑌 / (2 · π))) · (2 · π))
37	34, 36	eqtri 2783	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐶 = ((⌊‘(𝑌 / (2 · π))) · (2 · π))
38	37	oveq1i 7424	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐶 / (2 · π)) = (((⌊‘(𝑌 / (2 · π))) · (2 · π)) / (2 · π))
39		dirkercncflem4.y	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑌 ∈ ℝ)
40		2re 12340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 2 ∈ ℝ
41		pire 26693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ π ∈ ℝ
42	40, 41	remulcli 11250	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (2 · π) ∈ ℝ
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (2 · π) ∈ ℝ)
44		0re 11235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 ∈ ℝ
45		2pos 12370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 < 2
46		pipos 26697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 < π
47	40, 41, 45, 46	mulgt0ii 11368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 < (2 · π)
48	44, 47	gtneii 11347	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (2 · π) ≠ 0
49	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (2 · π) ≠ 0)
50	39, 43, 49	redivcld 12068	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑌 / (2 · π)) ∈ ℝ)
51	50	flcld 13860	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) ∈ ℤ)
52	51	zred 12726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) ∈ ℝ)
53	52	recnd 11262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) ∈ ℂ)
54	43	recnd 11262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (2 · π) ∈ ℂ)
55	53, 54, 49	divcan4d 12022	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((⌊‘(𝑌 / (2 · π))) · (2 · π)) / (2 · π)) = (⌊‘(𝑌 / (2 · π))))
56	38, 55	eqtrid 2807	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐶 / (2 · π)) = (⌊‘(𝑌 / (2 · π))))
57	56, 51	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐶 / (2 · π)) ∈ ℤ)
58	57	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝐶 / (2 · π)) ∈ ℤ)
59	52, 43	remulcld 11264	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) · (2 · π)) ∈ ℝ)
60	37, 59	eqeltrid 2864	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ ℝ)
61	60	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐶 ∈ ℝ)
62	29, 18	rpmulcld 13103	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℝ⁺)
63		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 ∈ (𝐶(,)𝐸))
64	60	rexrd 11284	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
65	64	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐶 ∈ ℝ^*)
66	35	eqcomi 2769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⌊‘(𝑌 / (2 · π))) = 𝐴
67	66	oveq1i 7424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((⌊‘(𝑌 / (2 · π))) + 1) = (𝐴 + 1)
68		dirkercncflem4.b	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 𝐵 = (𝐴 + 1)
69	67, 68	eqtr4i 2786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((⌊‘(𝑌 / (2 · π))) + 1) = 𝐵
70	69	oveq1i 7424	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) = (𝐵 · (2 · π))
71		dirkercncflem4.e	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝐸 = (𝐵 · (2 · π))
72	70, 71	eqtr4i 2786	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) = 𝐸
73	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) = 𝐸)
74		1red 11234	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 1 ∈ ℝ)
75	52, 74	readdcld 11263	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) + 1) ∈ ℝ)
76	75, 43	remulcld 11264	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) ∈ ℝ)
77	73, 76	eqeltrrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐸 ∈ ℝ)
78	77	rexrd 11284	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐸 ∈ ℝ^*)
79	78	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐸 ∈ ℝ^*)
80		elioo2 13440	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐸 ∈ ℝ^*) → (𝑦 ∈ (𝐶(,)𝐸) ↔ (𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸)))
81	65, 79, 80	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 ∈ (𝐶(,)𝐸) ↔ (𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸)))
82	63, 81	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸))
83	82	simp2d 1161	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐶 < 𝑦)
84	61, 23, 62, 83	ltdiv1dd 13144	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝐶 / (2 · π)) < (𝑦 / (2 · π)))
85	77	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐸 ∈ ℝ)
86	82	simp3d 1162	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 < 𝐸)
87	23, 85, 62, 86	ltdiv1dd 13144	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / (2 · π)) < (𝐸 / (2 · π)))
88	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐶 = (𝐴 · (2 · π)))
89	88	oveq1d 7429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐶 / (2 · π)) = ((𝐴 · (2 · π)) / (2 · π)))
90	89	oveq1d 7429	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝐶 / (2 · π)) + 1) = (((𝐴 · (2 · π)) / (2 · π)) + 1))
91	35, 53	eqeltrid 2864	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐴 ∈ ℂ)
92	91, 54, 49	divcan4d 12022	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 · (2 · π)) / (2 · π)) = 𝐴)
93	92	oveq1d 7429	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝐴 · (2 · π)) / (2 · π)) + 1) = (𝐴 + 1))
94	68	oveq1i 7424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐵 · (2 · π)) = ((𝐴 + 1) · (2 · π))
95	71, 94	eqtri 2783	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐸 = ((𝐴 + 1) · (2 · π))
96	95	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐸 = ((𝐴 + 1) · (2 · π)))
97	96	oveq1d 7429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐸 / (2 · π)) = (((𝐴 + 1) · (2 · π)) / (2 · π)))
98	91, 7	addcld 11253	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 + 1) ∈ ℂ)
99	98, 54, 49	divcan4d 12022	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴 + 1) · (2 · π)) / (2 · π)) = (𝐴 + 1))
100	97, 99	eqtr2d 2796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴 + 1) = (𝐸 / (2 · π)))
101	90, 93, 100	3eqtrrd 2800	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 / (2 · π)) = ((𝐶 / (2 · π)) + 1))
102	101	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝐸 / (2 · π)) = ((𝐶 / (2 · π)) + 1))
103	87, 102	breqtrd 5131	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / (2 · π)) < ((𝐶 / (2 · π)) + 1))
104		btwnnz 12698	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶 / (2 · π)) ∈ ℤ ∧ (𝐶 / (2 · π)) < (𝑦 / (2 · π)) ∧ (𝑦 / (2 · π)) < ((𝐶 / (2 · π)) + 1)) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
105	58, 84, 103, 104	syl3anc 1398	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
106	33, 105	eqneltrd 2880	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ ((𝑦 / 2) / π) ∈ ℤ)
107		sineq0 26762	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 / 2) ∈ ℂ → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
108	25, 107	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
109	106, 108	mtbird 328	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ (sin‘(𝑦 / 2)) = 0)
110	109	neqned 2962	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘(𝑦 / 2)) ≠ 0)
111	20, 26, 32, 110	mulne0d 11891	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ≠ 0)
112	111	neneqd 2960	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ ((2 · π) · (sin‘(𝑦 / 2))) = 0)
113	40	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ∈ ℝ)
114	41	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ∈ ℝ)
115	113, 114	remulcld 11264	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℝ)
116	23	rehalfcld 12516	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / 2) ∈ ℝ)
117	116	resincld 16232	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘(𝑦 / 2)) ∈ ℝ)
118	115, 117	remulcld 11264	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℝ)
119		elsng 4598	. . . . . . . . . . . . . 14 ⊢ (((2 · π) · (sin‘(𝑦 / 2))) ∈ ℝ → (((2 · π) · (sin‘(𝑦 / 2))) ∈ {0} ↔ ((2 · π) · (sin‘(𝑦 / 2))) = 0))
120	118, 119	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (((2 · π) · (sin‘(𝑦 / 2))) ∈ {0} ↔ ((2 · π) · (sin‘(𝑦 / 2))) = 0))
121	112, 120	mtbird 328	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ ((2 · π) · (sin‘(𝑦 / 2))) ∈ {0})
122	27, 121	eldifd 3910	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ (ℂ ∖ {0}))
123		eqidd 2761	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))))
124		eqidd 2761	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)))
125		oveq2 7422	. . . . . . . . . . 11 ⊢ (𝑥 = ((2 · π) · (sin‘(𝑦 / 2))) → (1 / 𝑥) = (1 / ((2 · π) · (sin‘(𝑦 / 2)))))
126	122, 123, 124, 125	fmptco 7124	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∘ (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ (𝐶(,)𝐸) ↦ (1 / ((2 · π) · (sin‘(𝑦 / 2))))))
127		eqid 2760	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
128		2cnd 12344	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℂ)
129	4, 128, 11	constcncfg 46701	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ 2) ∈ ((𝐶(,)𝐸)–cn→ℂ))
130	17	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → π ∈ ℝ⁺)
131	130	rpcnd 13089	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → π ∈ ℂ)
132	4, 131, 11	constcncfg 46701	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ π) ∈ ((𝐶(,)𝐸)–cn→ℂ))
133	129, 132	mulcncf 25675	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (2 · π)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
134	24, 16, 30	divrecd 12019	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / 2) = (𝑦 · (1 / 2)))
135	134	mpteq2dva 5198	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 / 2)) = (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 · (1 / 2))))
136	4, 8, 11	constcncfg 46701	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (1 / 2)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
137	13, 136	mulcncf 25675	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 · (1 / 2))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
138	135, 137	eqeltrd 2860	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 / 2)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
139	2, 138	cncfmpt1f 25143	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (sin‘(𝑦 / 2))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
140	133, 139	mulcncf 25675	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
141		ssid 3953	. . . . . . . . . . . . 13 ⊢ (𝐶(,)𝐸) ⊆ (𝐶(,)𝐸)
142	141	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶(,)𝐸) ⊆ (𝐶(,)𝐸))
143		difssd 4084	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
144	127, 140, 142, 143, 122	cncfmptssg 46700	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ∈ ((𝐶(,)𝐸)–cn→(ℂ ∖ {0})))
145		ax-1cn 11183	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
146		eqid 2760	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥))
147	146	cdivcncf 25150	. . . . . . . . . . . 12 ⊢ (1 ∈ ℂ → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∈ ((ℂ ∖ {0})–cn→ℂ))
148	145, 147	mp1i 14	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∈ ((ℂ ∖ {0})–cn→ℂ))
149	144, 148	cncfco 25136	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∘ (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
150	126, 149	eqeltrrd 2861	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (1 / ((2 · π) · (sin‘(𝑦 / 2))))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
151	15, 150	mulcncf 25675	. . . . . . . 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 46920	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) = (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
154	5, 153	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷‘𝑁) = (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
155	154	reseq1d 5971	. . . . . . . . 9 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) = ((𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) ↾ (𝐶(,)𝐸)))
156	22	resmptd 6036	. . . . . . . . 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 13103	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · π) ∈ ℝ⁺)
159	158	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℝ⁺)
160		mod0 13938	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℝ ∧ (2 · π) ∈ ℝ⁺) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
161	23, 159, 160	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
162	105, 161	mtbird 328	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ (𝑦 mod (2 · π)) = 0)
163	162	iffalsed 4493	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
164	6	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑁 ∈ ℂ)
165		1cnd 11227	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 1 ∈ ℂ)
166	165	halfcld 12514	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (1 / 2) ∈ ℂ)
167	164, 166	addcld 11253	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑁 + (1 / 2)) ∈ ℂ)
168	167, 24	mulcld 11254	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
169	168	sincld 16219	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
170	169, 27, 111	divrecd 12019	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2))))))
171	163, 170	eqtrd 2795	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2))))))
172	171	mpteq2dva 5198	. . . . . . . . 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 2800	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2)))))) = ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)))
174		eqid 2760	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
175		tgioo4 25032	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
176	175	oveq1i 7424	. . . . . . . . . . 11 ⊢ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) = (((TopOpen‘ℂ_fld) ↾_t ℝ) ↾_t (𝐶(,)𝐸))
177	174	cnfldtop 25010	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) ∈ Top
178		reex 11216	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
179		restabs 23391	. . . . . . . . . . . 12 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ (𝐶(,)𝐸) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂ_fld) ↾_t ℝ) ↾_t (𝐶(,)𝐸)) = ((TopOpen‘ℂ_fld) ↾_t (𝐶(,)𝐸)))
180	177, 21, 178, 179	mp3an 1490	. . . . . . . . . . 11 ⊢ (((TopOpen‘ℂ_fld) ↾_t ℝ) ↾_t (𝐶(,)𝐸)) = ((TopOpen‘ℂ_fld) ↾_t (𝐶(,)𝐸))
181	176, 180	eqtri 2783	. . . . . . . . . 10 ⊢ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) = ((TopOpen‘ℂ_fld) ↾_t (𝐶(,)𝐸))
182		unicntop 25012	. . . . . . . . . . . . 13 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
183	182	restid 17519	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ∈ Top → ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld))
184	177, 183	ax-mp 5	. . . . . . . . . . 11 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld)
185	184	eqcomi 2769	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
186	174, 181, 185	cncfcn 25139	. . . . . . . . 9 ⊢ (((𝐶(,)𝐸) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐶(,)𝐸)–cn→ℂ) = (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) Cn (TopOpen‘ℂ_fld)))
187	4, 11, 186	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → ((𝐶(,)𝐸)–cn→ℂ) = (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) Cn (TopOpen‘ℂ_fld)))
188	151, 173, 187	3eltr3d 2874	. . . . . . 7 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) Cn (TopOpen‘ℂ_fld)))
189		retopon 24990	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
190	189	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (topGen‘ran (,)) ∈ (TopOn‘ℝ))
191		resttopon 23387	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (𝐶(,)𝐸) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) ∈ (TopOn‘(𝐶(,)𝐸)))
192	190, 22, 191	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) ∈ (TopOn‘(𝐶(,)𝐸)))
193	174	cnfldtopon 25009	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
194	193	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
195		cncnp 23506	. . . . . . . 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 596	. . . . . . 7 ⊢ (𝜑 → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) Cn (TopOpen‘ℂ_fld)) ↔ (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)):(𝐶(,)𝐸)⟶ℂ ∧ ∀𝑦 ∈ (𝐶(,)𝐸)((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦))))
197	188, 196	mpbid 235	. . . . . 6 ⊢ (𝜑 → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)):(𝐶(,)𝐸)⟶ℂ ∧ ∀𝑦 ∈ (𝐶(,)𝐸)((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦)))
198	197	simprd 501	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ (𝐶(,)𝐸)((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦))
199		dirkercncflem4.ymod0	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 mod (2 · π)) ≠ 0)
200	199	neneqd 2960	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝑌 mod (2 · π)) = 0)
201		mod0 13938	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ ℝ ∧ (2 · π) ∈ ℝ⁺) → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
202	39, 158, 201	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
203	200, 202	mtbid 327	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝑌 / (2 · π)) ∈ ℤ)
204		flltnz 13873	. . . . . . . . . 10 ⊢ (((𝑌 / (2 · π)) ∈ ℝ ∧ ¬ (𝑌 / (2 · π)) ∈ ℤ) → (⌊‘(𝑌 / (2 · π))) < (𝑌 / (2 · π)))
205	50, 203, 204	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) < (𝑌 / (2 · π)))
206	52, 50, 158, 205	ltmul1dd 13142	. . . . . . . 8 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) · (2 · π)) < ((𝑌 / (2 · π)) · (2 · π)))
207	39	recnd 11262	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ ℂ)
208	207, 54, 49	divcan1d 12017	. . . . . . . 8 ⊢ (𝜑 → ((𝑌 / (2 · π)) · (2 · π)) = 𝑌)
209	206, 208	breqtrd 5131	. . . . . . 7 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) · (2 · π)) < 𝑌)
210	37, 209	eqbrtrid 5140	. . . . . 6 ⊢ (𝜑 → 𝐶 < 𝑌)
211		fllelt 13859	. . . . . . . . . 10 ⊢ ((𝑌 / (2 · π)) ∈ ℝ → ((⌊‘(𝑌 / (2 · π))) ≤ (𝑌 / (2 · π)) ∧ (𝑌 / (2 · π)) < ((⌊‘(𝑌 / (2 · π))) + 1)))
212	50, 211	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) ≤ (𝑌 / (2 · π)) ∧ (𝑌 / (2 · π)) < ((⌊‘(𝑌 / (2 · π))) + 1)))
213	212	simprd 501	. . . . . . . 8 ⊢ (𝜑 → (𝑌 / (2 · π)) < ((⌊‘(𝑌 / (2 · π))) + 1))
214	50, 75, 158, 213	ltmul1dd 13142	. . . . . . 7 ⊢ (𝜑 → ((𝑌 / (2 · π)) · (2 · π)) < (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)))
215	214, 208, 73	3brtr3d 5136	. . . . . 6 ⊢ (𝜑 → 𝑌 < 𝐸)
216	64, 78, 39, 210, 215	eliood 46329	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ (𝐶(,)𝐸))
217		fveq2 6879	. . . . . . 7 ⊢ (𝑦 = 𝑌 → ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦) = ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌))
218	217	eleq2d 2846	. . . . . 6 ⊢ (𝑦 = 𝑌 → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦) ↔ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌)))
219	218	rspccva 3575	. . . . 5 ⊢ ((∀𝑦 ∈ (𝐶(,)𝐸)((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦) ∧ 𝑌 ∈ (𝐶(,)𝐸)) → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌))
220	198, 216, 219	syl2anc 596	. . . 4 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌))
221	177	a1i 11	. . . . 5 ⊢ (𝜑 → (TopOpen‘ℂ_fld) ∈ Top)
222	152	dirkerf 46926	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁):ℝ⟶ℝ)
223	5, 222	syl 18	. . . . . 6 ⊢ (𝜑 → (𝐷‘𝑁):ℝ⟶ℝ)
224	223, 22	fssresd 6743	. . . . 5 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)):(𝐶(,)𝐸)⟶ℝ)
225		ax-resscn 11182	. . . . . 6 ⊢ ℝ ⊆ ℂ
226	225	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ⊆ ℂ)
227		retop 24988	. . . . . . 7 ⊢ (topGen‘ran (,)) ∈ Top
228		uniretop 24989	. . . . . . . 8 ⊢ ℝ = ∪ (topGen‘ran (,))
229	228	restuni 23388	. . . . . . 7 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐶(,)𝐸) ⊆ ℝ) → (𝐶(,)𝐸) = ∪ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)))
230	227, 21, 229	mp2an 705	. . . . . 6 ⊢ (𝐶(,)𝐸) = ∪ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸))
231	230, 182	cnprest2 23516	. . . . 5 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)):(𝐶(,)𝐸)⟶ℝ ∧ ℝ ⊆ ℂ) → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌) ↔ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ))‘𝑌)))
232	221, 224, 226, 231	syl3anc 1398	. . . 4 ⊢ (𝜑 → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌) ↔ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ))‘𝑌)))
233	220, 232	mpbid 235	. . 3 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ))‘𝑌))
234	175	eqcomi 2769	. . . . . 6 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℝ) = (topGen‘ran (,))
235	234	a1i 11	. . . . 5 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t ℝ) = (topGen‘ran (,)))
236	235	oveq2d 7430	. . . 4 ⊢ (𝜑 → (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ)) = (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,))))
237	236	fveq1d 6881	. . 3 ⊢ (𝜑 → ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ))‘𝑌) = ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,)))‘𝑌))
238	233, 237	eleqtrd 2862	. 2 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,)))‘𝑌))
239	227	a1i 11	. . 3 ⊢ (𝜑 → (topGen‘ran (,)) ∈ Top)
240		iooretop 24992	. . . . . . 7 ⊢ (𝐶(,)𝐸) ∈ (topGen‘ran (,))
241	228	isopn3 23292	. . . . . . 7 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐶(,)𝐸) ⊆ ℝ) → ((𝐶(,)𝐸) ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)) = (𝐶(,)𝐸)))
242	240, 241	mpbii 236	. . . . . 6 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐶(,)𝐸) ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)) = (𝐶(,)𝐸))
243	239, 22, 242	syl2anc 596	. . . . 5 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)) = (𝐶(,)𝐸))
244	243	eqcomd 2766	. . . 4 ⊢ (𝜑 → (𝐶(,)𝐸) = ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)))
245	216, 244	eleqtrd 2862	. . 3 ⊢ (𝜑 → 𝑌 ∈ ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)))
246	228, 228	cnprest 23515	. . 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 852	. 2 ⊢ (𝜑 → ((𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP (topGen‘ran (,)))‘𝑌) ↔ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,)))‘𝑌)))
248	238, 247	mpbird 260	1 ⊢ (𝜑 → (𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP (topGen‘ran (,)))‘𝑌))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ∀wral 3076 Vcvv 3450 ∖ cdif 3896 ⊆ wss 3899 ifcif 4482 {csn 4584 ∪ cuni 4867 class class class wbr 5103 ↦ cmpt 5186 ran crn 5656 ↾ cres 5657 ∘ ccom 5659 ⟶wf 6529 ‘cfv 6533 (class class class)co 7414 ℂcc 11123 ℝcr 11124 0cc0 11125 1c1 11126 + caddc 11128 · cmul 11130 ℝ^*cxr 11267 < clt 11268 ≤ cle 11269 / cdiv 11896 ℕcn 12258 2c2 12320 ℤcz 12616 ℝ⁺crp 13043 (,)cioo 13399 ⌊cfl 13852 mod cmo 13931 sincsin 16150 πcpi 16153 ↾_t crest 17506 TopOpenctopn 17507 topGenctg 17523 ℂ_fldccnfld 21586 Topctop 23119 TopOnctopon 23136 intcnt 23243 Cn ccn 23450 CnP ccnp 23451 –cn→ccncf 25105

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-inf2 9621 ax-cnex 11181 ax-resscn 11182 ax-1cn 11183 ax-icn 11184 ax-addcl 11185 ax-addrcl 11186 ax-mulcl 11187 ax-mulrcl 11188 ax-mulcom 11189 ax-addass 11190 ax-mulass 11191 ax-distr 11192 ax-i2m1 11193 ax-1ne0 11194 ax-1rid 11195 ax-rnegex 11196 ax-rrecex 11197 ax-cnre 11198 ax-pre-lttri 11199 ax-pre-lttrn 11200 ax-pre-ltadd 11201 ax-pre-mulgt0 11202 ax-pre-sup 11203 ax-addf 11204

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-of 7679 df-om 7864 df-1st 7987 df-2nd 7988 df-supp 8160 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8456 df-2o 8457 df-er 8697 df-map 8829 df-pm 8830 df-ixp 8906 df-en 8954 df-dom 8955 df-sdom 8956 df-fin 8957 df-fsupp 9333 df-fi 9382 df-sup 9413 df-inf 9414 df-oi 9483 df-card 9945 df-pnf 11270 df-mnf 11271 df-xr 11272 df-ltxr 11273 df-le 11274 df-sub 11468 df-neg 11469 df-div 11897 df-nn 12259 df-2 12328 df-3 12329 df-4 12330 df-5 12331 df-6 12332 df-7 12333 df-8 12334 df-9 12335 df-n0 12530 df-z 12617 df-dec 12738 df-uz 12889 df-q 12999 df-rp 13044 df-xneg 13164 df-xadd 13165 df-xmul 13166 df-ioo 13403 df-ioc 13404 df-ico 13405 df-icc 13406 df-fz 13563 df-fzo 13711 df-fl 13854 df-mod 13932 df-seq 14067 df-exp 14127 df-fac 14339 df-bc 14368 df-hash 14396 df-shft 15141 df-cj 15187 df-re 15188 df-im 15189 df-sqrt 15323 df-abs 15324 df-limsup 15559 df-clim 15576 df-rlim 15577 df-sum 15775 df-ef 16154 df-sin 16156 df-cos 16157 df-pi 16159 df-struct 17240 df-sets 17257 df-slot 17275 df-ndx 17287 df-base 17303 df-ress 17324 df-plusg 17356 df-mulr 17357 df-starv 17358 df-sca 17359 df-vsca 17360 df-ip 17361 df-tset 17362 df-ple 17363 df-ds 17365 df-unif 17366 df-hom 17367 df-cco 17368 df-rest 17508 df-topn 17509 df-0g 17527 df-gsum 17528 df-topgen 17529 df-pt 17530 df-prds 17533 df-xrs 17589 df-qtop 17594 df-imas 17595 df-xps 17597 df-mre 17671 df-mrc 17672 df-acs 17674 df-mgm 18731 df-sgrp 18822 df-mnd 18838 df-submnd 18893 df-mulg 19192 df-cntz 19445 df-cmn 19910 df-psmet 21578 df-xmet 21579 df-met 21580 df-bl 21581 df-mopn 21582 df-fbas 21583 df-fg 21584 df-cnfld 21587 df-top 23120 df-topon 23137 df-topsp 23159 df-bases 23172 df-cld 23245 df-ntr 23246 df-cls 23247 df-nei 23324 df-lp 23362 df-perf 23363 df-cn 23453 df-cnp 23454 df-haus 23541 df-tx 23789 df-hmeo 23982 df-fil 24073 df-fm 24165 df-flim 24166 df-flf 24167 df-xms 24547 df-ms 24548 df-tms 24549 df-cncf 25107 df-limc 26094 df-dv 26095

This theorem is used by: dirkercncf 46936

W3C validator