dirkercncflem2 - Mathbox for Glauco Siliprandi

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

Theorem dirkercncflem2 46141

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 4086	. . . . 5 ⊢ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ (𝐴(,)𝐵)
2		ioossre 13304	. . . . 5 ⊢ (𝐴(,)𝐵) ⊆ ℝ
3	1, 2	sstri 3944	. . . 4 ⊢ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ
4	3	a1i 11	. . 3 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)
5		dirkercncflem2.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℕ)
7	6	nnred 12137	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℝ)
8		halfre 12331	. . . . . . . 8 ⊢ (1 / 2) ∈ ℝ
9	8	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈ ℝ)
10	7, 9	readdcld 11138	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑁 + (1 / 2)) ∈ ℝ)
11	4	sselda 3934	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℝ)
12	10, 11	remulcld 11139	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℝ)
13	12	resincld 16049	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℝ)
14		dirkercncflem2.f	. . . 4 ⊢ 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
15	13, 14	fmptd 7047	. . 3 ⊢ (𝜑 → 𝐹:((𝐴(,)𝐵) ∖ {𝑌})⟶ℝ)
16		2re 12196	. . . . . . 7 ⊢ 2 ∈ ℝ
17		pire 26391	. . . . . . 7 ⊢ π ∈ ℝ
18	16, 17	remulcli 11125	. . . . . 6 ⊢ (2 · π) ∈ ℝ
19	18	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈ ℝ)
20	11	rehalfcld 12365	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℝ)
21	20	resincld 16049	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ∈ ℝ)
22	19, 21	remulcld 11139	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℝ)
23		dirkercncflem2.g	. . . 4 ⊢ 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
24	22, 23	fmptd 7047	. . 3 ⊢ (𝜑 → 𝐺:((𝐴(,)𝐵) ∖ {𝑌})⟶ℝ)
25		iooretop 24678	. . . 4 ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))
26	25	a1i 11	. . 3 ⊢ (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran (,)))
27		dirkercncflem2.y	. . 3 ⊢ (𝜑 → 𝑌 ∈ (𝐴(,)𝐵))
28		eqid 2731	. . 3 ⊢ ((𝐴(,)𝐵) ∖ {𝑌}) = ((𝐴(,)𝐵) ∖ {𝑌})
29	14	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
30	29	oveq2d 7362	. . . . . . 7 ⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
31		resmpt 5986	. . . . . . . . . . . 12 ⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
32	3, 31	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
33	32	eqcomi 2740	. . . . . . . . . 10 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))
34	33	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
35	34	oveq2d 7362	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))))
36		ax-resscn 11060	. . . . . . . . . 10 ⊢ ℝ ⊆ ℂ
37	36	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℝ ⊆ ℂ)
38	5	nncnd 12138	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℂ)
39		halfcn 12332	. . . . . . . . . . . . . . 15 ⊢ (1 / 2) ∈ ℂ
40	39	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
41	38, 40	addcld 11128	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ)
42	41	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑁 + (1 / 2)) ∈ ℂ)
43	37	sselda 3934	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
44	42, 43	mulcld 11129	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
45	44	sincld 16036	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
46		eqid 2731	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
47	45, 46	fmptd 7047	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℝ⟶ℂ)
48		ssid 3957	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℝ
49	48, 3	pm3.2i 470	. . . . . . . . . 10 ⊢ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)
50	49	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ))
51		eqid 2731	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
52		tgioo4 24718	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
53	51, 52	dvres 25837	. . . . . . . . 9 ⊢ (((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)) → (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
54	37, 47, 50, 53	syl21anc 837	. . . . . . . 8 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
55		retop 24674	. . . . . . . . . . 11 ⊢ (topGen‘ran (,)) ∈ Top
56		rehaus 24712	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) ∈ Haus
57	27	elioored 45588	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ ℝ)
58		uniretop 24675	. . . . . . . . . . . . . 14 ⊢ ℝ = ∪ (topGen‘ran (,))
59	58	sncld 23284	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ∈ Haus ∧ 𝑌 ∈ ℝ) → {𝑌} ∈ (Clsd‘(topGen‘ran (,))))
60	56, 57, 59	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑌} ∈ (Clsd‘(topGen‘ran (,))))
61	58	difopn 22947	. . . . . . . . . . . 12 ⊢ (((𝐴(,)𝐵) ∈ (topGen‘ran (,)) ∧ {𝑌} ∈ (Clsd‘(topGen‘ran (,)))) → ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,)))
62	25, 60, 61	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,)))
63		isopn3i 22995	. . . . . . . . . . 11 ⊢ (((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})) = ((𝐴(,)𝐵) ∖ {𝑌}))
64	55, 62, 63	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})) = ((𝐴(,)𝐵) ∖ {𝑌}))
65	64	reseq2d 5928	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
66		reelprrecn 11095	. . . . . . . . . . . . 13 ⊢ ℝ ∈ {ℝ, ℂ}
67	66	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
68	41	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑁 + (1 / 2)) ∈ ℂ)
69		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
70	68, 69	mulcld 11129	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
71	70	sincld 16036	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
72		eqid 2731	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
73	71, 72	fmptd 7047	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℂ⟶ℂ)
74		ssid 3957	. . . . . . . . . . . . 13 ⊢ ℂ ⊆ ℂ
75	74	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ ⊆ ℂ)
76		dvsinax 45950	. . . . . . . . . . . . . . . 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 5845	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = dom (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
79		eqid 2731	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
80	70	coscld 16037	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
81	68, 80	mulcld 11129	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ)
82	79, 81	dmmptd 6626	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = ℂ)
83	78, 82	eqtrd 2766	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = ℂ)
84	36, 83	sseqtrrid 3978	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
85		dvres3 25839	. . . . . . . . . . . 12 ⊢ (((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℂ⟶ℂ) ∧ (ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))) → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ))
86	67, 73, 75, 84, 85	syl22anc 838	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ))
87		resmpt 5986	. . . . . . . . . . . . 13 ⊢ (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
88	36, 87	mp1i 13	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
89	88	oveq2d 7362	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
90	77	reseq1d 5927	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = ((𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ))
91		resmpt 5986	. . . . . . . . . . . . 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 2782	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
94	86, 89, 93	3eqtr3d 2774	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
95	94	reseq1d 5927	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
96		resmpt 5986	. . . . . . . . . 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 2770	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
99	35, 54, 98	3eqtrd 2770	. . . . . . 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 2737	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = 𝐻)
103	30, 99, 102	3eqtrd 2770	. . . . . 6 ⊢ (𝜑 → (ℝ D 𝐹) = 𝐻)
104	103	dmeqd 5845	. . . . 5 ⊢ (𝜑 → dom (ℝ D 𝐹) = dom 𝐻)
105	11	recnd 11137	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℂ)
106	105, 81	syldan 591	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ)
107	100, 106	dmmptd 6626	. . . . 5 ⊢ (𝜑 → dom 𝐻 = ((𝐴(,)𝐵) ∖ {𝑌}))
108	104, 107	eqtr2d 2767	. . . 4 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐹))
109		eqimss 3993	. . . 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 5986	. . . . . . . . . . . . 13 ⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))))
114	3, 113	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
115	114	eqcomi 2740	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))
116	115	oveq2i 7357	. . . . . . . . . 10 ⊢ (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
117	116	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))))
118		2cn 12197	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
119		picn 26392	. . . . . . . . . . . . . 14 ⊢ π ∈ ℂ
120	118, 119	mulcli 11116	. . . . . . . . . . . . 13 ⊢ (2 · π) ∈ ℂ
121	120	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (2 · π) ∈ ℂ)
122	43	halfcld 12363	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 / 2) ∈ ℂ)
123	122	sincld 16036	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (sin‘(𝑦 / 2)) ∈ ℂ)
124	121, 123	mulcld 11129	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
125		eqid 2731	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))
126	124, 125	fmptd 7047	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))):ℝ⟶ℂ)
127	51, 52	dvres 25837	. . . . . . . . . 10 ⊢ (((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)) → (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
128	37, 126, 50, 127	syl21anc 837	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
129	64	reseq2d 5928	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
130	36	sseli 3930	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
131		1cnd 11104	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℂ → 1 ∈ ℂ)
132		2cnd 12200	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℂ → 2 ∈ ℂ)
133		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
134		2ne0 12226	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
135	134	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℂ → 2 ≠ 0)
136	131, 132, 133, 135	div13d 11918	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℂ → ((1 / 2) · 𝑦) = ((𝑦 / 2) · 1))
137		halfcl 12344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℂ → (𝑦 / 2) ∈ ℂ)
138	137	mulridd 11126	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℂ → ((𝑦 / 2) · 1) = (𝑦 / 2))
139	136, 138	eqtrd 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℂ → ((1 / 2) · 𝑦) = (𝑦 / 2))
140	139	fveq2d 6826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℂ → (sin‘((1 / 2) · 𝑦)) = (sin‘(𝑦 / 2)))
141	140	oveq2d 7362	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℂ → ((2 · π) · (sin‘((1 / 2) · 𝑦))) = ((2 · π) · (sin‘(𝑦 / 2))))
142	141	eqcomd 2737	. . . . . . . . . . . . . . . 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 5184	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))))
146	145	oveq2d 7362	. . . . . . . . . . . 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 11129	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((1 / 2) · 𝑦) ∈ ℂ)
150	149	sincld 16036	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (sin‘((1 / 2) · 𝑦)) ∈ ℂ)
151	147, 150	mulcld 11129	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · π) · (sin‘((1 / 2) · 𝑦))) ∈ ℂ)
152		eqid 2731	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))
153	151, 152	fmptd 7047	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))):ℂ⟶ℂ)
154		2cnd 12200	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 2 ∈ ℂ)
155	119	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → π ∈ ℂ)
156	154, 155	mulcld 11129	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (2 · π) ∈ ℂ)
157		dvasinbx 45957	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2 · π) ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦)))))
158	156, 39, 157	sylancl 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦)))))
159		2cnd 12200	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 2 ∈ ℂ)
160	119	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → π ∈ ℂ)
161	159, 160, 148	mul32d 11320	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · π) · (1 / 2)) = ((2 · (1 / 2)) · π))
162	134	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 2 ≠ 0)
163	159, 162	recidd 11889	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (2 · (1 / 2)) = 1)
164	163	oveq1d 7361	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · (1 / 2)) · π) = (1 · π))
165	160	mullidd 11127	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (1 · π) = π)
166	161, 164, 165	3eqtrd 2770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · π) · (1 / 2)) = π)
167	139	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℂ → (cos‘((1 / 2) · 𝑦)) = (cos‘(𝑦 / 2)))
168	167	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘((1 / 2) · 𝑦)) = (cos‘(𝑦 / 2)))
169	166, 168	oveq12d 7364	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦))) = (π · (cos‘(𝑦 / 2))))
170	169	mpteq2dva 5184	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦)))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
171	158, 170	eqtrd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
172	171	dmeqd 5845	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = dom (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
173		eqid 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2))))
174	69	halfcld 12363	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑦 / 2) ∈ ℂ)
175	174	coscld 16037	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘(𝑦 / 2)) ∈ ℂ)
176	160, 175	mulcld 11129	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (π · (cos‘(𝑦 / 2))) ∈ ℂ)
177	173, 176	dmmptd 6626	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) = ℂ)
178	172, 177	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = ℂ)
179	36, 178	sseqtrrid 3978	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))
180		dvres3 25839	. . . . . . . . . . . . . . 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 838	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ))
182		resmpt 5986	. . . . . . . . . . . . . . . 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 7362	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))
185	171	reseq1d 5927	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ) = ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ))
186	181, 184, 185	3eqtr3d 2774	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ))
187		resmpt 5986	. . . . . . . . . . . . . 14 ⊢ (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
188	36, 187	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2))))
189	186, 188	eqtrdi 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
190	146, 189	eqtrd 2766	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
191	190	reseq1d 5927	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
192	4	resmptd 5989	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
193	129, 191, 192	3eqtrd 2770	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
194	117, 128, 193	3eqtrd 2770	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
195	194	eqcomd 2737	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))))
196	23	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))))
197	196	oveq2d 7362	. . . . . . . 8 ⊢ (𝜑 → (ℝ D 𝐺) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))))
198	197	eqcomd 2737	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D 𝐺))
199	112, 195, 198	3eqtrrd 2771	. . . . . 6 ⊢ (𝜑 → (ℝ D 𝐺) = 𝐼)
200	199	dmeqd 5845	. . . . 5 ⊢ (𝜑 → dom (ℝ D 𝐺) = dom 𝐼)
201	105, 176	syldan 591	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (π · (cos‘(𝑦 / 2))) ∈ ℂ)
202	111, 201	dmmptd 6626	. . . . 5 ⊢ (𝜑 → dom 𝐼 = ((𝐴(,)𝐵) ∖ {𝑌}))
203	200, 202	eqtr2d 2767	. . . 4 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐺))
204		eqimss 3993	. . . 4 ⊢ (((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐺) → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐺))
205	203, 204	syl 17	. . 3 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐺))
206	105, 70	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
207	206	ralrimiva 3124	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
208		eqid 2731	. . . . . . . 8 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))
209	208	fnmpt 6621	. . . . . . 7 ⊢ (∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}))
210	207, 209	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}))
211		eqidd 2732	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
212		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
213	212	oveq2d 7362	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
214		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
215	38	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℂ)
216		1cnd 11104	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈ ℂ)
217	216	halfcld 12363	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈ ℂ)
218	215, 217	addcld 11128	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑁 + (1 / 2)) ∈ ℂ)
219		eldifi 4081	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ (𝐴(,)𝐵))
220	219	elioored 45588	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ ℝ)
221	220	recnd 11137	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ ℂ)
222	221	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑤 ∈ ℂ)
223	218, 222	mulcld 11129	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
224	211, 213, 214, 223	fvmptd 6936	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
225		eleq1w 2814	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↔ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})))
226	225	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ↔ (𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))))
227		oveq1 7353	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → (𝑦 mod (2 · π)) = (𝑤 mod (2 · π)))
228	227	neeq1d 2987	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → ((𝑦 mod (2 · π)) ≠ 0 ↔ (𝑤 mod (2 · π)) ≠ 0))
229	226, 228	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 mod (2 · π)) ≠ 0) ↔ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑤 mod (2 · π)) ≠ 0)))
230		eldifi 4081	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ (𝐴(,)𝐵))
231		elioore 13272	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (𝐴(,)𝐵) → 𝑦 ∈ ℝ)
232	230, 231, 130	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ ℂ)
233		2cnd 12200	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 2 ∈ ℂ)
234	119	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → π ∈ ℂ)
235	134	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 2 ≠ 0)
236		0re 11111	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ
237		pipos 26393	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < π
238	236, 237	gtneii 11222	. . . . . . . . . . . . . . . . . . . . 21 ⊢ π ≠ 0
239	238	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → π ≠ 0)
240	232, 233, 234, 235, 239	divdiv1d 11925	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
241	240	eqcomd 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
242	241	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
243		dirkercncflem2.yne0	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ≠ 0)
244	243	neneqd 2933	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (sin‘(𝑦 / 2)) = 0)
245	105	halfcld 12363	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℂ)
246		sineq0 26458	. . . . . . . . . . . . . . . . . . 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 2851	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
250		2rp 12892	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ⁺
251		pirp 26395	. . . . . . . . . . . . . . . . . 18 ⊢ π ∈ ℝ⁺
252		rpmulcl 12912	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ⁺ ∧ π ∈ ℝ⁺) → (2 · π) ∈ ℝ⁺)
253	250, 251, 252	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (2 · π) ∈ ℝ⁺
254		mod0 13777	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℝ ∧ (2 · π) ∈ ℝ⁺) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
255	11, 253, 254	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
256	249, 255	mtbird 325	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 mod (2 · π)) = 0)
257	256	neqned 2935	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 mod (2 · π)) ≠ 0)
258	229, 257	chvarvv 1990	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑤 mod (2 · π)) ≠ 0)
259	258	neneqd 2933	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑤 mod (2 · π)) = 0)
260		simpll 766	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝜑)
261		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))
262	221	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑤 ∈ ℂ)
263	57	recnd 11137	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ∈ ℂ)
264	263	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑌 ∈ ℂ)
265		0red 11112	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 ∈ ℝ)
266	5	nnred 12137	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℝ)
267		1red 11110	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ∈ ℝ)
268	267	rehalfcld 12365	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
269	266, 268	readdcld 11138	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ)
270	5	nngt0d 12171	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 < 𝑁)
271	250	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 2 ∈ ℝ⁺)
272	271	rpreccld 12941	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 / 2) ∈ ℝ⁺)
273	266, 272	ltaddrpd 12964	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 < (𝑁 + (1 / 2)))
274	265, 266, 269, 270, 273	lttrd 11271	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 < (𝑁 + (1 / 2)))
275	274	gt0ne0d 11678	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 + (1 / 2)) ≠ 0)
276	41, 275	jca 511	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠ 0))
277	276	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠ 0))
278		mulcan 11751	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠ 0)) → (((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌) ↔ 𝑤 = 𝑌))
279	262, 264, 277, 278	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → (((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌) ↔ 𝑤 = 𝑌))
280	261, 279	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑤 = 𝑌)
281		oveq1 7353	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑌 → (𝑤 mod (2 · π)) = (𝑌 mod (2 · π)))
282		dirkercncflem2.ymod	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑌 mod (2 · π)) = 0)
283	281, 282	sylan9eqr 2788	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (𝑤 mod (2 · π)) = 0)
284	260, 280, 283	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → (𝑤 mod (2 · π)) = 0)
285	259, 284	mtand 815	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))
286	41, 263	mulcld 11129	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ)
287	286	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ)
288		elsn2g 4617	. . . . . . . . . . . 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 3913	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑤) ∈ (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
292	224, 291	eqeltrd 2831	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
293		sinf 16030	. . . . . . . . . . . 12 ⊢ sin:ℂ⟶ℂ
294	293	fdmi 6662	. . . . . . . . . . 11 ⊢ dom sin = ℂ
295	294	eqcomi 2740	. . . . . . . . . 10 ⊢ ℂ = dom sin
296	295	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ℂ = dom sin)
297	296	difeq1d 4075	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}) = (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
298	292, 297	eleqtrd 2833	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
299	298	ralrimiva 3124	. . . . . 6 ⊢ (𝜑 → ∀𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
300		fnfvrnss 7054	. . . . . 6 ⊢ (((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ∀𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) → ran (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ⊆ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
301	210, 299, 300	syl2anc 584	. . . . 5 ⊢ (𝜑 → ran (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ⊆ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
302		uncom 4108	. . . . . . . . . 10 ⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌}))
303	302	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})))
304	27	snssd 4761	. . . . . . . . . 10 ⊢ (𝜑 → {𝑌} ⊆ (𝐴(,)𝐵))
305		undif 4432	. . . . . . . . . 10 ⊢ ({𝑌} ⊆ (𝐴(,)𝐵) ↔ ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐴(,)𝐵))
306	304, 305	sylib 218	. . . . . . . . 9 ⊢ (𝜑 → ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐴(,)𝐵))
307	303, 306	eqtrd 2766	. . . . . . . 8 ⊢ (𝜑 → (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = (𝐴(,)𝐵))
308	307	mpteq1d 5181	. . . . . . 7 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
309		iftrue 4481	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑌))
310		oveq2 7354	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑌 → ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))
311	309, 310	eqtr4d 2769	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
312	311	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
313		iffalse 4484	. . . . . . . . . . . . 13 ⊢ (¬ 𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))
314	313	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))
315		eqidd 2732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
316		oveq2 7354	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
317	316	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
318		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ (𝐴(,)𝐵))
319		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑤 = 𝑌 → ¬ 𝑤 = 𝑌)
320		velsn 4592	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ {𝑌} ↔ 𝑤 = 𝑌)
321	319, 320	sylnibr 329	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑤 = 𝑌 → ¬ 𝑤 ∈ {𝑌})
322	321	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → ¬ 𝑤 ∈ {𝑌})
323	318, 322	eldifd 3913	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
324	323	adantll 714	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
325	41	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑁 + (1 / 2)) ∈ ℂ)
326		elioore 13272	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → 𝑤 ∈ ℝ)
327	326	recnd 11137	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → 𝑤 ∈ ℂ)
328	327	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 𝑤 ∈ ℂ)
329	325, 328	mulcld 11129	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
330	329	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
331	315, 317, 324, 330	fvmptd 6936	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
332	314, 331	eqtrd 2766	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
333	312, 332	pm2.61dan 812	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
334	333	mpteq2dva 5184	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)))
335		ioosscn 13305	. . . . . . . . . . . . . 14 ⊢ (𝐴(,)𝐵) ⊆ ℂ
336		resmpt 5986	. . . . . . . . . . . . . 14 ⊢ ((𝐴(,)𝐵) ⊆ ℂ → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)))
337	335, 336	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤))
338		eqid 2731	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) = (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤))
339	338	mulc1cncf 24823	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 + (1 / 2)) ∈ ℂ → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (ℂ–cn→ℂ))
340	41, 339	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (ℂ–cn→ℂ))
341	51	cnfldtop 24696	. . . . . . . . . . . . . . . . . . 19 ⊢ (TopOpen‘ℂ_fld) ∈ Top
342		unicntop 24698	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
343	342	restid 17334	. . . . . . . . . . . . . . . . . . 19 ⊢ ((TopOpen‘ℂ_fld) ∈ Top → ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld))
344	341, 343	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld)
345	344	eqcomi 2740	. . . . . . . . . . . . . . . . 17 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
346	51, 345, 345	cncfcn 24828	. . . . . . . . . . . . . . . 16 ⊢ ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℂ) = ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
347	74, 75, 346	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℂ–cn→ℂ) = ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
348	340, 347	eleqtrd 2833	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)))
349	2, 37	sstrid 3946	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
350	342	cnrest 23198	. . . . . . . . . . . . . 14 ⊢ (((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((TopOpen‘ℂ_fld) Cn (TopOpen‘ℂ_fld)) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)))
351	348, 349, 350	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)))
352	337, 351	eqeltrrid 2836	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)))
353	51	cnfldtopon 24695	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
354		resttopon 23074	. . . . . . . . . . . . . 14 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)))
355	353, 349, 354	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)))
356		cncnp 23193	. . . . . . . . . . . . 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 586	. . . . . . . . . . . 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 6822	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦) = ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
361	360	eleq2d 2817	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌)))
362	361	rspccva 3576	. . . . . . . . . 10 ⊢ ((∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
363	359, 27, 362	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
364	334, 363	eqeltrd 2831	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
365	307	eqcomd 2737	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(,)𝐵) = (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}))
366	365	oveq2d 7362	. . . . . . . . . 10 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) = ((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})))
367	366	oveq1d 7361	. . . . . . . . 9 ⊢ (𝜑 → (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld)) = (((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld)))
368	367	fveq1d 6824	. . . . . . . 8 ⊢ (𝜑 → ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌) = ((((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld))‘𝑌))
369	364, 368	eleqtrd 2833	. . . . . . 7 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld))‘𝑌))
370	308, 369	eqeltrd 2831	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld))‘𝑌))
371		eqid 2731	. . . . . . 7 ⊢ ((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) = ((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}))
372		eqid 2731	. . . . . . 7 ⊢ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))
373	206, 208	fmptd 7047	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
374	4, 36	sstrdi 3947	. . . . . . 7 ⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℂ)
375	371, 51, 372, 373, 374, 263	ellimc 25799	. . . . . 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 11766	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · π) ≠ 0)
380	263, 156, 379	divcan1d 11895	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑌 / (2 · π)) · (2 · π)) = 𝑌)
381	380	eqcomd 2737	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 = ((𝑌 / (2 · π)) · (2 · π)))
382	381	oveq2d 7362	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))))
383	382	fveq2d 6826	. . . . . . 7 ⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) = (sin‘((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π)))))
384	263, 156, 379	divcld 11894	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 / (2 · π)) ∈ ℂ)
385	41, 384, 156	mul12d 11319	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = ((𝑌 / (2 · π)) · ((𝑁 + (1 / 2)) · (2 · π))))
386	41, 154, 155	mulassd 11132	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · 2) · π) = ((𝑁 + (1 / 2)) · (2 · π)))
387	386	eqcomd 2737	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · (2 · π)) = (((𝑁 + (1 / 2)) · 2) · π))
388	387	oveq2d 7362	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑌 / (2 · π)) · ((𝑁 + (1 / 2)) · (2 · π))) = ((𝑌 / (2 · π)) · (((𝑁 + (1 / 2)) · 2) · π)))
389	38, 40, 154	adddird 11134	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 2) = ((𝑁 · 2) + ((1 / 2) · 2)))
390	154, 377	recid2d 11890	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1 / 2) · 2) = 1)
391	390	oveq2d 7362	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 · 2) + ((1 / 2) · 2)) = ((𝑁 · 2) + 1))
392	389, 391	eqtrd 2766	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 2) = ((𝑁 · 2) + 1))
393	392	oveq1d 7361	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · 2) · π) = (((𝑁 · 2) + 1) · π))
394	393	oveq2d 7362	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑌 / (2 · π)) · (((𝑁 + (1 / 2)) · 2) · π)) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
395	385, 388, 394	3eqtrd 2770	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
396	38, 154	mulcld 11129	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 · 2) ∈ ℂ)
397		1cnd 11104	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
398	396, 397	addcld 11128	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 · 2) + 1) ∈ ℂ)
399	384, 398, 155	mulassd 11132	. . . . . . . . 9 ⊢ (𝜑 → (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
400	395, 399	eqtr4d 2769	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π))
401	400	fveq2d 6826	. . . . . . 7 ⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π)))) = (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π)))
402		mod0 13777	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ ℝ ∧ (2 · π) ∈ ℝ⁺) → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
403	57, 253, 402	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
404	282, 403	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → (𝑌 / (2 · π)) ∈ ℤ)
405	5	nnzd 12492	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℤ)
406		2z 12501	. . . . . . . . . . . 12 ⊢ 2 ∈ ℤ
407	406	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℤ)
408	405, 407	zmulcld 12580	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 · 2) ∈ ℤ)
409	408	peano2zd 12577	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 · 2) + 1) ∈ ℤ)
410	404, 409	zmulcld 12580	. . . . . . . 8 ⊢ (𝜑 → ((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ∈ ℤ)
411		sinkpi 26456	. . . . . . . 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 2770	. . . . . 6 ⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) = 0)
414		sincn 26379	. . . . . . . 8 ⊢ sin ∈ (ℂ–cn→ℂ)
415	414	a1i 11	. . . . . . 7 ⊢ (𝜑 → sin ∈ (ℂ–cn→ℂ))
416	415, 286	cnlimci 25815	. . . . . 6 ⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) ∈ (sin lim_ℂ ((𝑁 + (1 / 2)) · 𝑌)))
417	413, 416	eqeltrrd 2832	. . . . 5 ⊢ (𝜑 → 0 ∈ (sin lim_ℂ ((𝑁 + (1 / 2)) · 𝑌)))
418	301, 376, 417	limccog 45659	. . . 4 ⊢ (𝜑 → 0 ∈ ((sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) lim_ℂ 𝑌))
419	14	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
420	213	fveq2d 6826	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
421	223	sincld 16036	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑤)) ∈ ℂ)
422	419, 420, 214, 421	fvmptd 6936	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹‘𝑤) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
423	224	fveq2d 6826	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
424	422, 423	eqtr4d 2769	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹‘𝑤) = (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))
425	424	mpteq2dva 5184	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (𝐹‘𝑤)) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
426	15	feqmptd 6890	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (𝐹‘𝑤)))
427		fcompt 7066	. . . . . . 7 ⊢ ((sin:ℂ⟶ℂ ∧ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
428	293, 373, 427	sylancr 587	. . . . . 6 ⊢ (𝜑 → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
429	425, 426, 428	3eqtr4rd 2777	. . . . 5 ⊢ (𝜑 → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = 𝐹)
430	429	oveq1d 7361	. . . 4 ⊢ (𝜑 → ((sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) lim_ℂ 𝑌) = (𝐹 lim_ℂ 𝑌))
431	418, 430	eleqtrd 2833	. . 3 ⊢ (𝜑 → 0 ∈ (𝐹 lim_ℂ 𝑌))
432		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → 𝑤 = 𝑌)
433	432	iftrued 4483	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = 0)
434	263, 154, 156, 377, 379	divdiv32d 11919	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑌 / 2) / (2 · π)) = ((𝑌 / (2 · π)) / 2))
435	434	oveq1d 7361	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑌 / 2) / (2 · π)) · (2 · π)) = (((𝑌 / (2 · π)) / 2) · (2 · π)))
436	263	halfcld 12363	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑌 / 2) ∈ ℂ)
437	436, 156, 379	divcan1d 11895	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑌 / 2) / (2 · π)) · (2 · π)) = (𝑌 / 2))
438	384, 154, 156, 377	div32d 11917	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑌 / (2 · π)) / 2) · (2 · π)) = ((𝑌 / (2 · π)) · ((2 · π) / 2)))
439	155, 154, 377	divcan3d 11899	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2 · π) / 2) = π)
440	439	oveq2d 7362	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑌 / (2 · π)) · ((2 · π) / 2)) = ((𝑌 / (2 · π)) · π))
441	438, 440	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑌 / (2 · π)) / 2) · (2 · π)) = ((𝑌 / (2 · π)) · π))
442	435, 437, 441	3eqtr3d 2774	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 / 2) = ((𝑌 / (2 · π)) · π))
443	442	fveq2d 6826	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (sin‘(𝑌 / 2)) = (sin‘((𝑌 / (2 · π)) · π)))
444		sinkpi 26456	. . . . . . . . . . . . . . 15 ⊢ ((𝑌 / (2 · π)) ∈ ℤ → (sin‘((𝑌 / (2 · π)) · π)) = 0)
445	404, 444	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (sin‘((𝑌 / (2 · π)) · π)) = 0)
446	443, 445	eqtrd 2766	. . . . . . . . . . . . 13 ⊢ (𝜑 → (sin‘(𝑌 / 2)) = 0)
447	446	oveq2d 7362	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · 0))
448	156	mul01d 11309	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · π) · 0) = 0)
449	447, 448	eqtrd 2766	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · π) · (sin‘(𝑌 / 2))) = 0)
450	449	eqcomd 2737	. . . . . . . . . 10 ⊢ (𝜑 → 0 = ((2 · π) · (sin‘(𝑌 / 2))))
451	450	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → 0 = ((2 · π) · (sin‘(𝑌 / 2))))
452		fvoveq1 7369	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑌 → (sin‘(𝑤 / 2)) = (sin‘(𝑌 / 2)))
453	452	oveq2d 7362	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑌 → ((2 · π) · (sin‘(𝑤 / 2))) = ((2 · π) · (sin‘(𝑌 / 2))))
454	453	eqcomd 2737	. . . . . . . . . 10 ⊢ (𝑤 = 𝑌 → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
455	454	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
456	433, 451, 455	3eqtrd 2770	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
457		iffalse 4484	. . . . . . . . . 10 ⊢ (¬ 𝑤 = 𝑌 → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = (𝐺‘𝑤))
458	457	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = (𝐺‘𝑤))
459		fvoveq1 7369	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → (sin‘(𝑦 / 2)) = (sin‘(𝑤 / 2)))
460	459	oveq2d 7362	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
461	120	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (2 · π) ∈ ℂ)
462	328	halfcld 12363	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 / 2) ∈ ℂ)
463	462	sincld 16036	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (sin‘(𝑤 / 2)) ∈ ℂ)
464	461, 463	mulcld 11129	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((2 · π) · (sin‘(𝑤 / 2))) ∈ ℂ)
465	464	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((2 · π) · (sin‘(𝑤 / 2))) ∈ ℂ)
466	23, 460, 324, 465	fvmptd3 6952	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐺‘𝑤) = ((2 · π) · (sin‘(𝑤 / 2))))
467	458, 466	eqtrd 2766	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
468	456, 467	pm2.61dan 812	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
469	468	mpteq2dva 5184	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))))
470		eqid 2731	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2)))) = (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2))))
471	75, 156, 75	constcncfg 45909	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (2 · π)) ∈ (ℂ–cn→ℂ))
472		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℂ → 𝑤 ∈ ℂ)
473		2cnd 12200	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℂ → 2 ∈ ℂ)
474	134	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℂ → 2 ≠ 0)
475	472, 473, 474	divrec2d 11898	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ℂ → (𝑤 / 2) = ((1 / 2) · 𝑤))
476	475	mpteq2ia 5186	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ ℂ ↦ (𝑤 / 2)) = (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤))
477		eqid 2731	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) = (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤))
478	477	mulc1cncf 24823	. . . . . . . . . . . . . . . 16 ⊢ ((1 / 2) ∈ ℂ → (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) ∈ (ℂ–cn→ℂ))
479	39, 478	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) ∈ (ℂ–cn→ℂ)
480	476, 479	eqeltri 2827	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ ℂ ↦ (𝑤 / 2)) ∈ (ℂ–cn→ℂ)
481	480	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (𝑤 / 2)) ∈ (ℂ–cn→ℂ))
482	415, 481	cncfmpt1f 24832	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (sin‘(𝑤 / 2))) ∈ (ℂ–cn→ℂ))
483	471, 482	mulcncf 25371	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ (ℂ–cn→ℂ))
484	470, 483, 349, 75, 464	cncfmptssg 45908	. . . . . . . . . 10 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
485		eqid 2731	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) = ((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵))
486	51, 485, 345	cncfcn 24828	. . . . . . . . . . 11 ⊢ (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)))
487	349, 74, 486	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)))
488	484, 487	eleqtrd 2833	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)))
489		cncnp 23193	. . . . . . . . . 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 586	. . . . . . . . 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 2817	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌)))
494	493	rspccva 3576	. . . . . . 7 ⊢ ((∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
495	492, 27, 494	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
496	469, 495	eqeltrd 2831	. . . . 5 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
497	307	mpteq1d 5181	. . . . 5 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))))
498	366	eqcomd 2737	. . . . . . 7 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) = ((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)))
499	498	oveq1d 7361	. . . . . 6 ⊢ (𝜑 → (((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld)) = (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld)))
500	499	fveq1d 6824	. . . . 5 ⊢ (𝜑 → ((((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld))‘𝑌) = ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
501	496, 497, 500	3eltr4d 2846	. . . 4 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld))‘𝑌))
502		eqid 2731	. . . . 5 ⊢ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤)))
503	11, 124	syldan 591	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
504	503, 23	fmptd 7047	. . . . 5 ⊢ (𝜑 → 𝐺:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
505	371, 51, 502, 504, 374, 263	ellimc 25799	. . . 4 ⊢ (𝜑 → (0 ∈ (𝐺 lim_ℂ 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld))‘𝑌)))
506	501, 505	mpbird 257	. . 3 ⊢ (𝜑 → 0 ∈ (𝐺 lim_ℂ 𝑌))
507	256	nrexdv 3127	. . . 4 ⊢ (𝜑 → ¬ ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0)
508	504	ffund 6655	. . . . . 6 ⊢ (𝜑 → Fun 𝐺)
509		fvelima 6887	. . . . . 6 ⊢ ((Fun 𝐺 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0)
510	508, 509	sylan 580	. . . . 5 ⊢ ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0)
511		2cnd 12200	. . . . . . . . . . . . 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 11925	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
516	515	eqcomd 2737	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
517	516	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
518		2cnd 12200	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → 2 ∈ ℂ)
519	119	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → π ∈ ℂ)
520	518, 519	mulcld 11129	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (2 · π) ∈ ℂ)
521	232	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → 𝑦 ∈ ℂ)
522	521	halfcld 12363	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (𝑦 / 2) ∈ ℂ)
523	522	sincld 16036	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (sin‘(𝑦 / 2)) ∈ ℂ)
524	520, 523	mulcld 11129	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
525	23	fvmpt2 6940	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ) → (𝐺‘𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
526	524, 525	syldan 591	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (𝐺‘𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
527	526	eqcomd 2737	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) = (𝐺‘𝑦))
528		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (𝐺‘𝑦) = 0)
529	527, 528	eqtrd 2766	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) = 0)
530	120	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (2 · π) ∈ ℂ)
531	232	halfcld 12363	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (𝑦 / 2) ∈ ℂ)
532	531	sincld 16036	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (sin‘(𝑦 / 2)) ∈ ℂ)
533	530, 532	mul0ord 11762	. . . . . . . . . . . . . . 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 12327	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
537	119, 238	pm3.2i 470	. . . . . . . . . . . . . . 15 ⊢ (π ∈ ℂ ∧ π ≠ 0)
538		mulne0 11756	. . . . . . . . . . . . . . 15 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → (2 · π) ≠ 0)
539	536, 537, 538	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (2 · π) ≠ 0
540	539	neii 2930	. . . . . . . . . . . . 13 ⊢ ¬ (2 · π) = 0
541		pm2.53 851	. . . . . . . . . . . . 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 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (sin‘(𝑦 / 2)) = 0)
544	105	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → 𝑦 ∈ ℂ)
545	544	halfcld 12363	. . . . . . . . . . . 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 2831	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 / (2 · π)) ∈ ℤ)
549	11	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → 𝑦 ∈ ℝ)
550	549, 253, 254	sylancl 586	. . . . . . . . 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 3145	. . . . . 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 815	. . 3 ⊢ (𝜑 → ¬ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌})))
557		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
558	111	fvmpt2 6940	. . . . . . . . 9 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (π · (cos‘(𝑦 / 2))) ∈ ℂ) → (𝐼‘𝑦) = (π · (cos‘(𝑦 / 2))))
559	557, 201, 558	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐼‘𝑦) = (π · (cos‘(𝑦 / 2))))
560	531	coscld 16037	. . . . . . . . . 10 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (cos‘(𝑦 / 2)) ∈ ℂ)
561	560	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ∈ ℂ)
562		dirkercncflem2.11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0)
563	512, 561, 514, 562	mulne0d 11766	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (π · (cos‘(𝑦 / 2))) ≠ 0)
564	559, 563	eqnetrd 2995	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐼‘𝑦) ≠ 0)
565	564	neneqd 2933	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝐼‘𝑦) = 0)
566	565	nrexdv 3127	. . . . 5 ⊢ (𝜑 → ¬ ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼‘𝑦) = 0)
567	201, 111	fmptd 7047	. . . . . . 7 ⊢ (𝜑 → 𝐼:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
568	567	ffund 6655	. . . . . 6 ⊢ (𝜑 → Fun 𝐼)
569		fvelima 6887	. . . . . 6 ⊢ ((Fun 𝐼 ∧ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼‘𝑦) = 0)
570	568, 569	sylan 580	. . . . 5 ⊢ ((𝜑 ∧ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼‘𝑦) = 0)
571	566, 570	mtand 815	. . . 4 ⊢ (𝜑 → ¬ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌})))
572	199	imaeq1d 6008	. . . 4 ⊢ (𝜑 → ((ℝ D 𝐺) “ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌})))
573	571, 572	neleqtrrd 2854	. . 3 ⊢ (𝜑 → ¬ 0 ∈ ((ℝ D 𝐺) “ ((𝐴(,)𝐵) ∖ {𝑌})))
574		dirkercncflem2.d	. . . . . 6 ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
575	574	dirkerval2 46131	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ ℝ) → ((𝐷‘𝑁)‘𝑌) = if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))))
576	5, 57, 575	syl2anc 584	. . . 4 ⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) = if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))))
577	282	iftrued 4483	. . . . 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 4481	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑌 → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = (((2 · 𝑁) + 1) / (2 · π)))
581	580	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = (((2 · 𝑁) + 1) / (2 · π)))
582	154, 38	mulcld 11129	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
583	582, 397	addcld 11128	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 · 𝑁) + 1) ∈ ℂ)
584	583, 154, 155, 377, 378	divdiv1d 11925	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((2 · 𝑁) + 1) / 2) / π) = (((2 · 𝑁) + 1) / (2 · π)))
585	584	eqcomd 2737	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) = ((((2 · 𝑁) + 1) / 2) / π))
586	582, 397, 154, 377	divdird 11932	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2 · 𝑁) + 1) / 2) = (((2 · 𝑁) / 2) + (1 / 2)))
587	38, 154, 377	divcan3d 11899	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2 · 𝑁) / 2) = 𝑁)
588	587	oveq1d 7361	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2 · 𝑁) / 2) + (1 / 2)) = (𝑁 + (1 / 2)))
589	586, 588	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((2 · 𝑁) + 1) / 2) = (𝑁 + (1 / 2)))
590	589	oveq1d 7361	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((2 · 𝑁) + 1) / 2) / π) = ((𝑁 + (1 / 2)) / π))
591	585, 590	eqtrd 2766	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) = ((𝑁 + (1 / 2)) / π))
592	591	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((2 · 𝑁) + 1) / (2 · π)) = ((𝑁 + (1 / 2)) / π))
593	310	fveq2d 6826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑌 → (cos‘((𝑁 + (1 / 2)) · 𝑤)) = (cos‘((𝑁 + (1 / 2)) · 𝑌)))
594	593	oveq2d 7362	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑌 → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))))
595		fvoveq1 7369	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑌 → (cos‘(𝑤 / 2)) = (cos‘(𝑌 / 2)))
596	595	oveq2d 7362	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑌 → (π · (cos‘(𝑤 / 2))) = (π · (cos‘(𝑌 / 2))))
597	594, 596	oveq12d 7364	. . . . . . . . . . . . . . 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 11134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑁 · 𝑌) + ((1 / 2) · 𝑌)))
600	397, 154, 263, 377	div32d 11917	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((1 / 2) · 𝑌) = (1 · (𝑌 / 2)))
601	436	mullidd 11127	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · (𝑌 / 2)) = (𝑌 / 2))
602	600, 601	eqtrd 2766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1 / 2) · 𝑌) = (𝑌 / 2))
603	602	oveq2d 7362	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 · 𝑌) + ((1 / 2) · 𝑌)) = ((𝑁 · 𝑌) + (𝑌 / 2)))
604	38, 263	mulcld 11129	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑁 · 𝑌) ∈ ℂ)
605	604, 436	addcomd 11312	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 · 𝑌) + (𝑌 / 2)) = ((𝑌 / 2) + (𝑁 · 𝑌)))
606	599, 603, 605	3eqtrd 2770	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑌 / 2) + (𝑁 · 𝑌)))
607	606	fveq2d 6826	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (cos‘((𝑁 + (1 / 2)) · 𝑌)) = (cos‘((𝑌 / 2) + (𝑁 · 𝑌))))
608	604, 156, 379	divcan1d 11895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝑁 · 𝑌) / (2 · π)) · (2 · π)) = (𝑁 · 𝑌))
609	608	eqcomd 2737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑁 · 𝑌) = (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))
610	609	oveq2d 7362	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑌 / 2) + (𝑁 · 𝑌)) = ((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π))))
611	610	fveq2d 6826	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (cos‘((𝑌 / 2) + (𝑁 · 𝑌))) = (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))))
612	38, 263, 156, 379	divassd 11929	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑁 · 𝑌) / (2 · π)) = (𝑁 · (𝑌 / (2 · π))))
613	405, 404	zmulcld 12580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑁 · (𝑌 / (2 · π))) ∈ ℤ)
614	612, 613	eqeltrd 2831	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 · 𝑌) / (2 · π)) ∈ ℤ)
615		cosper 26416	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑌 / 2) ∈ ℂ ∧ ((𝑁 · 𝑌) / (2 · π)) ∈ ℤ) → (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))) = (cos‘(𝑌 / 2)))
616	436, 614, 615	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))) = (cos‘(𝑌 / 2)))
617	607, 611, 616	3eqtrd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (cos‘((𝑁 + (1 / 2)) · 𝑌)) = (cos‘(𝑌 / 2)))
618	617	oveq2d 7362	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) = ((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))))
619	618	oveq1d 7361	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = (((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))) / (π · (cos‘(𝑌 / 2)))))
620	436	coscld 16037	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (cos‘(𝑌 / 2)) ∈ ℂ)
621	263, 154, 155, 377, 378	divdiv1d 11925	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑌 / 2) / π) = (𝑌 / (2 · π)))
622	621, 404	eqeltrd 2831	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑌 / 2) / π) ∈ ℤ)
623	622	zred 12574	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑌 / 2) / π) ∈ ℝ)
624	623, 272	ltaddrpd 12964	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑌 / 2) / π) < (((𝑌 / 2) / π) + (1 / 2)))
625		halflt1 12335	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 / 2) < 1
626	625	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (1 / 2) < 1)
627	268, 267, 623, 626	ltadd2dd 11269	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑌 / 2) / π) + (1 / 2)) < (((𝑌 / 2) / π) + 1))
628		btwnnz 12546	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑌 / 2) / π) ∈ ℤ ∧ ((𝑌 / 2) / π) < (((𝑌 / 2) / π) + (1 / 2)) ∧ (((𝑌 / 2) / π) + (1 / 2)) < (((𝑌 / 2) / π) + 1)) → ¬ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ)
629	622, 624, 627, 628	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ¬ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ)
630		coseq0 45901	. . . . . . . . . . . . . . . . . . . 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 2935	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (cos‘(𝑌 / 2)) ≠ 0)
634	41, 155, 620, 378, 633	divcan5rd 11921	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
635	619, 634	eqtrd 2766	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
636	635	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
637	598, 636	eqtr2d 2767	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) / π) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))))
638	581, 592, 637	3eqtrrd 2771	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)))
639		iffalse 4484	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑤 = 𝑌 → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))
640	639	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))
641		eqidd 2732	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))))
642		fveq2 6822	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → (𝐻‘𝑦) = (𝐻‘𝑤))
643		fveq2 6822	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → (𝐼‘𝑦) = (𝐼‘𝑤))
644	642, 643	oveq12d 7364	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → ((𝐻‘𝑦) / (𝐼‘𝑦)) = ((𝐻‘𝑤) / (𝐼‘𝑤)))
645	644	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝐻‘𝑦) / (𝐼‘𝑦)) = ((𝐻‘𝑤) / (𝐼‘𝑤)))
646	106, 100	fmptd 7047	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐻:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
647	646	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐻:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
648	647, 324	ffvelcdmd 7018	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐻‘𝑤) ∈ ℂ)
649	567	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐼:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
650	649, 324	ffvelcdmd 7018	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼‘𝑤) ∈ ℂ)
651	111	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
652		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
653	652	fvoveq1d 7368	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (cos‘(𝑦 / 2)) = (cos‘(𝑤 / 2)))
654	653	oveq2d 7362	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (π · (cos‘(𝑦 / 2))) = (π · (cos‘(𝑤 / 2))))
655	119	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → π ∈ ℂ)
656	327	halfcld 12363	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → (𝑤 / 2) ∈ ℂ)
657	656	coscld 16037	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → (cos‘(𝑤 / 2)) ∈ ℂ)
658	655, 657	mulcld 11129	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (𝐴(,)𝐵) → (π · (cos‘(𝑤 / 2))) ∈ ℂ)
659	658	ad2antlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π · (cos‘(𝑤 / 2))) ∈ ℂ)
660	651, 654, 324, 659	fvmptd 6936	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼‘𝑤) = (π · (cos‘(𝑤 / 2))))
661	537	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π ∈ ℂ ∧ π ≠ 0))
662	657	ad2antlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ∈ ℂ)
663		simpll 766	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝜑)
664		fvoveq1 7369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑤 → (cos‘(𝑦 / 2)) = (cos‘(𝑤 / 2)))
665	664	neeq1d 2987	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑤 → ((cos‘(𝑦 / 2)) ≠ 0 ↔ (cos‘(𝑤 / 2)) ≠ 0))
666	226, 665	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑤 → (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0) ↔ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑤 / 2)) ≠ 0)))
667	666, 562	chvarvv 1990	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑤 / 2)) ≠ 0)
668	663, 324, 667	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
669		mulne0 11756	. . . . . . . . . . . . . . . . 17 ⊢ (((π ∈ ℂ ∧ π ≠ 0) ∧ ((cos‘(𝑤 / 2)) ∈ ℂ ∧ (cos‘(𝑤 / 2)) ≠ 0)) → (π · (cos‘(𝑤 / 2))) ≠ 0)
670	661, 662, 668, 669	syl12anc 836	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π · (cos‘(𝑤 / 2))) ≠ 0)
671	660, 670	eqnetrd 2995	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼‘𝑤) ≠ 0)
672	648, 650, 671	divcld 11894	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝐻‘𝑤) / (𝐼‘𝑤)) ∈ ℂ)
673	641, 645, 324, 672	fvmptd 6936	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤) = ((𝐻‘𝑤) / (𝐼‘𝑤)))
674	100	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
675	317	fveq2d 6826	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (cos‘((𝑁 + (1 / 2)) · 𝑦)) = (cos‘((𝑁 + (1 / 2)) · 𝑤)))
676	675	oveq2d 7362	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))))
677	329	coscld 16037	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘((𝑁 + (1 / 2)) · 𝑤)) ∈ ℂ)
678	325, 677	mulcld 11129	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ℂ)
679	678	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ℂ)
680	674, 676, 324, 679	fvmptd 6936	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐻‘𝑤) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))))
681	680, 660	oveq12d 7364	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝐻‘𝑤) / (𝐼‘𝑤)) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))))
682	640, 673, 681	3eqtrrd 2771	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)))
683	638, 682	pm2.61dan 812	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)))
684	683	mpteq2dva 5184	. . . . . . . . . 10 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))))
685	579, 684	eqtr2d 2767	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) = 𝐿)
686	349, 41, 75	constcncfg 45909	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
687		cosf 16031	. . . . . . . . . . . . . . . . . . 19 ⊢ cos:ℂ⟶ℂ
688	231, 44	sylan2 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
689		eqid 2731	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))
690	688, 689	fmptd 7047	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)):(𝐴(,)𝐵)⟶ℂ)
691		fcompt 7066	. . . . . . . . . . . . . . . . . . 19 ⊢ ((cos:ℂ⟶ℂ ∧ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)):(𝐴(,)𝐵)⟶ℂ) → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
692	687, 690, 691	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
693		eqidd 2732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
694	316	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
695		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 𝑤 ∈ (𝐴(,)𝐵))
696	693, 694, 695, 329	fvmptd 6936	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
697	696	fveq2d 6826	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = (cos‘((𝑁 + (1 / 2)) · 𝑤)))
698	697	mpteq2dva 5184	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))))
699	692, 698	eqtr2d 2767	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))) = (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))))
700	349, 41, 75	constcncfg 45909	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
701	349, 75	idcncfg 45910	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 𝑦) ∈ ((𝐴(,)𝐵)–cn→ℂ))
702	700, 701	mulcncf 25371	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
703		coscn 26380	. . . . . . . . . . . . . . . . . . 19 ⊢ cos ∈ (ℂ–cn→ℂ)
704	703	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → cos ∈ (ℂ–cn→ℂ))
705	702, 704	cncfco 24825	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
706	699, 705	eqeltrd 2831	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
707	686, 706	mulcncf 25371	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
708		eqid 2731	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2))))
709	349, 155, 75	constcncfg 45909	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ π) ∈ ((𝐴(,)𝐵)–cn→ℂ))
710		2cnd 12200	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ)
711	134	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 2 ≠ 0)
712	328, 710, 711	divrecd 11897	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 / 2) = (𝑤 · (1 / 2)))
713	712	mpteq2dva 5184	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 / 2)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 · (1 / 2))))
714		eqid 2731	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2))) = (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2)))
715		cncfmptid 24831	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ))
716	74, 74, 715	mp2an 692	. . . . . . . . . . . . . . . . . . . . . 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 45909	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 / 2) ∈ ℂ → (𝑤 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
721	39, 720	mp1i 13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
722	717, 721	mulcncf 25371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2))) ∈ (ℂ–cn→ℂ))
723	712, 462	eqeltrrd 2832	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 · (1 / 2)) ∈ ℂ)
724	714, 722, 349, 75, 723	cncfmptssg 45908	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 · (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
725	713, 724	eqeltrd 2831	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 / 2)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
726	704, 725	cncfmpt1f 24832	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑤 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
727	709, 726	mulcncf 25371	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
728		ssid 3957	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)
729	728	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵))
730		difssd 4087	. . . . . . . . . . . . . . . 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 2995	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
738	737	adantlr 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
739	738, 668	pm2.61dan 812	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘(𝑤 / 2)) ≠ 0)
740	732, 733, 734, 739	mulne0d 11766	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ≠ 0)
741	740	neneqd 2933	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ¬ (π · (cos‘(𝑤 / 2))) = 0)
742		elsng 4590	. . . . . . . . . . . . . . . . . . 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 3913	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ∈ (ℂ ∖ {0}))
746	708, 727, 729, 730, 745	cncfmptssg 45908	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→(ℂ ∖ {0})))
747	707, 746	divcncf 25373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
748	747, 487	eleqtrd 2833	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)))
749	579, 748	eqeltrd 2831	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ (((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) Cn (TopOpen‘ℂ_fld)))
750		cncnp 23193	. . . . . . . . . . . . 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 586	. . . . . . . . . . . 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 2817	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → (𝐿 ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦) ↔ 𝐿 ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌)))
755	754	rspccva 3576	. . . . . . . . . 10 ⊢ ((∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → 𝐿 ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
756	753, 27, 755	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
757	685, 756	eqeltrd 2831	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝐴(,)𝐵)) CnP (TopOpen‘ℂ_fld))‘𝑌))
758	307	mpteq1d 5181	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))))
759	757, 758, 500	3eltr4d 2846	. . . . . . 7 ⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂ_fld))‘𝑌))
760		eqid 2731	. . . . . . . 8 ⊢ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)))
761	100	fvmpt2 6940	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ) → (𝐻‘𝑦) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
762	557, 106, 761	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐻‘𝑦) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
763	762, 559	oveq12d 7364	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐻‘𝑦) / (𝐼‘𝑦)) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) / (π · (cos‘(𝑦 / 2)))))
764	106, 201, 563	divcld 11894	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) / (π · (cos‘(𝑦 / 2)))) ∈ ℂ)
765	763, 764	eqeltrd 2831	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐻‘𝑦) / (𝐼‘𝑦)) ∈ ℂ)
766		eqid 2731	. . . . . . . . 9 ⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))
767	765, 766	fmptd 7047	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
768	371, 51, 760, 767, 374, 263	ellimc 25799	. . . . . . 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 2737	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 = (ℝ D 𝐹))
771	770	fveq1d 6824	. . . . . . . . 9 ⊢ (𝜑 → (𝐻‘𝑦) = ((ℝ D 𝐹)‘𝑦))
772	199	eqcomd 2737	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 = (ℝ D 𝐺))
773	772	fveq1d 6824	. . . . . . . . 9 ⊢ (𝜑 → (𝐼‘𝑦) = ((ℝ D 𝐺)‘𝑦))
774	771, 773	oveq12d 7364	. . . . . . . 8 ⊢ (𝜑 → ((𝐻‘𝑦) / (𝐼‘𝑦)) = (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)))
775	774	mpteq2dv 5185	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))))
776	775	oveq1d 7361	. . . . . 6 ⊢ (𝜑 → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) lim_ℂ 𝑌) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim_ℂ 𝑌))
777	769, 776	eleqtrd 2833	. . . . 5 ⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim_ℂ 𝑌))
778	577, 777	eqeltrd 2831	. . . 4 ⊢ (𝜑 → if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim_ℂ 𝑌))
779	576, 778	eqeltrd 2831	. . 3 ⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim_ℂ 𝑌))
780	4, 15, 24, 26, 27, 28, 110, 205, 431, 506, 556, 573, 779	lhop 25946	. 2 ⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))) lim_ℂ 𝑌))
781	574	dirkerval 46128	. . . . . 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 5927	. . . 4 ⊢ (𝜑 → ((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
784	4	resmptd 5989	. . . 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 4486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
786	13	recnd 11137	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
787	14	fvmpt2 6940	. . . . . . . 8 ⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ) → (𝐹‘𝑦) = (sin‘((𝑁 + (1 / 2)) · 𝑦)))
788	557, 786, 787	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹‘𝑦) = (sin‘((𝑁 + (1 / 2)) · 𝑦)))
789	557, 503, 525	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐺‘𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
790	788, 789	oveq12d 7364	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐹‘𝑦) / (𝐺‘𝑦)) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
791	785, 790	eqtr4d 2769	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((𝐹‘𝑦) / (𝐺‘𝑦)))
792	791	mpteq2dva 5184	. . . 4 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))))
793	783, 784, 792	3eqtrrd 2771	. . 3 ⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))) = ((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
794	793	oveq1d 7361	. 2 ⊢ (𝜑 → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))) lim_ℂ 𝑌) = (((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) lim_ℂ 𝑌))
795	780, 794	eleqtrd 2833	1 ⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ (((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) lim_ℂ 𝑌))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 ∃wrex 3056 ∖ cdif 3899 ∪ cun 3900 ⊆ wss 3902 ifcif 4475 {csn 4576 {cpr 4578 class class class wbr 5091 ↦ cmpt 5172 dom cdm 5616 ran crn 5617 ↾ cres 5618 “ cima 5619 ∘ ccom 5620 Fun wfun 6475 Fn wfn 6476 ⟶wf 6477 ‘cfv 6481 (class class class)co 7346 ℂcc 11001 ℝcr 11002 0cc0 11003 1c1 11004 + caddc 11006 · cmul 11008 < clt 11143 / cdiv 11771 ℕcn 12122 2c2 12177 ℤcz 12465 ℝ⁺crp 12887 (,)cioo 13242 mod cmo 13770 sincsin 15967 cosccos 15968 πcpi 15970 ↾_t crest 17321 TopOpenctopn 17322 topGenctg 17338 ℂ_fldccnfld 21289 Topctop 22806 TopOnctopon 22823 Clsdccld 22929 intcnt 22930 Cn ccn 23137 CnP ccnp 23138 Hauscha 23221 –cn→ccncf 24794 lim_ℂ climc 25788 D cdv 25789

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

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-tp 4581 df-op 4583 df-uni 4860 df-int 4898 df-iun 4943 df-iin 4944 df-br 5092 df-opab 5154 df-mpt 5173 df-tr 5199 df-id 5511 df-eprel 5516 df-po 5524 df-so 5525 df-fr 5569 df-se 5570 df-we 5571 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-of 7610 df-om 7797 df-1st 7921 df-2nd 7922 df-supp 8091 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-2o 8386 df-er 8622 df-map 8752 df-pm 8753 df-ixp 8822 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-fsupp 9246 df-fi 9295 df-sup 9326 df-inf 9327 df-oi 9396 df-card 9829 df-pnf 11145 df-mnf 11146 df-xr 11147 df-ltxr 11148 df-le 11149 df-sub 11343 df-neg 11344 df-div 11772 df-nn 12123 df-2 12185 df-3 12186 df-4 12187 df-5 12188 df-6 12189 df-7 12190 df-8 12191 df-9 12192 df-n0 12379 df-z 12466 df-dec 12586 df-uz 12730 df-q 12844 df-rp 12888 df-xneg 13008 df-xadd 13009 df-xmul 13010 df-ioo 13246 df-ioc 13247 df-ico 13248 df-icc 13249 df-fz 13405 df-fzo 13552 df-fl 13693 df-mod 13771 df-seq 13906 df-exp 13966 df-fac 14178 df-bc 14207 df-hash 14235 df-shft 14971 df-cj 15003 df-re 15004 df-im 15005 df-sqrt 15139 df-abs 15140 df-limsup 15375 df-clim 15392 df-rlim 15393 df-sum 15591 df-ef 15971 df-sin 15973 df-cos 15974 df-pi 15976 df-struct 17055 df-sets 17072 df-slot 17090 df-ndx 17102 df-base 17118 df-ress 17139 df-plusg 17171 df-mulr 17172 df-starv 17173 df-sca 17174 df-vsca 17175 df-ip 17176 df-tset 17177 df-ple 17178 df-ds 17180 df-unif 17181 df-hom 17182 df-cco 17183 df-rest 17323 df-topn 17324 df-0g 17342 df-gsum 17343 df-topgen 17344 df-pt 17345 df-prds 17348 df-xrs 17403 df-qtop 17408 df-imas 17409 df-xps 17411 df-mre 17485 df-mrc 17486 df-acs 17488 df-mgm 18545 df-sgrp 18624 df-mnd 18640 df-submnd 18689 df-mulg 18978 df-cntz 19227 df-cmn 19692 df-psmet 21281 df-xmet 21282 df-met 21283 df-bl 21284 df-mopn 21285 df-fbas 21286 df-fg 21287 df-cnfld 21290 df-top 22807 df-topon 22824 df-topsp 22846 df-bases 22859 df-cld 22932 df-ntr 22933 df-cls 22934 df-nei 23011 df-lp 23049 df-perf 23050 df-cn 23140 df-cnp 23141 df-t1 23227 df-haus 23228 df-cmp 23300 df-tx 23475 df-hmeo 23668 df-fil 23759 df-fm 23851 df-flim 23852 df-flf 23853 df-xms 24233 df-ms 24234 df-tms 24235 df-cncf 24796 df-limc 25792 df-dv 25793

This theorem is referenced by: dirkercncflem3 46142

W3C validator