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

Theorem dirkercncflem2 43171
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
StepHypRef Expression
1 difss 4020 . . . . 5 ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ (𝐴(,)𝐵)
2 ioossre 12875 . . . . 5 (𝐴(,)𝐵) ⊆ ℝ
31, 2sstri 3884 . . . 4 ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ
43a1i 11 . . 3 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)
5 dirkercncflem2.n . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
65adantr 484 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℕ)
76nnred 11724 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℝ)
8 halfre 11923 . . . . . . . 8 (1 / 2) ∈ ℝ
98a1i 11 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈ ℝ)
107, 9readdcld 10741 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑁 + (1 / 2)) ∈ ℝ)
114sselda 3875 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℝ)
1210, 11remulcld 10742 . . . . 5 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℝ)
1312resincld 15581 . . . 4 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℝ)
14 dirkercncflem2.f . . . 4 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
1513, 14fmptd 6882 . . 3 (𝜑𝐹:((𝐴(,)𝐵) ∖ {𝑌})⟶ℝ)
16 2re 11783 . . . . . . 7 2 ∈ ℝ
17 pire 25195 . . . . . . 7 π ∈ ℝ
1816, 17remulcli 10728 . . . . . 6 (2 · π) ∈ ℝ
1918a1i 11 . . . . 5 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈ ℝ)
2011rehalfcld 11956 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℝ)
2120resincld 15581 . . . . 5 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ∈ ℝ)
2219, 21remulcld 10742 . . . 4 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℝ)
23 dirkercncflem2.g . . . 4 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
2422, 23fmptd 6882 . . 3 (𝜑𝐺:((𝐴(,)𝐵) ∖ {𝑌})⟶ℝ)
25 iooretop 23511 . . . 4 (𝐴(,)𝐵) ∈ (topGen‘ran (,))
2625a1i 11 . . 3 (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran (,)))
27 dirkercncflem2.y . . 3 (𝜑𝑌 ∈ (𝐴(,)𝐵))
28 eqid 2738 . . 3 ((𝐴(,)𝐵) ∖ {𝑌}) = ((𝐴(,)𝐵) ∖ {𝑌})
2914a1i 11 . . . . . . . 8 (𝜑𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
3029oveq2d 7180 . . . . . . 7 (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
31 resmpt 5873 . . . . . . . . . . . 12 (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
323, 31ax-mp 5 . . . . . . . . . . 11 ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
3332eqcomi 2747 . . . . . . . . . 10 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))
3433a1i 11 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
3534oveq2d 7180 . . . . . . . 8 (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))))
36 ax-resscn 10665 . . . . . . . . . 10 ℝ ⊆ ℂ
3736a1i 11 . . . . . . . . 9 (𝜑 → ℝ ⊆ ℂ)
385nncnd 11725 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℂ)
39 halfcn 11924 . . . . . . . . . . . . . . 15 (1 / 2) ∈ ℂ
4039a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (1 / 2) ∈ ℂ)
4138, 40addcld 10731 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ)
4241adantr 484 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (𝑁 + (1 / 2)) ∈ ℂ)
4337sselda 3875 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
4442, 43mulcld 10732 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
4544sincld 15568 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
46 eqid 2738 . . . . . . . . . 10 (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
4745, 46fmptd 6882 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℝ⟶ℂ)
48 ssid 3897 . . . . . . . . . . 11 ℝ ⊆ ℝ
4948, 3pm3.2i 474 . . . . . . . . . 10 (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)
5049a1i 11 . . . . . . . . 9 (𝜑 → (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ))
51 eqid 2738 . . . . . . . . . 10 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
5251tgioo2 23548 . . . . . . . . . 10 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
5351, 52dvres 24655 . . . . . . . . 9 (((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)) → (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
5437, 47, 50, 53syl21anc 837 . . . . . . . 8 (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
55 retop 23507 . . . . . . . . . . 11 (topGen‘ran (,)) ∈ Top
56 rehaus 23544 . . . . . . . . . . . . 13 (topGen‘ran (,)) ∈ Haus
5727elioored 42611 . . . . . . . . . . . . 13 (𝜑𝑌 ∈ ℝ)
58 uniretop 23508 . . . . . . . . . . . . . 14 ℝ = (topGen‘ran (,))
5958sncld 22115 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ Haus ∧ 𝑌 ∈ ℝ) → {𝑌} ∈ (Clsd‘(topGen‘ran (,))))
6056, 57, 59sylancr 590 . . . . . . . . . . . 12 (𝜑 → {𝑌} ∈ (Clsd‘(topGen‘ran (,))))
6158difopn 21778 . . . . . . . . . . . 12 (((𝐴(,)𝐵) ∈ (topGen‘ran (,)) ∧ {𝑌} ∈ (Clsd‘(topGen‘ran (,)))) → ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,)))
6225, 60, 61sylancr 590 . . . . . . . . . . 11 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,)))
63 isopn3i 21826 . . . . . . . . . . 11 (((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})) = ((𝐴(,)𝐵) ∖ {𝑌}))
6455, 62, 63sylancr 590 . . . . . . . . . 10 (𝜑 → ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})) = ((𝐴(,)𝐵) ∖ {𝑌}))
6564reseq2d 5819 . . . . . . . . 9 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
66 reelprrecn 10700 . . . . . . . . . . . . 13 ℝ ∈ {ℝ, ℂ}
6766a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ {ℝ, ℂ})
6841adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℂ) → (𝑁 + (1 / 2)) ∈ ℂ)
69 simpr 488 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
7068, 69mulcld 10732 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℂ) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
7170sincld 15568 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℂ) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
72 eqid 2738 . . . . . . . . . . . . 13 (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
7371, 72fmptd 6882 . . . . . . . . . . . 12 (𝜑 → (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℂ⟶ℂ)
74 ssid 3897 . . . . . . . . . . . . 13 ℂ ⊆ ℂ
7574a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ⊆ ℂ)
76 dvsinax 42980 . . . . . . . . . . . . . . . 16 ((𝑁 + (1 / 2)) ∈ ℂ → (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
7741, 76syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
7877dmeqd 5742 . . . . . . . . . . . . . 14 (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = dom (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
79 eqid 2738 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
8070coscld 15569 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ℂ) → (cos‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
8168, 80mulcld 10732 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℂ) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ)
8279, 81dmmptd 6476 . . . . . . . . . . . . . 14 (𝜑 → dom (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = ℂ)
8378, 82eqtrd 2773 . . . . . . . . . . . . 13 (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = ℂ)
8436, 83sseqtrrid 3928 . . . . . . . . . . . 12 (𝜑 → ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
85 dvres3 24657 . . . . . . . . . . . 12 (((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℂ⟶ℂ) ∧ (ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))) → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ))
8667, 73, 75, 84, 85syl22anc 838 . . . . . . . . . . 11 (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ))
87 resmpt 5873 . . . . . . . . . . . . 13 (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
8836, 87mp1i 13 . . . . . . . . . . . 12 (𝜑 → ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
8988oveq2d 7180 . . . . . . . . . . 11 (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
9077reseq1d 5818 . . . . . . . . . . . 12 (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = ((𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ))
91 resmpt 5873 . . . . . . . . . . . . 13 (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
9236, 91ax-mp 5 . . . . . . . . . . . 12 ((𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
9390, 92eqtrdi 2789 . . . . . . . . . . 11 (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
9486, 89, 933eqtr3d 2781 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
9594reseq1d 5818 . . . . . . . . 9 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
96 resmpt 5873 . . . . . . . . . 10 (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
973, 96mp1i 13 . . . . . . . . 9 (𝜑 → ((𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
9865, 95, 973eqtrd 2777 . . . . . . . 8 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
9935, 54, 983eqtrd 2777 . . . . . . 7 (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
100 dirkercncflem2.h . . . . . . . . 9 𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
101100a1i 11 . . . . . . . 8 (𝜑𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
102101eqcomd 2744 . . . . . . 7 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = 𝐻)
10330, 99, 1023eqtrd 2777 . . . . . 6 (𝜑 → (ℝ D 𝐹) = 𝐻)
104103dmeqd 5742 . . . . 5 (𝜑 → dom (ℝ D 𝐹) = dom 𝐻)
10511recnd 10740 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℂ)
106105, 81syldan 594 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ)
107100, 106dmmptd 6476 . . . . 5 (𝜑 → dom 𝐻 = ((𝐴(,)𝐵) ∖ {𝑌}))
108104, 107eqtr2d 2774 . . . 4 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐹))
109 eqimss 3931 . . . 4 (((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐹) → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐹))
110108, 109syl 17 . . 3 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐹))
111 dirkercncflem2.i . . . . . . . 8 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2))))
112111a1i 11 . . . . . . 7 (𝜑𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
113 resmpt 5873 . . . . . . . . . . . . 13 (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))))
1143, 113ax-mp 5 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
115114eqcomi 2747 . . . . . . . . . . 11 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))
116115oveq2i 7175 . . . . . . . . . 10 (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
117116a1i 11 . . . . . . . . 9 (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))))
118 2cn 11784 . . . . . . . . . . . . . 14 2 ∈ ℂ
119 picn 25196 . . . . . . . . . . . . . 14 π ∈ ℂ
120118, 119mulcli 10719 . . . . . . . . . . . . 13 (2 · π) ∈ ℂ
121120a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (2 · π) ∈ ℂ)
12243halfcld 11954 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → (𝑦 / 2) ∈ ℂ)
123122sincld 15568 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (sin‘(𝑦 / 2)) ∈ ℂ)
124121, 123mulcld 10732 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
125 eqid 2738 . . . . . . . . . . 11 (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))
126124, 125fmptd 6882 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))):ℝ⟶ℂ)
12751, 52dvres 24655 . . . . . . . . . 10 (((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)) → (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
12837, 126, 50, 127syl21anc 837 . . . . . . . . 9 (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
12964reseq2d 5819 . . . . . . . . . 10 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
13036sseli 3871 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
131 1cnd 10707 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → 1 ∈ ℂ)
132 2cnd 11787 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → 2 ∈ ℂ)
133 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
134 2ne0 11813 . . . . . . . . . . . . . . . . . . . . . 22 2 ≠ 0
135134a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → 2 ≠ 0)
136131, 132, 133, 135div13d 11511 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℂ → ((1 / 2) · 𝑦) = ((𝑦 / 2) · 1))
137 halfcl 11934 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → (𝑦 / 2) ∈ ℂ)
138137mulid1d 10729 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℂ → ((𝑦 / 2) · 1) = (𝑦 / 2))
139136, 138eqtrd 2773 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℂ → ((1 / 2) · 𝑦) = (𝑦 / 2))
140139fveq2d 6672 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℂ → (sin‘((1 / 2) · 𝑦)) = (sin‘(𝑦 / 2)))
141140oveq2d 7180 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℂ → ((2 · π) · (sin‘((1 / 2) · 𝑦))) = ((2 · π) · (sin‘(𝑦 / 2))))
142141eqcomd 2744 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℂ → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘((1 / 2) · 𝑦))))
143130, 142syl 17 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘((1 / 2) · 𝑦))))
144143adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘((1 / 2) · 𝑦))))
145144mpteq2dva 5122 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))))
146145oveq2d 7180 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))
147120a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ℂ) → (2 · π) ∈ ℂ)
14839a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ℂ) → (1 / 2) ∈ ℂ)
149148, 69mulcld 10732 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℂ) → ((1 / 2) · 𝑦) ∈ ℂ)
150149sincld 15568 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ℂ) → (sin‘((1 / 2) · 𝑦)) ∈ ℂ)
151147, 150mulcld 10732 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ℂ) → ((2 · π) · (sin‘((1 / 2) · 𝑦))) ∈ ℂ)
152 eqid 2738 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))
153151, 152fmptd 6882 . . . . . . . . . . . . . . 15 (𝜑 → (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))):ℂ⟶ℂ)
154 2cnd 11787 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ∈ ℂ)
155119a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → π ∈ ℂ)
156154, 155mulcld 10732 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2 · π) ∈ ℂ)
157 dvasinbx 42987 . . . . . . . . . . . . . . . . . . . 20 (((2 · π) ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦)))))
158156, 39, 157sylancl 589 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦)))))
159 2cnd 11787 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ ℂ) → 2 ∈ ℂ)
160119a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ ℂ) → π ∈ ℂ)
161159, 160, 148mul32d 10921 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ ℂ) → ((2 · π) · (1 / 2)) = ((2 · (1 / 2)) · π))
162134a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ ℂ) → 2 ≠ 0)
163159, 162recidd 11482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ ℂ) → (2 · (1 / 2)) = 1)
164163oveq1d 7179 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ ℂ) → ((2 · (1 / 2)) · π) = (1 · π))
165160mulid2d 10730 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ ℂ) → (1 · π) = π)
166161, 164, 1653eqtrd 2777 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ ℂ) → ((2 · π) · (1 / 2)) = π)
167139fveq2d 6672 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℂ → (cos‘((1 / 2) · 𝑦)) = (cos‘(𝑦 / 2)))
168167adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ ℂ) → (cos‘((1 / 2) · 𝑦)) = (cos‘(𝑦 / 2)))
169166, 168oveq12d 7182 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ ℂ) → (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦))) = (π · (cos‘(𝑦 / 2))))
170169mpteq2dva 5122 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ ℂ ↦ (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦)))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
171158, 170eqtrd 2773 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
172171dmeqd 5742 . . . . . . . . . . . . . . . . 17 (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = dom (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
173 eqid 2738 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2))))
17469halfcld 11954 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ ℂ) → (𝑦 / 2) ∈ ℂ)
175174coscld 15569 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ℂ) → (cos‘(𝑦 / 2)) ∈ ℂ)
176160, 175mulcld 10732 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℂ) → (π · (cos‘(𝑦 / 2))) ∈ ℂ)
177173, 176dmmptd 6476 . . . . . . . . . . . . . . . . 17 (𝜑 → dom (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) = ℂ)
178172, 177eqtrd 2773 . . . . . . . . . . . . . . . 16 (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = ℂ)
17936, 178sseqtrrid 3928 . . . . . . . . . . . . . . 15 (𝜑 → ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))
180 dvres3 24657 . . . . . . . . . . . . . . 15 (((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))):ℂ⟶ℂ) ∧ (ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))) → (ℝ D ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ))
18167, 153, 75, 179, 180syl22anc 838 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ))
182 resmpt 5873 . . . . . . . . . . . . . . . 16 (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))))
18336, 182mp1i 13 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))))
184183oveq2d 7180 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))
185171reseq1d 5818 . . . . . . . . . . . . . 14 (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ) = ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ))
186181, 184, 1853eqtr3d 2781 . . . . . . . . . . . . 13 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ))
187 resmpt 5873 . . . . . . . . . . . . . 14 (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
18836, 187ax-mp 5 . . . . . . . . . . . . 13 ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2))))
189186, 188eqtrdi 2789 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
190146, 189eqtrd 2773 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
191190reseq1d 5818 . . . . . . . . . 10 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
1924resmptd 5876 . . . . . . . . . 10 (𝜑 → ((𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
193129, 191, 1923eqtrd 2777 . . . . . . . . 9 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
194117, 128, 1933eqtrd 2777 . . . . . . . 8 (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
195194eqcomd 2744 . . . . . . 7 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))))
19623a1i 11 . . . . . . . . 9 (𝜑𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))))
197196oveq2d 7180 . . . . . . . 8 (𝜑 → (ℝ D 𝐺) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))))
198197eqcomd 2744 . . . . . . 7 (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D 𝐺))
199112, 195, 1983eqtrrd 2778 . . . . . 6 (𝜑 → (ℝ D 𝐺) = 𝐼)
200199dmeqd 5742 . . . . 5 (𝜑 → dom (ℝ D 𝐺) = dom 𝐼)
201105, 176syldan 594 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (π · (cos‘(𝑦 / 2))) ∈ ℂ)
202111, 201dmmptd 6476 . . . . 5 (𝜑 → dom 𝐼 = ((𝐴(,)𝐵) ∖ {𝑌}))
203200, 202eqtr2d 2774 . . . 4 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐺))
204 eqimss 3931 . . . 4 (((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐺) → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐺))
205203, 204syl 17 . . 3 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐺))
206105, 70syldan 594 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
207206ralrimiva 3096 . . . . . . 7 (𝜑 → ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
208 eqid 2738 . . . . . . . 8 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))
209208fnmpt 6471 . . . . . . 7 (∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}))
210207, 209syl 17 . . . . . 6 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}))
211 eqidd 2739 . . . . . . . . . 10 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
212 simpr 488 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
213212oveq2d 7180 . . . . . . . . . 10 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
214 simpr 488 . . . . . . . . . 10 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
21538adantr 484 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℂ)
216 1cnd 10707 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈ ℂ)
217216halfcld 11954 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈ ℂ)
218215, 217addcld 10731 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑁 + (1 / 2)) ∈ ℂ)
219 eldifi 4015 . . . . . . . . . . . . . 14 (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ (𝐴(,)𝐵))
220219elioored 42611 . . . . . . . . . . . . 13 (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ ℝ)
221220recnd 10740 . . . . . . . . . . . 12 (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ ℂ)
222221adantl 485 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑤 ∈ ℂ)
223218, 222mulcld 10732 . . . . . . . . . 10 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
224211, 213, 214, 223fvmptd 6776 . . . . . . . . 9 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
225 eleq1w 2815 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑤 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↔ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})))
226225anbi2d 632 . . . . . . . . . . . . . . 15 (𝑦 = 𝑤 → ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ↔ (𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))))
227 oveq1 7171 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑤 → (𝑦 mod (2 · π)) = (𝑤 mod (2 · π)))
228227neeq1d 2993 . . . . . . . . . . . . . . 15 (𝑦 = 𝑤 → ((𝑦 mod (2 · π)) ≠ 0 ↔ (𝑤 mod (2 · π)) ≠ 0))
229226, 228imbi12d 348 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 mod (2 · π)) ≠ 0) ↔ ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑤 mod (2 · π)) ≠ 0)))
230 eldifi 4015 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ (𝐴(,)𝐵))
231 elioore 12844 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝐴(,)𝐵) → 𝑦 ∈ ℝ)
232230, 231, 1303syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ ℂ)
233 2cnd 11787 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 2 ∈ ℂ)
234119a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → π ∈ ℂ)
235134a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 2 ≠ 0)
236 0re 10714 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℝ
237 pipos 25197 . . . . . . . . . . . . . . . . . . . . . 22 0 < π
238236, 237gtneii 10823 . . . . . . . . . . . . . . . . . . . . 21 π ≠ 0
239238a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → π ≠ 0)
240232, 233, 234, 235, 239divdiv1d 11518 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
241240eqcomd 2744 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
242241adantl 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
243 dirkercncflem2.yne0 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ≠ 0)
244243neneqd 2939 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (sin‘(𝑦 / 2)) = 0)
245105halfcld 11954 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℂ)
246 sineq0 25260 . . . . . . . . . . . . . . . . . . 19 ((𝑦 / 2) ∈ ℂ → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
247245, 246syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
248244, 247mtbid 327 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / 2) / π) ∈ ℤ)
249242, 248eqneltrd 2852 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
250 2rp 12470 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ+
251 pirp 25198 . . . . . . . . . . . . . . . . . 18 π ∈ ℝ+
252 rpmulcl 12488 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℝ+ ∧ π ∈ ℝ+) → (2 · π) ∈ ℝ+)
253250, 251, 252mp2an 692 . . . . . . . . . . . . . . . . 17 (2 · π) ∈ ℝ+
254 mod0 13328 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℝ ∧ (2 · π) ∈ ℝ+) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
25511, 253, 254sylancl 589 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
256249, 255mtbird 328 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 mod (2 · π)) = 0)
257256neqned 2941 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 mod (2 · π)) ≠ 0)
258229, 257chvarvv 2009 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑤 mod (2 · π)) ≠ 0)
259258neneqd 2939 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑤 mod (2 · π)) = 0)
260 simpll 767 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝜑)
261 simpr 488 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))
262221ad2antlr 727 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑤 ∈ ℂ)
26357recnd 10740 . . . . . . . . . . . . . . . 16 (𝜑𝑌 ∈ ℂ)
264263ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑌 ∈ ℂ)
265 0red 10715 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ∈ ℝ)
2665nnred 11724 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℝ)
267 1red 10713 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ∈ ℝ)
268267rehalfcld 11956 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 / 2) ∈ ℝ)
269266, 268readdcld 10741 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ)
2705nngt0d 11758 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 𝑁)
271250a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ∈ ℝ+)
272271rpreccld 12517 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 / 2) ∈ ℝ+)
273266, 272ltaddrpd 12540 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 < (𝑁 + (1 / 2)))
274265, 266, 269, 270, 273lttrd 10872 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 < (𝑁 + (1 / 2)))
275274gt0ne0d 11275 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 + (1 / 2)) ≠ 0)
27641, 275jca 515 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠ 0))
277276ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠ 0))
278 mulcan 11348 . . . . . . . . . . . . . . 15 ((𝑤 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠ 0)) → (((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌) ↔ 𝑤 = 𝑌))
279262, 264, 277, 278syl3anc 1372 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → (((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌) ↔ 𝑤 = 𝑌))
280261, 279mpbid 235 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑤 = 𝑌)
281 oveq1 7171 . . . . . . . . . . . . . 14 (𝑤 = 𝑌 → (𝑤 mod (2 · π)) = (𝑌 mod (2 · π)))
282 dirkercncflem2.ymod . . . . . . . . . . . . . 14 (𝜑 → (𝑌 mod (2 · π)) = 0)
283281, 282sylan9eqr 2795 . . . . . . . . . . . . 13 ((𝜑𝑤 = 𝑌) → (𝑤 mod (2 · π)) = 0)
284260, 280, 283syl2anc 587 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → (𝑤 mod (2 · π)) = 0)
285259, 284mtand 816 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))
28641, 263mulcld 10732 . . . . . . . . . . . . 13 (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ)
287286adantr 484 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ)
288 elsn2g 4551 . . . . . . . . . . . 12 (((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ → (((𝑁 + (1 / 2)) · 𝑤) ∈ {((𝑁 + (1 / 2)) · 𝑌)} ↔ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)))
289287, 288syl 17 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑁 + (1 / 2)) · 𝑤) ∈ {((𝑁 + (1 / 2)) · 𝑌)} ↔ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)))
290285, 289mtbird 328 . . . . . . . . . 10 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑁 + (1 / 2)) · 𝑤) ∈ {((𝑁 + (1 / 2)) · 𝑌)})
291223, 290eldifd 3852 . . . . . . . . 9 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑤) ∈ (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
292224, 291eqeltrd 2833 . . . . . . . 8 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
293 sinf 15562 . . . . . . . . . . . 12 sin:ℂ⟶ℂ
294293fdmi 6510 . . . . . . . . . . 11 dom sin = ℂ
295294eqcomi 2747 . . . . . . . . . 10 ℂ = dom sin
296295a1i 11 . . . . . . . . 9 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ℂ = dom sin)
297296difeq1d 4010 . . . . . . . 8 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}) = (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
298292, 297eleqtrd 2835 . . . . . . 7 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
299298ralrimiva 3096 . . . . . 6 (𝜑 → ∀𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
300 fnfvrnss 6888 . . . . . 6 (((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ∀𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) → ran (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ⊆ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
301210, 299, 300syl2anc 587 . . . . 5 (𝜑 → ran (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ⊆ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
302 uncom 4041 . . . . . . . . . 10 (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌}))
303302a1i 11 . . . . . . . . 9 (𝜑 → (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})))
30427snssd 4694 . . . . . . . . . 10 (𝜑 → {𝑌} ⊆ (𝐴(,)𝐵))
305 undif 4368 . . . . . . . . . 10 ({𝑌} ⊆ (𝐴(,)𝐵) ↔ ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐴(,)𝐵))
306304, 305sylib 221 . . . . . . . . 9 (𝜑 → ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐴(,)𝐵))
307303, 306eqtrd 2773 . . . . . . . 8 (𝜑 → (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = (𝐴(,)𝐵))
308307mpteq1d 5116 . . . . . . 7 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
309 iftrue 4417 . . . . . . . . . . . . 13 (𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑌))
310 oveq2 7172 . . . . . . . . . . . . 13 (𝑤 = 𝑌 → ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))
311309, 310eqtr4d 2776 . . . . . . . . . . . 12 (𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
312311adantl 485 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
313 iffalse 4420 . . . . . . . . . . . . 13 𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))
314313adantl 485 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))
315 eqidd 2739 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
316 oveq2 7172 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
317316adantl 485 . . . . . . . . . . . . 13 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
318 simpl 486 . . . . . . . . . . . . . . 15 ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ (𝐴(,)𝐵))
319 id 22 . . . . . . . . . . . . . . . . 17 𝑤 = 𝑌 → ¬ 𝑤 = 𝑌)
320 velsn 4529 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ {𝑌} ↔ 𝑤 = 𝑌)
321319, 320sylnibr 332 . . . . . . . . . . . . . . . 16 𝑤 = 𝑌 → ¬ 𝑤 ∈ {𝑌})
322321adantl 485 . . . . . . . . . . . . . . 15 ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → ¬ 𝑤 ∈ {𝑌})
323318, 322eldifd 3852 . . . . . . . . . . . . . 14 ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
324323adantll 714 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
32541adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (𝑁 + (1 / 2)) ∈ ℂ)
326 elioore 12844 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (𝐴(,)𝐵) → 𝑤 ∈ ℝ)
327326recnd 10740 . . . . . . . . . . . . . . . 16 (𝑤 ∈ (𝐴(,)𝐵) → 𝑤 ∈ ℂ)
328327adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → 𝑤 ∈ ℂ)
329325, 328mulcld 10732 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
330329adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
331315, 317, 324, 330fvmptd 6776 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
332314, 331eqtrd 2773 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
333312, 332pm2.61dan 813 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
334333mpteq2dva 5122 . . . . . . . . 9 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)))
335 ioosscn 12876 . . . . . . . . . . . . . 14 (𝐴(,)𝐵) ⊆ ℂ
336 resmpt 5873 . . . . . . . . . . . . . 14 ((𝐴(,)𝐵) ⊆ ℂ → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)))
337335, 336ax-mp 5 . . . . . . . . . . . . 13 ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤))
338 eqid 2738 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) = (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤))
339338mulc1cncf 23650 . . . . . . . . . . . . . . . 16 ((𝑁 + (1 / 2)) ∈ ℂ → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (ℂ–cn→ℂ))
34041, 339syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (ℂ–cn→ℂ))
34151cnfldtop 23529 . . . . . . . . . . . . . . . . . . 19 (TopOpen‘ℂfld) ∈ Top
342 unicntop 23531 . . . . . . . . . . . . . . . . . . . 20 ℂ = (TopOpen‘ℂfld)
343342restid 16803 . . . . . . . . . . . . . . . . . . 19 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
344341, 343ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
345344eqcomi 2747 . . . . . . . . . . . . . . . . 17 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
34651, 345, 345cncfcn 23655 . . . . . . . . . . . . . . . 16 ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℂ) = ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
34774, 75, 346sylancr 590 . . . . . . . . . . . . . . 15 (𝜑 → (ℂ–cn→ℂ) = ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
348340, 347eleqtrd 2835 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
3492, 37sstrid 3886 . . . . . . . . . . . . . 14 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
350342cnrest 22029 . . . . . . . . . . . . . 14 (((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
351348, 349, 350syl2anc 587 . . . . . . . . . . . . 13 (𝜑 → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
352337, 351eqeltrrid 2838 . . . . . . . . . . . 12 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
35351cnfldtopon 23528 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
354 resttopon 21905 . . . . . . . . . . . . . 14 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)))
355353, 349, 354sylancr 590 . . . . . . . . . . . . 13 (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)))
356 cncnp 22024 . . . . . . . . . . . . 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))‘𝑦))))
357355, 353, 356sylancl 589 . . . . . . . . . . . 12 (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ↔ ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))))
358352, 357mpbid 235 . . . . . . . . . . 11 (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦)))
359358simprd 499 . . . . . . . . . 10 (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
360 fveq2 6668 . . . . . . . . . . . 12 (𝑦 = 𝑌 → ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
361360eleq2d 2818 . . . . . . . . . . 11 (𝑦 = 𝑌 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌)))
362361rspccva 3523 . . . . . . . . . 10 ((∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
363359, 27, 362syl2anc 587 . . . . . . . . 9 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
364334, 363eqeltrd 2833 . . . . . . . 8 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
365307eqcomd 2744 . . . . . . . . . . 11 (𝜑 → (𝐴(,)𝐵) = (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}))
366365oveq2d 7180 . . . . . . . . . 10 (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})))
367366oveq1d 7179 . . . . . . . . 9 (𝜑 → (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld)))
368367fveq1d 6670 . . . . . . . 8 (𝜑 → ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌) = ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
369364, 368eleqtrd 2835 . . . . . . 7 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
370308, 369eqeltrd 2833 . . . . . 6 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
371 eqid 2738 . . . . . . 7 ((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) = ((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}))
372 eqid 2738 . . . . . . 7 (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))
373206, 208fmptd 6882 . . . . . . 7 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
3744, 36sstrdi 3887 . . . . . . 7 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℂ)
375371, 51, 372, 373, 374, 263ellimc 24617 . . . . . 6 (𝜑 → (((𝑁 + (1 / 2)) · 𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) lim 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌)))
376370, 375mpbird 260 . . . . 5 (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) lim 𝑌))
377134a1i 11 . . . . . . . . . . . 12 (𝜑 → 2 ≠ 0)
378238a1i 11 . . . . . . . . . . . 12 (𝜑 → π ≠ 0)
379154, 155, 377, 378mulne0d 11363 . . . . . . . . . . 11 (𝜑 → (2 · π) ≠ 0)
380263, 156, 379divcan1d 11488 . . . . . . . . . 10 (𝜑 → ((𝑌 / (2 · π)) · (2 · π)) = 𝑌)
381380eqcomd 2744 . . . . . . . . 9 (𝜑𝑌 = ((𝑌 / (2 · π)) · (2 · π)))
382381oveq2d 7180 . . . . . . . 8 (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))))
383382fveq2d 6672 . . . . . . 7 (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) = (sin‘((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π)))))
384263, 156, 379divcld 11487 . . . . . . . . . . 11 (𝜑 → (𝑌 / (2 · π)) ∈ ℂ)
38541, 384, 156mul12d 10920 . . . . . . . . . 10 (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = ((𝑌 / (2 · π)) · ((𝑁 + (1 / 2)) · (2 · π))))
38641, 154, 155mulassd 10735 . . . . . . . . . . . 12 (𝜑 → (((𝑁 + (1 / 2)) · 2) · π) = ((𝑁 + (1 / 2)) · (2 · π)))
387386eqcomd 2744 . . . . . . . . . . 11 (𝜑 → ((𝑁 + (1 / 2)) · (2 · π)) = (((𝑁 + (1 / 2)) · 2) · π))
388387oveq2d 7180 . . . . . . . . . 10 (𝜑 → ((𝑌 / (2 · π)) · ((𝑁 + (1 / 2)) · (2 · π))) = ((𝑌 / (2 · π)) · (((𝑁 + (1 / 2)) · 2) · π)))
38938, 40, 154adddird 10737 . . . . . . . . . . . . 13 (𝜑 → ((𝑁 + (1 / 2)) · 2) = ((𝑁 · 2) + ((1 / 2) · 2)))
390154, 377recid2d 11483 . . . . . . . . . . . . . 14 (𝜑 → ((1 / 2) · 2) = 1)
391390oveq2d 7180 . . . . . . . . . . . . 13 (𝜑 → ((𝑁 · 2) + ((1 / 2) · 2)) = ((𝑁 · 2) + 1))
392389, 391eqtrd 2773 . . . . . . . . . . . 12 (𝜑 → ((𝑁 + (1 / 2)) · 2) = ((𝑁 · 2) + 1))
393392oveq1d 7179 . . . . . . . . . . 11 (𝜑 → (((𝑁 + (1 / 2)) · 2) · π) = (((𝑁 · 2) + 1) · π))
394393oveq2d 7180 . . . . . . . . . 10 (𝜑 → ((𝑌 / (2 · π)) · (((𝑁 + (1 / 2)) · 2) · π)) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
395385, 388, 3943eqtrd 2777 . . . . . . . . 9 (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
39638, 154mulcld 10732 . . . . . . . . . . 11 (𝜑 → (𝑁 · 2) ∈ ℂ)
397 1cnd 10707 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
398396, 397addcld 10731 . . . . . . . . . 10 (𝜑 → ((𝑁 · 2) + 1) ∈ ℂ)
399384, 398, 155mulassd 10735 . . . . . . . . 9 (𝜑 → (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
400395, 399eqtr4d 2776 . . . . . . . 8 (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π))
401400fveq2d 6672 . . . . . . 7 (𝜑 → (sin‘((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π)))) = (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π)))
402 mod0 13328 . . . . . . . . . . 11 ((𝑌 ∈ ℝ ∧ (2 · π) ∈ ℝ+) → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
40357, 253, 402sylancl 589 . . . . . . . . . 10 (𝜑 → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
404282, 403mpbid 235 . . . . . . . . 9 (𝜑 → (𝑌 / (2 · π)) ∈ ℤ)
4055nnzd 12160 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℤ)
406 2z 12088 . . . . . . . . . . . 12 2 ∈ ℤ
407406a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℤ)
408405, 407zmulcld 12167 . . . . . . . . . 10 (𝜑 → (𝑁 · 2) ∈ ℤ)
409408peano2zd 12164 . . . . . . . . 9 (𝜑 → ((𝑁 · 2) + 1) ∈ ℤ)
410404, 409zmulcld 12167 . . . . . . . 8 (𝜑 → ((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ∈ ℤ)
411 sinkpi 25258 . . . . . . . 8 (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ∈ ℤ → (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π)) = 0)
412410, 411syl 17 . . . . . . 7 (𝜑 → (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π)) = 0)
413383, 401, 4123eqtrd 2777 . . . . . 6 (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) = 0)
414 sincn 25183 . . . . . . . 8 sin ∈ (ℂ–cn→ℂ)
415414a1i 11 . . . . . . 7 (𝜑 → sin ∈ (ℂ–cn→ℂ))
416415, 286cnlimci 24633 . . . . . 6 (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) ∈ (sin lim ((𝑁 + (1 / 2)) · 𝑌)))
417413, 416eqeltrrd 2834 . . . . 5 (𝜑 → 0 ∈ (sin lim ((𝑁 + (1 / 2)) · 𝑌)))
418301, 376, 417limccog 42687 . . . 4 (𝜑 → 0 ∈ ((sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) lim 𝑌))
41914a1i 11 . . . . . . . . 9 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
420213fveq2d 6672 . . . . . . . . 9 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
421223sincld 15568 . . . . . . . . 9 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑤)) ∈ ℂ)
422419, 420, 214, 421fvmptd 6776 . . . . . . . 8 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹𝑤) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
423224fveq2d 6672 . . . . . . . 8 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
424422, 423eqtr4d 2776 . . . . . . 7 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹𝑤) = (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))
425424mpteq2dva 5122 . . . . . 6 (𝜑 → (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (𝐹𝑤)) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
42615feqmptd 6731 . . . . . 6 (𝜑𝐹 = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (𝐹𝑤)))
427 fcompt 6899 . . . . . . 7 ((sin:ℂ⟶ℂ ∧ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
428293, 373, 427sylancr 590 . . . . . 6 (𝜑 → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
429425, 426, 4283eqtr4rd 2784 . . . . 5 (𝜑 → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = 𝐹)
430429oveq1d 7179 . . . 4 (𝜑 → ((sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) lim 𝑌) = (𝐹 lim 𝑌))
431418, 430eleqtrd 2835 . . 3 (𝜑 → 0 ∈ (𝐹 lim 𝑌))
432 simpr 488 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → 𝑤 = 𝑌)
433432iftrued 4419 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = 0)
434263, 154, 156, 377, 379divdiv32d 11512 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑌 / 2) / (2 · π)) = ((𝑌 / (2 · π)) / 2))
435434oveq1d 7179 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑌 / 2) / (2 · π)) · (2 · π)) = (((𝑌 / (2 · π)) / 2) · (2 · π)))
436263halfcld 11954 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑌 / 2) ∈ ℂ)
437436, 156, 379divcan1d 11488 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑌 / 2) / (2 · π)) · (2 · π)) = (𝑌 / 2))
438384, 154, 156, 377div32d 11510 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑌 / (2 · π)) / 2) · (2 · π)) = ((𝑌 / (2 · π)) · ((2 · π) / 2)))
439155, 154, 377divcan3d 11492 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2 · π) / 2) = π)
440439oveq2d 7180 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑌 / (2 · π)) · ((2 · π) / 2)) = ((𝑌 / (2 · π)) · π))
441438, 440eqtrd 2773 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑌 / (2 · π)) / 2) · (2 · π)) = ((𝑌 / (2 · π)) · π))
442435, 437, 4413eqtr3d 2781 . . . . . . . . . . . . . . 15 (𝜑 → (𝑌 / 2) = ((𝑌 / (2 · π)) · π))
443442fveq2d 6672 . . . . . . . . . . . . . 14 (𝜑 → (sin‘(𝑌 / 2)) = (sin‘((𝑌 / (2 · π)) · π)))
444 sinkpi 25258 . . . . . . . . . . . . . . 15 ((𝑌 / (2 · π)) ∈ ℤ → (sin‘((𝑌 / (2 · π)) · π)) = 0)
445404, 444syl 17 . . . . . . . . . . . . . 14 (𝜑 → (sin‘((𝑌 / (2 · π)) · π)) = 0)
446443, 445eqtrd 2773 . . . . . . . . . . . . 13 (𝜑 → (sin‘(𝑌 / 2)) = 0)
447446oveq2d 7180 . . . . . . . . . . . 12 (𝜑 → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · 0))
448156mul01d 10910 . . . . . . . . . . . 12 (𝜑 → ((2 · π) · 0) = 0)
449447, 448eqtrd 2773 . . . . . . . . . . 11 (𝜑 → ((2 · π) · (sin‘(𝑌 / 2))) = 0)
450449eqcomd 2744 . . . . . . . . . 10 (𝜑 → 0 = ((2 · π) · (sin‘(𝑌 / 2))))
451450ad2antrr 726 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → 0 = ((2 · π) · (sin‘(𝑌 / 2))))
452 fvoveq1 7187 . . . . . . . . . . . 12 (𝑤 = 𝑌 → (sin‘(𝑤 / 2)) = (sin‘(𝑌 / 2)))
453452oveq2d 7180 . . . . . . . . . . 11 (𝑤 = 𝑌 → ((2 · π) · (sin‘(𝑤 / 2))) = ((2 · π) · (sin‘(𝑌 / 2))))
454453eqcomd 2744 . . . . . . . . . 10 (𝑤 = 𝑌 → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
455454adantl 485 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
456433, 451, 4553eqtrd 2777 . . . . . . . 8 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
457 iffalse 4420 . . . . . . . . . 10 𝑤 = 𝑌 → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = (𝐺𝑤))
458457adantl 485 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = (𝐺𝑤))
459 fvoveq1 7187 . . . . . . . . . . 11 (𝑦 = 𝑤 → (sin‘(𝑦 / 2)) = (sin‘(𝑤 / 2)))
460459oveq2d 7180 . . . . . . . . . 10 (𝑦 = 𝑤 → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
461120a1i 11 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (2 · π) ∈ ℂ)
462328halfcld 11954 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 / 2) ∈ ℂ)
463462sincld 15568 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (sin‘(𝑤 / 2)) ∈ ℂ)
464461, 463mulcld 10732 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ((2 · π) · (sin‘(𝑤 / 2))) ∈ ℂ)
465464adantr 484 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((2 · π) · (sin‘(𝑤 / 2))) ∈ ℂ)
46623, 460, 324, 465fvmptd3 6792 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐺𝑤) = ((2 · π) · (sin‘(𝑤 / 2))))
467458, 466eqtrd 2773 . . . . . . . 8 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
468456, 467pm2.61dan 813 . . . . . . 7 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
469468mpteq2dva 5122 . . . . . 6 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))))
470 eqid 2738 . . . . . . . . . . 11 (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2)))) = (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2))))
47175, 156, 75constcncfg 42939 . . . . . . . . . . . 12 (𝜑 → (𝑤 ∈ ℂ ↦ (2 · π)) ∈ (ℂ–cn→ℂ))
472 id 22 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ → 𝑤 ∈ ℂ)
473 2cnd 11787 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ → 2 ∈ ℂ)
474134a1i 11 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ → 2 ≠ 0)
475472, 473, 474divrec2d 11491 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℂ → (𝑤 / 2) = ((1 / 2) · 𝑤))
476475mpteq2ia 5118 . . . . . . . . . . . . . . 15 (𝑤 ∈ ℂ ↦ (𝑤 / 2)) = (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤))
477 eqid 2738 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) = (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤))
478477mulc1cncf 23650 . . . . . . . . . . . . . . . 16 ((1 / 2) ∈ ℂ → (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) ∈ (ℂ–cn→ℂ))
47939, 478ax-mp 5 . . . . . . . . . . . . . . 15 (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) ∈ (ℂ–cn→ℂ)
480476, 479eqeltri 2829 . . . . . . . . . . . . . 14 (𝑤 ∈ ℂ ↦ (𝑤 / 2)) ∈ (ℂ–cn→ℂ)
481480a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ∈ ℂ ↦ (𝑤 / 2)) ∈ (ℂ–cn→ℂ))
482415, 481cncfmpt1f 23659 . . . . . . . . . . . 12 (𝜑 → (𝑤 ∈ ℂ ↦ (sin‘(𝑤 / 2))) ∈ (ℂ–cn→ℂ))
483471, 482mulcncf 24191 . . . . . . . . . . 11 (𝜑 → (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ (ℂ–cn→ℂ))
484470, 483, 349, 75, 464cncfmptssg 42938 . . . . . . . . . 10 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
485 eqid 2738 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
48651, 485, 345cncfcn 23655 . . . . . . . . . . 11 (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
487349, 74, 486sylancl 589 . . . . . . . . . 10 (𝜑 → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
488484, 487eleqtrd 2835 . . . . . . . . 9 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
489 cncnp 22024 . . . . . . . . . 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))‘𝑦))))
490355, 353, 489sylancl 589 . . . . . . . . 9 (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ↔ ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))))
491488, 490mpbid 235 . . . . . . . 8 (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦)))
492491simprd 499 . . . . . . 7 (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
493360eleq2d 2818 . . . . . . . 8 (𝑦 = 𝑌 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌)))
494493rspccva 3523 . . . . . . 7 ((∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
495492, 27, 494syl2anc 587 . . . . . 6 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
496469, 495eqeltrd 2833 . . . . 5 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
497307mpteq1d 5116 . . . . 5 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))))
498366eqcomd 2744 . . . . . . 7 (𝜑 → ((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
499498oveq1d 7179 . . . . . 6 (𝜑 → (((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld)))
500499fveq1d 6670 . . . . 5 (𝜑 → ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌) = ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
501496, 497, 5003eltr4d 2848 . . . 4 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
502 eqid 2738 . . . . 5 (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤)))
50311, 124syldan 594 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
504503, 23fmptd 6882 . . . . 5 (𝜑𝐺:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
505371, 51, 502, 504, 374, 263ellimc 24617 . . . 4 (𝜑 → (0 ∈ (𝐺 lim 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌)))
506501, 505mpbird 260 . . 3 (𝜑 → 0 ∈ (𝐺 lim 𝑌))
507256nrexdv 3179 . . . 4 (𝜑 → ¬ ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0)
508504ffund 6502 . . . . . 6 (𝜑 → Fun 𝐺)
509 fvelima 6729 . . . . . 6 ((Fun 𝐺 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺𝑦) = 0)
510508, 509sylan 583 . . . . 5 ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺𝑦) = 0)
511 2cnd 11787 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ∈ ℂ)
512119a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ∈ ℂ)
513134a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ≠ 0)
514238a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ≠ 0)
515105, 511, 512, 513, 514divdiv1d 11518 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
516515eqcomd 2744 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
517516adantr 484 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
518 2cnd 11787 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → 2 ∈ ℂ)
519119a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → π ∈ ℂ)
520518, 519mulcld 10732 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (2 · π) ∈ ℂ)
521232adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → 𝑦 ∈ ℂ)
522521halfcld 11954 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (𝑦 / 2) ∈ ℂ)
523522sincld 15568 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (sin‘(𝑦 / 2)) ∈ ℂ)
524520, 523mulcld 10732 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
52523fvmpt2 6780 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ) → (𝐺𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
526524, 525syldan 594 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (𝐺𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
527526eqcomd 2744 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) = (𝐺𝑦))
528 simpr 488 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (𝐺𝑦) = 0)
529527, 528eqtrd 2773 . . . . . . . . . . . . . 14 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) = 0)
530120a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (2 · π) ∈ ℂ)
531232halfcld 11954 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (𝑦 / 2) ∈ ℂ)
532531sincld 15568 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (sin‘(𝑦 / 2)) ∈ ℂ)
533530, 532mul0ord 11361 . . . . . . . . . . . . . . 15 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (((2 · π) · (sin‘(𝑦 / 2))) = 0 ↔ ((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0)))
534533adantr 484 . . . . . . . . . . . . . 14 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (((2 · π) · (sin‘(𝑦 / 2))) = 0 ↔ ((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0)))
535529, 534mpbid 235 . . . . . . . . . . . . 13 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → ((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0))
536 2cnne0 11919 . . . . . . . . . . . . . . 15 (2 ∈ ℂ ∧ 2 ≠ 0)
537119, 238pm3.2i 474 . . . . . . . . . . . . . . 15 (π ∈ ℂ ∧ π ≠ 0)
538 mulne0 11353 . . . . . . . . . . . . . . 15 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → (2 · π) ≠ 0)
539536, 537, 538mp2an 692 . . . . . . . . . . . . . 14 (2 · π) ≠ 0
540539neii 2936 . . . . . . . . . . . . 13 ¬ (2 · π) = 0
541 pm2.53 850 . . . . . . . . . . . . 13 (((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0) → (¬ (2 · π) = 0 → (sin‘(𝑦 / 2)) = 0))
542535, 540, 541mpisyl 21 . . . . . . . . . . . 12 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (sin‘(𝑦 / 2)) = 0)
543542adantll 714 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → (sin‘(𝑦 / 2)) = 0)
544105adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → 𝑦 ∈ ℂ)
545544halfcld 11954 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → (𝑦 / 2) ∈ ℂ)
546545, 246syl 17 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
547543, 546mpbid 235 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → ((𝑦 / 2) / π) ∈ ℤ)
548517, 547eqeltrd 2833 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → (𝑦 / (2 · π)) ∈ ℤ)
54911adantr 484 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → 𝑦 ∈ ℝ)
550549, 253, 254sylancl 589 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
551548, 550mpbird 260 . . . . . . . 8 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → (𝑦 mod (2 · π)) = 0)
552551ex 416 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐺𝑦) = 0 → (𝑦 mod (2 · π)) = 0))
553552reximdva 3183 . . . . . 6 (𝜑 → (∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺𝑦) = 0 → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0))
554553adantr 484 . . . . 5 ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → (∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺𝑦) = 0 → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0))
555510, 554mpd 15 . . . 4 ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0)
556507, 555mtand 816 . . 3 (𝜑 → ¬ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌})))
557 simpr 488 . . . . . . . . 9 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
558111fvmpt2 6780 . . . . . . . . 9 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (π · (cos‘(𝑦 / 2))) ∈ ℂ) → (𝐼𝑦) = (π · (cos‘(𝑦 / 2))))
559557, 201, 558syl2anc 587 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐼𝑦) = (π · (cos‘(𝑦 / 2))))
560531coscld 15569 . . . . . . . . . 10 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (cos‘(𝑦 / 2)) ∈ ℂ)
561560adantl 485 . . . . . . . . 9 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ∈ ℂ)
562 dirkercncflem2.11 . . . . . . . . 9 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0)
563512, 561, 514, 562mulne0d 11363 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (π · (cos‘(𝑦 / 2))) ≠ 0)
564559, 563eqnetrd 3001 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐼𝑦) ≠ 0)
565564neneqd 2939 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝐼𝑦) = 0)
566565nrexdv 3179 . . . . 5 (𝜑 → ¬ ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼𝑦) = 0)
567201, 111fmptd 6882 . . . . . . 7 (𝜑𝐼:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
568567ffund 6502 . . . . . 6 (𝜑 → Fun 𝐼)
569 fvelima 6729 . . . . . 6 ((Fun 𝐼 ∧ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼𝑦) = 0)
570568, 569sylan 583 . . . . 5 ((𝜑 ∧ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼𝑦) = 0)
571566, 570mtand 816 . . . 4 (𝜑 → ¬ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌})))
572199imaeq1d 5896 . . . 4 (𝜑 → ((ℝ D 𝐺) “ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌})))
573571, 572neleqtrrd 2855 . . 3 (𝜑 → ¬ 0 ∈ ((ℝ D 𝐺) “ ((𝐴(,)𝐵) ∖ {𝑌})))
574 dirkercncflem2.d . . . . . 6 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
575574dirkerval2 43161 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑌 ∈ ℝ) → ((𝐷𝑁)‘𝑌) = if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))))
5765, 57, 575syl2anc 587 . . . 4 (𝜑 → ((𝐷𝑁)‘𝑌) = if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))))
577282iftrued 4419 . . . . 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)))))
579578a1i 11 . . . . . . . . . 10 (𝜑𝐿 = (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))))
580 iftrue 4417 . . . . . . . . . . . . . 14 (𝑤 = 𝑌 → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)) = (((2 · 𝑁) + 1) / (2 · π)))
581580adantl 485 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)) = (((2 · 𝑁) + 1) / (2 · π)))
582154, 38mulcld 10732 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2 · 𝑁) ∈ ℂ)
583582, 397addcld 10731 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2 · 𝑁) + 1) ∈ ℂ)
584583, 154, 155, 377, 378divdiv1d 11518 . . . . . . . . . . . . . . . 16 (𝜑 → ((((2 · 𝑁) + 1) / 2) / π) = (((2 · 𝑁) + 1) / (2 · π)))
585584eqcomd 2744 . . . . . . . . . . . . . . 15 (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) = ((((2 · 𝑁) + 1) / 2) / π))
586582, 397, 154, 377divdird 11525 . . . . . . . . . . . . . . . . 17 (𝜑 → (((2 · 𝑁) + 1) / 2) = (((2 · 𝑁) / 2) + (1 / 2)))
58738, 154, 377divcan3d 11492 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2 · 𝑁) / 2) = 𝑁)
588587oveq1d 7179 . . . . . . . . . . . . . . . . 17 (𝜑 → (((2 · 𝑁) / 2) + (1 / 2)) = (𝑁 + (1 / 2)))
589586, 588eqtrd 2773 . . . . . . . . . . . . . . . 16 (𝜑 → (((2 · 𝑁) + 1) / 2) = (𝑁 + (1 / 2)))
590589oveq1d 7179 . . . . . . . . . . . . . . 15 (𝜑 → ((((2 · 𝑁) + 1) / 2) / π) = ((𝑁 + (1 / 2)) / π))
591585, 590eqtrd 2773 . . . . . . . . . . . . . 14 (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) = ((𝑁 + (1 / 2)) / π))
592591ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((2 · 𝑁) + 1) / (2 · π)) = ((𝑁 + (1 / 2)) / π))
593310fveq2d 6672 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑌 → (cos‘((𝑁 + (1 / 2)) · 𝑤)) = (cos‘((𝑁 + (1 / 2)) · 𝑌)))
594593oveq2d 7180 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑌 → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))))
595 fvoveq1 7187 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑌 → (cos‘(𝑤 / 2)) = (cos‘(𝑌 / 2)))
596595oveq2d 7180 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑌 → (π · (cos‘(𝑤 / 2))) = (π · (cos‘(𝑌 / 2))))
597594, 596oveq12d 7182 . . . . . . . . . . . . . . 15 (𝑤 = 𝑌 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))))
598597adantl 485 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))))
59938, 40, 263adddird 10737 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑁 · 𝑌) + ((1 / 2) · 𝑌)))
600397, 154, 263, 377div32d 11510 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((1 / 2) · 𝑌) = (1 · (𝑌 / 2)))
601436mulid2d 10730 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 · (𝑌 / 2)) = (𝑌 / 2))
602600, 601eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1 / 2) · 𝑌) = (𝑌 / 2))
603602oveq2d 7180 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑁 · 𝑌) + ((1 / 2) · 𝑌)) = ((𝑁 · 𝑌) + (𝑌 / 2)))
60438, 263mulcld 10732 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑁 · 𝑌) ∈ ℂ)
605604, 436addcomd 10913 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑁 · 𝑌) + (𝑌 / 2)) = ((𝑌 / 2) + (𝑁 · 𝑌)))
606599, 603, 6053eqtrd 2777 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑌 / 2) + (𝑁 · 𝑌)))
607606fveq2d 6672 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (cos‘((𝑁 + (1 / 2)) · 𝑌)) = (cos‘((𝑌 / 2) + (𝑁 · 𝑌))))
608604, 156, 379divcan1d 11488 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑁 · 𝑌) / (2 · π)) · (2 · π)) = (𝑁 · 𝑌))
609608eqcomd 2744 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑁 · 𝑌) = (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))
610609oveq2d 7180 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑌 / 2) + (𝑁 · 𝑌)) = ((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π))))
611610fveq2d 6672 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (cos‘((𝑌 / 2) + (𝑁 · 𝑌))) = (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))))
61238, 263, 156, 379divassd 11522 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑁 · 𝑌) / (2 · π)) = (𝑁 · (𝑌 / (2 · π))))
613405, 404zmulcld 12167 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑁 · (𝑌 / (2 · π))) ∈ ℤ)
614612, 613eqeltrd 2833 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑁 · 𝑌) / (2 · π)) ∈ ℤ)
615 cosper 25219 . . . . . . . . . . . . . . . . . . . 20 (((𝑌 / 2) ∈ ℂ ∧ ((𝑁 · 𝑌) / (2 · π)) ∈ ℤ) → (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))) = (cos‘(𝑌 / 2)))
616436, 614, 615syl2anc 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))) = (cos‘(𝑌 / 2)))
617607, 611, 6163eqtrd 2777 . . . . . . . . . . . . . . . . . 18 (𝜑 → (cos‘((𝑁 + (1 / 2)) · 𝑌)) = (cos‘(𝑌 / 2)))
618617oveq2d 7180 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) = ((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))))
619618oveq1d 7179 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = (((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))) / (π · (cos‘(𝑌 / 2)))))
620436coscld 15569 . . . . . . . . . . . . . . . . 17 (𝜑 → (cos‘(𝑌 / 2)) ∈ ℂ)
621263, 154, 155, 377, 378divdiv1d 11518 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑌 / 2) / π) = (𝑌 / (2 · π)))
622621, 404eqeltrd 2833 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑌 / 2) / π) ∈ ℤ)
623622zred 12161 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑌 / 2) / π) ∈ ℝ)
624623, 272ltaddrpd 12540 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑌 / 2) / π) < (((𝑌 / 2) / π) + (1 / 2)))
625 halflt1 11927 . . . . . . . . . . . . . . . . . . . . . 22 (1 / 2) < 1
626625a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (1 / 2) < 1)
627268, 267, 623, 626ltadd2dd 10870 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝑌 / 2) / π) + (1 / 2)) < (((𝑌 / 2) / π) + 1))
628 btwnnz 12132 . . . . . . . . . . . . . . . . . . . 20 ((((𝑌 / 2) / π) ∈ ℤ ∧ ((𝑌 / 2) / π) < (((𝑌 / 2) / π) + (1 / 2)) ∧ (((𝑌 / 2) / π) + (1 / 2)) < (((𝑌 / 2) / π) + 1)) → ¬ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ)
629622, 624, 627, 628syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ)
630 coseq0 42931 . . . . . . . . . . . . . . . . . . . 20 ((𝑌 / 2) ∈ ℂ → ((cos‘(𝑌 / 2)) = 0 ↔ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ))
631436, 630syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((cos‘(𝑌 / 2)) = 0 ↔ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ))
632629, 631mtbird 328 . . . . . . . . . . . . . . . . . 18 (𝜑 → ¬ (cos‘(𝑌 / 2)) = 0)
633632neqned 2941 . . . . . . . . . . . . . . . . 17 (𝜑 → (cos‘(𝑌 / 2)) ≠ 0)
63441, 155, 620, 378, 633divcan5rd 11514 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
635619, 634eqtrd 2773 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
636635ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
637598, 636eqtr2d 2774 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) / π) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))))
638581, 592, 6373eqtrrd 2778 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)))
639 iffalse 4420 . . . . . . . . . . . . . 14 𝑤 = 𝑌 → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))
640639adantl 485 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))
641 eqidd 2739 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))))
642 fveq2 6668 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑤 → (𝐻𝑦) = (𝐻𝑤))
643 fveq2 6668 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑤 → (𝐼𝑦) = (𝐼𝑤))
644642, 643oveq12d 7182 . . . . . . . . . . . . . . 15 (𝑦 = 𝑤 → ((𝐻𝑦) / (𝐼𝑦)) = ((𝐻𝑤) / (𝐼𝑤)))
645644adantl 485 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝐻𝑦) / (𝐼𝑦)) = ((𝐻𝑤) / (𝐼𝑤)))
646106, 100fmptd 6882 . . . . . . . . . . . . . . . . 17 (𝜑𝐻:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
647646ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐻:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
648647, 324ffvelrnd 6856 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐻𝑤) ∈ ℂ)
649567ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐼:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
650649, 324ffvelrnd 6856 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼𝑤) ∈ ℂ)
651111a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
652 simpr 488 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
653652fvoveq1d 7186 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (cos‘(𝑦 / 2)) = (cos‘(𝑤 / 2)))
654653oveq2d 7180 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (π · (cos‘(𝑦 / 2))) = (π · (cos‘(𝑤 / 2))))
655119a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (𝐴(,)𝐵) → π ∈ ℂ)
656327halfcld 11954 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝐴(,)𝐵) → (𝑤 / 2) ∈ ℂ)
657656coscld 15569 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (𝐴(,)𝐵) → (cos‘(𝑤 / 2)) ∈ ℂ)
658655, 657mulcld 10732 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (𝐴(,)𝐵) → (π · (cos‘(𝑤 / 2))) ∈ ℂ)
659658ad2antlr 727 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π · (cos‘(𝑤 / 2))) ∈ ℂ)
660651, 654, 324, 659fvmptd 6776 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼𝑤) = (π · (cos‘(𝑤 / 2))))
661537a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π ∈ ℂ ∧ π ≠ 0))
662657ad2antlr 727 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ∈ ℂ)
663 simpll 767 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝜑)
664 fvoveq1 7187 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑤 → (cos‘(𝑦 / 2)) = (cos‘(𝑤 / 2)))
665664neeq1d 2993 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑤 → ((cos‘(𝑦 / 2)) ≠ 0 ↔ (cos‘(𝑤 / 2)) ≠ 0))
666226, 665imbi12d 348 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑤 → (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0) ↔ ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑤 / 2)) ≠ 0)))
667666, 562chvarvv 2009 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑤 / 2)) ≠ 0)
668663, 324, 667syl2anc 587 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
669 mulne0 11353 . . . . . . . . . . . . . . . . 17 (((π ∈ ℂ ∧ π ≠ 0) ∧ ((cos‘(𝑤 / 2)) ∈ ℂ ∧ (cos‘(𝑤 / 2)) ≠ 0)) → (π · (cos‘(𝑤 / 2))) ≠ 0)
670661, 662, 668, 669syl12anc 836 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π · (cos‘(𝑤 / 2))) ≠ 0)
671660, 670eqnetrd 3001 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼𝑤) ≠ 0)
672648, 650, 671divcld 11487 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝐻𝑤) / (𝐼𝑤)) ∈ ℂ)
673641, 645, 324, 672fvmptd 6776 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤) = ((𝐻𝑤) / (𝐼𝑤)))
674100a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
675317fveq2d 6672 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (cos‘((𝑁 + (1 / 2)) · 𝑦)) = (cos‘((𝑁 + (1 / 2)) · 𝑤)))
676675oveq2d 7180 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))))
677329coscld 15569 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (cos‘((𝑁 + (1 / 2)) · 𝑤)) ∈ ℂ)
678325, 677mulcld 10732 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ℂ)
679678adantr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ℂ)
680674, 676, 324, 679fvmptd 6776 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐻𝑤) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))))
681680, 660oveq12d 7182 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝐻𝑤) / (𝐼𝑤)) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))))
682640, 673, 6813eqtrrd 2778 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)))
683638, 682pm2.61dan 813 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)))
684683mpteq2dva 5122 . . . . . . . . . 10 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))))
685579, 684eqtr2d 2774 . . . . . . . . 9 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) = 𝐿)
686349, 41, 75constcncfg 42939 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
687 cosf 15563 . . . . . . . . . . . . . . . . . . 19 cos:ℂ⟶ℂ
688231, 44sylan2 596 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
689 eqid 2738 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))
690688, 689fmptd 6882 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)):(𝐴(,)𝐵)⟶ℂ)
691 fcompt 6899 . . . . . . . . . . . . . . . . . . 19 ((cos:ℂ⟶ℂ ∧ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)):(𝐴(,)𝐵)⟶ℂ) → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
692687, 690, 691sylancr 590 . . . . . . . . . . . . . . . . . 18 (𝜑 → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
693 eqidd 2739 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
694316adantl 485 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
695 simpr 488 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → 𝑤 ∈ (𝐴(,)𝐵))
696693, 694, 695, 329fvmptd 6776 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
697696fveq2d 6672 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = (cos‘((𝑁 + (1 / 2)) · 𝑤)))
698697mpteq2dva 5122 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))))
699692, 698eqtr2d 2774 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))) = (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))))
700349, 41, 75constcncfg 42939 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
701349, 75idcncfg 42940 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 𝑦) ∈ ((𝐴(,)𝐵)–cn→ℂ))
702700, 701mulcncf 24191 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
703 coscn 25184 . . . . . . . . . . . . . . . . . . 19 cos ∈ (ℂ–cn→ℂ)
704703a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → cos ∈ (ℂ–cn→ℂ))
705702, 704cncfco 23652 . . . . . . . . . . . . . . . . 17 (𝜑 → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
706699, 705eqeltrd 2833 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
707686, 706mulcncf 24191 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
708 eqid 2738 . . . . . . . . . . . . . . . 16 (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2))))
709349, 155, 75constcncfg 42939 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ π) ∈ ((𝐴(,)𝐵)–cn→ℂ))
710 2cnd 11787 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ)
711134a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → 2 ≠ 0)
712328, 710, 711divrecd 11490 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 / 2) = (𝑤 · (1 / 2)))
713712mpteq2dva 5122 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 / 2)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 · (1 / 2))))
714 eqid 2738 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2))) = (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2)))
715 cncfmptid 23658 . . . . . . . . . . . . . . . . . . . . . . 23 ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ))
71674, 74, 715mp2an 692 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ)
717716a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ))
71874a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 / 2) ∈ ℂ → ℂ ⊆ ℂ)
719 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 / 2) ∈ ℂ → (1 / 2) ∈ ℂ)
720718, 719, 718constcncfg 42939 . . . . . . . . . . . . . . . . . . . . . 22 ((1 / 2) ∈ ℂ → (𝑤 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
72139, 720mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑤 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
722717, 721mulcncf 24191 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2))) ∈ (ℂ–cn→ℂ))
723712, 462eqeltrrd 2834 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 · (1 / 2)) ∈ ℂ)
724714, 722, 349, 75, 723cncfmptssg 42938 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 · (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
725713, 724eqeltrd 2833 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 / 2)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
726704, 725cncfmpt1f 23659 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑤 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
727709, 726mulcncf 24191 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
728 ssid 3897 . . . . . . . . . . . . . . . . 17 (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)
729728a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵))
730 difssd 4021 . . . . . . . . . . . . . . . 16 (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
731658adantl 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ∈ ℂ)
732119a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → π ∈ ℂ)
733657adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (cos‘(𝑤 / 2)) ∈ ℂ)
734238a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → π ≠ 0)
735595adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤 = 𝑌) → (cos‘(𝑤 / 2)) = (cos‘(𝑌 / 2)))
736633adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤 = 𝑌) → (cos‘(𝑌 / 2)) ≠ 0)
737735, 736eqnetrd 3001 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
738737adantlr 715 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
739738, 668pm2.61dan 813 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (cos‘(𝑤 / 2)) ≠ 0)
740732, 733, 734, 739mulne0d 11363 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ≠ 0)
741740neneqd 2939 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ¬ (π · (cos‘(𝑤 / 2))) = 0)
742 elsng 4527 . . . . . . . . . . . . . . . . . . 19 ((π · (cos‘(𝑤 / 2))) ∈ ℂ → ((π · (cos‘(𝑤 / 2))) ∈ {0} ↔ (π · (cos‘(𝑤 / 2))) = 0))
743731, 742syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ((π · (cos‘(𝑤 / 2))) ∈ {0} ↔ (π · (cos‘(𝑤 / 2))) = 0))
744741, 743mtbird 328 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ¬ (π · (cos‘(𝑤 / 2))) ∈ {0})
745731, 744eldifd 3852 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ∈ (ℂ ∖ {0}))
746708, 727, 729, 730, 745cncfmptssg 42938 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→(ℂ ∖ {0})))
747707, 746divcncf 24192 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
748747, 487eleqtrd 2835 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
749579, 748eqeltrd 2833 . . . . . . . . . . . 12 (𝜑𝐿 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
750 cncnp 22024 . . . . . . . . . . . . 13 ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → (𝐿 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))))
751355, 353, 750sylancl 589 . . . . . . . . . . . 12 (𝜑 → (𝐿 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))))
752749, 751mpbid 235 . . . . . . . . . . 11 (𝜑 → (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦)))
753752simprd 499 . . . . . . . . . 10 (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
754360eleq2d 2818 . . . . . . . . . . 11 (𝑦 = 𝑌 → (𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ↔ 𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌)))
755754rspccva 3523 . . . . . . . . . 10 ((∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → 𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
756753, 27, 755syl2anc 587 . . . . . . . . 9 (𝜑𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
757685, 756eqeltrd 2833 . . . . . . . 8 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
758307mpteq1d 5116 . . . . . . . 8 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))))
759757, 758, 5003eltr4d 2848 . . . . . . 7 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
760 eqid 2738 . . . . . . . 8 (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)))
761100fvmpt2 6780 . . . . . . . . . . . 12 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ) → (𝐻𝑦) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
762557, 106, 761syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐻𝑦) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
763762, 559oveq12d 7182 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐻𝑦) / (𝐼𝑦)) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) / (π · (cos‘(𝑦 / 2)))))
764106, 201, 563divcld 11487 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) / (π · (cos‘(𝑦 / 2)))) ∈ ℂ)
765763, 764eqeltrd 2833 . . . . . . . . 9 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐻𝑦) / (𝐼𝑦)) ∈ ℂ)
766 eqid 2738 . . . . . . . . 9 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))
767765, 766fmptd 6882 . . . . . . . 8 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
768371, 51, 760, 767, 374, 263ellimc 24617 . . . . . . 7 (𝜑 → ((((2 · 𝑁) + 1) / (2 · π)) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) lim 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌)))
769759, 768mpbird 260 . . . . . 6 (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) lim 𝑌))
770103eqcomd 2744 . . . . . . . . . 10 (𝜑𝐻 = (ℝ D 𝐹))
771770fveq1d 6670 . . . . . . . . 9 (𝜑 → (𝐻𝑦) = ((ℝ D 𝐹)‘𝑦))
772199eqcomd 2744 . . . . . . . . . 10 (𝜑𝐼 = (ℝ D 𝐺))
773772fveq1d 6670 . . . . . . . . 9 (𝜑 → (𝐼𝑦) = ((ℝ D 𝐺)‘𝑦))
774771, 773oveq12d 7182 . . . . . . . 8 (𝜑 → ((𝐻𝑦) / (𝐼𝑦)) = (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)))
775774mpteq2dv 5123 . . . . . . 7 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))))
776775oveq1d 7179 . . . . . 6 (𝜑 → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) lim 𝑌) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim 𝑌))
777769, 776eleqtrd 2835 . . . . 5 (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim 𝑌))
778577, 777eqeltrd 2833 . . . 4 (𝜑 → if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim 𝑌))
779576, 778eqeltrd 2833 . . 3 (𝜑 → ((𝐷𝑁)‘𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim 𝑌))
7804, 15, 24, 26, 27, 28, 110, 205, 431, 506, 556, 573, 779lhop 24760 . 2 (𝜑 → ((𝐷𝑁)‘𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹𝑦) / (𝐺𝑦))) lim 𝑌))
781574dirkerval 43158 . . . . . 6 (𝑁 ∈ ℕ → (𝐷𝑁) = (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
7825, 781syl 17 . . . . 5 (𝜑 → (𝐷𝑁) = (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
783782reseq1d 5818 . . . 4 (𝜑 → ((𝐷𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
7844resmptd 5876 . . . 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)))))))
785256iffalsed 4422 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
78613recnd 10740 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
78714fvmpt2 6780 . . . . . . . 8 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ) → (𝐹𝑦) = (sin‘((𝑁 + (1 / 2)) · 𝑦)))
788557, 786, 787syl2anc 587 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹𝑦) = (sin‘((𝑁 + (1 / 2)) · 𝑦)))
789557, 503, 525syl2anc 587 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐺𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
790788, 789oveq12d 7182 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐹𝑦) / (𝐺𝑦)) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
791785, 790eqtr4d 2776 . . . . 5 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((𝐹𝑦) / (𝐺𝑦)))
792791mpteq2dva 5122 . . . 4 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹𝑦) / (𝐺𝑦))))
793783, 784, 7923eqtrrd 2778 . . 3 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹𝑦) / (𝐺𝑦))) = ((𝐷𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
794793oveq1d 7179 . 2 (𝜑 → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹𝑦) / (𝐺𝑦))) lim 𝑌) = (((𝐷𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) lim 𝑌))
795780, 794eleqtrd 2835 1 (𝜑 → ((𝐷𝑁)‘𝑌) ∈ (((𝐷𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) lim 𝑌))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 846   = wceq 1542  wcel 2113  wne 2934  wral 3053  wrex 3054  cdif 3838  cun 3839  wss 3841  ifcif 4411  {csn 4513  {cpr 4515   class class class wbr 5027  cmpt 5107  dom cdm 5519  ran crn 5520  cres 5521  cima 5522  ccom 5523  Fun wfun 6327   Fn wfn 6328  wf 6329  cfv 6333  (class class class)co 7164  cc 10606  cr 10607  0cc0 10608  1c1 10609   + caddc 10611   · cmul 10613   < clt 10746   / cdiv 11368  cn 11709  2c2 11764  cz 12055  +crp 12465  (,)cioo 12814   mod cmo 13321  sincsin 15502  cosccos 15503  πcpi 15505  t crest 16790  TopOpenctopn 16791  topGenctg 16807  fldccnfld 20210  Topctop 21637  TopOnctopon 21654  Clsdccld 21760  intcnt 21761   Cn ccn 21968   CnP ccnp 21969  Hauscha 22052  cnccncf 23621   lim climc 24606   D cdv 24607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473  ax-inf2 9170  ax-cnex 10664  ax-resscn 10665  ax-1cn 10666  ax-icn 10667  ax-addcl 10668  ax-addrcl 10669  ax-mulcl 10670  ax-mulrcl 10671  ax-mulcom 10672  ax-addass 10673  ax-mulass 10674  ax-distr 10675  ax-i2m1 10676  ax-1ne0 10677  ax-1rid 10678  ax-rnegex 10679  ax-rrecex 10680  ax-cnre 10681  ax-pre-lttri 10682  ax-pre-lttrn 10683  ax-pre-ltadd 10684  ax-pre-mulgt0 10685  ax-pre-sup 10686  ax-addf 10687  ax-mulf 10688
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-int 4834  df-iun 4880  df-iin 4881  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-isom 6342  df-riota 7121  df-ov 7167  df-oprab 7168  df-mpo 7169  df-of 7419  df-om 7594  df-1st 7707  df-2nd 7708  df-supp 7850  df-wrecs 7969  df-recs 8030  df-rdg 8068  df-1o 8124  df-2o 8125  df-er 8313  df-map 8432  df-pm 8433  df-ixp 8501  df-en 8549  df-dom 8550  df-sdom 8551  df-fin 8552  df-fsupp 8900  df-fi 8941  df-sup 8972  df-inf 8973  df-oi 9040  df-card 9434  df-pnf 10748  df-mnf 10749  df-xr 10750  df-ltxr 10751  df-le 10752  df-sub 10943  df-neg 10944  df-div 11369  df-nn 11710  df-2 11772  df-3 11773  df-4 11774  df-5 11775  df-6 11776  df-7 11777  df-8 11778  df-9 11779  df-n0 11970  df-z 12056  df-dec 12173  df-uz 12318  df-q 12424  df-rp 12466  df-xneg 12583  df-xadd 12584  df-xmul 12585  df-ioo 12818  df-ioc 12819  df-ico 12820  df-icc 12821  df-fz 12975  df-fzo 13118  df-fl 13246  df-mod 13322  df-seq 13454  df-exp 13515  df-fac 13719  df-bc 13748  df-hash 13776  df-shft 14509  df-cj 14541  df-re 14542  df-im 14543  df-sqrt 14677  df-abs 14678  df-limsup 14911  df-clim 14928  df-rlim 14929  df-sum 15129  df-ef 15506  df-sin 15508  df-cos 15509  df-pi 15511  df-struct 16581  df-ndx 16582  df-slot 16583  df-base 16585  df-sets 16586  df-ress 16587  df-plusg 16674  df-mulr 16675  df-starv 16676  df-sca 16677  df-vsca 16678  df-ip 16679  df-tset 16680  df-ple 16681  df-ds 16683  df-unif 16684  df-hom 16685  df-cco 16686  df-rest 16792  df-topn 16793  df-0g 16811  df-gsum 16812  df-topgen 16813  df-pt 16814  df-prds 16817  df-xrs 16871  df-qtop 16876  df-imas 16877  df-xps 16879  df-mre 16953  df-mrc 16954  df-acs 16956  df-mgm 17961  df-sgrp 18010  df-mnd 18021  df-submnd 18066  df-mulg 18336  df-cntz 18558  df-cmn 19019  df-psmet 20202  df-xmet 20203  df-met 20204  df-bl 20205  df-mopn 20206  df-fbas 20207  df-fg 20208  df-cnfld 20211  df-top 21638  df-topon 21655  df-topsp 21677  df-bases 21690  df-cld 21763  df-ntr 21764  df-cls 21765  df-nei 21842  df-lp 21880  df-perf 21881  df-cn 21971  df-cnp 21972  df-t1 22058  df-haus 22059  df-cmp 22131  df-tx 22306  df-hmeo 22499  df-fil 22590  df-fm 22682  df-flim 22683  df-flf 22684  df-xms 23066  df-ms 23067  df-tms 23068  df-cncf 23623  df-limc 24610  df-dv 24611
This theorem is referenced by:  dirkercncflem3  43172
  Copyright terms: Public domain W3C validator