Theorem dirkercncflem2 46456

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 4090	. . . . 5 ⊢ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ (𝐴(,)𝐵)
2		ioossre 13335	. . . . 5 ⊢ (𝐴(,)𝐵) ⊆ ℝ
3	1, 2	sstri 3945	. . . 4 ⊢ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ
4	3	a1i 11	. . 3 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)
5		dirkercncflem2.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℕ)
7	6	nnred 12172	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℝ)
8		halfre 12366	. . . . . . . 8 ⊢ (1 / 2) ∈ ℝ
9	8	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈ ℝ)
10	7, 9	readdcld 11173	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑁 + (1 / 2)) ∈ ℝ)
11	4	sselda 3935	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℝ)
12	10, 11	remulcld 11174	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℝ)
13	12	resincld 16080	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℝ)
14		dirkercncflem2.f	. . . 4 ⊢ 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
15	13, 14	fmptd 7068	. . 3 ⊢ (𝜑 → 𝐹:((𝐴(,)𝐵) ∖ {𝑌})⟶ℝ)
16		2re 12231	. . . . . . 7 ⊢ 2 ∈ ℝ
17		pire 26434	. . . . . . 7 ⊢ π ∈ ℝ
18	16, 17	remulcli 11160	. . . . . 6 ⊢ (2 · π) ∈ ℝ
19	18	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈ ℝ)
20	11	rehalfcld 12400	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℝ)
21	20	resincld 16080	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ∈ ℝ)
22	19, 21	remulcld 11174	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℝ)
23		dirkercncflem2.g	. . . 4 ⊢ 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
24	22, 23	fmptd 7068	. . 3 ⊢ (𝜑 → 𝐺:((𝐴(,)𝐵) ∖ {𝑌})⟶ℝ)
25		iooretop 24721	. . . 4 ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))
26	25	a1i 11	. . 3 ⊢ (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran (,)))
27		dirkercncflem2.y	. . 3 ⊢ (𝜑 → 𝑌 ∈ (𝐴(,)𝐵))
28		eqid 2737	. . 3 ⊢ ((𝐴(,)𝐵) ∖ {𝑌}) = ((𝐴(,)𝐵) ∖ {𝑌})
29	14	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
30	29	oveq2d 7384	. . . . . . 7 ⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
31		resmpt 6004	. . . . . . . . . . . 12 ⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
32	3, 31	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
33	32	eqcomi 2746	. . . . . . . . . 10 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))
34	33	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
35	34	oveq2d 7384	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))))
36		ax-resscn 11095	. . . . . . . . . 10 ⊢ ℝ ⊆ ℂ
37	36	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℝ ⊆ ℂ)
38	5	nncnd 12173	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℂ)
39		halfcn 12367	. . . . . . . . . . . . . . 15 ⊢ (1 / 2) ∈ ℂ
40	39	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
41	38, 40	addcld 11163	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ)
42	41	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑁 + (1 / 2)) ∈ ℂ)
43	37	sselda 3935	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
44	42, 43	mulcld 11164	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
45	44	sincld 16067	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
46		eqid 2737	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
47	45, 46	fmptd 7068	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℝ⟶ℂ)
48		ssid 3958	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℝ
49	48, 3	pm3.2i 470	. . . . . . . . . 10 ⊢ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)
50	49	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ))
51		eqid 2737	. . . . . . . . . 10 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
52		tgioo4 24761	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
53	51, 52	dvres 25880	. . . . . . . . 9 ⊢ (((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)) → (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
54	37, 47, 50, 53	syl21anc 838	. . . . . . . 8 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
55		retop 24717	. . . . . . . . . . 11 ⊢ (topGen‘ran (,)) ∈ Top
56		rehaus 24755	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) ∈ Haus
57	27	elioored 45903	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ ℝ)
58		uniretop 24718	. . . . . . . . . . . . . 14 ⊢ ℝ = ∪ (topGen‘ran (,))
59	58	sncld 23327	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ∈ Haus ∧ 𝑌 ∈ ℝ) → {𝑌} ∈ (Clsd‘(topGen‘ran (,))))
60	56, 57, 59	sylancr 588	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑌} ∈ (Clsd‘(topGen‘ran (,))))
61	58	difopn 22990	. . . . . . . . . . . 12 ⊢ (((𝐴(,)𝐵) ∈ (topGen‘ran (,)) ∧ {𝑌} ∈ (Clsd‘(topGen‘ran (,)))) → ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,)))
62	25, 60, 61	sylancr 588	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,)))
63		isopn3i 23038	. . . . . . . . . . 11 ⊢ (((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})) = ((𝐴(,)𝐵) ∖ {𝑌}))
64	55, 62, 63	sylancr 588	. . . . . . . . . 10 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})) = ((𝐴(,)𝐵) ∖ {𝑌}))
65	64	reseq2d 5946	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
66		reelprrecn 11130	. . . . . . . . . . . . 13 ⊢ ℝ ∈ {ℝ, ℂ}
67	66	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
68	41	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑁 + (1 / 2)) ∈ ℂ)
69		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
70	68, 69	mulcld 11164	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
71	70	sincld 16067	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
72		eqid 2737	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
73	71, 72	fmptd 7068	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℂ⟶ℂ)
74		ssid 3958	. . . . . . . . . . . . 13 ⊢ ℂ ⊆ ℂ
75	74	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ ⊆ ℂ)
76		dvsinax 46265	. . . . . . . . . . . . . . . 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 5862	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = dom (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
79		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
80	70	coscld 16068	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
81	68, 80	mulcld 11164	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ)
82	79, 81	dmmptd 6645	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = ℂ)
83	78, 82	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = ℂ)
84	36, 83	sseqtrrid 3979	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
85		dvres3 25882	. . . . . . . . . . . 12 ⊢ (((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℂ⟶ℂ) ∧ (ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))) → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ))
86	67, 73, 75, 84, 85	syl22anc 839	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ))
87		resmpt 6004	. . . . . . . . . . . . 13 ⊢ (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
88	36, 87	mp1i 13	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
89	88	oveq2d 7384	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
90	77	reseq1d 5945	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = ((𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ))
91		resmpt 6004	. . . . . . . . . . . . 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 2788	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
94	86, 89, 93	3eqtr3d 2780	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
95	94	reseq1d 5945	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
96		resmpt 6004	. . . . . . . . . 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 2776	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
99	35, 54, 98	3eqtrd 2776	. . . . . . 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 2743	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = 𝐻)
103	30, 99, 102	3eqtrd 2776	. . . . . 6 ⊢ (𝜑 → (ℝ D 𝐹) = 𝐻)
104	103	dmeqd 5862	. . . . 5 ⊢ (𝜑 → dom (ℝ D 𝐹) = dom 𝐻)
105	11	recnd 11172	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℂ)
106	105, 81	syldan 592	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ)
107	100, 106	dmmptd 6645	. . . . 5 ⊢ (𝜑 → dom 𝐻 = ((𝐴(,)𝐵) ∖ {𝑌}))
108	104, 107	eqtr2d 2773	. . . 4 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐹))
109		eqimss 3994	. . . 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 6004	. . . . . . . . . . . . 13 ⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))))
114	3, 113	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
115	114	eqcomi 2746	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))
116	115	oveq2i 7379	. . . . . . . . . 10 ⊢ (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
117	116	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))))
118		2cn 12232	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
119		picn 26435	. . . . . . . . . . . . . 14 ⊢ π ∈ ℂ
120	118, 119	mulcli 11151	. . . . . . . . . . . . 13 ⊢ (2 · π) ∈ ℂ
121	120	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (2 · π) ∈ ℂ)
122	43	halfcld 12398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 / 2) ∈ ℂ)
123	122	sincld 16067	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (sin‘(𝑦 / 2)) ∈ ℂ)
124	121, 123	mulcld 11164	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
125		eqid 2737	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))
126	124, 125	fmptd 7068	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))):ℝ⟶ℂ)
127	51, 52	dvres 25880	. . . . . . . . . 10 ⊢ (((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)) → (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
128	37, 126, 50, 127	syl21anc 838	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
129	64	reseq2d 5946	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
130	36	sseli 3931	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
131		1cnd 11139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℂ → 1 ∈ ℂ)
132		2cnd 12235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℂ → 2 ∈ ℂ)
133		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
134		2ne0 12261	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
135	134	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℂ → 2 ≠ 0)
136	131, 132, 133, 135	div13d 11953	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℂ → ((1 / 2) · 𝑦) = ((𝑦 / 2) · 1))
137		halfcl 12379	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℂ → (𝑦 / 2) ∈ ℂ)
138	137	mulridd 11161	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℂ → ((𝑦 / 2) · 1) = (𝑦 / 2))
139	136, 138	eqtrd 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℂ → ((1 / 2) · 𝑦) = (𝑦 / 2))
140	139	fveq2d 6846	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℂ → (sin‘((1 / 2) · 𝑦)) = (sin‘(𝑦 / 2)))
141	140	oveq2d 7384	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℂ → ((2 · π) · (sin‘((1 / 2) · 𝑦))) = ((2 · π) · (sin‘(𝑦 / 2))))
142	141	eqcomd 2743	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℂ → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘((1 / 2) · 𝑦))))
143	130, 142	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘((1 / 2) · 𝑦))))
144	143	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘((1 / 2) · 𝑦))))
145	144	mpteq2dva 5193	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))))
146	145	oveq2d 7384	. . . . . . . . . . . 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 11164	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((1 / 2) · 𝑦) ∈ ℂ)
150	149	sincld 16067	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (sin‘((1 / 2) · 𝑦)) ∈ ℂ)
151	147, 150	mulcld 11164	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · π) · (sin‘((1 / 2) · 𝑦))) ∈ ℂ)
152		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))
153	151, 152	fmptd 7068	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))):ℂ⟶ℂ)
154		2cnd 12235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 2 ∈ ℂ)
155	119	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → π ∈ ℂ)
156	154, 155	mulcld 11164	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (2 · π) ∈ ℂ)
157		dvasinbx 46272	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2 · π) ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦)))))
158	156, 39, 157	sylancl 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦)))))
159		2cnd 12235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 2 ∈ ℂ)
160	119	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → π ∈ ℂ)
161	159, 160, 148	mul32d 11355	. . . . . . . . . . . . . . . . . . . . . 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 7383	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · (1 / 2)) · π) = (1 · π))
165	160	mullidd 11162	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (1 · π) = π)
166	161, 164, 165	3eqtrd 2776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · π) · (1 / 2)) = π)
167	139	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℂ → (cos‘((1 / 2) · 𝑦)) = (cos‘(𝑦 / 2)))
168	167	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘((1 / 2) · 𝑦)) = (cos‘(𝑦 / 2)))
169	166, 168	oveq12d 7386	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦))) = (π · (cos‘(𝑦 / 2))))
170	169	mpteq2dva 5193	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦)))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
171	158, 170	eqtrd 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
172	171	dmeqd 5862	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = dom (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
173		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2))))
174	69	halfcld 12398	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑦 / 2) ∈ ℂ)
175	174	coscld 16068	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘(𝑦 / 2)) ∈ ℂ)
176	160, 175	mulcld 11164	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (π · (cos‘(𝑦 / 2))) ∈ ℂ)
177	173, 176	dmmptd 6645	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) = ℂ)
178	172, 177	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = ℂ)
179	36, 178	sseqtrrid 3979	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))
180		dvres3 25882	. . . . . . . . . . . . . . 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 839	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ))
182		resmpt 6004	. . . . . . . . . . . . . . . 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 7384	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))
185	171	reseq1d 5945	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ) = ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ))
186	181, 184, 185	3eqtr3d 2780	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ))
187		resmpt 6004	. . . . . . . . . . . . . 14 ⊢ (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
188	36, 187	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2))))
189	186, 188	eqtrdi 2788	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
190	146, 189	eqtrd 2772	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
191	190	reseq1d 5945	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
192	4	resmptd 6007	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
193	129, 191, 192	3eqtrd 2776	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
194	117, 128, 193	3eqtrd 2776	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
195	194	eqcomd 2743	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))))
196	23	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))))
197	196	oveq2d 7384	. . . . . . . 8 ⊢ (𝜑 → (ℝ D 𝐺) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))))
198	197	eqcomd 2743	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D 𝐺))
199	112, 195, 198	3eqtrrd 2777	. . . . . 6 ⊢ (𝜑 → (ℝ D 𝐺) = 𝐼)
200	199	dmeqd 5862	. . . . 5 ⊢ (𝜑 → dom (ℝ D 𝐺) = dom 𝐼)
201	105, 176	syldan 592	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (π · (cos‘(𝑦 / 2))) ∈ ℂ)
202	111, 201	dmmptd 6645	. . . . 5 ⊢ (𝜑 → dom 𝐼 = ((𝐴(,)𝐵) ∖ {𝑌}))
203	200, 202	eqtr2d 2773	. . . 4 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐺))
204		eqimss 3994	. . . 4 ⊢ (((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐺) → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐺))
205	203, 204	syl 17	. . 3 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐺))
206	105, 70	syldan 592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
207	206	ralrimiva 3130	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
208		eqid 2737	. . . . . . . 8 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))
209	208	fnmpt 6640	. . . . . . 7 ⊢ (∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}))
210	207, 209	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}))
211		eqidd 2738	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
212		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
213	212	oveq2d 7384	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
214		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
215	38	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℂ)
216		1cnd 11139	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈ ℂ)
217	216	halfcld 12398	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈ ℂ)
218	215, 217	addcld 11163	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑁 + (1 / 2)) ∈ ℂ)
219		eldifi 4085	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ (𝐴(,)𝐵))
220	219	elioored 45903	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ ℝ)
221	220	recnd 11172	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ ℂ)
222	221	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑤 ∈ ℂ)
223	218, 222	mulcld 11164	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
224	211, 213, 214, 223	fvmptd 6957	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
225		eleq1w 2820	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↔ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})))
226	225	anbi2d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ↔ (𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))))
227		oveq1 7375	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → (𝑦 mod (2 · π)) = (𝑤 mod (2 · π)))
228	227	neeq1d 2992	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → ((𝑦 mod (2 · π)) ≠ 0 ↔ (𝑤 mod (2 · π)) ≠ 0))
229	226, 228	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 mod (2 · π)) ≠ 0) ↔ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑤 mod (2 · π)) ≠ 0)))
230		eldifi 4085	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ (𝐴(,)𝐵))
231		elioore 13303	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (𝐴(,)𝐵) → 𝑦 ∈ ℝ)
232	230, 231, 130	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ ℂ)
233		2cnd 12235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 2 ∈ ℂ)
234	119	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → π ∈ ℂ)
235	134	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 2 ≠ 0)
236		0re 11146	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ
237		pipos 26436	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < π
238	236, 237	gtneii 11257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ π ≠ 0
239	238	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → π ≠ 0)
240	232, 233, 234, 235, 239	divdiv1d 11960	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
241	240	eqcomd 2743	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
242	241	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
243		dirkercncflem2.yne0	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ≠ 0)
244	243	neneqd 2938	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (sin‘(𝑦 / 2)) = 0)
245	105	halfcld 12398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℂ)
246		sineq0 26501	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 / 2) ∈ ℂ → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
247	245, 246	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
248	244, 247	mtbid 324	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / 2) / π) ∈ ℤ)
249	242, 248	eqneltrd 2857	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
250		2rp 12922	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ+
251		pirp 26438	. . . . . . . . . . . . . . . . . 18 ⊢ π ∈ ℝ+
252		rpmulcl 12942	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ+ ∧ π ∈ ℝ+) → (2 · π) ∈ ℝ+)
253	250, 251, 252	mp2an 693	. . . . . . . . . . . . . . . . 17 ⊢ (2 · π) ∈ ℝ+
254		mod0 13808	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℝ ∧ (2 · π) ∈ ℝ+) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
255	11, 253, 254	sylancl 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
256	249, 255	mtbird 325	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 mod (2 · π)) = 0)
257	256	neqned 2940	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 mod (2 · π)) ≠ 0)
258	229, 257	chvarvv 1991	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑤 mod (2 · π)) ≠ 0)
259	258	neneqd 2938	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑤 mod (2 · π)) = 0)
260		simpll 767	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝜑)
261		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))
262	221	ad2antlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑤 ∈ ℂ)
263	57	recnd 11172	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ∈ ℂ)
264	263	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑌 ∈ ℂ)
265		0red 11147	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ∈ ℝ)
266	5	nnred 12172	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℝ)
267		1red 11145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ∈ ℝ)
268	267	rehalfcld 12400	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
269	266, 268	readdcld 11173	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ)
270	5	nngt0d 12206	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 < 𝑁)
271	250	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 2 ∈ ℝ+)
272	271	rpreccld 12971	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 / 2) ∈ ℝ+)
273	266, 272	ltaddrpd 12994	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 < (𝑁 + (1 / 2)))
274	265, 266, 269, 270, 273	lttrd 11306	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 < (𝑁 + (1 / 2)))
275	274	gt0ne0d 11713	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 + (1 / 2)) ≠ 0)
276	41, 275	jca 511	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠ 0))
277	276	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠ 0))
278		mulcan 11786	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠ 0)) → (((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌) ↔ 𝑤 = 𝑌))
279	262, 264, 277, 278	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → (((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌) ↔ 𝑤 = 𝑌))
280	261, 279	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑤 = 𝑌)
281		oveq1 7375	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑌 → (𝑤 mod (2 · π)) = (𝑌 mod (2 · π)))
282		dirkercncflem2.ymod	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 mod (2 · π)) = 0)
283	281, 282	sylan9eqr 2794	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (𝑤 mod (2 · π)) = 0)
284	260, 280, 283	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → (𝑤 mod (2 · π)) = 0)
285	259, 284	mtand 816	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))
286	41, 263	mulcld 11164	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ)
287	286	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ)
288		elsn2g 4623	. . . . . . . . . . . 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 325	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑁 + (1 / 2)) · 𝑤) ∈ {((𝑁 + (1 / 2)) · 𝑌)})
291	223, 290	eldifd 3914	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑤) ∈ (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
292	224, 291	eqeltrd 2837	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
293		sinf 16061	. . . . . . . . . . . 12 ⊢ sin:ℂ⟶ℂ
294	293	fdmi 6681	. . . . . . . . . . 11 ⊢ dom sin = ℂ
295	294	eqcomi 2746	. . . . . . . . . 10 ⊢ ℂ = dom sin
296	295	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ℂ = dom sin)
297	296	difeq1d 4079	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}) = (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
298	292, 297	eleqtrd 2839	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
299	298	ralrimiva 3130	. . . . . 6 ⊢ (𝜑 → ∀𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
300		fnfvrnss 7075	. . . . . 6 ⊢ (((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ∀𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) → ran (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ⊆ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
301	210, 299, 300	syl2anc 585	. . . . 5 ⊢ (𝜑 → ran (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ⊆ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
302		uncom 4112	. . . . . . . . . 10 ⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌}))
303	302	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})))
304	27	snssd 4767	. . . . . . . . . 10 ⊢ (𝜑 → {𝑌} ⊆ (𝐴(,)𝐵))
305		undif 4436	. . . . . . . . . 10 ⊢ ({𝑌} ⊆ (𝐴(,)𝐵) ↔ ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐴(,)𝐵))
306	304, 305	sylib 218	. . . . . . . . 9 ⊢ (𝜑 → ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐴(,)𝐵))
307	303, 306	eqtrd 2772	. . . . . . . 8 ⊢ (𝜑 → (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = (𝐴(,)𝐵))
308	307	mpteq1d 5190	. . . . . . 7 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
309		iftrue 4487	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑌))
310		oveq2 7376	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑌 → ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))
311	309, 310	eqtr4d 2775	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
312	311	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
313		iffalse 4490	. . . . . . . . . . . . 13 ⊢ (¬ 𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))
314	313	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))
315		eqidd 2738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
316		oveq2 7376	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
317	316	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
318		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ (𝐴(,)𝐵))
319		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑤 = 𝑌 → ¬ 𝑤 = 𝑌)
320		velsn 4598	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ {𝑌} ↔ 𝑤 = 𝑌)
321	319, 320	sylnibr 329	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑤 = 𝑌 → ¬ 𝑤 ∈ {𝑌})
322	321	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → ¬ 𝑤 ∈ {𝑌})
323	318, 322	eldifd 3914	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
324	323	adantll 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
325	41	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑁 + (1 / 2)) ∈ ℂ)
326		elioore 13303	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → 𝑤 ∈ ℝ)
327	326	recnd 11172	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → 𝑤 ∈ ℂ)
328	327	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 𝑤 ∈ ℂ)
329	325, 328	mulcld 11164	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
330	329	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
331	315, 317, 324, 330	fvmptd 6957	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
332	314, 331	eqtrd 2772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
333	312, 332	pm2.61dan 813	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
334	333	mpteq2dva 5193	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)))
335		ioosscn 13336	. . . . . . . . . . . . . 14 ⊢ (𝐴(,)𝐵) ⊆ ℂ
336		resmpt 6004	. . . . . . . . . . . . . 14 ⊢ ((𝐴(,)𝐵) ⊆ ℂ → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)))
337	335, 336	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤))
338		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) = (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤))
339	338	mulc1cncf 24866	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 + (1 / 2)) ∈ ℂ → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (ℂ–cn→ℂ))
340	41, 339	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (ℂ–cn→ℂ))
341	51	cnfldtop 24739	. . . . . . . . . . . . . . . . . . 19 ⊢ (TopOpen‘ℂfld) ∈ Top
342		unicntop 24741	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℂ = ∪ (TopOpen‘ℂfld)
343	342	restid 17365	. . . . . . . . . . . . . . . . . . 19 ⊢ ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
344	341, 343	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
345	344	eqcomi 2746	. . . . . . . . . . . . . . . . 17 ⊢ (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
346	51, 345, 345	cncfcn 24871	. . . . . . . . . . . . . . . 16 ⊢ ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℂ) = ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
347	74, 75, 346	sylancr 588	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℂ–cn→ℂ) = ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
348	340, 347	eleqtrd 2839	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
349	2, 37	sstrid 3947	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
350	342	cnrest 23241	. . . . . . . . . . . . . 14 ⊢ (((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
351	348, 349, 350	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
352	337, 351	eqeltrrid 2842	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
353	51	cnfldtopon 24738	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
354		resttopon 23117	. . . . . . . . . . . . . 14 ⊢ (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)))
355	353, 349, 354	sylancr 588	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)))
356		cncnp 23236	. . . . . . . . . . . . 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 587	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ↔ ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))))
358	352, 357	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦)))
359	358	simprd 495	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
360		fveq2 6842	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
361	360	eleq2d 2823	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌)))
362	361	rspccva 3577	. . . . . . . . . 10 ⊢ ((∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
363	359, 27, 362	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
364	334, 363	eqeltrd 2837	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
365	307	eqcomd 2743	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(,)𝐵) = (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}))
366	365	oveq2d 7384	. . . . . . . . . 10 ⊢ (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})))
367	366	oveq1d 7383	. . . . . . . . 9 ⊢ (𝜑 → (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld)))
368	367	fveq1d 6844	. . . . . . . 8 ⊢ (𝜑 → ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌) = ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
369	364, 368	eleqtrd 2839	. . . . . . 7 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
370	308, 369	eqeltrd 2837	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
371		eqid 2737	. . . . . . 7 ⊢ ((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) = ((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}))
372		eqid 2737	. . . . . . 7 ⊢ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))
373	206, 208	fmptd 7068	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
374	4, 36	sstrdi 3948	. . . . . . 7 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℂ)
375	371, 51, 372, 373, 374, 263	ellimc 25842	. . . . . 6 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · 𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) limℂ 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌)))
376	370, 375	mpbird 257	. . . . 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 11801	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · π) ≠ 0)
380	263, 156, 379	divcan1d 11930	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑌 / (2 · π)) · (2 · π)) = 𝑌)
381	380	eqcomd 2743	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 = ((𝑌 / (2 · π)) · (2 · π)))
382	381	oveq2d 7384	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))))
383	382	fveq2d 6846	. . . . . . 7 ⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) = (sin‘((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π)))))
384	263, 156, 379	divcld 11929	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 / (2 · π)) ∈ ℂ)
385	41, 384, 156	mul12d 11354	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = ((𝑌 / (2 · π)) · ((𝑁 + (1 / 2)) · (2 · π))))
386	41, 154, 155	mulassd 11167	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · 2) · π) = ((𝑁 + (1 / 2)) · (2 · π)))
387	386	eqcomd 2743	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · (2 · π)) = (((𝑁 + (1 / 2)) · 2) · π))
388	387	oveq2d 7384	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑌 / (2 · π)) · ((𝑁 + (1 / 2)) · (2 · π))) = ((𝑌 / (2 · π)) · (((𝑁 + (1 / 2)) · 2) · π)))
389	38, 40, 154	adddird 11169	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 2) = ((𝑁 · 2) + ((1 / 2) · 2)))
390	154, 377	recid2d 11925	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1 / 2) · 2) = 1)
391	390	oveq2d 7384	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 · 2) + ((1 / 2) · 2)) = ((𝑁 · 2) + 1))
392	389, 391	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 2) = ((𝑁 · 2) + 1))
393	392	oveq1d 7383	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · 2) · π) = (((𝑁 · 2) + 1) · π))
394	393	oveq2d 7384	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑌 / (2 · π)) · (((𝑁 + (1 / 2)) · 2) · π)) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
395	385, 388, 394	3eqtrd 2776	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
396	38, 154	mulcld 11164	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 · 2) ∈ ℂ)
397		1cnd 11139	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
398	396, 397	addcld 11163	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 · 2) + 1) ∈ ℂ)
399	384, 398, 155	mulassd 11167	. . . . . . . . 9 ⊢ (𝜑 → (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
400	395, 399	eqtr4d 2775	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π))
401	400	fveq2d 6846	. . . . . . 7 ⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π)))) = (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π)))
402		mod0 13808	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ ℝ ∧ (2 · π) ∈ ℝ+) → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
403	57, 253, 402	sylancl 587	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
404	282, 403	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → (𝑌 / (2 · π)) ∈ ℤ)
405	5	nnzd 12526	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℤ)
406		2z 12535	. . . . . . . . . . . 12 ⊢ 2 ∈ ℤ
407	406	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℤ)
408	405, 407	zmulcld 12614	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 · 2) ∈ ℤ)
409	408	peano2zd 12611	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 · 2) + 1) ∈ ℤ)
410	404, 409	zmulcld 12614	. . . . . . . 8 ⊢ (𝜑 → ((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ∈ ℤ)
411		sinkpi 26499	. . . . . . . 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 2776	. . . . . 6 ⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) = 0)
414		sincn 26422	. . . . . . . 8 ⊢ sin ∈ (ℂ–cn→ℂ)
415	414	a1i 11	. . . . . . 7 ⊢ (𝜑 → sin ∈ (ℂ–cn→ℂ))
416	415, 286	cnlimci 25858	. . . . . 6 ⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) ∈ (sin limℂ ((𝑁 + (1 / 2)) · 𝑌)))
417	413, 416	eqeltrrd 2838	. . . . 5 ⊢ (𝜑 → 0 ∈ (sin limℂ ((𝑁 + (1 / 2)) · 𝑌)))
418	301, 376, 417	limccog 45974	. . . 4 ⊢ (𝜑 → 0 ∈ ((sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) limℂ 𝑌))
419	14	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
420	213	fveq2d 6846	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
421	223	sincld 16067	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑤)) ∈ ℂ)
422	419, 420, 214, 421	fvmptd 6957	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹‘𝑤) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
423	224	fveq2d 6846	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
424	422, 423	eqtr4d 2775	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹‘𝑤) = (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))
425	424	mpteq2dva 5193	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (𝐹‘𝑤)) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
426	15	feqmptd 6910	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (𝐹‘𝑤)))
427		fcompt 7088	. . . . . . 7 ⊢ ((sin:ℂ⟶ℂ ∧ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
428	293, 373, 427	sylancr 588	. . . . . 6 ⊢ (𝜑 → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
429	425, 426, 428	3eqtr4rd 2783	. . . . 5 ⊢ (𝜑 → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = 𝐹)
430	429	oveq1d 7383	. . . 4 ⊢ (𝜑 → ((sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) limℂ 𝑌) = (𝐹 limℂ 𝑌))
431	418, 430	eleqtrd 2839	. . 3 ⊢ (𝜑 → 0 ∈ (𝐹 limℂ 𝑌))
432		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → 𝑤 = 𝑌)
433	432	iftrued 4489	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = 0)
434	263, 154, 156, 377, 379	divdiv32d 11954	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑌 / 2) / (2 · π)) = ((𝑌 / (2 · π)) / 2))
435	434	oveq1d 7383	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑌 / 2) / (2 · π)) · (2 · π)) = (((𝑌 / (2 · π)) / 2) · (2 · π)))
436	263	halfcld 12398	. . . . . . . . . . . . . . . . 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 7384	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑌 / (2 · π)) · ((2 · π) / 2)) = ((𝑌 / (2 · π)) · π))
441	438, 440	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑌 / (2 · π)) / 2) · (2 · π)) = ((𝑌 / (2 · π)) · π))
442	435, 437, 441	3eqtr3d 2780	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 / 2) = ((𝑌 / (2 · π)) · π))
443	442	fveq2d 6846	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (sin‘(𝑌 / 2)) = (sin‘((𝑌 / (2 · π)) · π)))
444		sinkpi 26499	. . . . . . . . . . . . . . 15 ⊢ ((𝑌 / (2 · π)) ∈ ℤ → (sin‘((𝑌 / (2 · π)) · π)) = 0)
445	404, 444	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (sin‘((𝑌 / (2 · π)) · π)) = 0)
446	443, 445	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → (sin‘(𝑌 / 2)) = 0)
447	446	oveq2d 7384	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · 0))
448	156	mul01d 11344	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · π) · 0) = 0)
449	447, 448	eqtrd 2772	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · π) · (sin‘(𝑌 / 2))) = 0)
450	449	eqcomd 2743	. . . . . . . . . 10 ⊢ (𝜑 → 0 = ((2 · π) · (sin‘(𝑌 / 2))))
451	450	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → 0 = ((2 · π) · (sin‘(𝑌 / 2))))
452		fvoveq1 7391	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑌 → (sin‘(𝑤 / 2)) = (sin‘(𝑌 / 2)))
453	452	oveq2d 7384	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑌 → ((2 · π) · (sin‘(𝑤 / 2))) = ((2 · π) · (sin‘(𝑌 / 2))))
454	453	eqcomd 2743	. . . . . . . . . 10 ⊢ (𝑤 = 𝑌 → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
455	454	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
456	433, 451, 455	3eqtrd 2776	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
457		iffalse 4490	. . . . . . . . . 10 ⊢ (¬ 𝑤 = 𝑌 → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = (𝐺‘𝑤))
458	457	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = (𝐺‘𝑤))
459		fvoveq1 7391	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → (sin‘(𝑦 / 2)) = (sin‘(𝑤 / 2)))
460	459	oveq2d 7384	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
461	120	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (2 · π) ∈ ℂ)
462	328	halfcld 12398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 / 2) ∈ ℂ)
463	462	sincld 16067	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (sin‘(𝑤 / 2)) ∈ ℂ)
464	461, 463	mulcld 11164	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((2 · π) · (sin‘(𝑤 / 2))) ∈ ℂ)
465	464	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((2 · π) · (sin‘(𝑤 / 2))) ∈ ℂ)
466	23, 460, 324, 465	fvmptd3 6973	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐺‘𝑤) = ((2 · π) · (sin‘(𝑤 / 2))))
467	458, 466	eqtrd 2772	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
468	456, 467	pm2.61dan 813	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
469	468	mpteq2dva 5193	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))))
470		eqid 2737	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2)))) = (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2))))
471	75, 156, 75	constcncfg 46224	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (2 · π)) ∈ (ℂ–cn→ℂ))
472		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℂ → 𝑤 ∈ ℂ)
473		2cnd 12235	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℂ → 2 ∈ ℂ)
474	134	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℂ → 2 ≠ 0)
475	472, 473, 474	divrec2d 11933	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ℂ → (𝑤 / 2) = ((1 / 2) · 𝑤))
476	475	mpteq2ia 5195	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ ℂ ↦ (𝑤 / 2)) = (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤))
477		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) = (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤))
478	477	mulc1cncf 24866	. . . . . . . . . . . . . . . 16 ⊢ ((1 / 2) ∈ ℂ → (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) ∈ (ℂ–cn→ℂ))
479	39, 478	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) ∈ (ℂ–cn→ℂ)
480	476, 479	eqeltri 2833	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ ℂ ↦ (𝑤 / 2)) ∈ (ℂ–cn→ℂ)
481	480	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (𝑤 / 2)) ∈ (ℂ–cn→ℂ))
482	415, 481	cncfmpt1f 24875	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (sin‘(𝑤 / 2))) ∈ (ℂ–cn→ℂ))
483	471, 482	mulcncf 25414	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ (ℂ–cn→ℂ))
484	470, 483, 349, 75, 464	cncfmptssg 46223	. . . . . . . . . 10 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
485		eqid 2737	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
486	51, 485, 345	cncfcn 24871	. . . . . . . . . . 11 ⊢ (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
487	349, 74, 486	sylancl 587	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
488	484, 487	eleqtrd 2839	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
489		cncnp 23236	. . . . . . . . . 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 587	. . . . . . . . 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 232	. . . . . . . 8 ⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦)))
492	491	simprd 495	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
493	360	eleq2d 2823	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌)))
494	493	rspccva 3577	. . . . . . 7 ⊢ ((∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
495	492, 27, 494	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
496	469, 495	eqeltrd 2837	. . . . 5 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
497	307	mpteq1d 5190	. . . . 5 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))))
498	366	eqcomd 2743	. . . . . . 7 ⊢ (𝜑 → ((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
499	498	oveq1d 7383	. . . . . 6 ⊢ (𝜑 → (((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld)))
500	499	fveq1d 6844	. . . . 5 ⊢ (𝜑 → ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌) = ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
501	496, 497, 500	3eltr4d 2852	. . . 4 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
502		eqid 2737	. . . . 5 ⊢ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤)))
503	11, 124	syldan 592	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
504	503, 23	fmptd 7068	. . . . 5 ⊢ (𝜑 → 𝐺:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
505	371, 51, 502, 504, 374, 263	ellimc 25842	. . . 4 ⊢ (𝜑 → (0 ∈ (𝐺 limℂ 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌)))
506	501, 505	mpbird 257	. . 3 ⊢ (𝜑 → 0 ∈ (𝐺 limℂ 𝑌))
507	256	nrexdv 3133	. . . 4 ⊢ (𝜑 → ¬ ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0)
508	504	ffund 6674	. . . . . 6 ⊢ (𝜑 → Fun 𝐺)
509		fvelima 6907	. . . . . 6 ⊢ ((Fun 𝐺 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0)
510	508, 509	sylan 581	. . . . 5 ⊢ ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0)
511		2cnd 12235	. . . . . . . . . . . . 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 2743	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
517	516	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
518		2cnd 12235	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → 2 ∈ ℂ)
519	119	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → π ∈ ℂ)
520	518, 519	mulcld 11164	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (2 · π) ∈ ℂ)
521	232	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → 𝑦 ∈ ℂ)
522	521	halfcld 12398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (𝑦 / 2) ∈ ℂ)
523	522	sincld 16067	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (sin‘(𝑦 / 2)) ∈ ℂ)
524	520, 523	mulcld 11164	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
525	23	fvmpt2 6961	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ) → (𝐺‘𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
526	524, 525	syldan 592	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (𝐺‘𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
527	526	eqcomd 2743	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) = (𝐺‘𝑦))
528		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (𝐺‘𝑦) = 0)
529	527, 528	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) = 0)
530	120	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (2 · π) ∈ ℂ)
531	232	halfcld 12398	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (𝑦 / 2) ∈ ℂ)
532	531	sincld 16067	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (sin‘(𝑦 / 2)) ∈ ℂ)
533	530, 532	mul0ord 11797	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (((2 · π) · (sin‘(𝑦 / 2))) = 0 ↔ ((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0)))
534	533	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (((2 · π) · (sin‘(𝑦 / 2))) = 0 ↔ ((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0)))
535	529, 534	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0))
536		2cnne0 12362	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
537	119, 238	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (π ∈ ℂ ∧ π ≠ 0)
538		mulne0 11791	. . . . . . . . . . . . . . 15 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → (2 · π) ≠ 0)
539	536, 537, 538	mp2an 693	. . . . . . . . . . . . . 14 ⊢ (2 · π) ≠ 0
540	539	neii 2935	. . . . . . . . . . . . 13 ⊢ ¬ (2 · π) = 0
541		pm2.53 852	. . . . . . . . . . . . 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 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (sin‘(𝑦 / 2)) = 0)
544	105	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → 𝑦 ∈ ℂ)
545	544	halfcld 12398	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 / 2) ∈ ℂ)
546	545, 246	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
547	543, 546	mpbid 232	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → ((𝑦 / 2) / π) ∈ ℤ)
548	517, 547	eqeltrd 2837	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 / (2 · π)) ∈ ℤ)
549	11	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → 𝑦 ∈ ℝ)
550	549, 253, 254	sylancl 587	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
551	548, 550	mpbird 257	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 mod (2 · π)) = 0)
552	551	ex 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐺‘𝑦) = 0 → (𝑦 mod (2 · π)) = 0))
553	552	reximdva 3151	. . . . . 6 ⊢ (𝜑 → (∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0 → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0))
554	553	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → (∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0 → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0))
555	510, 554	mpd 15	. . . 4 ⊢ ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0)
556	507, 555	mtand 816	. . 3 ⊢ (𝜑 → ¬ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌})))
557		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
558	111	fvmpt2 6961	. . . . . . . . 9 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (π · (cos‘(𝑦 / 2))) ∈ ℂ) → (𝐼‘𝑦) = (π · (cos‘(𝑦 / 2))))
559	557, 201, 558	syl2anc 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐼‘𝑦) = (π · (cos‘(𝑦 / 2))))
560	531	coscld 16068	. . . . . . . . . 10 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (cos‘(𝑦 / 2)) ∈ ℂ)
561	560	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ∈ ℂ)
562		dirkercncflem2.11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0)
563	512, 561, 514, 562	mulne0d 11801	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (π · (cos‘(𝑦 / 2))) ≠ 0)
564	559, 563	eqnetrd 3000	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐼‘𝑦) ≠ 0)
565	564	neneqd 2938	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝐼‘𝑦) = 0)
566	565	nrexdv 3133	. . . . 5 ⊢ (𝜑 → ¬ ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼‘𝑦) = 0)
567	201, 111	fmptd 7068	. . . . . . 7 ⊢ (𝜑 → 𝐼:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
568	567	ffund 6674	. . . . . 6 ⊢ (𝜑 → Fun 𝐼)
569		fvelima 6907	. . . . . 6 ⊢ ((Fun 𝐼 ∧ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼‘𝑦) = 0)
570	568, 569	sylan 581	. . . . 5 ⊢ ((𝜑 ∧ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼‘𝑦) = 0)
571	566, 570	mtand 816	. . . 4 ⊢ (𝜑 → ¬ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌})))
572	199	imaeq1d 6026	. . . 4 ⊢ (𝜑 → ((ℝ D 𝐺) “ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌})))
573	571, 572	neleqtrrd 2860	. . 3 ⊢ (𝜑 → ¬ 0 ∈ ((ℝ D 𝐺) “ ((𝐴(,)𝐵) ∖ {𝑌})))
574		dirkercncflem2.d	. . . . . 6 ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
575	574	dirkerval2 46446	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ ℝ) → ((𝐷‘𝑁)‘𝑌) = if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))))
576	5, 57, 575	syl2anc 585	. . . 4 ⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) = if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))))
577	282	iftrued 4489	. . . . 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 4487	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑌 → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = (((2 · 𝑁) + 1) / (2 · π)))
581	580	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = (((2 · 𝑁) + 1) / (2 · π)))
582	154, 38	mulcld 11164	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
583	582, 397	addcld 11163	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 · 𝑁) + 1) ∈ ℂ)
584	583, 154, 155, 377, 378	divdiv1d 11960	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((2 · 𝑁) + 1) / 2) / π) = (((2 · 𝑁) + 1) / (2 · π)))
585	584	eqcomd 2743	. . . . . . . . . . . . . . 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 7383	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2 · 𝑁) / 2) + (1 / 2)) = (𝑁 + (1 / 2)))
589	586, 588	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((2 · 𝑁) + 1) / 2) = (𝑁 + (1 / 2)))
590	589	oveq1d 7383	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((2 · 𝑁) + 1) / 2) / π) = ((𝑁 + (1 / 2)) / π))
591	585, 590	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) = ((𝑁 + (1 / 2)) / π))
592	591	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((2 · 𝑁) + 1) / (2 · π)) = ((𝑁 + (1 / 2)) / π))
593	310	fveq2d 6846	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑌 → (cos‘((𝑁 + (1 / 2)) · 𝑤)) = (cos‘((𝑁 + (1 / 2)) · 𝑌)))
594	593	oveq2d 7384	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑌 → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))))
595		fvoveq1 7391	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑌 → (cos‘(𝑤 / 2)) = (cos‘(𝑌 / 2)))
596	595	oveq2d 7384	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑌 → (π · (cos‘(𝑤 / 2))) = (π · (cos‘(𝑌 / 2))))
597	594, 596	oveq12d 7386	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑌 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))))
598	597	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))))
599	38, 40, 263	adddird 11169	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑁 · 𝑌) + ((1 / 2) · 𝑌)))
600	397, 154, 263, 377	div32d 11952	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((1 / 2) · 𝑌) = (1 · (𝑌 / 2)))
601	436	mullidd 11162	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · (𝑌 / 2)) = (𝑌 / 2))
602	600, 601	eqtrd 2772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1 / 2) · 𝑌) = (𝑌 / 2))
603	602	oveq2d 7384	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 · 𝑌) + ((1 / 2) · 𝑌)) = ((𝑁 · 𝑌) + (𝑌 / 2)))
604	38, 263	mulcld 11164	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑁 · 𝑌) ∈ ℂ)
605	604, 436	addcomd 11347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 · 𝑌) + (𝑌 / 2)) = ((𝑌 / 2) + (𝑁 · 𝑌)))
606	599, 603, 605	3eqtrd 2776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑌 / 2) + (𝑁 · 𝑌)))
607	606	fveq2d 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (cos‘((𝑁 + (1 / 2)) · 𝑌)) = (cos‘((𝑌 / 2) + (𝑁 · 𝑌))))
608	604, 156, 379	divcan1d 11930	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝑁 · 𝑌) / (2 · π)) · (2 · π)) = (𝑁 · 𝑌))
609	608	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑁 · 𝑌) = (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))
610	609	oveq2d 7384	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑌 / 2) + (𝑁 · 𝑌)) = ((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π))))
611	610	fveq2d 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (cos‘((𝑌 / 2) + (𝑁 · 𝑌))) = (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))))
612	38, 263, 156, 379	divassd 11964	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 · 𝑌) / (2 · π)) = (𝑁 · (𝑌 / (2 · π))))
613	405, 404	zmulcld 12614	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑁 · (𝑌 / (2 · π))) ∈ ℤ)
614	612, 613	eqeltrd 2837	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 · 𝑌) / (2 · π)) ∈ ℤ)
615		cosper 26459	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑌 / 2) ∈ ℂ ∧ ((𝑁 · 𝑌) / (2 · π)) ∈ ℤ) → (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))) = (cos‘(𝑌 / 2)))
616	436, 614, 615	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))) = (cos‘(𝑌 / 2)))
617	607, 611, 616	3eqtrd 2776	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (cos‘((𝑁 + (1 / 2)) · 𝑌)) = (cos‘(𝑌 / 2)))
618	617	oveq2d 7384	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) = ((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))))
619	618	oveq1d 7383	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = (((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))) / (π · (cos‘(𝑌 / 2)))))
620	436	coscld 16068	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (cos‘(𝑌 / 2)) ∈ ℂ)
621	263, 154, 155, 377, 378	divdiv1d 11960	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑌 / 2) / π) = (𝑌 / (2 · π)))
622	621, 404	eqeltrd 2837	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑌 / 2) / π) ∈ ℤ)
623	622	zred 12608	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑌 / 2) / π) ∈ ℝ)
624	623, 272	ltaddrpd 12994	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑌 / 2) / π) < (((𝑌 / 2) / π) + (1 / 2)))
625		halflt1 12370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 / 2) < 1
626	625	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (1 / 2) < 1)
627	268, 267, 623, 626	ltadd2dd 11304	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑌 / 2) / π) + (1 / 2)) < (((𝑌 / 2) / π) + 1))
628		btwnnz 12580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑌 / 2) / π) ∈ ℤ ∧ ((𝑌 / 2) / π) < (((𝑌 / 2) / π) + (1 / 2)) ∧ (((𝑌 / 2) / π) + (1 / 2)) < (((𝑌 / 2) / π) + 1)) → ¬ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ)
629	622, 624, 627, 628	syl3anc 1374	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ¬ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ)
630		coseq0 46216	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑌 / 2) ∈ ℂ → ((cos‘(𝑌 / 2)) = 0 ↔ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ))
631	436, 630	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((cos‘(𝑌 / 2)) = 0 ↔ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ))
632	629, 631	mtbird 325	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ (cos‘(𝑌 / 2)) = 0)
633	632	neqned 2940	. . . . . . . . . . . . . . . . 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 2772	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
636	635	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
637	598, 636	eqtr2d 2773	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) / π) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))))
638	581, 592, 637	3eqtrrd 2777	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)))
639		iffalse 4490	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑤 = 𝑌 → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))
640	639	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))
641		eqidd 2738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))))
642		fveq2 6842	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → (𝐻‘𝑦) = (𝐻‘𝑤))
643		fveq2 6842	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → (𝐼‘𝑦) = (𝐼‘𝑤))
644	642, 643	oveq12d 7386	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → ((𝐻‘𝑦) / (𝐼‘𝑦)) = ((𝐻‘𝑤) / (𝐼‘𝑤)))
645	644	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝐻‘𝑦) / (𝐼‘𝑦)) = ((𝐻‘𝑤) / (𝐼‘𝑤)))
646	106, 100	fmptd 7068	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐻:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
647	646	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐻:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
648	647, 324	ffvelcdmd 7039	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐻‘𝑤) ∈ ℂ)
649	567	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐼:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
650	649, 324	ffvelcdmd 7039	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼‘𝑤) ∈ ℂ)
651	111	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
652		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
653	652	fvoveq1d 7390	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (cos‘(𝑦 / 2)) = (cos‘(𝑤 / 2)))
654	653	oveq2d 7384	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (π · (cos‘(𝑦 / 2))) = (π · (cos‘(𝑤 / 2))))
655	119	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → π ∈ ℂ)
656	327	halfcld 12398	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → (𝑤 / 2) ∈ ℂ)
657	656	coscld 16068	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → (cos‘(𝑤 / 2)) ∈ ℂ)
658	655, 657	mulcld 11164	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → (π · (cos‘(𝑤 / 2))) ∈ ℂ)
659	658	ad2antlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π · (cos‘(𝑤 / 2))) ∈ ℂ)
660	651, 654, 324, 659	fvmptd 6957	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼‘𝑤) = (π · (cos‘(𝑤 / 2))))
661	537	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π ∈ ℂ ∧ π ≠ 0))
662	657	ad2antlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ∈ ℂ)
663		simpll 767	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝜑)
664		fvoveq1 7391	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑤 → (cos‘(𝑦 / 2)) = (cos‘(𝑤 / 2)))
665	664	neeq1d 2992	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑤 → ((cos‘(𝑦 / 2)) ≠ 0 ↔ (cos‘(𝑤 / 2)) ≠ 0))
666	226, 665	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑤 → (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0) ↔ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑤 / 2)) ≠ 0)))
667	666, 562	chvarvv 1991	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑤 / 2)) ≠ 0)
668	663, 324, 667	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
669		mulne0 11791	. . . . . . . . . . . . . . . . 17 ⊢ (((π ∈ ℂ ∧ π ≠ 0) ∧ ((cos‘(𝑤 / 2)) ∈ ℂ ∧ (cos‘(𝑤 / 2)) ≠ 0)) → (π · (cos‘(𝑤 / 2))) ≠ 0)
670	661, 662, 668, 669	syl12anc 837	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π · (cos‘(𝑤 / 2))) ≠ 0)
671	660, 670	eqnetrd 3000	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼‘𝑤) ≠ 0)
672	648, 650, 671	divcld 11929	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝐻‘𝑤) / (𝐼‘𝑤)) ∈ ℂ)
673	641, 645, 324, 672	fvmptd 6957	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤) = ((𝐻‘𝑤) / (𝐼‘𝑤)))
674	100	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
675	317	fveq2d 6846	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (cos‘((𝑁 + (1 / 2)) · 𝑦)) = (cos‘((𝑁 + (1 / 2)) · 𝑤)))
676	675	oveq2d 7384	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))))
677	329	coscld 16068	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘((𝑁 + (1 / 2)) · 𝑤)) ∈ ℂ)
678	325, 677	mulcld 11164	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ℂ)
679	678	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ℂ)
680	674, 676, 324, 679	fvmptd 6957	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐻‘𝑤) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))))
681	680, 660	oveq12d 7386	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝐻‘𝑤) / (𝐼‘𝑤)) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))))
682	640, 673, 681	3eqtrrd 2777	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)))
683	638, 682	pm2.61dan 813	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)))
684	683	mpteq2dva 5193	. . . . . . . . . 10 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))))
685	579, 684	eqtr2d 2773	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) = 𝐿)
686	349, 41, 75	constcncfg 46224	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
687		cosf 16062	. . . . . . . . . . . . . . . . . . 19 ⊢ cos:ℂ⟶ℂ
688	231, 44	sylan2 594	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
689		eqid 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))
690	688, 689	fmptd 7068	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)):(𝐴(,)𝐵)⟶ℂ)
691		fcompt 7088	. . . . . . . . . . . . . . . . . . 19 ⊢ ((cos:ℂ⟶ℂ ∧ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)):(𝐴(,)𝐵)⟶ℂ) → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
692	687, 690, 691	sylancr 588	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
693		eqidd 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
694	316	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
695		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 𝑤 ∈ (𝐴(,)𝐵))
696	693, 694, 695, 329	fvmptd 6957	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
697	696	fveq2d 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = (cos‘((𝑁 + (1 / 2)) · 𝑤)))
698	697	mpteq2dva 5193	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))))
699	692, 698	eqtr2d 2773	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))) = (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))))
700	349, 41, 75	constcncfg 46224	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
701	349, 75	idcncfg 46225	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 𝑦) ∈ ((𝐴(,)𝐵)–cn→ℂ))
702	700, 701	mulcncf 25414	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
703		coscn 26423	. . . . . . . . . . . . . . . . . . 19 ⊢ cos ∈ (ℂ–cn→ℂ)
704	703	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → cos ∈ (ℂ–cn→ℂ))
705	702, 704	cncfco 24868	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
706	699, 705	eqeltrd 2837	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
707	686, 706	mulcncf 25414	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
708		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2))))
709	349, 155, 75	constcncfg 46224	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ π) ∈ ((𝐴(,)𝐵)–cn→ℂ))
710		2cnd 12235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ)
711	134	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 2 ≠ 0)
712	328, 710, 711	divrecd 11932	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 / 2) = (𝑤 · (1 / 2)))
713	712	mpteq2dva 5193	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 / 2)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 · (1 / 2))))
714		eqid 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2))) = (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2)))
715		cncfmptid 24874	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ))
716	74, 74, 715	mp2an 693	. . . . . . . . . . . . . . . . . . . . . 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 46224	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 / 2) ∈ ℂ → (𝑤 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
721	39, 720	mp1i 13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
722	717, 721	mulcncf 25414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2))) ∈ (ℂ–cn→ℂ))
723	712, 462	eqeltrrd 2838	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 · (1 / 2)) ∈ ℂ)
724	714, 722, 349, 75, 723	cncfmptssg 46223	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 · (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
725	713, 724	eqeltrd 2837	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 / 2)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
726	704, 725	cncfmpt1f 24875	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑤 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
727	709, 726	mulcncf 25414	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
728		ssid 3958	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)
729	728	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵))
730		difssd 4091	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
731	658	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ∈ ℂ)
732	119	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → π ∈ ℂ)
733	657	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘(𝑤 / 2)) ∈ ℂ)
734	238	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → π ≠ 0)
735	595	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) = (cos‘(𝑌 / 2)))
736	633	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (cos‘(𝑌 / 2)) ≠ 0)
737	735, 736	eqnetrd 3000	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
738	737	adantlr 716	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
739	738, 668	pm2.61dan 813	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘(𝑤 / 2)) ≠ 0)
740	732, 733, 734, 739	mulne0d 11801	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ≠ 0)
741	740	neneqd 2938	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ¬ (π · (cos‘(𝑤 / 2))) = 0)
742		elsng 4596	. . . . . . . . . . . . . . . . . . 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 325	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ¬ (π · (cos‘(𝑤 / 2))) ∈ {0})
745	731, 744	eldifd 3914	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ∈ (ℂ ∖ {0}))
746	708, 727, 729, 730, 745	cncfmptssg 46223	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→(ℂ ∖ {0})))
747	707, 746	divcncf 25416	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
748	747, 487	eleqtrd 2839	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
749	579, 748	eqeltrd 2837	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
750		cncnp 23236	. . . . . . . . . . . . 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 587	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))))
752	749, 751	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦)))
753	752	simprd 495	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
754	360	eleq2d 2823	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → (𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ↔ 𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌)))
755	754	rspccva 3577	. . . . . . . . . 10 ⊢ ((∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → 𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
756	753, 27, 755	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
757	685, 756	eqeltrd 2837	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
758	307	mpteq1d 5190	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))))
759	757, 758, 500	3eltr4d 2852	. . . . . . 7 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
760		eqid 2737	. . . . . . . 8 ⊢ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)))
761	100	fvmpt2 6961	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ) → (𝐻‘𝑦) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
762	557, 106, 761	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐻‘𝑦) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
763	762, 559	oveq12d 7386	. . . . . . . . . 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 2837	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐻‘𝑦) / (𝐼‘𝑦)) ∈ ℂ)
766		eqid 2737	. . . . . . . . 9 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))
767	765, 766	fmptd 7068	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
768	371, 51, 760, 767, 374, 263	ellimc 25842	. . . . . . 7 ⊢ (𝜑 → ((((2 · 𝑁) + 1) / (2 · π)) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) limℂ 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌)))
769	759, 768	mpbird 257	. . . . . 6 ⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) limℂ 𝑌))
770	103	eqcomd 2743	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 = (ℝ D 𝐹))
771	770	fveq1d 6844	. . . . . . . . 9 ⊢ (𝜑 → (𝐻‘𝑦) = ((ℝ D 𝐹)‘𝑦))
772	199	eqcomd 2743	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 = (ℝ D 𝐺))
773	772	fveq1d 6844	. . . . . . . . 9 ⊢ (𝜑 → (𝐼‘𝑦) = ((ℝ D 𝐺)‘𝑦))
774	771, 773	oveq12d 7386	. . . . . . . 8 ⊢ (𝜑 → ((𝐻‘𝑦) / (𝐼‘𝑦)) = (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)))
775	774	mpteq2dv 5194	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))))
776	775	oveq1d 7383	. . . . . 6 ⊢ (𝜑 → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) limℂ 𝑌) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) limℂ 𝑌))
777	769, 776	eleqtrd 2839	. . . . 5 ⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) limℂ 𝑌))
778	577, 777	eqeltrd 2837	. . . 4 ⊢ (𝜑 → if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) limℂ 𝑌))
779	576, 778	eqeltrd 2837	. . 3 ⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) limℂ 𝑌))
780	4, 15, 24, 26, 27, 28, 110, 205, 431, 506, 556, 573, 779	lhop 25989	. 2 ⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))) limℂ 𝑌))
781	574	dirkerval 46443	. . . . . 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 5945	. . . 4 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
784	4	resmptd 6007	. . . 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 4492	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
786	13	recnd 11172	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
787	14	fvmpt2 6961	. . . . . . . 8 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ) → (𝐹‘𝑦) = (sin‘((𝑁 + (1 / 2)) · 𝑦)))
788	557, 786, 787	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹‘𝑦) = (sin‘((𝑁 + (1 / 2)) · 𝑦)))
789	557, 503, 525	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐺‘𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
790	788, 789	oveq12d 7386	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐹‘𝑦) / (𝐺‘𝑦)) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
791	785, 790	eqtr4d 2775	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((𝐹‘𝑦) / (𝐺‘𝑦)))
792	791	mpteq2dva 5193	. . . 4 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))))
793	783, 784, 792	3eqtrrd 2777	. . 3 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))) = ((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
794	793	oveq1d 7383	. 2 ⊢ (𝜑 → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))) limℂ 𝑌) = (((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) limℂ 𝑌))
795	780, 794	eleqtrd 2839	1 ⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ (((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) limℂ 𝑌))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062   ∖ cdif 3900   ∪ cun 3901   ⊆ wss 3903  ifcif 4481  {csn 4582  {cpr 4584   class class class wbr 5100   ↦ cmpt 5181  dom cdm 5632  ran crn 5633   ↾ cres 5634   “ cima 5635   ∘ ccom 5636  Fun wfun 6494   Fn wfn 6495  ⟶wf 6496  ‘cfv 6500  (class class class)co 7368  ℂcc 11036  ℝcr 11037  0cc0 11038  1c1 11039   + caddc 11041   · cmul 11043   < clt 11178   / cdiv 11806  ℕcn 12157  2c2 12212  ℤcz 12500  ℝ⁺crp 12917  (,)cioo 13273   mod cmo 13801  sincsin 15998  cosccos 15999  πcpi 16001   ↾_t crest 17352  TopOpenctopn 17353  topGenctg 17369  ℂ_fldccnfld 21321  Topctop 22849  TopOnctopon 22866  Clsdccld 22972  intcnt 22973   Cn ccn 23180   CnP ccnp 23181  Hauscha 23264  –cn→ccncf 24837   lim_ℂ climc 25831   D cdv 25832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-inf2 9562  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116  ax-addf 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-iin 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-se 5586  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-of 7632  df-om 7819  df-1st 7943  df-2nd 7944  df-supp 8113  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-2o 8408  df-er 8645  df-map 8777  df-pm 8778  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9277  df-fi 9326  df-sup 9357  df-inf 9358  df-oi 9427  df-card 9863  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-div 11807  df-nn 12158  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224  df-7 12225  df-8 12226  df-9 12227  df-n0 12414  df-z 12501  df-dec 12620  df-uz 12764  df-q 12874  df-rp 12918  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-ioo 13277  df-ioc 13278  df-ico 13279  df-icc 13280  df-fz 13436  df-fzo 13583  df-fl 13724  df-mod 13802  df-seq 13937  df-exp 13997  df-fac 14209  df-bc 14238  df-hash 14266  df-shft 15002  df-cj 15034  df-re 15035  df-im 15036  df-sqrt 15170  df-abs 15171  df-limsup 15406  df-clim 15423  df-rlim 15424  df-sum 15622  df-ef 16002  df-sin 16004  df-cos 16005  df-pi 16007  df-struct 17086  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17149  df-ress 17170  df-plusg 17202  df-mulr 17203  df-starv 17204  df-sca 17205  df-vsca 17206  df-ip 17207  df-tset 17208  df-ple 17209  df-ds 17211  df-unif 17212  df-hom 17213  df-cco 17214  df-rest 17354  df-topn 17355  df-0g 17373  df-gsum 17374  df-topgen 17375  df-pt 17376  df-prds 17379  df-xrs 17435  df-qtop 17440  df-imas 17441  df-xps 17443  df-mre 17517  df-mrc 17518  df-acs 17520  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-submnd 18721  df-mulg 19010  df-cntz 19258  df-cmn 19723  df-psmet 21313  df-xmet 21314  df-met 21315  df-bl 21316  df-mopn 21317  df-fbas 21318  df-fg 21319  df-cnfld 21322  df-top 22850  df-topon 22867  df-topsp 22889  df-bases 22902  df-cld 22975  df-ntr 22976  df-cls 22977  df-nei 23054  df-lp 23092  df-perf 23093  df-cn 23183  df-cnp 23184  df-t1 23270  df-haus 23271  df-cmp 23343  df-tx 23518  df-hmeo 23711  df-fil 23802  df-fm 23894  df-flim 23895  df-flf 23896  df-xms 24276  df-ms 24277  df-tms 24278  df-cncf 24839  df-limc 25835  df-dv 25836

This theorem is referenced by:  dirkercncflem3  46457