dirkercncflem2 - Mathbox for Glauco Siliprandi

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

Theorem dirkercncflem2 46554

Description: Lemma used to prove that the Dirichlet kernel is continuous at 𝑌 points that are multiples of (2 · π). (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
dirkercncflem2.d	⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
dirkercncflem2.f	⊢ 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
dirkercncflem2.g	⊢ 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
dirkercncflem2.yne0	⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ≠ 0)
dirkercncflem2.h	⊢ 𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
dirkercncflem2.i	⊢ 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2))))
dirkercncflem2.l	⊢ 𝐿 = (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))))
dirkercncflem2.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
dirkercncflem2.y	⊢ (𝜑 → 𝑌 ∈ (𝐴(,)𝐵))
dirkercncflem2.ymod	⊢ (𝜑 → (𝑌 mod (2 · π)) = 0)
dirkercncflem2.11	⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0)

**Assertion**
Ref	Expression
dirkercncflem2	⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ (((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) lim_ℂ 𝑌))

Distinct variable groups: 𝑤,𝐴,𝑦 𝑤,𝐵,𝑦 𝑦,𝐷 𝑤,𝐹,𝑦 𝑤,𝐺,𝑦 𝑤,𝐻,𝑦 𝑤,𝐼,𝑦 𝑦,𝐿 𝑤,𝑁,𝑦 𝑤,𝑌,𝑦 𝑦,𝑛 𝜑,𝑤,𝑦 Allowed substitution hints: 𝜑(𝑛) 𝐴(𝑛) 𝐵(𝑛) 𝐷(𝑤,𝑛) 𝐹(𝑛) 𝐺(𝑛) 𝐻(𝑛) 𝐼(𝑛) 𝐿(𝑤,𝑛) 𝑁(𝑛) 𝑌(𝑛)

**Proof of Theorem dirkercncflem2**
Step	Hyp	Ref	Expression
1		difss 4073	. . . . 5 ⊢ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ (𝐴(,)𝐵)
2		ioossre 13358	. . . . 5 ⊢ (𝐴(,)𝐵) ⊆ ℝ
3	1, 2	sstri 3931	. . . 4 ⊢ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ
4	3	a1i 11	. . 3 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)
5		dirkercncflem2.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℕ)
7	6	nnred 12187	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℝ)
8		halfre 12388	. . . . . . . 8 ⊢ (1 / 2) ∈ ℝ
9	8	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈ ℝ)
10	7, 9	readdcld 11172	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑁 + (1 / 2)) ∈ ℝ)
11	4	sselda 3922	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℝ)
12	10, 11	remulcld 11173	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℝ)
13	12	resincld 16108	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℝ)
14		dirkercncflem2.f	. . . 4 ⊢ 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
15	13, 14	fmptd 7062	. . 3 ⊢ (𝜑 → 𝐹:((𝐴(,)𝐵) ∖ {𝑌})⟶ℝ)
16		2re 12253	. . . . . . 7 ⊢ 2 ∈ ℝ
17		pire 26446	. . . . . . 7 ⊢ π ∈ ℝ
18	16, 17	remulcli 11159	. . . . . 6 ⊢ (2 · π) ∈ ℝ
19	18	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈ ℝ)
20	11	rehalfcld 12422	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℝ)
21	20	resincld 16108	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ∈ ℝ)
22	19, 21	remulcld 11173	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℝ)
23		dirkercncflem2.g	. . . 4 ⊢ 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
24	22, 23	fmptd 7062	. . 3 ⊢ (𝜑 → 𝐺:((𝐴(,)𝐵) ∖ {𝑌})⟶ℝ)
25		iooretop 24755	. . . 4 ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))
26	25	a1i 11	. . 3 ⊢ (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran (,)))
27		dirkercncflem2.y	. . 3 ⊢ (𝜑 → 𝑌 ∈ (𝐴(,)𝐵))
28		eqid 2740	. . 3 ⊢ ((𝐴(,)𝐵) ∖ {𝑌}) = ((𝐴(,)𝐵) ∖ {𝑌})
29	14	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
30	29	oveq2d 7379	. . . . . . 7 ⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
31		resmpt 5996	. . . . . . . . . . . 12 ⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
32	3, 31	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
33	32	eqcomi 2749	. . . . . . . . . 10 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))
34	33	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
35	34	oveq2d 7379	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))))
36		ax-resscn 11093	. . . . . . . . . 10 ⊢ ℝ ⊆ ℂ
37	36	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℝ ⊆ ℂ)
38	5	nncnd 12188	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℂ)
39		halfcn 12389	. . . . . . . . . . . . . . 15 ⊢ (1 / 2) ∈ ℂ
40	39	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
41	38, 40	addcld 11162	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ)
42	41	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑁 + (1 / 2)) ∈ ℂ)
43	37	sselda 3922	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
44	42, 43	mulcld 11163	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
45	44	sincld 16095	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
46		eqid 2740	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
47	45, 46	fmptd 7062	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℝ⟶ℂ)
48		ssid 3944	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℝ
49	48, 3	pm3.2i 471	. . . . . . . . . 10 ⊢ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)
50	49	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ))
51		eqid 2740	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
52		tgioo4 24795	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
53	51, 52	dvres 25903	. . . . . . . . 9 ⊢ (((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)) → (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
54	37, 47, 50, 53	syl21anc 843	. . . . . . . 8 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
55		retop 24751	. . . . . . . . . . 11 ⊢ (topGen‘ran (,)) ∈ Top
56		rehaus 24789	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) ∈ Haus
57	27	elioored 46001	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ ℝ)
58		uniretop 24752	. . . . . . . . . . . . . 14 ⊢ ℝ = ∪ (topGen‘ran (,))
59	58	sncld 23361	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ∈ Haus ∧ 𝑌 ∈ ℝ) → {𝑌} ∈ (Clsd‘(topGen‘ran (,))))
60	56, 57, 59	sylancr 593	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑌} ∈ (Clsd‘(topGen‘ran (,))))
61	58	difopn 23024	. . . . . . . . . . . 12 ⊢ (((𝐴(,)𝐵) ∈ (topGen‘ran (,)) ∧ {𝑌} ∈ (Clsd‘(topGen‘ran (,)))) → ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,)))
62	25, 60, 61	sylancr 593	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,)))
63		isopn3i 23072	. . . . . . . . . . 11 ⊢ (((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})) = ((𝐴(,)𝐵) ∖ {𝑌}))
64	55, 62, 63	sylancr 593	. . . . . . . . . 10 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})) = ((𝐴(,)𝐵) ∖ {𝑌}))
65	64	reseq2d 5938	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
66		reelprrecn 11128	. . . . . . . . . . . . 13 ⊢ ℝ ∈ {ℝ, ℂ}
67	66	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
68	41	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑁 + (1 / 2)) ∈ ℂ)
69		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
70	68, 69	mulcld 11163	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
71	70	sincld 16095	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
72		eqid 2740	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
73	71, 72	fmptd 7062	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℂ⟶ℂ)
74		ssid 3944	. . . . . . . . . . . . 13 ⊢ ℂ ⊆ ℂ
75	74	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ ⊆ ℂ)
76		dvsinax 46363	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 + (1 / 2)) ∈ ℂ → (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
77	41, 76	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
78	77	dmeqd 5854	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = dom (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
79		eqid 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
80	70	coscld 16096	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
81	68, 80	mulcld 11163	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ)
82	79, 81	dmmptd 6637	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = ℂ)
83	78, 82	eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = ℂ)
84	36, 83	sseqtrrid 3965	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
85		dvres3 25905	. . . . . . . . . . . 12 ⊢ (((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℂ⟶ℂ) ∧ (ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))) → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ))
86	67, 73, 75, 84, 85	syl22anc 844	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ))
87		resmpt 5996	. . . . . . . . . . . . 13 ⊢ (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
88	36, 87	mp1i 13	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
89	88	oveq2d 7379	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
90	77	reseq1d 5937	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = ((𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ))
91		resmpt 5996	. . . . . . . . . . . . 13 ⊢ (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
92	36, 91	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
93	90, 92	eqtrdi 2791	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
94	86, 89, 93	3eqtr3d 2783	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
95	94	reseq1d 5937	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
96		resmpt 5996	. . . . . . . . . 10 ⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
97	3, 96	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
98	65, 95, 97	3eqtrd 2779	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
99	35, 54, 98	3eqtrd 2779	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
100		dirkercncflem2.h	. . . . . . . . 9 ⊢ 𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
101	100	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
102	101	eqcomd 2746	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = 𝐻)
103	30, 99, 102	3eqtrd 2779	. . . . . 6 ⊢ (𝜑 → (ℝ D 𝐹) = 𝐻)
104	103	dmeqd 5854	. . . . 5 ⊢ (𝜑 → dom (ℝ D 𝐹) = dom 𝐻)
105	11	recnd 11171	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℂ)
106	105, 81	syldan 597	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ)
107	100, 106	dmmptd 6637	. . . . 5 ⊢ (𝜑 → dom 𝐻 = ((𝐴(,)𝐵) ∖ {𝑌}))
108	104, 107	eqtr2d 2776	. . . 4 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐹))
109		eqimss 3980	. . . 4 ⊢ (((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐹) → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐹))
110	108, 109	syl 17	. . 3 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐹))
111		dirkercncflem2.i	. . . . . . . 8 ⊢ 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2))))
112	111	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
113		resmpt 5996	. . . . . . . . . . . . 13 ⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))))
114	3, 113	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
115	114	eqcomi 2749	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))
116	115	oveq2i 7374	. . . . . . . . . 10 ⊢ (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
117	116	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))))
118		2cn 12254	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
119		picn 26447	. . . . . . . . . . . . . 14 ⊢ π ∈ ℂ
120	118, 119	mulcli 11150	. . . . . . . . . . . . 13 ⊢ (2 · π) ∈ ℂ
121	120	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (2 · π) ∈ ℂ)
122	43	halfcld 12420	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 / 2) ∈ ℂ)
123	122	sincld 16095	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (sin‘(𝑦 / 2)) ∈ ℂ)
124	121, 123	mulcld 11163	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
125		eqid 2740	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))
126	124, 125	fmptd 7062	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))):ℝ⟶ℂ)
127	51, 52	dvres 25903	. . . . . . . . . 10 ⊢ (((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)) → (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
128	37, 126, 50, 127	syl21anc 843	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
129	64	reseq2d 5938	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
130	36	sseli 3918	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
131		1cnd 11137	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℂ → 1 ∈ ℂ)
132		2cnd 12257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℂ → 2 ∈ ℂ)
133		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
134		2ne0 12283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
135	134	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℂ → 2 ≠ 0)
136	131, 132, 133, 135	div13d 11953	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℂ → ((1 / 2) · 𝑦) = ((𝑦 / 2) · 1))
137		halfcl 12401	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℂ → (𝑦 / 2) ∈ ℂ)
138	137	mulridd 11160	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℂ → ((𝑦 / 2) · 1) = (𝑦 / 2))
139	136, 138	eqtrd 2775	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℂ → ((1 / 2) · 𝑦) = (𝑦 / 2))
140	139	fveq2d 6838	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℂ → (sin‘((1 / 2) · 𝑦)) = (sin‘(𝑦 / 2)))
141	140	oveq2d 7379	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℂ → ((2 · π) · (sin‘((1 / 2) · 𝑦))) = ((2 · π) · (sin‘(𝑦 / 2))))
142	141	eqcomd 2746	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℂ → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘((1 / 2) · 𝑦))))
143	130, 142	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘((1 / 2) · 𝑦))))
144	143	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘((1 / 2) · 𝑦))))
145	144	mpteq2dva 5172	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))))
146	145	oveq2d 7379	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))
147	120	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (2 · π) ∈ ℂ)
148	39	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (1 / 2) ∈ ℂ)
149	148, 69	mulcld 11163	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((1 / 2) · 𝑦) ∈ ℂ)
150	149	sincld 16095	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (sin‘((1 / 2) · 𝑦)) ∈ ℂ)
151	147, 150	mulcld 11163	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · π) · (sin‘((1 / 2) · 𝑦))) ∈ ℂ)
152		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))
153	151, 152	fmptd 7062	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))):ℂ⟶ℂ)
154		2cnd 12257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 2 ∈ ℂ)
155	119	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → π ∈ ℂ)
156	154, 155	mulcld 11163	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (2 · π) ∈ ℂ)
157		dvasinbx 46370	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2 · π) ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦)))))
158	156, 39, 157	sylancl 592	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦)))))
159		2cnd 12257	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 2 ∈ ℂ)
160	119	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → π ∈ ℂ)
161	159, 160, 148	mul32d 11354	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · π) · (1 / 2)) = ((2 · (1 / 2)) · π))
162	134	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 2 ≠ 0)
163	159, 162	recidd 11924	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (2 · (1 / 2)) = 1)
164	163	oveq1d 7378	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · (1 / 2)) · π) = (1 · π))
165	160	mullidd 11161	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (1 · π) = π)
166	161, 164, 165	3eqtrd 2779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · π) · (1 / 2)) = π)
167	139	fveq2d 6838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℂ → (cos‘((1 / 2) · 𝑦)) = (cos‘(𝑦 / 2)))
168	167	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘((1 / 2) · 𝑦)) = (cos‘(𝑦 / 2)))
169	166, 168	oveq12d 7381	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦))) = (π · (cos‘(𝑦 / 2))))
170	169	mpteq2dva 5172	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦)))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
171	158, 170	eqtrd 2775	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
172	171	dmeqd 5854	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = dom (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
173		eqid 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2))))
174	69	halfcld 12420	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑦 / 2) ∈ ℂ)
175	174	coscld 16096	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘(𝑦 / 2)) ∈ ℂ)
176	160, 175	mulcld 11163	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (π · (cos‘(𝑦 / 2))) ∈ ℂ)
177	173, 176	dmmptd 6637	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) = ℂ)
178	172, 177	eqtrd 2775	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = ℂ)
179	36, 178	sseqtrrid 3965	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))
180		dvres3 25905	. . . . . . . . . . . . . . 15 ⊢ (((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))):ℂ⟶ℂ) ∧ (ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))) → (ℝ D ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ))
181	67, 153, 75, 179, 180	syl22anc 844	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ))
182		resmpt 5996	. . . . . . . . . . . . . . . 16 ⊢ (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))))
183	36, 182	mp1i 13	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))))
184	183	oveq2d 7379	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))
185	171	reseq1d 5937	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ) = ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ))
186	181, 184, 185	3eqtr3d 2783	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ))
187		resmpt 5996	. . . . . . . . . . . . . 14 ⊢ (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
188	36, 187	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2))))
189	186, 188	eqtrdi 2791	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
190	146, 189	eqtrd 2775	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
191	190	reseq1d 5937	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
192	4	resmptd 5999	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
193	129, 191, 192	3eqtrd 2779	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
194	117, 128, 193	3eqtrd 2779	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
195	194	eqcomd 2746	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))))
196	23	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))))
197	196	oveq2d 7379	. . . . . . . 8 ⊢ (𝜑 → (ℝ D 𝐺) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))))
198	197	eqcomd 2746	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D 𝐺))
199	112, 195, 198	3eqtrrd 2780	. . . . . 6 ⊢ (𝜑 → (ℝ D 𝐺) = 𝐼)
200	199	dmeqd 5854	. . . . 5 ⊢ (𝜑 → dom (ℝ D 𝐺) = dom 𝐼)
201	105, 176	syldan 597	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (π · (cos‘(𝑦 / 2))) ∈ ℂ)
202	111, 201	dmmptd 6637	. . . . 5 ⊢ (𝜑 → dom 𝐼 = ((𝐴(,)𝐵) ∖ {𝑌}))
203	200, 202	eqtr2d 2776	. . . 4 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐺))
204		eqimss 3980	. . . 4 ⊢ (((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐺) → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐺))
205	203, 204	syl 17	. . 3 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐺))
206	105, 70	syldan 597	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
207	206	ralrimiva 3132	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
208		eqid 2740	. . . . . . . 8 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))
209	208	fnmpt 6632	. . . . . . 7 ⊢ (∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}))
210	207, 209	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}))
211		eqidd 2741	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
212		simpr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
213	212	oveq2d 7379	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
214		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
215	38	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℂ)
216		1cnd 11137	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈ ℂ)
217	216	halfcld 12420	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈ ℂ)
218	215, 217	addcld 11162	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑁 + (1 / 2)) ∈ ℂ)
219		eldifi 4068	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ (𝐴(,)𝐵))
220	219	elioored 46001	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ ℝ)
221	220	recnd 11171	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ ℂ)
222	221	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑤 ∈ ℂ)
223	218, 222	mulcld 11163	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
224	211, 213, 214, 223	fvmptd 6950	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
225		eleq1w 2823	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↔ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})))
226	225	anbi2d 636	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ↔ (𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))))
227		oveq1 7370	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → (𝑦 mod (2 · π)) = (𝑤 mod (2 · π)))
228	227	neeq1d 2994	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → ((𝑦 mod (2 · π)) ≠ 0 ↔ (𝑤 mod (2 · π)) ≠ 0))
229	226, 228	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 mod (2 · π)) ≠ 0) ↔ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑤 mod (2 · π)) ≠ 0)))
230		eldifi 4068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ (𝐴(,)𝐵))
231		elioore 13326	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (𝐴(,)𝐵) → 𝑦 ∈ ℝ)
232	230, 231, 130	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ ℂ)
233		2cnd 12257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 2 ∈ ℂ)
234	119	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → π ∈ ℂ)
235	134	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 2 ≠ 0)
236		0re 11144	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ
237		pipos 26448	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < π
238	236, 237	gtneii 11256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ π ≠ 0
239	238	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → π ≠ 0)
240	232, 233, 234, 235, 239	divdiv1d 11960	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
241	240	eqcomd 2746	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
242	241	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
243		dirkercncflem2.yne0	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ≠ 0)
244	243	neneqd 2940	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (sin‘(𝑦 / 2)) = 0)
245	105	halfcld 12420	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℂ)
246		sineq0 26513	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 / 2) ∈ ℂ → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
247	245, 246	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
248	244, 247	mtbid 325	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / 2) / π) ∈ ℤ)
249	242, 248	eqneltrd 2860	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
250		2rp 12945	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ⁺
251		pirp 26450	. . . . . . . . . . . . . . . . . 18 ⊢ π ∈ ℝ⁺
252		rpmulcl 12965	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ⁺ ∧ π ∈ ℝ⁺) → (2 · π) ∈ ℝ⁺)
253	250, 251, 252	mp2an 698	. . . . . . . . . . . . . . . . 17 ⊢ (2 · π) ∈ ℝ⁺
254		mod0 13833	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℝ ∧ (2 · π) ∈ ℝ⁺) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
255	11, 253, 254	sylancl 592	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
256	249, 255	mtbird 326	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 mod (2 · π)) = 0)
257	256	neqned 2942	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 mod (2 · π)) ≠ 0)
258	229, 257	chvarvv 1996	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑤 mod (2 · π)) ≠ 0)
259	258	neneqd 2940	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑤 mod (2 · π)) = 0)
260		simpll 772	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝜑)
261		simpr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))
262	221	ad2antlr 733	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑤 ∈ ℂ)
263	57	recnd 11171	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ∈ ℂ)
264	263	ad2antrr 732	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑌 ∈ ℂ)
265		0red 11145	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ∈ ℝ)
266	5	nnred 12187	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℝ)
267		1red 11143	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ∈ ℝ)
268	267	rehalfcld 12422	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
269	266, 268	readdcld 11172	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ)
270	5	nngt0d 12224	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 < 𝑁)
271	250	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 2 ∈ ℝ⁺)
272	271	rpreccld 12994	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 / 2) ∈ ℝ⁺)
273	266, 272	ltaddrpd 13017	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 < (𝑁 + (1 / 2)))
274	265, 266, 269, 270, 273	lttrd 11305	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 < (𝑁 + (1 / 2)))
275	274	gt0ne0d 11712	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 + (1 / 2)) ≠ 0)
276	41, 275	jca 516	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠ 0))
277	276	ad2antrr 732	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠ 0))
278		mulcan 11785	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠ 0)) → (((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌) ↔ 𝑤 = 𝑌))
279	262, 264, 277, 278	syl3anc 1379	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → (((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌) ↔ 𝑤 = 𝑌))
280	261, 279	mpbid 233	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑤 = 𝑌)
281		oveq1 7370	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑌 → (𝑤 mod (2 · π)) = (𝑌 mod (2 · π)))
282		dirkercncflem2.ymod	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 mod (2 · π)) = 0)
283	281, 282	sylan9eqr 2797	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (𝑤 mod (2 · π)) = 0)
284	260, 280, 283	syl2anc 590	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → (𝑤 mod (2 · π)) = 0)
285	259, 284	mtand 821	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))
286	41, 263	mulcld 11163	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ)
287	286	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ)
288		elsn2g 4603	. . . . . . . . . . . 12 ⊢ (((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ → (((𝑁 + (1 / 2)) · 𝑤) ∈ {((𝑁 + (1 / 2)) · 𝑌)} ↔ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)))
289	287, 288	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑁 + (1 / 2)) · 𝑤) ∈ {((𝑁 + (1 / 2)) · 𝑌)} ↔ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)))
290	285, 289	mtbird 326	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑁 + (1 / 2)) · 𝑤) ∈ {((𝑁 + (1 / 2)) · 𝑌)})
291	223, 290	eldifd 3901	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑤) ∈ (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
292	224, 291	eqeltrd 2840	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
293		sinf 16089	. . . . . . . . . . . 12 ⊢ sin:ℂ⟶ℂ
294	293	fdmi 6673	. . . . . . . . . . 11 ⊢ dom sin = ℂ
295	294	eqcomi 2749	. . . . . . . . . 10 ⊢ ℂ = dom sin
296	295	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ℂ = dom sin)
297	296	difeq1d 4063	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}) = (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
298	292, 297	eleqtrd 2842	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
299	298	ralrimiva 3132	. . . . . 6 ⊢ (𝜑 → ∀𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
300		fnfvrnss 7069	. . . . . 6 ⊢ (((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ∀𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) → ran (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ⊆ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
301	210, 299, 300	syl2anc 590	. . . . 5 ⊢ (𝜑 → ran (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ⊆ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
302		uncom 4095	. . . . . . . . . 10 ⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌}))
303	302	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})))
304	27	snssd 4725	. . . . . . . . . 10 ⊢ (𝜑 → {𝑌} ⊆ (𝐴(,)𝐵))
305		undif 4417	. . . . . . . . . 10 ⊢ ({𝑌} ⊆ (𝐴(,)𝐵) ↔ ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐴(,)𝐵))
306	304, 305	sylib 219	. . . . . . . . 9 ⊢ (𝜑 → ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐴(,)𝐵))
307	303, 306	eqtrd 2775	. . . . . . . 8 ⊢ (𝜑 → (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = (𝐴(,)𝐵))
308	307	mpteq1d 5169	. . . . . . 7 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
309		iftrue 4467	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑌))
310		oveq2 7371	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑌 → ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))
311	309, 310	eqtr4d 2778	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
312	311	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
313		iffalse 4470	. . . . . . . . . . . . 13 ⊢ (¬ 𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))
314	313	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))
315		eqidd 2741	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
316		oveq2 7371	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
317	316	adantl 482	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
318		simpl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ (𝐴(,)𝐵))
319		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑤 = 𝑌 → ¬ 𝑤 = 𝑌)
320		velsn 4578	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ {𝑌} ↔ 𝑤 = 𝑌)
321	319, 320	sylnibr 330	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑤 = 𝑌 → ¬ 𝑤 ∈ {𝑌})
322	321	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → ¬ 𝑤 ∈ {𝑌})
323	318, 322	eldifd 3901	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
324	323	adantll 720	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
325	41	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑁 + (1 / 2)) ∈ ℂ)
326		elioore 13326	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → 𝑤 ∈ ℝ)
327	326	recnd 11171	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → 𝑤 ∈ ℂ)
328	327	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 𝑤 ∈ ℂ)
329	325, 328	mulcld 11163	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
330	329	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
331	315, 317, 324, 330	fvmptd 6950	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
332	314, 331	eqtrd 2775	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
333	312, 332	pm2.61dan 818	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
334	333	mpteq2dva 5172	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)))
335		ioosscn 13359	. . . . . . . . . . . . . 14 ⊢ (𝐴(,)𝐵) ⊆ ℂ
336		resmpt 5996	. . . . . . . . . . . . . 14 ⊢ ((𝐴(,)𝐵) ⊆ ℂ → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)))
337	335, 336	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤))
338		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) = (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤))
339	338	mulc1cncf 24897	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 + (1 / 2)) ∈ ℂ → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (ℂ–cn→ℂ))
340	41, 339	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (ℂ–cn→ℂ))
341	51	cnfldtop 24773	. . . . . . . . . . . . . . . . . . 19 ⊢ (TopOpen‘ℂ_fld) ∈ Top
342		unicntop 24775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
343	342	restid 17394	. . . . . . . . . . . . . . . . . . 19 ⊢ ((TopOpen‘ℂ_fld) ∈ Top → ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld))
344	341, 343	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld)
345	344	eqcomi 2749	. . . . . . . . . . . . . . . . 17 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
346	51, 345, 345	cncfcn 24902	. . . . . . . . . . . . . . . 16 ⊢ ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℂ) = ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
347	74, 75, 346	sylancr 593	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℂ–cn→ℂ) = ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
348	340, 347	eleqtrd 2842	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
349	2, 37	sstrid 3933	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
350	342	cnrest 23275	. . . . . . . . . . . . . 14 ⊢ (((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)))
351	348, 349, 350	syl2anc 590	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)))
352	337, 351	eqeltrrid 2845	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)))
353	51	cnfldtopon 24772	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
354		resttopon 23151	. . . . . . . . . . . . . 14 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)))
355	353, 349, 354	sylancr 593	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)))
356		cncnp 23270	. . . . . . . . . . . . 13 ⊢ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)) ∧ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)) ↔ ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦))))
357	355, 353, 356	sylancl 592	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)) ↔ ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦))))
358	352, 357	mpbid 233	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦)))
359	358	simprd 496	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦))
360		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦) = ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
361	360	eleq2d 2826	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌)))
362	361	rspccva 3566	. . . . . . . . . 10 ⊢ ((∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
363	359, 27, 362	syl2anc 590	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
364	334, 363	eqeltrd 2840	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
365	307	eqcomd 2746	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(,)𝐵) = (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}))
366	365	oveq2d 7379	. . . . . . . . . 10 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) = ((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})))
367	366	oveq1d 7378	. . . . . . . . 9 ⊢ (𝜑 → (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld)) = (((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld)))
368	367	fveq1d 6836	. . . . . . . 8 ⊢ (𝜑 → ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌) = ((((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld))‘𝑌))
369	364, 368	eleqtrd 2842	. . . . . . 7 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld))‘𝑌))
370	308, 369	eqeltrd 2840	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld))‘𝑌))
371		eqid 2740	. . . . . . 7 ⊢ ((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) = ((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}))
372		eqid 2740	. . . . . . 7 ⊢ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))
373	206, 208	fmptd 7062	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
374	4, 36	sstrdi 3934	. . . . . . 7 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℂ)
375	371, 51, 372, 373, 374, 263	ellimc 25865	. . . . . 6 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · 𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) lim_ℂ 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld))‘𝑌)))
376	370, 375	mpbird 258	. . . . 5 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) lim_ℂ 𝑌))
377	134	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ≠ 0)
378	238	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → π ≠ 0)
379	154, 155, 377, 378	mulne0d 11800	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · π) ≠ 0)
380	263, 156, 379	divcan1d 11930	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑌 / (2 · π)) · (2 · π)) = 𝑌)
381	380	eqcomd 2746	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 = ((𝑌 / (2 · π)) · (2 · π)))
382	381	oveq2d 7379	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))))
383	382	fveq2d 6838	. . . . . . 7 ⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) = (sin‘((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π)))))
384	263, 156, 379	divcld 11929	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 / (2 · π)) ∈ ℂ)
385	41, 384, 156	mul12d 11353	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = ((𝑌 / (2 · π)) · ((𝑁 + (1 / 2)) · (2 · π))))
386	41, 154, 155	mulassd 11166	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · 2) · π) = ((𝑁 + (1 / 2)) · (2 · π)))
387	386	eqcomd 2746	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · (2 · π)) = (((𝑁 + (1 / 2)) · 2) · π))
388	387	oveq2d 7379	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑌 / (2 · π)) · ((𝑁 + (1 / 2)) · (2 · π))) = ((𝑌 / (2 · π)) · (((𝑁 + (1 / 2)) · 2) · π)))
389	38, 40, 154	adddird 11168	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 2) = ((𝑁 · 2) + ((1 / 2) · 2)))
390	154, 377	recid2d 11925	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1 / 2) · 2) = 1)
391	390	oveq2d 7379	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 · 2) + ((1 / 2) · 2)) = ((𝑁 · 2) + 1))
392	389, 391	eqtrd 2775	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 2) = ((𝑁 · 2) + 1))
393	392	oveq1d 7378	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · 2) · π) = (((𝑁 · 2) + 1) · π))
394	393	oveq2d 7379	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑌 / (2 · π)) · (((𝑁 + (1 / 2)) · 2) · π)) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
395	385, 388, 394	3eqtrd 2779	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
396	38, 154	mulcld 11163	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 · 2) ∈ ℂ)
397		1cnd 11137	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
398	396, 397	addcld 11162	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 · 2) + 1) ∈ ℂ)
399	384, 398, 155	mulassd 11166	. . . . . . . . 9 ⊢ (𝜑 → (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
400	395, 399	eqtr4d 2778	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π))
401	400	fveq2d 6838	. . . . . . 7 ⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π)))) = (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π)))
402		mod0 13833	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ ℝ ∧ (2 · π) ∈ ℝ⁺) → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
403	57, 253, 402	sylancl 592	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
404	282, 403	mpbid 233	. . . . . . . . 9 ⊢ (𝜑 → (𝑌 / (2 · π)) ∈ ℤ)
405	5	nnzd 12548	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℤ)
406		2z 12557	. . . . . . . . . . . 12 ⊢ 2 ∈ ℤ
407	406	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℤ)
408	405, 407	zmulcld 12637	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 · 2) ∈ ℤ)
409	408	peano2zd 12634	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 · 2) + 1) ∈ ℤ)
410	404, 409	zmulcld 12637	. . . . . . . 8 ⊢ (𝜑 → ((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ∈ ℤ)
411		sinkpi 26511	. . . . . . . 8 ⊢ (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ∈ ℤ → (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π)) = 0)
412	410, 411	syl 17	. . . . . . 7 ⊢ (𝜑 → (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π)) = 0)
413	383, 401, 412	3eqtrd 2779	. . . . . 6 ⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) = 0)
414		sincn 26434	. . . . . . . 8 ⊢ sin ∈ (ℂ–cn→ℂ)
415	414	a1i 11	. . . . . . 7 ⊢ (𝜑 → sin ∈ (ℂ–cn→ℂ))
416	415, 286	cnlimci 25881	. . . . . 6 ⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) ∈ (sin lim_ℂ ((𝑁 + (1 / 2)) · 𝑌)))
417	413, 416	eqeltrrd 2841	. . . . 5 ⊢ (𝜑 → 0 ∈ (sin lim_ℂ ((𝑁 + (1 / 2)) · 𝑌)))
418	301, 376, 417	limccog 46072	. . . 4 ⊢ (𝜑 → 0 ∈ ((sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) lim_ℂ 𝑌))
419	14	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
420	213	fveq2d 6838	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
421	223	sincld 16095	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑤)) ∈ ℂ)
422	419, 420, 214, 421	fvmptd 6950	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹‘𝑤) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
423	224	fveq2d 6838	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
424	422, 423	eqtr4d 2778	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹‘𝑤) = (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))
425	424	mpteq2dva 5172	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (𝐹‘𝑤)) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
426	15	feqmptd 6902	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (𝐹‘𝑤)))
427		fcompt 7082	. . . . . . 7 ⊢ ((sin:ℂ⟶ℂ ∧ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
428	293, 373, 427	sylancr 593	. . . . . 6 ⊢ (𝜑 → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
429	425, 426, 428	3eqtr4rd 2786	. . . . 5 ⊢ (𝜑 → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = 𝐹)
430	429	oveq1d 7378	. . . 4 ⊢ (𝜑 → ((sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) lim_ℂ 𝑌) = (𝐹 lim_ℂ 𝑌))
431	418, 430	eleqtrd 2842	. . 3 ⊢ (𝜑 → 0 ∈ (𝐹 lim_ℂ 𝑌))
432		simpr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → 𝑤 = 𝑌)
433	432	iftrued 4469	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = 0)
434	263, 154, 156, 377, 379	divdiv32d 11954	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑌 / 2) / (2 · π)) = ((𝑌 / (2 · π)) / 2))
435	434	oveq1d 7378	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑌 / 2) / (2 · π)) · (2 · π)) = (((𝑌 / (2 · π)) / 2) · (2 · π)))
436	263	halfcld 12420	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑌 / 2) ∈ ℂ)
437	436, 156, 379	divcan1d 11930	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑌 / 2) / (2 · π)) · (2 · π)) = (𝑌 / 2))
438	384, 154, 156, 377	div32d 11952	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑌 / (2 · π)) / 2) · (2 · π)) = ((𝑌 / (2 · π)) · ((2 · π) / 2)))
439	155, 154, 377	divcan3d 11934	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2 · π) / 2) = π)
440	439	oveq2d 7379	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑌 / (2 · π)) · ((2 · π) / 2)) = ((𝑌 / (2 · π)) · π))
441	438, 440	eqtrd 2775	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑌 / (2 · π)) / 2) · (2 · π)) = ((𝑌 / (2 · π)) · π))
442	435, 437, 441	3eqtr3d 2783	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 / 2) = ((𝑌 / (2 · π)) · π))
443	442	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (sin‘(𝑌 / 2)) = (sin‘((𝑌 / (2 · π)) · π)))
444		sinkpi 26511	. . . . . . . . . . . . . . 15 ⊢ ((𝑌 / (2 · π)) ∈ ℤ → (sin‘((𝑌 / (2 · π)) · π)) = 0)
445	404, 444	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (sin‘((𝑌 / (2 · π)) · π)) = 0)
446	443, 445	eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (𝜑 → (sin‘(𝑌 / 2)) = 0)
447	446	oveq2d 7379	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · 0))
448	156	mul01d 11343	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · π) · 0) = 0)
449	447, 448	eqtrd 2775	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · π) · (sin‘(𝑌 / 2))) = 0)
450	449	eqcomd 2746	. . . . . . . . . 10 ⊢ (𝜑 → 0 = ((2 · π) · (sin‘(𝑌 / 2))))
451	450	ad2antrr 732	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → 0 = ((2 · π) · (sin‘(𝑌 / 2))))
452		fvoveq1 7386	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑌 → (sin‘(𝑤 / 2)) = (sin‘(𝑌 / 2)))
453	452	oveq2d 7379	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑌 → ((2 · π) · (sin‘(𝑤 / 2))) = ((2 · π) · (sin‘(𝑌 / 2))))
454	453	eqcomd 2746	. . . . . . . . . 10 ⊢ (𝑤 = 𝑌 → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
455	454	adantl 482	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
456	433, 451, 455	3eqtrd 2779	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
457		iffalse 4470	. . . . . . . . . 10 ⊢ (¬ 𝑤 = 𝑌 → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = (𝐺‘𝑤))
458	457	adantl 482	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = (𝐺‘𝑤))
459		fvoveq1 7386	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → (sin‘(𝑦 / 2)) = (sin‘(𝑤 / 2)))
460	459	oveq2d 7379	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
461	120	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (2 · π) ∈ ℂ)
462	328	halfcld 12420	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 / 2) ∈ ℂ)
463	462	sincld 16095	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (sin‘(𝑤 / 2)) ∈ ℂ)
464	461, 463	mulcld 11163	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((2 · π) · (sin‘(𝑤 / 2))) ∈ ℂ)
465	464	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((2 · π) · (sin‘(𝑤 / 2))) ∈ ℂ)
466	23, 460, 324, 465	fvmptd3 6966	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐺‘𝑤) = ((2 · π) · (sin‘(𝑤 / 2))))
467	458, 466	eqtrd 2775	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
468	456, 467	pm2.61dan 818	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
469	468	mpteq2dva 5172	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))))
470		eqid 2740	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2)))) = (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2))))
471	75, 156, 75	constcncfg 46322	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (2 · π)) ∈ (ℂ–cn→ℂ))
472		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℂ → 𝑤 ∈ ℂ)
473		2cnd 12257	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℂ → 2 ∈ ℂ)
474	134	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℂ → 2 ≠ 0)
475	472, 473, 474	divrec2d 11933	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ℂ → (𝑤 / 2) = ((1 / 2) · 𝑤))
476	475	mpteq2ia 5174	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ ℂ ↦ (𝑤 / 2)) = (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤))
477		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) = (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤))
478	477	mulc1cncf 24897	. . . . . . . . . . . . . . . 16 ⊢ ((1 / 2) ∈ ℂ → (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) ∈ (ℂ–cn→ℂ))
479	39, 478	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) ∈ (ℂ–cn→ℂ)
480	476, 479	eqeltri 2836	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ ℂ ↦ (𝑤 / 2)) ∈ (ℂ–cn→ℂ)
481	480	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (𝑤 / 2)) ∈ (ℂ–cn→ℂ))
482	415, 481	cncfmpt1f 24906	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (sin‘(𝑤 / 2))) ∈ (ℂ–cn→ℂ))
483	471, 482	mulcncf 25438	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ (ℂ–cn→ℂ))
484	470, 483, 349, 75, 464	cncfmptssg 46321	. . . . . . . . . 10 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
485		eqid 2740	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) = ((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵))
486	51, 485, 345	cncfcn 24902	. . . . . . . . . . 11 ⊢ (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)))
487	349, 74, 486	sylancl 592	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)))
488	484, 487	eleqtrd 2842	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)))
489		cncnp 23270	. . . . . . . . . 10 ⊢ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)) ∧ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)) → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)) ↔ ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦))))
490	355, 353, 489	sylancl 592	. . . . . . . . 9 ⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)) ↔ ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦))))
491	488, 490	mpbid 233	. . . . . . . 8 ⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦)))
492	491	simprd 496	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦))
493	360	eleq2d 2826	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌)))
494	493	rspccva 3566	. . . . . . 7 ⊢ ((∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
495	492, 27, 494	syl2anc 590	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
496	469, 495	eqeltrd 2840	. . . . 5 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
497	307	mpteq1d 5169	. . . . 5 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))))
498	366	eqcomd 2746	. . . . . . 7 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) = ((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)))
499	498	oveq1d 7378	. . . . . 6 ⊢ (𝜑 → (((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld)) = (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld)))
500	499	fveq1d 6836	. . . . 5 ⊢ (𝜑 → ((((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld))‘𝑌) = ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
501	496, 497, 500	3eltr4d 2855	. . . 4 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld))‘𝑌))
502		eqid 2740	. . . . 5 ⊢ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤)))
503	11, 124	syldan 597	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
504	503, 23	fmptd 7062	. . . . 5 ⊢ (𝜑 → 𝐺:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
505	371, 51, 502, 504, 374, 263	ellimc 25865	. . . 4 ⊢ (𝜑 → (0 ∈ (𝐺 lim_ℂ 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld))‘𝑌)))
506	501, 505	mpbird 258	. . 3 ⊢ (𝜑 → 0 ∈ (𝐺 lim_ℂ 𝑌))
507	256	nrexdv 3135	. . . 4 ⊢ (𝜑 → ¬ ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0)
508	504	ffund 6666	. . . . . 6 ⊢ (𝜑 → Fun 𝐺)
509		fvelima 6899	. . . . . 6 ⊢ ((Fun 𝐺 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0)
510	508, 509	sylan 586	. . . . 5 ⊢ ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0)
511		2cnd 12257	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ∈ ℂ)
512	119	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ∈ ℂ)
513	134	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ≠ 0)
514	238	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ≠ 0)
515	105, 511, 512, 513, 514	divdiv1d 11960	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
516	515	eqcomd 2746	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
517	516	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
518		2cnd 12257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → 2 ∈ ℂ)
519	119	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → π ∈ ℂ)
520	518, 519	mulcld 11163	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (2 · π) ∈ ℂ)
521	232	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → 𝑦 ∈ ℂ)
522	521	halfcld 12420	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (𝑦 / 2) ∈ ℂ)
523	522	sincld 16095	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (sin‘(𝑦 / 2)) ∈ ℂ)
524	520, 523	mulcld 11163	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
525	23	fvmpt2 6954	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ) → (𝐺‘𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
526	524, 525	syldan 597	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (𝐺‘𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
527	526	eqcomd 2746	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) = (𝐺‘𝑦))
528		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (𝐺‘𝑦) = 0)
529	527, 528	eqtrd 2775	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) = 0)
530	120	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (2 · π) ∈ ℂ)
531	232	halfcld 12420	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (𝑦 / 2) ∈ ℂ)
532	531	sincld 16095	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (sin‘(𝑦 / 2)) ∈ ℂ)
533	530, 532	mul0ord 11796	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (((2 · π) · (sin‘(𝑦 / 2))) = 0 ↔ ((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0)))
534	533	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (((2 · π) · (sin‘(𝑦 / 2))) = 0 ↔ ((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0)))
535	529, 534	mpbid 233	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0))
536		2cnne0 12384	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
537	119, 238	pm3.2i 471	. . . . . . . . . . . . . . 15 ⊢ (π ∈ ℂ ∧ π ≠ 0)
538		mulne0 11790	. . . . . . . . . . . . . . 15 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → (2 · π) ≠ 0)
539	536, 537, 538	mp2an 698	. . . . . . . . . . . . . 14 ⊢ (2 · π) ≠ 0
540	539	neii 2937	. . . . . . . . . . . . 13 ⊢ ¬ (2 · π) = 0
541		pm2.53 857	. . . . . . . . . . . . 13 ⊢ (((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0) → (¬ (2 · π) = 0 → (sin‘(𝑦 / 2)) = 0))
542	535, 540, 541	mpisyl 21	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (sin‘(𝑦 / 2)) = 0)
543	542	adantll 720	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (sin‘(𝑦 / 2)) = 0)
544	105	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → 𝑦 ∈ ℂ)
545	544	halfcld 12420	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 / 2) ∈ ℂ)
546	545, 246	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
547	543, 546	mpbid 233	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → ((𝑦 / 2) / π) ∈ ℤ)
548	517, 547	eqeltrd 2840	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 / (2 · π)) ∈ ℤ)
549	11	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → 𝑦 ∈ ℝ)
550	549, 253, 254	sylancl 592	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
551	548, 550	mpbird 258	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 mod (2 · π)) = 0)
552	551	ex 413	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐺‘𝑦) = 0 → (𝑦 mod (2 · π)) = 0))
553	552	reximdva 3153	. . . . . 6 ⊢ (𝜑 → (∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0 → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0))
554	553	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → (∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0 → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0))
555	510, 554	mpd 15	. . . 4 ⊢ ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0)
556	507, 555	mtand 821	. . 3 ⊢ (𝜑 → ¬ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌})))
557		simpr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
558	111	fvmpt2 6954	. . . . . . . . 9 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (π · (cos‘(𝑦 / 2))) ∈ ℂ) → (𝐼‘𝑦) = (π · (cos‘(𝑦 / 2))))
559	557, 201, 558	syl2anc 590	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐼‘𝑦) = (π · (cos‘(𝑦 / 2))))
560	531	coscld 16096	. . . . . . . . . 10 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (cos‘(𝑦 / 2)) ∈ ℂ)
561	560	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ∈ ℂ)
562		dirkercncflem2.11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0)
563	512, 561, 514, 562	mulne0d 11800	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (π · (cos‘(𝑦 / 2))) ≠ 0)
564	559, 563	eqnetrd 3002	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐼‘𝑦) ≠ 0)
565	564	neneqd 2940	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝐼‘𝑦) = 0)
566	565	nrexdv 3135	. . . . 5 ⊢ (𝜑 → ¬ ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼‘𝑦) = 0)
567	201, 111	fmptd 7062	. . . . . . 7 ⊢ (𝜑 → 𝐼:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
568	567	ffund 6666	. . . . . 6 ⊢ (𝜑 → Fun 𝐼)
569		fvelima 6899	. . . . . 6 ⊢ ((Fun 𝐼 ∧ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼‘𝑦) = 0)
570	568, 569	sylan 586	. . . . 5 ⊢ ((𝜑 ∧ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼‘𝑦) = 0)
571	566, 570	mtand 821	. . . 4 ⊢ (𝜑 → ¬ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌})))
572	199	imaeq1d 6018	. . . 4 ⊢ (𝜑 → ((ℝ D 𝐺) “ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌})))
573	571, 572	neleqtrrd 2863	. . 3 ⊢ (𝜑 → ¬ 0 ∈ ((ℝ D 𝐺) “ ((𝐴(,)𝐵) ∖ {𝑌})))
574		dirkercncflem2.d	. . . . . 6 ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
575	574	dirkerval2 46544	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ ℝ) → ((𝐷‘𝑁)‘𝑌) = if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))))
576	5, 57, 575	syl2anc 590	. . . 4 ⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) = if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))))
577	282	iftrued 4469	. . . . 5 ⊢ (𝜑 → if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))) = (((2 · 𝑁) + 1) / (2 · π)))
578		dirkercncflem2.l	. . . . . . . . . . 11 ⊢ 𝐿 = (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))))
579	578	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 = (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))))
580		iftrue 4467	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑌 → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = (((2 · 𝑁) + 1) / (2 · π)))
581	580	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = (((2 · 𝑁) + 1) / (2 · π)))
582	154, 38	mulcld 11163	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
583	582, 397	addcld 11162	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 · 𝑁) + 1) ∈ ℂ)
584	583, 154, 155, 377, 378	divdiv1d 11960	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((2 · 𝑁) + 1) / 2) / π) = (((2 · 𝑁) + 1) / (2 · π)))
585	584	eqcomd 2746	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) = ((((2 · 𝑁) + 1) / 2) / π))
586	582, 397, 154, 377	divdird 11967	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2 · 𝑁) + 1) / 2) = (((2 · 𝑁) / 2) + (1 / 2)))
587	38, 154, 377	divcan3d 11934	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2 · 𝑁) / 2) = 𝑁)
588	587	oveq1d 7378	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2 · 𝑁) / 2) + (1 / 2)) = (𝑁 + (1 / 2)))
589	586, 588	eqtrd 2775	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((2 · 𝑁) + 1) / 2) = (𝑁 + (1 / 2)))
590	589	oveq1d 7378	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((2 · 𝑁) + 1) / 2) / π) = ((𝑁 + (1 / 2)) / π))
591	585, 590	eqtrd 2775	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) = ((𝑁 + (1 / 2)) / π))
592	591	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((2 · 𝑁) + 1) / (2 · π)) = ((𝑁 + (1 / 2)) / π))
593	310	fveq2d 6838	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑌 → (cos‘((𝑁 + (1 / 2)) · 𝑤)) = (cos‘((𝑁 + (1 / 2)) · 𝑌)))
594	593	oveq2d 7379	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑌 → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))))
595		fvoveq1 7386	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑌 → (cos‘(𝑤 / 2)) = (cos‘(𝑌 / 2)))
596	595	oveq2d 7379	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑌 → (π · (cos‘(𝑤 / 2))) = (π · (cos‘(𝑌 / 2))))
597	594, 596	oveq12d 7381	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑌 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))))
598	597	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))))
599	38, 40, 263	adddird 11168	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑁 · 𝑌) + ((1 / 2) · 𝑌)))
600	397, 154, 263, 377	div32d 11952	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((1 / 2) · 𝑌) = (1 · (𝑌 / 2)))
601	436	mullidd 11161	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · (𝑌 / 2)) = (𝑌 / 2))
602	600, 601	eqtrd 2775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1 / 2) · 𝑌) = (𝑌 / 2))
603	602	oveq2d 7379	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 · 𝑌) + ((1 / 2) · 𝑌)) = ((𝑁 · 𝑌) + (𝑌 / 2)))
604	38, 263	mulcld 11163	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑁 · 𝑌) ∈ ℂ)
605	604, 436	addcomd 11346	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 · 𝑌) + (𝑌 / 2)) = ((𝑌 / 2) + (𝑁 · 𝑌)))
606	599, 603, 605	3eqtrd 2779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑌 / 2) + (𝑁 · 𝑌)))
607	606	fveq2d 6838	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (cos‘((𝑁 + (1 / 2)) · 𝑌)) = (cos‘((𝑌 / 2) + (𝑁 · 𝑌))))
608	604, 156, 379	divcan1d 11930	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝑁 · 𝑌) / (2 · π)) · (2 · π)) = (𝑁 · 𝑌))
609	608	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑁 · 𝑌) = (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))
610	609	oveq2d 7379	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑌 / 2) + (𝑁 · 𝑌)) = ((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π))))
611	610	fveq2d 6838	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (cos‘((𝑌 / 2) + (𝑁 · 𝑌))) = (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))))
612	38, 263, 156, 379	divassd 11964	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 · 𝑌) / (2 · π)) = (𝑁 · (𝑌 / (2 · π))))
613	405, 404	zmulcld 12637	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑁 · (𝑌 / (2 · π))) ∈ ℤ)
614	612, 613	eqeltrd 2840	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 · 𝑌) / (2 · π)) ∈ ℤ)
615		cosper 26471	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑌 / 2) ∈ ℂ ∧ ((𝑁 · 𝑌) / (2 · π)) ∈ ℤ) → (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))) = (cos‘(𝑌 / 2)))
616	436, 614, 615	syl2anc 590	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))) = (cos‘(𝑌 / 2)))
617	607, 611, 616	3eqtrd 2779	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (cos‘((𝑁 + (1 / 2)) · 𝑌)) = (cos‘(𝑌 / 2)))
618	617	oveq2d 7379	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) = ((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))))
619	618	oveq1d 7378	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = (((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))) / (π · (cos‘(𝑌 / 2)))))
620	436	coscld 16096	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (cos‘(𝑌 / 2)) ∈ ℂ)
621	263, 154, 155, 377, 378	divdiv1d 11960	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑌 / 2) / π) = (𝑌 / (2 · π)))
622	621, 404	eqeltrd 2840	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑌 / 2) / π) ∈ ℤ)
623	622	zred 12631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑌 / 2) / π) ∈ ℝ)
624	623, 272	ltaddrpd 13017	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑌 / 2) / π) < (((𝑌 / 2) / π) + (1 / 2)))
625		halflt1 12392	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 / 2) < 1
626	625	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (1 / 2) < 1)
627	268, 267, 623, 626	ltadd2dd 11303	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑌 / 2) / π) + (1 / 2)) < (((𝑌 / 2) / π) + 1))
628		btwnnz 12603	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑌 / 2) / π) ∈ ℤ ∧ ((𝑌 / 2) / π) < (((𝑌 / 2) / π) + (1 / 2)) ∧ (((𝑌 / 2) / π) + (1 / 2)) < (((𝑌 / 2) / π) + 1)) → ¬ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ)
629	622, 624, 627, 628	syl3anc 1379	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ¬ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ)
630		coseq0 46314	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑌 / 2) ∈ ℂ → ((cos‘(𝑌 / 2)) = 0 ↔ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ))
631	436, 630	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((cos‘(𝑌 / 2)) = 0 ↔ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ))
632	629, 631	mtbird 326	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ (cos‘(𝑌 / 2)) = 0)
633	632	neqned 2942	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (cos‘(𝑌 / 2)) ≠ 0)
634	41, 155, 620, 378, 633	divcan5rd 11956	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
635	619, 634	eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
636	635	ad2antrr 732	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
637	598, 636	eqtr2d 2776	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) / π) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))))
638	581, 592, 637	3eqtrrd 2780	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)))
639		iffalse 4470	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑤 = 𝑌 → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))
640	639	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))
641		eqidd 2741	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))))
642		fveq2 6834	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → (𝐻‘𝑦) = (𝐻‘𝑤))
643		fveq2 6834	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → (𝐼‘𝑦) = (𝐼‘𝑤))
644	642, 643	oveq12d 7381	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → ((𝐻‘𝑦) / (𝐼‘𝑦)) = ((𝐻‘𝑤) / (𝐼‘𝑤)))
645	644	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝐻‘𝑦) / (𝐼‘𝑦)) = ((𝐻‘𝑤) / (𝐼‘𝑤)))
646	106, 100	fmptd 7062	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐻:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
647	646	ad2antrr 732	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐻:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
648	647, 324	ffvelcdmd 7033	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐻‘𝑤) ∈ ℂ)
649	567	ad2antrr 732	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐼:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
650	649, 324	ffvelcdmd 7033	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼‘𝑤) ∈ ℂ)
651	111	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
652		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
653	652	fvoveq1d 7385	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (cos‘(𝑦 / 2)) = (cos‘(𝑤 / 2)))
654	653	oveq2d 7379	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (π · (cos‘(𝑦 / 2))) = (π · (cos‘(𝑤 / 2))))
655	119	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → π ∈ ℂ)
656	327	halfcld 12420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → (𝑤 / 2) ∈ ℂ)
657	656	coscld 16096	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → (cos‘(𝑤 / 2)) ∈ ℂ)
658	655, 657	mulcld 11163	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → (π · (cos‘(𝑤 / 2))) ∈ ℂ)
659	658	ad2antlr 733	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π · (cos‘(𝑤 / 2))) ∈ ℂ)
660	651, 654, 324, 659	fvmptd 6950	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼‘𝑤) = (π · (cos‘(𝑤 / 2))))
661	537	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π ∈ ℂ ∧ π ≠ 0))
662	657	ad2antlr 733	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ∈ ℂ)
663		simpll 772	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝜑)
664		fvoveq1 7386	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑤 → (cos‘(𝑦 / 2)) = (cos‘(𝑤 / 2)))
665	664	neeq1d 2994	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑤 → ((cos‘(𝑦 / 2)) ≠ 0 ↔ (cos‘(𝑤 / 2)) ≠ 0))
666	226, 665	imbi12d 345	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑤 → (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0) ↔ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑤 / 2)) ≠ 0)))
667	666, 562	chvarvv 1996	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑤 / 2)) ≠ 0)
668	663, 324, 667	syl2anc 590	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
669		mulne0 11790	. . . . . . . . . . . . . . . . 17 ⊢ (((π ∈ ℂ ∧ π ≠ 0) ∧ ((cos‘(𝑤 / 2)) ∈ ℂ ∧ (cos‘(𝑤 / 2)) ≠ 0)) → (π · (cos‘(𝑤 / 2))) ≠ 0)
670	661, 662, 668, 669	syl12anc 842	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π · (cos‘(𝑤 / 2))) ≠ 0)
671	660, 670	eqnetrd 3002	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼‘𝑤) ≠ 0)
672	648, 650, 671	divcld 11929	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝐻‘𝑤) / (𝐼‘𝑤)) ∈ ℂ)
673	641, 645, 324, 672	fvmptd 6950	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤) = ((𝐻‘𝑤) / (𝐼‘𝑤)))
674	100	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
675	317	fveq2d 6838	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (cos‘((𝑁 + (1 / 2)) · 𝑦)) = (cos‘((𝑁 + (1 / 2)) · 𝑤)))
676	675	oveq2d 7379	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))))
677	329	coscld 16096	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘((𝑁 + (1 / 2)) · 𝑤)) ∈ ℂ)
678	325, 677	mulcld 11163	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ℂ)
679	678	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ℂ)
680	674, 676, 324, 679	fvmptd 6950	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐻‘𝑤) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))))
681	680, 660	oveq12d 7381	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝐻‘𝑤) / (𝐼‘𝑤)) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))))
682	640, 673, 681	3eqtrrd 2780	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)))
683	638, 682	pm2.61dan 818	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)))
684	683	mpteq2dva 5172	. . . . . . . . . 10 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))))
685	579, 684	eqtr2d 2776	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) = 𝐿)
686	349, 41, 75	constcncfg 46322	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
687		cosf 16090	. . . . . . . . . . . . . . . . . . 19 ⊢ cos:ℂ⟶ℂ
688	231, 44	sylan2 599	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
689		eqid 2740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))
690	688, 689	fmptd 7062	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)):(𝐴(,)𝐵)⟶ℂ)
691		fcompt 7082	. . . . . . . . . . . . . . . . . . 19 ⊢ ((cos:ℂ⟶ℂ ∧ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)):(𝐴(,)𝐵)⟶ℂ) → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
692	687, 690, 691	sylancr 593	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
693		eqidd 2741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
694	316	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
695		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 𝑤 ∈ (𝐴(,)𝐵))
696	693, 694, 695, 329	fvmptd 6950	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
697	696	fveq2d 6838	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = (cos‘((𝑁 + (1 / 2)) · 𝑤)))
698	697	mpteq2dva 5172	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))))
699	692, 698	eqtr2d 2776	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))) = (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))))
700	349, 41, 75	constcncfg 46322	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
701	349, 75	idcncfg 46323	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 𝑦) ∈ ((𝐴(,)𝐵)–cn→ℂ))
702	700, 701	mulcncf 25438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
703		coscn 26435	. . . . . . . . . . . . . . . . . . 19 ⊢ cos ∈ (ℂ–cn→ℂ)
704	703	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → cos ∈ (ℂ–cn→ℂ))
705	702, 704	cncfco 24899	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
706	699, 705	eqeltrd 2840	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
707	686, 706	mulcncf 25438	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
708		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2))))
709	349, 155, 75	constcncfg 46322	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ π) ∈ ((𝐴(,)𝐵)–cn→ℂ))
710		2cnd 12257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ)
711	134	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 2 ≠ 0)
712	328, 710, 711	divrecd 11932	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 / 2) = (𝑤 · (1 / 2)))
713	712	mpteq2dva 5172	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 / 2)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 · (1 / 2))))
714		eqid 2740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2))) = (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2)))
715		cncfmptid 24905	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ))
716	74, 74, 715	mp2an 698	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ)
717	716	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ))
718	74	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 / 2) ∈ ℂ → ℂ ⊆ ℂ)
719		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 / 2) ∈ ℂ → (1 / 2) ∈ ℂ)
720	718, 719, 718	constcncfg 46322	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 / 2) ∈ ℂ → (𝑤 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
721	39, 720	mp1i 13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
722	717, 721	mulcncf 25438	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2))) ∈ (ℂ–cn→ℂ))
723	712, 462	eqeltrrd 2841	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 · (1 / 2)) ∈ ℂ)
724	714, 722, 349, 75, 723	cncfmptssg 46321	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 · (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
725	713, 724	eqeltrd 2840	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 / 2)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
726	704, 725	cncfmpt1f 24906	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑤 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
727	709, 726	mulcncf 25438	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
728		ssid 3944	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)
729	728	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵))
730		difssd 4074	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
731	658	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ∈ ℂ)
732	119	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → π ∈ ℂ)
733	657	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘(𝑤 / 2)) ∈ ℂ)
734	238	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → π ≠ 0)
735	595	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) = (cos‘(𝑌 / 2)))
736	633	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (cos‘(𝑌 / 2)) ≠ 0)
737	735, 736	eqnetrd 3002	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
738	737	adantlr 721	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
739	738, 668	pm2.61dan 818	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘(𝑤 / 2)) ≠ 0)
740	732, 733, 734, 739	mulne0d 11800	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ≠ 0)
741	740	neneqd 2940	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ¬ (π · (cos‘(𝑤 / 2))) = 0)
742		elsng 4576	. . . . . . . . . . . . . . . . . . 19 ⊢ ((π · (cos‘(𝑤 / 2))) ∈ ℂ → ((π · (cos‘(𝑤 / 2))) ∈ {0} ↔ (π · (cos‘(𝑤 / 2))) = 0))
743	731, 742	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((π · (cos‘(𝑤 / 2))) ∈ {0} ↔ (π · (cos‘(𝑤 / 2))) = 0))
744	741, 743	mtbird 326	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ¬ (π · (cos‘(𝑤 / 2))) ∈ {0})
745	731, 744	eldifd 3901	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ∈ (ℂ ∖ {0}))
746	708, 727, 729, 730, 745	cncfmptssg 46321	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→(ℂ ∖ {0})))
747	707, 746	divcncf 25439	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
748	747, 487	eleqtrd 2842	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)))
749	579, 748	eqeltrd 2840	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)))
750		cncnp 23270	. . . . . . . . . . . . 13 ⊢ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)) ∧ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)) → (𝐿 ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)) ↔ (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦))))
751	355, 353, 750	sylancl 592	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)) ↔ (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦))))
752	749, 751	mpbid 233	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦)))
753	752	simprd 496	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦))
754	360	eleq2d 2826	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → (𝐿 ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦) ↔ 𝐿 ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌)))
755	754	rspccva 3566	. . . . . . . . . 10 ⊢ ((∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → 𝐿 ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
756	753, 27, 755	syl2anc 590	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
757	685, 756	eqeltrd 2840	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
758	307	mpteq1d 5169	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))))
759	757, 758, 500	3eltr4d 2855	. . . . . . 7 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld))‘𝑌))
760		eqid 2740	. . . . . . . 8 ⊢ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)))
761	100	fvmpt2 6954	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ) → (𝐻‘𝑦) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
762	557, 106, 761	syl2anc 590	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐻‘𝑦) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
763	762, 559	oveq12d 7381	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐻‘𝑦) / (𝐼‘𝑦)) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) / (π · (cos‘(𝑦 / 2)))))
764	106, 201, 563	divcld 11929	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) / (π · (cos‘(𝑦 / 2)))) ∈ ℂ)
765	763, 764	eqeltrd 2840	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐻‘𝑦) / (𝐼‘𝑦)) ∈ ℂ)
766		eqid 2740	. . . . . . . . 9 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))
767	765, 766	fmptd 7062	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
768	371, 51, 760, 767, 374, 263	ellimc 25865	. . . . . . 7 ⊢ (𝜑 → ((((2 · 𝑁) + 1) / (2 · π)) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) lim_ℂ 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld))‘𝑌)))
769	759, 768	mpbird 258	. . . . . 6 ⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) lim_ℂ 𝑌))
770	103	eqcomd 2746	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 = (ℝ D 𝐹))
771	770	fveq1d 6836	. . . . . . . . 9 ⊢ (𝜑 → (𝐻‘𝑦) = ((ℝ D 𝐹)‘𝑦))
772	199	eqcomd 2746	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 = (ℝ D 𝐺))
773	772	fveq1d 6836	. . . . . . . . 9 ⊢ (𝜑 → (𝐼‘𝑦) = ((ℝ D 𝐺)‘𝑦))
774	771, 773	oveq12d 7381	. . . . . . . 8 ⊢ (𝜑 → ((𝐻‘𝑦) / (𝐼‘𝑦)) = (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)))
775	774	mpteq2dv 5173	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))))
776	775	oveq1d 7378	. . . . . 6 ⊢ (𝜑 → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) lim_ℂ 𝑌) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim_ℂ 𝑌))
777	769, 776	eleqtrd 2842	. . . . 5 ⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim_ℂ 𝑌))
778	577, 777	eqeltrd 2840	. . . 4 ⊢ (𝜑 → if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim_ℂ 𝑌))
779	576, 778	eqeltrd 2840	. . 3 ⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim_ℂ 𝑌))
780	4, 15, 24, 26, 27, 28, 110, 205, 431, 506, 556, 573, 779	lhop 26008	. 2 ⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))) lim_ℂ 𝑌))
781	574	dirkerval 46541	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) = (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
782	5, 781	syl 17	. . . . 5 ⊢ (𝜑 → (𝐷‘𝑁) = (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
783	782	reseq1d 5937	. . . 4 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
784	4	resmptd 5999	. . . 4 ⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ 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)))))))
785	256	iffalsed 4472	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
786	13	recnd 11171	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
787	14	fvmpt2 6954	. . . . . . . 8 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ) → (𝐹‘𝑦) = (sin‘((𝑁 + (1 / 2)) · 𝑦)))
788	557, 786, 787	syl2anc 590	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹‘𝑦) = (sin‘((𝑁 + (1 / 2)) · 𝑦)))
789	557, 503, 525	syl2anc 590	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐺‘𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
790	788, 789	oveq12d 7381	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐹‘𝑦) / (𝐺‘𝑦)) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
791	785, 790	eqtr4d 2778	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((𝐹‘𝑦) / (𝐺‘𝑦)))
792	791	mpteq2dva 5172	. . . 4 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))))
793	783, 784, 792	3eqtrrd 2780	. . 3 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))) = ((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
794	793	oveq1d 7378	. 2 ⊢ (𝜑 → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))) lim_ℂ 𝑌) = (((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) lim_ℂ 𝑌))
795	780, 794	eleqtrd 2842	1 ⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ (((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) lim_ℂ 𝑌))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∨ wo 853 = wceq 1547 ∈ wcel 2119 ≠ wne 2935 ∀wral 3054 ∃wrex 3064 ∖ cdif 3887 ∪ cun 3888 ⊆ wss 3890 ifcif 4461 {csn 4562 {cpr 4564 class class class wbr 5079 ↦ cmpt 5160 dom cdm 5625 ran crn 5626 ↾ cres 5627 “ cima 5628 ∘ ccom 5629 Fun wfun 6486 Fn wfn 6487 ⟶wf 6488 ‘cfv 6492 (class class class)co 7363 ℂcc 11034 ℝcr 11035 0cc0 11036 1c1 11037 + caddc 11039 · cmul 11041 < clt 11177 / cdiv 11805 ℕcn 12172 2c2 12234 ℤcz 12522 ℝ⁺crp 12940 (,)cioo 13296 mod cmo 13826 sincsin 16026 cosccos 16027 πcpi 16029 ↾_t crest 17381 TopOpenctopn 17382 topGenctg 17398 ℂ_fldccnfld 21354 Topctop 22883 TopOnctopon 22900 Clsdccld 23006 intcnt 23007 Cn ccn 23214 CnP ccnp 23215 Hauscha 23298 –cn→ccncf 24868 lim_ℂ climc 25854 D cdv 25855

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-rep 5206 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685 ax-inf2 9560 ax-cnex 11092 ax-resscn 11093 ax-1cn 11094 ax-icn 11095 ax-addcl 11096 ax-addrcl 11097 ax-mulcl 11098 ax-mulrcl 11099 ax-mulcom 11100 ax-addass 11101 ax-mulass 11102 ax-distr 11103 ax-i2m1 11104 ax-1ne0 11105 ax-1rid 11106 ax-rnegex 11107 ax-rrecex 11108 ax-cnre 11109 ax-pre-lttri 11110 ax-pre-lttrn 11111 ax-pre-ltadd 11112 ax-pre-mulgt0 11113 ax-pre-sup 11114 ax-addf 11115

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-nel 3040 df-ral 3055 df-rex 3065 df-rmo 3345 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4846 df-int 4885 df-iun 4930 df-iin 4931 df-br 5080 df-opab 5142 df-mpt 5161 df-tr 5187 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7320 df-ov 7366 df-oprab 7367 df-mpo 7368 df-of 7627 df-om 7814 df-1st 7938 df-2nd 7939 df-supp 8108 df-frecs 8228 df-wrecs 8259 df-recs 8308 df-rdg 8346 df-1o 8402 df-2o 8403 df-er 8640 df-map 8772 df-pm 8773 df-ixp 8843 df-en 8891 df-dom 8892 df-sdom 8893 df-fin 8894 df-fsupp 9272 df-fi 9321 df-sup 9352 df-inf 9353 df-oi 9422 df-card 9861 df-pnf 11179 df-mnf 11180 df-xr 11181 df-ltxr 11182 df-le 11183 df-sub 11377 df-neg 11378 df-div 11806 df-nn 12173 df-2 12242 df-3 12243 df-4 12244 df-5 12245 df-6 12246 df-7 12247 df-8 12248 df-9 12249 df-n0 12436 df-z 12523 df-dec 12643 df-uz 12787 df-q 12897 df-rp 12941 df-xneg 13061 df-xadd 13062 df-xmul 13063 df-ioo 13300 df-ioc 13301 df-ico 13302 df-icc 13303 df-fz 13460 df-fzo 13607 df-fl 13749 df-mod 13827 df-seq 13962 df-exp 14022 df-fac 14234 df-bc 14263 df-hash 14291 df-shft 15027 df-cj 15059 df-re 15060 df-im 15061 df-sqrt 15195 df-abs 15196 df-limsup 15431 df-clim 15448 df-rlim 15449 df-sum 15647 df-ef 16030 df-sin 16032 df-cos 16033 df-pi 16035 df-struct 17115 df-sets 17132 df-slot 17150 df-ndx 17162 df-base 17178 df-ress 17199 df-plusg 17231 df-mulr 17232 df-starv 17233 df-sca 17234 df-vsca 17235 df-ip 17236 df-tset 17237 df-ple 17238 df-ds 17240 df-unif 17241 df-hom 17242 df-cco 17243 df-rest 17383 df-topn 17384 df-0g 17402 df-gsum 17403 df-topgen 17404 df-pt 17405 df-prds 17408 df-xrs 17464 df-qtop 17469 df-imas 17470 df-xps 17472 df-mre 17546 df-mrc 17547 df-acs 17549 df-mgm 18606 df-sgrp 18685 df-mnd 18701 df-submnd 18750 df-mulg 19042 df-cntz 19290 df-cmn 19755 df-psmet 21346 df-xmet 21347 df-met 21348 df-bl 21349 df-mopn 21350 df-fbas 21351 df-fg 21352 df-cnfld 21355 df-top 22884 df-topon 22901 df-topsp 22923 df-bases 22936 df-cld 23009 df-ntr 23010 df-cls 23011 df-nei 23088 df-lp 23126 df-perf 23127 df-cn 23217 df-cnp 23218 df-t1 23304 df-haus 23305 df-cmp 23377 df-tx 23552 df-hmeo 23745 df-fil 23836 df-fm 23928 df-flim 23929 df-flf 23930 df-xms 24310 df-ms 24311 df-tms 24312 df-cncf 24870 df-limc 25858 df-dv 25859

This theorem is referenced by: dirkercncflem3 46555

W3C validator