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 43654

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 25612	. . . . . . . . . . 11 ⊢ sin ∈ (ℂ–cn→ℂ)
2	1	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → sin ∈ (ℂ–cn→ℂ))
3		ioosscn 13150	. . . . . . . . . . . . 13 ⊢ (𝐶(,)𝐸) ⊆ ℂ
4	3	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶(,)𝐸) ⊆ ℂ)
5		dirkercncflem4.n	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	nncnd 11998	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
7		1cnd 10979	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℂ)
8	7	halfcld 12227	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
9	6, 8	addcld 11003	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ)
10		ssid 3944	. . . . . . . . . . . . 13 ⊢ ℂ ⊆ ℂ
11	10	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ ⊆ ℂ)
12	4, 9, 11	constcncfg 43420	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑁 + (1 / 2))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
13	4, 11	idcncfg 43421	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ 𝑦) ∈ ((𝐶(,)𝐸)–cn→ℂ))
14	12, 13	mulcncf 24619	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
15	2, 14	cncfmpt1f 24086	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
16		2cnd 12060	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ∈ ℂ)
17		pirp 25627	. . . . . . . . . . . . . . . 16 ⊢ π ∈ ℝ⁺
18	17	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ∈ ℝ⁺)
19	18	rpcnd 12783	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ∈ ℂ)
20	16, 19	mulcld 11004	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℂ)
21		ioossre 13149	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶(,)𝐸) ⊆ ℝ
22	21	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐶(,)𝐸) ⊆ ℝ)
23	22	sselda 3922	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 ∈ ℝ)
24	23	recnd 11012	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 ∈ ℂ)
25	24	halfcld 12227	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / 2) ∈ ℂ)
26	25	sincld 15848	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘(𝑦 / 2)) ∈ ℂ)
27	20, 26	mulcld 11004	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
28		2rp 12744	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ⁺
29	28	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ∈ ℝ⁺)
30	29	rpne0d 12786	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ≠ 0)
31	18	rpne0d 12786	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ≠ 0)
32	16, 19, 30, 31	mulne0d 11636	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ≠ 0)
33	24, 16, 19, 30, 31	divdiv1d 11791	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
34		dirkercncflem4.c	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝐶 = (𝐴 · (2 · π))
35		dirkercncflem4.a	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐴 = (⌊‘(𝑌 / (2 · π)))
36	35	oveq1i 7294	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 · (2 · π)) = ((⌊‘(𝑌 / (2 · π))) · (2 · π))
37	34, 36	eqtri 2767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐶 = ((⌊‘(𝑌 / (2 · π))) · (2 · π))
38	37	oveq1i 7294	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐶 / (2 · π)) = (((⌊‘(𝑌 / (2 · π))) · (2 · π)) / (2 · π))
39		dirkercncflem4.y	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑌 ∈ ℝ)
40		2re 12056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 2 ∈ ℝ
41		pire 25624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ π ∈ ℝ
42	40, 41	remulcli 11000	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (2 · π) ∈ ℝ
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (2 · π) ∈ ℝ)
44		0re 10986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 ∈ ℝ
45		2pos 12085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 < 2
46		pipos 25626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 < π
47	40, 41, 45, 46	mulgt0ii 11117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 < (2 · π)
48	44, 47	gtneii 11096	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (2 · π) ≠ 0
49	48	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (2 · π) ≠ 0)
50	39, 43, 49	redivcld 11812	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑌 / (2 · π)) ∈ ℝ)
51	50	flcld 13527	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) ∈ ℤ)
52	51	zred 12435	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) ∈ ℝ)
53	52	recnd 11012	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) ∈ ℂ)
54	43	recnd 11012	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (2 · π) ∈ ℂ)
55	53, 54, 49	divcan4d 11766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((⌊‘(𝑌 / (2 · π))) · (2 · π)) / (2 · π)) = (⌊‘(𝑌 / (2 · π))))
56	38, 55	eqtrid 2791	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐶 / (2 · π)) = (⌊‘(𝑌 / (2 · π))))
57	56, 51	eqeltrd 2840	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐶 / (2 · π)) ∈ ℤ)
58	57	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝐶 / (2 · π)) ∈ ℤ)
59	52, 43	remulcld 11014	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) · (2 · π)) ∈ ℝ)
60	37, 59	eqeltrid 2844	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐶 ∈ ℝ)
61	60	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐶 ∈ ℝ)
62	29, 18	rpmulcld 12797	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℝ⁺)
63		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 ∈ (𝐶(,)𝐸))
64	60	rexrd 11034	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
65	64	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐶 ∈ ℝ^*)
66	35	eqcomi 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⌊‘(𝑌 / (2 · π))) = 𝐴
67	66	oveq1i 7294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((⌊‘(𝑌 / (2 · π))) + 1) = (𝐴 + 1)
68		dirkercncflem4.b	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 𝐵 = (𝐴 + 1)
69	67, 68	eqtr4i 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((⌊‘(𝑌 / (2 · π))) + 1) = 𝐵
70	69	oveq1i 7294	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) = (𝐵 · (2 · π))
71		dirkercncflem4.e	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝐸 = (𝐵 · (2 · π))
72	70, 71	eqtr4i 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) = 𝐸
73	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) = 𝐸)
74		1red 10985	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 1 ∈ ℝ)
75	52, 74	readdcld 11013	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) + 1) ∈ ℝ)
76	75, 43	remulcld 11014	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)) ∈ ℝ)
77	73, 76	eqeltrrd 2841	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐸 ∈ ℝ)
78	77	rexrd 11034	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐸 ∈ ℝ^*)
79	78	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐸 ∈ ℝ^*)
80		elioo2 13129	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐸 ∈ ℝ^*) → (𝑦 ∈ (𝐶(,)𝐸) ↔ (𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸)))
81	65, 79, 80	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 ∈ (𝐶(,)𝐸) ↔ (𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸)))
82	63, 81	mpbid 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 ∈ ℝ ∧ 𝐶 < 𝑦 ∧ 𝑦 < 𝐸))
83	82	simp2d 1142	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐶 < 𝑦)
84	61, 23, 62, 83	ltdiv1dd 12838	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝐶 / (2 · π)) < (𝑦 / (2 · π)))
85	77	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝐸 ∈ ℝ)
86	82	simp3d 1143	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑦 < 𝐸)
87	23, 85, 62, 86	ltdiv1dd 12838	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / (2 · π)) < (𝐸 / (2 · π)))
88	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐶 = (𝐴 · (2 · π)))
89	88	oveq1d 7299	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐶 / (2 · π)) = ((𝐴 · (2 · π)) / (2 · π)))
90	89	oveq1d 7299	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝐶 / (2 · π)) + 1) = (((𝐴 · (2 · π)) / (2 · π)) + 1))
91	35, 53	eqeltrid 2844	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐴 ∈ ℂ)
92	91, 54, 49	divcan4d 11766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 · (2 · π)) / (2 · π)) = 𝐴)
93	92	oveq1d 7299	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝐴 · (2 · π)) / (2 · π)) + 1) = (𝐴 + 1))
94	68	oveq1i 7294	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐵 · (2 · π)) = ((𝐴 + 1) · (2 · π))
95	71, 94	eqtri 2767	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐸 = ((𝐴 + 1) · (2 · π))
96	95	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐸 = ((𝐴 + 1) · (2 · π)))
97	96	oveq1d 7299	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐸 / (2 · π)) = (((𝐴 + 1) · (2 · π)) / (2 · π)))
98	91, 7	addcld 11003	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 + 1) ∈ ℂ)
99	98, 54, 49	divcan4d 11766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴 + 1) · (2 · π)) / (2 · π)) = (𝐴 + 1))
100	97, 99	eqtr2d 2780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴 + 1) = (𝐸 / (2 · π)))
101	90, 93, 100	3eqtrrd 2784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 / (2 · π)) = ((𝐶 / (2 · π)) + 1))
102	101	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝐸 / (2 · π)) = ((𝐶 / (2 · π)) + 1))
103	87, 102	breqtrd 5101	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / (2 · π)) < ((𝐶 / (2 · π)) + 1))
104		btwnnz 12405	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶 / (2 · π)) ∈ ℤ ∧ (𝐶 / (2 · π)) < (𝑦 / (2 · π)) ∧ (𝑦 / (2 · π)) < ((𝐶 / (2 · π)) + 1)) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
105	58, 84, 103, 104	syl3anc 1370	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
106	33, 105	eqneltrd 2859	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ ((𝑦 / 2) / π) ∈ ℤ)
107		sineq0 25689	. . . . . . . . . . . . . . . . . 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 2951	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘(𝑦 / 2)) ≠ 0)
111	20, 26, 32, 110	mulne0d 11636	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ≠ 0)
112	111	neneqd 2949	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ¬ ((2 · π) · (sin‘(𝑦 / 2))) = 0)
113	40	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 2 ∈ ℝ)
114	41	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → π ∈ ℝ)
115	113, 114	remulcld 11014	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℝ)
116	23	rehalfcld 12229	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / 2) ∈ ℝ)
117	116	resincld 15861	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘(𝑦 / 2)) ∈ ℝ)
118	115, 117	remulcld 11014	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℝ)
119		elsng 4576	. . . . . . . . . . . . . 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 3899	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ (ℂ ∖ {0}))
123		eqidd 2740	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))))
124		eqidd 2740	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)))
125		oveq2 7292	. . . . . . . . . . 11 ⊢ (𝑥 = ((2 · π) · (sin‘(𝑦 / 2))) → (1 / 𝑥) = (1 / ((2 · π) · (sin‘(𝑦 / 2)))))
126	122, 123, 124, 125	fmptco 7010	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∘ (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ (𝐶(,)𝐸) ↦ (1 / ((2 · π) · (sin‘(𝑦 / 2))))))
127		eqid 2739	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
128		2cnd 12060	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℂ)
129	4, 128, 11	constcncfg 43420	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ 2) ∈ ((𝐶(,)𝐸)–cn→ℂ))
130	17	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → π ∈ ℝ⁺)
131	130	rpcnd 12783	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → π ∈ ℂ)
132	4, 131, 11	constcncfg 43420	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ π) ∈ ((𝐶(,)𝐸)–cn→ℂ))
133	129, 132	mulcncf 24619	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (2 · π)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
134	24, 16, 30	divrecd 11763	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑦 / 2) = (𝑦 · (1 / 2)))
135	134	mpteq2dva 5175	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 / 2)) = (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 · (1 / 2))))
136	4, 8, 11	constcncfg 43420	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (1 / 2)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
137	13, 136	mulcncf 24619	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 · (1 / 2))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
138	135, 137	eqeltrd 2840	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (𝑦 / 2)) ∈ ((𝐶(,)𝐸)–cn→ℂ))
139	2, 138	cncfmpt1f 24086	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (sin‘(𝑦 / 2))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
140	133, 139	mulcncf 24619	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
141		ssid 3944	. . . . . . . . . . . . 13 ⊢ (𝐶(,)𝐸) ⊆ (𝐶(,)𝐸)
142	141	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶(,)𝐸) ⊆ (𝐶(,)𝐸))
143		difssd 4068	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
144	127, 140, 142, 143, 122	cncfmptssg 43419	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ∈ ((𝐶(,)𝐸)–cn→(ℂ ∖ {0})))
145		ax-1cn 10938	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
146		eqid 2739	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥))
147	146	cdivcncf 24093	. . . . . . . . . . . 12 ⊢ (1 ∈ ℂ → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∈ ((ℂ ∖ {0})–cn→ℂ))
148	145, 147	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∈ ((ℂ ∖ {0})–cn→ℂ))
149	144, 148	cncfco 24079	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑥)) ∘ (𝑦 ∈ (𝐶(,)𝐸) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
150	126, 149	eqeltrrd 2841	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ (1 / ((2 · π) · (sin‘(𝑦 / 2))))) ∈ ((𝐶(,)𝐸)–cn→ℂ))
151	15, 150	mulcncf 24619	. . . . . . . 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 43639	. . . . . . . . . . 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 5893	. . . . . . . . 9 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) = ((𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) ↾ (𝐶(,)𝐸)))
156	22	resmptd 5951	. . . . . . . . 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 12797	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · π) ∈ ℝ⁺)
159	158	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (2 · π) ∈ ℝ⁺)
160		mod0 13605	. . . . . . . . . . . . . 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 4471	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
164	6	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 𝑁 ∈ ℂ)
165		1cnd 10979	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → 1 ∈ ℂ)
166	165	halfcld 12227	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (1 / 2) ∈ ℂ)
167	164, 166	addcld 11003	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (𝑁 + (1 / 2)) ∈ ℂ)
168	167, 24	mulcld 11004	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
169	168	sincld 15848	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
170	169, 27, 111	divrecd 11763	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2))))))
171	163, 170	eqtrd 2779	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐶(,)𝐸)) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2))))))
172	171	mpteq2dva 5175	. . . . . . . . 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 2784	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ (𝐶(,)𝐸) ↦ ((sin‘((𝑁 + (1 / 2)) · 𝑦)) · (1 / ((2 · π) · (sin‘(𝑦 / 2)))))) = ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)))
174		eqid 2739	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
175	174	tgioo2 23975	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
176	175	oveq1i 7294	. . . . . . . . . . 11 ⊢ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) = (((TopOpen‘ℂ_fld) ↾_t ℝ) ↾_t (𝐶(,)𝐸))
177	174	cnfldtop 23956	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) ∈ Top
178		reex 10971	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
179		restabs 22325	. . . . . . . . . . . 12 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ (𝐶(,)𝐸) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂ_fld) ↾_t ℝ) ↾_t (𝐶(,)𝐸)) = ((TopOpen‘ℂ_fld) ↾_t (𝐶(,)𝐸)))
180	177, 21, 178, 179	mp3an 1460	. . . . . . . . . . 11 ⊢ (((TopOpen‘ℂ_fld) ↾_t ℝ) ↾_t (𝐶(,)𝐸)) = ((TopOpen‘ℂ_fld) ↾_t (𝐶(,)𝐸))
181	176, 180	eqtri 2767	. . . . . . . . . 10 ⊢ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) = ((TopOpen‘ℂ_fld) ↾_t (𝐶(,)𝐸))
182		unicntop 23958	. . . . . . . . . . . . 13 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
183	182	restid 17153	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ∈ Top → ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld))
184	177, 183	ax-mp 5	. . . . . . . . . . 11 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld)
185	184	eqcomi 2748	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
186	174, 181, 185	cncfcn 24082	. . . . . . . . 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 2854	. . . . . . 7 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) Cn (TopOpen‘ℂ_fld)))
189		retopon 23936	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ)
190	189	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (topGen‘ran (,)) ∈ (TopOn‘ℝ))
191		resttopon 22321	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (𝐶(,)𝐸) ⊆ ℝ) → ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) ∈ (TopOn‘(𝐶(,)𝐸)))
192	190, 22, 191	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) ∈ (TopOn‘(𝐶(,)𝐸)))
193	174	cnfldtopon 23955	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
194	193	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
195		cncnp 22440	. . . . . . . 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 231	. . . . . 6 ⊢ (𝜑 → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)):(𝐶(,)𝐸)⟶ℂ ∧ ∀𝑦 ∈ (𝐶(,)𝐸)((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦)))
198	197	simprd 496	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ (𝐶(,)𝐸)((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦))
199		dirkercncflem4.ymod0	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 mod (2 · π)) ≠ 0)
200	199	neneqd 2949	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝑌 mod (2 · π)) = 0)
201		mod0 13605	. . . . . . . . . . . 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 13540	. . . . . . . . . 10 ⊢ (((𝑌 / (2 · π)) ∈ ℝ ∧ ¬ (𝑌 / (2 · π)) ∈ ℤ) → (⌊‘(𝑌 / (2 · π))) < (𝑌 / (2 · π)))
205	50, 203, 204	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (⌊‘(𝑌 / (2 · π))) < (𝑌 / (2 · π)))
206	52, 50, 158, 205	ltmul1dd 12836	. . . . . . . 8 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) · (2 · π)) < ((𝑌 / (2 · π)) · (2 · π)))
207	39	recnd 11012	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ ℂ)
208	207, 54, 49	divcan1d 11761	. . . . . . . 8 ⊢ (𝜑 → ((𝑌 / (2 · π)) · (2 · π)) = 𝑌)
209	206, 208	breqtrd 5101	. . . . . . 7 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) · (2 · π)) < 𝑌)
210	37, 209	eqbrtrid 5110	. . . . . 6 ⊢ (𝜑 → 𝐶 < 𝑌)
211		fllelt 13526	. . . . . . . . . 10 ⊢ ((𝑌 / (2 · π)) ∈ ℝ → ((⌊‘(𝑌 / (2 · π))) ≤ (𝑌 / (2 · π)) ∧ (𝑌 / (2 · π)) < ((⌊‘(𝑌 / (2 · π))) + 1)))
212	50, 211	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((⌊‘(𝑌 / (2 · π))) ≤ (𝑌 / (2 · π)) ∧ (𝑌 / (2 · π)) < ((⌊‘(𝑌 / (2 · π))) + 1)))
213	212	simprd 496	. . . . . . . 8 ⊢ (𝜑 → (𝑌 / (2 · π)) < ((⌊‘(𝑌 / (2 · π))) + 1))
214	50, 75, 158, 213	ltmul1dd 12836	. . . . . . 7 ⊢ (𝜑 → ((𝑌 / (2 · π)) · (2 · π)) < (((⌊‘(𝑌 / (2 · π))) + 1) · (2 · π)))
215	214, 208, 73	3brtr3d 5106	. . . . . 6 ⊢ (𝜑 → 𝑌 < 𝐸)
216	64, 78, 39, 210, 215	eliood 43043	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ (𝐶(,)𝐸))
217		fveq2 6783	. . . . . . 7 ⊢ (𝑦 = 𝑌 → ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦) = ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌))
218	217	eleq2d 2825	. . . . . 6 ⊢ (𝑦 = 𝑌 → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑦) ↔ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌)))
219	218	rspccva 3561	. . . . 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 43645	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁):ℝ⟶ℝ)
223	5, 222	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐷‘𝑁):ℝ⟶ℝ)
224	223, 22	fssresd 6650	. . . . 5 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)):(𝐶(,)𝐸)⟶ℝ)
225		ax-resscn 10937	. . . . . 6 ⊢ ℝ ⊆ ℂ
226	225	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ⊆ ℂ)
227		retop 23934	. . . . . . 7 ⊢ (topGen‘ran (,)) ∈ Top
228		uniretop 23935	. . . . . . . 8 ⊢ ℝ = ∪ (topGen‘ran (,))
229	228	restuni 22322	. . . . . . 7 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐶(,)𝐸) ⊆ ℝ) → (𝐶(,)𝐸) = ∪ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)))
230	227, 21, 229	mp2an 689	. . . . . 6 ⊢ (𝐶(,)𝐸) = ∪ ((topGen‘ran (,)) ↾_t (𝐶(,)𝐸))
231	230, 182	cnprest2 22450	. . . . 5 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)):(𝐶(,)𝐸)⟶ℝ ∧ ℝ ⊆ ℂ) → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌) ↔ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ))‘𝑌)))
232	221, 224, 226, 231	syl3anc 1370	. . . 4 ⊢ (𝜑 → (((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (TopOpen‘ℂ_fld))‘𝑌) ↔ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ))‘𝑌)))
233	220, 232	mpbid 231	. . 3 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ))‘𝑌))
234	175	eqcomi 2748	. . . . . 6 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℝ) = (topGen‘ran (,))
235	234	a1i 11	. . . . 5 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t ℝ) = (topGen‘ran (,)))
236	235	oveq2d 7300	. . . 4 ⊢ (𝜑 → (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ)) = (((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,))))
237	236	fveq1d 6785	. . 3 ⊢ (𝜑 → ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP ((TopOpen‘ℂ_fld) ↾_t ℝ))‘𝑌) = ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,)))‘𝑌))
238	233, 237	eleqtrd 2842	. 2 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,)))‘𝑌))
239	227	a1i 11	. . 3 ⊢ (𝜑 → (topGen‘ran (,)) ∈ Top)
240		iooretop 23938	. . . . . . 7 ⊢ (𝐶(,)𝐸) ∈ (topGen‘ran (,))
241	228	isopn3 22226	. . . . . . 7 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐶(,)𝐸) ⊆ ℝ) → ((𝐶(,)𝐸) ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)) = (𝐶(,)𝐸)))
242	240, 241	mpbii 232	. . . . . 6 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐶(,)𝐸) ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)) = (𝐶(,)𝐸))
243	239, 22, 242	syl2anc 584	. . . . 5 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)) = (𝐶(,)𝐸))
244	243	eqcomd 2745	. . . 4 ⊢ (𝜑 → (𝐶(,)𝐸) = ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)))
245	216, 244	eleqtrd 2842	. . 3 ⊢ (𝜑 → 𝑌 ∈ ((int‘(topGen‘ran (,)))‘(𝐶(,)𝐸)))
246	228, 228	cnprest 22449	. . 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 836	. 2 ⊢ (𝜑 → ((𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP (topGen‘ran (,)))‘𝑌) ↔ ((𝐷‘𝑁) ↾ (𝐶(,)𝐸)) ∈ ((((topGen‘ran (,)) ↾_t (𝐶(,)𝐸)) CnP (topGen‘ran (,)))‘𝑌)))
248	238, 247	mpbird 256	1 ⊢ (𝜑 → (𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP (topGen‘ran (,)))‘𝑌))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2944 ∀wral 3065 Vcvv 3433 ∖ cdif 3885 ⊆ wss 3888 ifcif 4460 {csn 4562 ∪ cuni 4840 class class class wbr 5075 ↦ cmpt 5158 ran crn 5591 ↾ cres 5592 ∘ ccom 5594 ⟶wf 6433 ‘cfv 6437 (class class class)co 7284 ℂcc 10878 ℝcr 10879 0cc0 10880 1c1 10881 + caddc 10883 · cmul 10885 ℝ^*cxr 11017 < clt 11018 ≤ cle 11019 / cdiv 11641 ℕcn 11982 2c2 12037 ℤcz 12328 ℝ⁺crp 12739 (,)cioo 13088 ⌊cfl 13519 mod cmo 13598 sincsin 15782 πcpi 15785 ↾_t crest 17140 TopOpenctopn 17141 topGenctg 17157 ℂ_fldccnfld 20606 Topctop 22051 TopOnctopon 22068 intcnt 22177 Cn ccn 22384 CnP ccnp 22385 –cn→ccncf 24048

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2710 ax-rep 5210 ax-sep 5224 ax-nul 5231 ax-pow 5289 ax-pr 5353 ax-un 7597 ax-inf2 9408 ax-cnex 10936 ax-resscn 10937 ax-1cn 10938 ax-icn 10939 ax-addcl 10940 ax-addrcl 10941 ax-mulcl 10942 ax-mulrcl 10943 ax-mulcom 10944 ax-addass 10945 ax-mulass 10946 ax-distr 10947 ax-i2m1 10948 ax-1ne0 10949 ax-1rid 10950 ax-rnegex 10951 ax-rrecex 10952 ax-cnre 10953 ax-pre-lttri 10954 ax-pre-lttrn 10955 ax-pre-ltadd 10956 ax-pre-mulgt0 10957 ax-pre-sup 10958 ax-addf 10959 ax-mulf 10960

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-rmo 3072 df-reu 3073 df-rab 3074 df-v 3435 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4841 df-int 4881 df-iun 4927 df-iin 4928 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-se 5546 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6395 df-fun 6439 df-fn 6440 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444 df-fv 6445 df-isom 6446 df-riota 7241 df-ov 7287 df-oprab 7288 df-mpo 7289 df-of 7542 df-om 7722 df-1st 7840 df-2nd 7841 df-supp 7987 df-frecs 8106 df-wrecs 8137 df-recs 8211 df-rdg 8250 df-1o 8306 df-2o 8307 df-er 8507 df-map 8626 df-pm 8627 df-ixp 8695 df-en 8743 df-dom 8744 df-sdom 8745 df-fin 8746 df-fsupp 9138 df-fi 9179 df-sup 9210 df-inf 9211 df-oi 9278 df-card 9706 df-pnf 11020 df-mnf 11021 df-xr 11022 df-ltxr 11023 df-le 11024 df-sub 11216 df-neg 11217 df-div 11642 df-nn 11983 df-2 12045 df-3 12046 df-4 12047 df-5 12048 df-6 12049 df-7 12050 df-8 12051 df-9 12052 df-n0 12243 df-z 12329 df-dec 12447 df-uz 12592 df-q 12698 df-rp 12740 df-xneg 12857 df-xadd 12858 df-xmul 12859 df-ioo 13092 df-ioc 13093 df-ico 13094 df-icc 13095 df-fz 13249 df-fzo 13392 df-fl 13521 df-mod 13599 df-seq 13731 df-exp 13792 df-fac 13997 df-bc 14026 df-hash 14054 df-shft 14787 df-cj 14819 df-re 14820 df-im 14821 df-sqrt 14955 df-abs 14956 df-limsup 15189 df-clim 15206 df-rlim 15207 df-sum 15407 df-ef 15786 df-sin 15788 df-cos 15789 df-pi 15791 df-struct 16857 df-sets 16874 df-slot 16892 df-ndx 16904 df-base 16922 df-ress 16951 df-plusg 16984 df-mulr 16985 df-starv 16986 df-sca 16987 df-vsca 16988 df-ip 16989 df-tset 16990 df-ple 16991 df-ds 16993 df-unif 16994 df-hom 16995 df-cco 16996 df-rest 17142 df-topn 17143 df-0g 17161 df-gsum 17162 df-topgen 17163 df-pt 17164 df-prds 17167 df-xrs 17222 df-qtop 17227 df-imas 17228 df-xps 17230 df-mre 17304 df-mrc 17305 df-acs 17307 df-mgm 18335 df-sgrp 18384 df-mnd 18395 df-submnd 18440 df-mulg 18710 df-cntz 18932 df-cmn 19397 df-psmet 20598 df-xmet 20599 df-met 20600 df-bl 20601 df-mopn 20602 df-fbas 20603 df-fg 20604 df-cnfld 20607 df-top 22052 df-topon 22069 df-topsp 22091 df-bases 22105 df-cld 22179 df-ntr 22180 df-cls 22181 df-nei 22258 df-lp 22296 df-perf 22297 df-cn 22387 df-cnp 22388 df-haus 22475 df-tx 22722 df-hmeo 22915 df-fil 23006 df-fm 23098 df-flim 23099 df-flf 23100 df-xms 23482 df-ms 23483 df-tms 23484 df-cncf 24050 df-limc 25039 df-dv 25040

This theorem is referenced by: dirkercncf 43655

W3C validator