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 44593
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 4127 . . . . 5 ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ (𝐴(,)𝐵)
2 ioossre 13367 . . . . 5 (𝐴(,)𝐵) ⊆ ℝ
31, 2sstri 3987 . . . 4 ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ
43a1i 11 . . 3 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)
5 dirkercncflem2.n . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
65adantr 481 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℕ)
76nnred 12209 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℝ)
8 halfre 12408 . . . . . . . 8 (1 / 2) ∈ ℝ
98a1i 11 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈ ℝ)
107, 9readdcld 11225 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑁 + (1 / 2)) ∈ ℝ)
114sselda 3978 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℝ)
1210, 11remulcld 11226 . . . . 5 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℝ)
1312resincld 16068 . . . 4 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℝ)
14 dirkercncflem2.f . . . 4 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
1513, 14fmptd 7098 . . 3 (𝜑𝐹:((𝐴(,)𝐵) ∖ {𝑌})⟶ℝ)
16 2re 12268 . . . . . . 7 2 ∈ ℝ
17 pire 25897 . . . . . . 7 π ∈ ℝ
1816, 17remulcli 11212 . . . . . 6 (2 · π) ∈ ℝ
1918a1i 11 . . . . 5 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈ ℝ)
2011rehalfcld 12441 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℝ)
2120resincld 16068 . . . . 5 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ∈ ℝ)
2219, 21remulcld 11226 . . . 4 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℝ)
23 dirkercncflem2.g . . . 4 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
2422, 23fmptd 7098 . . 3 (𝜑𝐺:((𝐴(,)𝐵) ∖ {𝑌})⟶ℝ)
25 iooretop 24211 . . . 4 (𝐴(,)𝐵) ∈ (topGen‘ran (,))
2625a1i 11 . . 3 (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran (,)))
27 dirkercncflem2.y . . 3 (𝜑𝑌 ∈ (𝐴(,)𝐵))
28 eqid 2731 . . 3 ((𝐴(,)𝐵) ∖ {𝑌}) = ((𝐴(,)𝐵) ∖ {𝑌})
2914a1i 11 . . . . . . . 8 (𝜑𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
3029oveq2d 7409 . . . . . . 7 (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
31 resmpt 6027 . . . . . . . . . . . 12 (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
323, 31ax-mp 5 . . . . . . . . . . 11 ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
3332eqcomi 2740 . . . . . . . . . 10 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))
3433a1i 11 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
3534oveq2d 7409 . . . . . . . 8 (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))))
36 ax-resscn 11149 . . . . . . . . . 10 ℝ ⊆ ℂ
3736a1i 11 . . . . . . . . 9 (𝜑 → ℝ ⊆ ℂ)
385nncnd 12210 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℂ)
39 halfcn 12409 . . . . . . . . . . . . . . 15 (1 / 2) ∈ ℂ
4039a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (1 / 2) ∈ ℂ)
4138, 40addcld 11215 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ)
4241adantr 481 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (𝑁 + (1 / 2)) ∈ ℂ)
4337sselda 3978 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
4442, 43mulcld 11216 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
4544sincld 16055 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
46 eqid 2731 . . . . . . . . . 10 (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
4745, 46fmptd 7098 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℝ⟶ℂ)
48 ssid 4000 . . . . . . . . . . 11 ℝ ⊆ ℝ
4948, 3pm3.2i 471 . . . . . . . . . 10 (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)
5049a1i 11 . . . . . . . . 9 (𝜑 → (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ))
51 eqid 2731 . . . . . . . . . 10 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
5251tgioo2 24248 . . . . . . . . . 10 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
5351, 52dvres 25357 . . . . . . . . 9 (((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)) → (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
5437, 47, 50, 53syl21anc 836 . . . . . . . 8 (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
55 retop 24207 . . . . . . . . . . 11 (topGen‘ran (,)) ∈ Top
56 rehaus 24244 . . . . . . . . . . . . 13 (topGen‘ran (,)) ∈ Haus
5727elioored 44035 . . . . . . . . . . . . 13 (𝜑𝑌 ∈ ℝ)
58 uniretop 24208 . . . . . . . . . . . . . 14 ℝ = (topGen‘ran (,))
5958sncld 22804 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ Haus ∧ 𝑌 ∈ ℝ) → {𝑌} ∈ (Clsd‘(topGen‘ran (,))))
6056, 57, 59sylancr 587 . . . . . . . . . . . 12 (𝜑 → {𝑌} ∈ (Clsd‘(topGen‘ran (,))))
6158difopn 22467 . . . . . . . . . . . 12 (((𝐴(,)𝐵) ∈ (topGen‘ran (,)) ∧ {𝑌} ∈ (Clsd‘(topGen‘ran (,)))) → ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,)))
6225, 60, 61sylancr 587 . . . . . . . . . . 11 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,)))
63 isopn3i 22515 . . . . . . . . . . 11 (((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})) = ((𝐴(,)𝐵) ∖ {𝑌}))
6455, 62, 63sylancr 587 . . . . . . . . . 10 (𝜑 → ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})) = ((𝐴(,)𝐵) ∖ {𝑌}))
6564reseq2d 5973 . . . . . . . . 9 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
66 reelprrecn 11184 . . . . . . . . . . . . 13 ℝ ∈ {ℝ, ℂ}
6766a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ {ℝ, ℂ})
6841adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℂ) → (𝑁 + (1 / 2)) ∈ ℂ)
69 simpr 485 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
7068, 69mulcld 11216 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℂ) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
7170sincld 16055 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℂ) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
72 eqid 2731 . . . . . . . . . . . . 13 (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
7371, 72fmptd 7098 . . . . . . . . . . . 12 (𝜑 → (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℂ⟶ℂ)
74 ssid 4000 . . . . . . . . . . . . 13 ℂ ⊆ ℂ
7574a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ⊆ ℂ)
76 dvsinax 44402 . . . . . . . . . . . . . . . 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 5897 . . . . . . . . . . . . . 14 (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = dom (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
79 eqid 2731 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
8070coscld 16056 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ℂ) → (cos‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
8168, 80mulcld 11216 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℂ) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ)
8279, 81dmmptd 6682 . . . . . . . . . . . . . 14 (𝜑 → dom (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = ℂ)
8378, 82eqtrd 2771 . . . . . . . . . . . . 13 (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = ℂ)
8436, 83sseqtrrid 4031 . . . . . . . . . . . 12 (𝜑 → ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
85 dvres3 25359 . . . . . . . . . . . 12 (((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℂ⟶ℂ) ∧ (ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))) → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ))
8667, 73, 75, 84, 85syl22anc 837 . . . . . . . . . . 11 (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ))
87 resmpt 6027 . . . . . . . . . . . . 13 (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
8836, 87mp1i 13 . . . . . . . . . . . 12 (𝜑 → ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
8988oveq2d 7409 . . . . . . . . . . 11 (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
9077reseq1d 5972 . . . . . . . . . . . 12 (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = ((𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ))
91 resmpt 6027 . . . . . . . . . . . . 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 2787 . . . . . . . . . . 11 (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
9486, 89, 933eqtr3d 2779 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
9594reseq1d 5972 . . . . . . . . 9 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
96 resmpt 6027 . . . . . . . . . 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 2775 . . . . . . . 8 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
9935, 54, 983eqtrd 2775 . . . . . . 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 2737 . . . . . . 7 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = 𝐻)
10330, 99, 1023eqtrd 2775 . . . . . 6 (𝜑 → (ℝ D 𝐹) = 𝐻)
104103dmeqd 5897 . . . . 5 (𝜑 → dom (ℝ D 𝐹) = dom 𝐻)
10511recnd 11224 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℂ)
106105, 81syldan 591 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ)
107100, 106dmmptd 6682 . . . . 5 (𝜑 → dom 𝐻 = ((𝐴(,)𝐵) ∖ {𝑌}))
108104, 107eqtr2d 2772 . . . 4 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐹))
109 eqimss 4036 . . . 4 (((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐹) → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐹))
110108, 109syl 17 . . 3 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐹))
111 dirkercncflem2.i . . . . . . . 8 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2))))
112111a1i 11 . . . . . . 7 (𝜑𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
113 resmpt 6027 . . . . . . . . . . . . 13 (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))))
1143, 113ax-mp 5 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
115114eqcomi 2740 . . . . . . . . . . 11 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))
116115oveq2i 7404 . . . . . . . . . 10 (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
117116a1i 11 . . . . . . . . 9 (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))))
118 2cn 12269 . . . . . . . . . . . . . 14 2 ∈ ℂ
119 picn 25898 . . . . . . . . . . . . . 14 π ∈ ℂ
120118, 119mulcli 11203 . . . . . . . . . . . . 13 (2 · π) ∈ ℂ
121120a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (2 · π) ∈ ℂ)
12243halfcld 12439 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → (𝑦 / 2) ∈ ℂ)
123122sincld 16055 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (sin‘(𝑦 / 2)) ∈ ℂ)
124121, 123mulcld 11216 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
125 eqid 2731 . . . . . . . . . . 11 (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))
126124, 125fmptd 7098 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))):ℝ⟶ℂ)
12751, 52dvres 25357 . . . . . . . . . 10 (((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)) → (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
12837, 126, 50, 127syl21anc 836 . . . . . . . . 9 (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))))
12964reseq2d 5973 . . . . . . . . . 10 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
13036sseli 3974 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
131 1cnd 11191 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → 1 ∈ ℂ)
132 2cnd 12272 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → 2 ∈ ℂ)
133 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
134 2ne0 12298 . . . . . . . . . . . . . . . . . . . . . 22 2 ≠ 0
135134a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → 2 ≠ 0)
136131, 132, 133, 135div13d 11996 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℂ → ((1 / 2) · 𝑦) = ((𝑦 / 2) · 1))
137 halfcl 12419 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → (𝑦 / 2) ∈ ℂ)
138137mulridd 11213 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℂ → ((𝑦 / 2) · 1) = (𝑦 / 2))
139136, 138eqtrd 2771 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℂ → ((1 / 2) · 𝑦) = (𝑦 / 2))
140139fveq2d 6882 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℂ → (sin‘((1 / 2) · 𝑦)) = (sin‘(𝑦 / 2)))
141140oveq2d 7409 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℂ → ((2 · π) · (sin‘((1 / 2) · 𝑦))) = ((2 · π) · (sin‘(𝑦 / 2))))
142141eqcomd 2737 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℂ → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘((1 / 2) · 𝑦))))
143130, 142syl 17 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘((1 / 2) · 𝑦))))
144143adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘((1 / 2) · 𝑦))))
145144mpteq2dva 5241 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))))
146145oveq2d 7409 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))
147120a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ℂ) → (2 · π) ∈ ℂ)
14839a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ℂ) → (1 / 2) ∈ ℂ)
149148, 69mulcld 11216 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℂ) → ((1 / 2) · 𝑦) ∈ ℂ)
150149sincld 16055 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ℂ) → (sin‘((1 / 2) · 𝑦)) ∈ ℂ)
151147, 150mulcld 11216 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ℂ) → ((2 · π) · (sin‘((1 / 2) · 𝑦))) ∈ ℂ)
152 eqid 2731 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))
153151, 152fmptd 7098 . . . . . . . . . . . . . . 15 (𝜑 → (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))):ℂ⟶ℂ)
154 2cnd 12272 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ∈ ℂ)
155119a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → π ∈ ℂ)
156154, 155mulcld 11216 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2 · π) ∈ ℂ)
157 dvasinbx 44409 . . . . . . . . . . . . . . . . . . . 20 (((2 · π) ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦)))))
158156, 39, 157sylancl 586 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦)))))
159 2cnd 12272 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ ℂ) → 2 ∈ ℂ)
160119a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ ℂ) → π ∈ ℂ)
161159, 160, 148mul32d 11406 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ ℂ) → ((2 · π) · (1 / 2)) = ((2 · (1 / 2)) · π))
162134a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ ℂ) → 2 ≠ 0)
163159, 162recidd 11967 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ ℂ) → (2 · (1 / 2)) = 1)
164163oveq1d 7408 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ ℂ) → ((2 · (1 / 2)) · π) = (1 · π))
165160mullidd 11214 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ ℂ) → (1 · π) = π)
166161, 164, 1653eqtrd 2775 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ ℂ) → ((2 · π) · (1 / 2)) = π)
167139fveq2d 6882 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℂ → (cos‘((1 / 2) · 𝑦)) = (cos‘(𝑦 / 2)))
168167adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ ℂ) → (cos‘((1 / 2) · 𝑦)) = (cos‘(𝑦 / 2)))
169166, 168oveq12d 7411 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ ℂ) → (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦))) = (π · (cos‘(𝑦 / 2))))
170169mpteq2dva 5241 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ ℂ ↦ (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦)))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
171158, 170eqtrd 2771 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
172171dmeqd 5897 . . . . . . . . . . . . . . . . 17 (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = dom (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
173 eqid 2731 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2))))
17469halfcld 12439 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ ℂ) → (𝑦 / 2) ∈ ℂ)
175174coscld 16056 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ℂ) → (cos‘(𝑦 / 2)) ∈ ℂ)
176160, 175mulcld 11216 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℂ) → (π · (cos‘(𝑦 / 2))) ∈ ℂ)
177173, 176dmmptd 6682 . . . . . . . . . . . . . . . . 17 (𝜑 → dom (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) = ℂ)
178172, 177eqtrd 2771 . . . . . . . . . . . . . . . 16 (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = ℂ)
17936, 178sseqtrrid 4031 . . . . . . . . . . . . . . 15 (𝜑 → ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))
180 dvres3 25359 . . . . . . . . . . . . . . 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 837 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ))
182 resmpt 6027 . . . . . . . . . . . . . . . 16 (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))))
18336, 182mp1i 13 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))))
184183oveq2d 7409 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))
185171reseq1d 5972 . . . . . . . . . . . . . 14 (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ) = ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ))
186181, 184, 1853eqtr3d 2779 . . . . . . . . . . . . 13 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ))
187 resmpt 6027 . . . . . . . . . . . . . 14 (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
18836, 187ax-mp 5 . . . . . . . . . . . . 13 ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2))))
189186, 188eqtrdi 2787 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
190146, 189eqtrd 2771 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
191190reseq1d 5972 . . . . . . . . . 10 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
1924resmptd 6030 . . . . . . . . . 10 (𝜑 → ((𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
193129, 191, 1923eqtrd 2775 . . . . . . . . 9 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
194117, 128, 1933eqtrd 2775 . . . . . . . 8 (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
195194eqcomd 2737 . . . . . . 7 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))))
19623a1i 11 . . . . . . . . 9 (𝜑𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))))
197196oveq2d 7409 . . . . . . . 8 (𝜑 → (ℝ D 𝐺) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))))
198197eqcomd 2737 . . . . . . 7 (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D 𝐺))
199112, 195, 1983eqtrrd 2776 . . . . . 6 (𝜑 → (ℝ D 𝐺) = 𝐼)
200199dmeqd 5897 . . . . 5 (𝜑 → dom (ℝ D 𝐺) = dom 𝐼)
201105, 176syldan 591 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (π · (cos‘(𝑦 / 2))) ∈ ℂ)
202111, 201dmmptd 6682 . . . . 5 (𝜑 → dom 𝐼 = ((𝐴(,)𝐵) ∖ {𝑌}))
203200, 202eqtr2d 2772 . . . 4 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐺))
204 eqimss 4036 . . . 4 (((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐺) → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐺))
205203, 204syl 17 . . 3 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐺))
206105, 70syldan 591 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
207206ralrimiva 3145 . . . . . . 7 (𝜑 → ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
208 eqid 2731 . . . . . . . 8 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))
209208fnmpt 6677 . . . . . . 7 (∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}))
210207, 209syl 17 . . . . . 6 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}))
211 eqidd 2732 . . . . . . . . . 10 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
212 simpr 485 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
213212oveq2d 7409 . . . . . . . . . 10 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
214 simpr 485 . . . . . . . . . 10 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
21538adantr 481 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℂ)
216 1cnd 11191 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈ ℂ)
217216halfcld 12439 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈ ℂ)
218215, 217addcld 11215 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑁 + (1 / 2)) ∈ ℂ)
219 eldifi 4122 . . . . . . . . . . . . . 14 (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ (𝐴(,)𝐵))
220219elioored 44035 . . . . . . . . . . . . 13 (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ ℝ)
221220recnd 11224 . . . . . . . . . . . 12 (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ ℂ)
222221adantl 482 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑤 ∈ ℂ)
223218, 222mulcld 11216 . . . . . . . . . 10 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
224211, 213, 214, 223fvmptd 6991 . . . . . . . . 9 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
225 eleq1w 2815 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑤 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↔ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})))
226225anbi2d 629 . . . . . . . . . . . . . . 15 (𝑦 = 𝑤 → ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ↔ (𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))))
227 oveq1 7400 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑤 → (𝑦 mod (2 · π)) = (𝑤 mod (2 · π)))
228227neeq1d 2999 . . . . . . . . . . . . . . 15 (𝑦 = 𝑤 → ((𝑦 mod (2 · π)) ≠ 0 ↔ (𝑤 mod (2 · π)) ≠ 0))
229226, 228imbi12d 344 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 mod (2 · π)) ≠ 0) ↔ ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑤 mod (2 · π)) ≠ 0)))
230 eldifi 4122 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ (𝐴(,)𝐵))
231 elioore 13336 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝐴(,)𝐵) → 𝑦 ∈ ℝ)
232230, 231, 1303syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ ℂ)
233 2cnd 12272 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 2 ∈ ℂ)
234119a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → π ∈ ℂ)
235134a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 2 ≠ 0)
236 0re 11198 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℝ
237 pipos 25899 . . . . . . . . . . . . . . . . . . . . . 22 0 < π
238236, 237gtneii 11308 . . . . . . . . . . . . . . . . . . . . 21 π ≠ 0
239238a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → π ≠ 0)
240232, 233, 234, 235, 239divdiv1d 12003 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
241240eqcomd 2737 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
242241adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
243 dirkercncflem2.yne0 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ≠ 0)
244243neneqd 2944 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (sin‘(𝑦 / 2)) = 0)
245105halfcld 12439 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℂ)
246 sineq0 25962 . . . . . . . . . . . . . . . . . . 19 ((𝑦 / 2) ∈ ℂ → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
247245, 246syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
248244, 247mtbid 323 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / 2) / π) ∈ ℤ)
249242, 248eqneltrd 2852 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
250 2rp 12961 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ+
251 pirp 25900 . . . . . . . . . . . . . . . . . 18 π ∈ ℝ+
252 rpmulcl 12979 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℝ+ ∧ π ∈ ℝ+) → (2 · π) ∈ ℝ+)
253250, 251, 252mp2an 690 . . . . . . . . . . . . . . . . 17 (2 · π) ∈ ℝ+
254 mod0 13823 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℝ ∧ (2 · π) ∈ ℝ+) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
25511, 253, 254sylancl 586 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
256249, 255mtbird 324 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 mod (2 · π)) = 0)
257256neqned 2946 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 mod (2 · π)) ≠ 0)
258229, 257chvarvv 2002 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑤 mod (2 · π)) ≠ 0)
259258neneqd 2944 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑤 mod (2 · π)) = 0)
260 simpll 765 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝜑)
261 simpr 485 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))
262221ad2antlr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑤 ∈ ℂ)
26357recnd 11224 . . . . . . . . . . . . . . . 16 (𝜑𝑌 ∈ ℂ)
264263ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑌 ∈ ℂ)
265 0red 11199 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ∈ ℝ)
2665nnred 12209 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℝ)
267 1red 11197 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ∈ ℝ)
268267rehalfcld 12441 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 / 2) ∈ ℝ)
269266, 268readdcld 11225 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ)
2705nngt0d 12243 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 𝑁)
271250a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ∈ ℝ+)
272271rpreccld 13008 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 / 2) ∈ ℝ+)
273266, 272ltaddrpd 13031 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 < (𝑁 + (1 / 2)))
274265, 266, 269, 270, 273lttrd 11357 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 < (𝑁 + (1 / 2)))
275274gt0ne0d 11760 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 + (1 / 2)) ≠ 0)
27641, 275jca 512 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠ 0))
277276ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠ 0))
278 mulcan 11833 . . . . . . . . . . . . . . 15 ((𝑤 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠ 0)) → (((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌) ↔ 𝑤 = 𝑌))
279262, 264, 277, 278syl3anc 1371 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → (((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌) ↔ 𝑤 = 𝑌))
280261, 279mpbid 231 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑤 = 𝑌)
281 oveq1 7400 . . . . . . . . . . . . . 14 (𝑤 = 𝑌 → (𝑤 mod (2 · π)) = (𝑌 mod (2 · π)))
282 dirkercncflem2.ymod . . . . . . . . . . . . . 14 (𝜑 → (𝑌 mod (2 · π)) = 0)
283281, 282sylan9eqr 2793 . . . . . . . . . . . . 13 ((𝜑𝑤 = 𝑌) → (𝑤 mod (2 · π)) = 0)
284260, 280, 283syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → (𝑤 mod (2 · π)) = 0)
285259, 284mtand 814 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))
28641, 263mulcld 11216 . . . . . . . . . . . . 13 (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ)
287286adantr 481 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ)
288 elsn2g 4660 . . . . . . . . . . . 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 324 . . . . . . . . . 10 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑁 + (1 / 2)) · 𝑤) ∈ {((𝑁 + (1 / 2)) · 𝑌)})
291223, 290eldifd 3955 . . . . . . . . 9 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑤) ∈ (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
292224, 291eqeltrd 2832 . . . . . . . 8 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
293 sinf 16049 . . . . . . . . . . . 12 sin:ℂ⟶ℂ
294293fdmi 6716 . . . . . . . . . . 11 dom sin = ℂ
295294eqcomi 2740 . . . . . . . . . 10 ℂ = dom sin
296295a1i 11 . . . . . . . . 9 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ℂ = dom sin)
297296difeq1d 4117 . . . . . . . 8 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}) = (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
298292, 297eleqtrd 2834 . . . . . . 7 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
299298ralrimiva 3145 . . . . . 6 (𝜑 → ∀𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
300 fnfvrnss 7104 . . . . . 6 (((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ∀𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) → ran (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ⊆ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
301210, 299, 300syl2anc 584 . . . . 5 (𝜑 → ran (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ⊆ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
302 uncom 4149 . . . . . . . . . 10 (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌}))
303302a1i 11 . . . . . . . . 9 (𝜑 → (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})))
30427snssd 4805 . . . . . . . . . 10 (𝜑 → {𝑌} ⊆ (𝐴(,)𝐵))
305 undif 4477 . . . . . . . . . 10 ({𝑌} ⊆ (𝐴(,)𝐵) ↔ ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐴(,)𝐵))
306304, 305sylib 217 . . . . . . . . 9 (𝜑 → ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐴(,)𝐵))
307303, 306eqtrd 2771 . . . . . . . 8 (𝜑 → (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = (𝐴(,)𝐵))
308307mpteq1d 5236 . . . . . . 7 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
309 iftrue 4528 . . . . . . . . . . . . 13 (𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑌))
310 oveq2 7401 . . . . . . . . . . . . 13 (𝑤 = 𝑌 → ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))
311309, 310eqtr4d 2774 . . . . . . . . . . . 12 (𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
312311adantl 482 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
313 iffalse 4531 . . . . . . . . . . . . 13 𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))
314313adantl 482 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))
315 eqidd 2732 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
316 oveq2 7401 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
317316adantl 482 . . . . . . . . . . . . 13 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
318 simpl 483 . . . . . . . . . . . . . . 15 ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ (𝐴(,)𝐵))
319 id 22 . . . . . . . . . . . . . . . . 17 𝑤 = 𝑌 → ¬ 𝑤 = 𝑌)
320 velsn 4638 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ {𝑌} ↔ 𝑤 = 𝑌)
321319, 320sylnibr 328 . . . . . . . . . . . . . . . 16 𝑤 = 𝑌 → ¬ 𝑤 ∈ {𝑌})
322321adantl 482 . . . . . . . . . . . . . . 15 ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → ¬ 𝑤 ∈ {𝑌})
323318, 322eldifd 3955 . . . . . . . . . . . . . 14 ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
324323adantll 712 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
32541adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (𝑁 + (1 / 2)) ∈ ℂ)
326 elioore 13336 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (𝐴(,)𝐵) → 𝑤 ∈ ℝ)
327326recnd 11224 . . . . . . . . . . . . . . . 16 (𝑤 ∈ (𝐴(,)𝐵) → 𝑤 ∈ ℂ)
328327adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → 𝑤 ∈ ℂ)
329325, 328mulcld 11216 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
330329adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
331315, 317, 324, 330fvmptd 6991 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
332314, 331eqtrd 2771 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
333312, 332pm2.61dan 811 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
334333mpteq2dva 5241 . . . . . . . . 9 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)))
335 ioosscn 13368 . . . . . . . . . . . . . 14 (𝐴(,)𝐵) ⊆ ℂ
336 resmpt 6027 . . . . . . . . . . . . . 14 ((𝐴(,)𝐵) ⊆ ℂ → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)))
337335, 336ax-mp 5 . . . . . . . . . . . . 13 ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤))
338 eqid 2731 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) = (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤))
339338mulc1cncf 24350 . . . . . . . . . . . . . . . 16 ((𝑁 + (1 / 2)) ∈ ℂ → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (ℂ–cn→ℂ))
34041, 339syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (ℂ–cn→ℂ))
34151cnfldtop 24229 . . . . . . . . . . . . . . . . . . 19 (TopOpen‘ℂfld) ∈ Top
342 unicntop 24231 . . . . . . . . . . . . . . . . . . . 20 ℂ = (TopOpen‘ℂfld)
343342restid 17361 . . . . . . . . . . . . . . . . . . 19 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
344341, 343ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
345344eqcomi 2740 . . . . . . . . . . . . . . . . 17 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
34651, 345, 345cncfcn 24355 . . . . . . . . . . . . . . . 16 ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℂ) = ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
34774, 75, 346sylancr 587 . . . . . . . . . . . . . . 15 (𝜑 → (ℂ–cn→ℂ) = ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
348340, 347eleqtrd 2834 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
3492, 37sstrid 3989 . . . . . . . . . . . . . 14 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
350342cnrest 22718 . . . . . . . . . . . . . 14 (((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
351348, 349, 350syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
352337, 351eqeltrrid 2837 . . . . . . . . . . . 12 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
35351cnfldtopon 24228 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
354 resttopon 22594 . . . . . . . . . . . . . 14 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)))
355353, 349, 354sylancr 587 . . . . . . . . . . . . 13 (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)))
356 cncnp 22713 . . . . . . . . . . . . 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 586 . . . . . . . . . . . 12 (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ↔ ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))))
358352, 357mpbid 231 . . . . . . . . . . 11 (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦)))
359358simprd 496 . . . . . . . . . 10 (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
360 fveq2 6878 . . . . . . . . . . . 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 3608 . . . . . . . . . 10 ((∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
363359, 27, 362syl2anc 584 . . . . . . . . 9 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
364334, 363eqeltrd 2832 . . . . . . . 8 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
365307eqcomd 2737 . . . . . . . . . . 11 (𝜑 → (𝐴(,)𝐵) = (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}))
366365oveq2d 7409 . . . . . . . . . 10 (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})))
367366oveq1d 7408 . . . . . . . . 9 (𝜑 → (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld)))
368367fveq1d 6880 . . . . . . . 8 (𝜑 → ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌) = ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
369364, 368eleqtrd 2834 . . . . . . 7 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
370308, 369eqeltrd 2832 . . . . . 6 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
371 eqid 2731 . . . . . . 7 ((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) = ((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}))
372 eqid 2731 . . . . . . 7 (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))
373206, 208fmptd 7098 . . . . . . 7 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
3744, 36sstrdi 3990 . . . . . . 7 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℂ)
375371, 51, 372, 373, 374, 263ellimc 25319 . . . . . 6 (𝜑 → (((𝑁 + (1 / 2)) · 𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) lim 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌)))
376370, 375mpbird 256 . . . . 5 (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) lim 𝑌))
377134a1i 11 . . . . . . . . . . . 12 (𝜑 → 2 ≠ 0)
378238a1i 11 . . . . . . . . . . . 12 (𝜑 → π ≠ 0)
379154, 155, 377, 378mulne0d 11848 . . . . . . . . . . 11 (𝜑 → (2 · π) ≠ 0)
380263, 156, 379divcan1d 11973 . . . . . . . . . 10 (𝜑 → ((𝑌 / (2 · π)) · (2 · π)) = 𝑌)
381380eqcomd 2737 . . . . . . . . 9 (𝜑𝑌 = ((𝑌 / (2 · π)) · (2 · π)))
382381oveq2d 7409 . . . . . . . 8 (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))))
383382fveq2d 6882 . . . . . . 7 (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) = (sin‘((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π)))))
384263, 156, 379divcld 11972 . . . . . . . . . . 11 (𝜑 → (𝑌 / (2 · π)) ∈ ℂ)
38541, 384, 156mul12d 11405 . . . . . . . . . 10 (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = ((𝑌 / (2 · π)) · ((𝑁 + (1 / 2)) · (2 · π))))
38641, 154, 155mulassd 11219 . . . . . . . . . . . 12 (𝜑 → (((𝑁 + (1 / 2)) · 2) · π) = ((𝑁 + (1 / 2)) · (2 · π)))
387386eqcomd 2737 . . . . . . . . . . 11 (𝜑 → ((𝑁 + (1 / 2)) · (2 · π)) = (((𝑁 + (1 / 2)) · 2) · π))
388387oveq2d 7409 . . . . . . . . . 10 (𝜑 → ((𝑌 / (2 · π)) · ((𝑁 + (1 / 2)) · (2 · π))) = ((𝑌 / (2 · π)) · (((𝑁 + (1 / 2)) · 2) · π)))
38938, 40, 154adddird 11221 . . . . . . . . . . . . 13 (𝜑 → ((𝑁 + (1 / 2)) · 2) = ((𝑁 · 2) + ((1 / 2) · 2)))
390154, 377recid2d 11968 . . . . . . . . . . . . . 14 (𝜑 → ((1 / 2) · 2) = 1)
391390oveq2d 7409 . . . . . . . . . . . . 13 (𝜑 → ((𝑁 · 2) + ((1 / 2) · 2)) = ((𝑁 · 2) + 1))
392389, 391eqtrd 2771 . . . . . . . . . . . 12 (𝜑 → ((𝑁 + (1 / 2)) · 2) = ((𝑁 · 2) + 1))
393392oveq1d 7408 . . . . . . . . . . 11 (𝜑 → (((𝑁 + (1 / 2)) · 2) · π) = (((𝑁 · 2) + 1) · π))
394393oveq2d 7409 . . . . . . . . . 10 (𝜑 → ((𝑌 / (2 · π)) · (((𝑁 + (1 / 2)) · 2) · π)) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
395385, 388, 3943eqtrd 2775 . . . . . . . . 9 (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
39638, 154mulcld 11216 . . . . . . . . . . 11 (𝜑 → (𝑁 · 2) ∈ ℂ)
397 1cnd 11191 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
398396, 397addcld 11215 . . . . . . . . . 10 (𝜑 → ((𝑁 · 2) + 1) ∈ ℂ)
399384, 398, 155mulassd 11219 . . . . . . . . 9 (𝜑 → (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
400395, 399eqtr4d 2774 . . . . . . . 8 (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π))
401400fveq2d 6882 . . . . . . 7 (𝜑 → (sin‘((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π)))) = (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π)))
402 mod0 13823 . . . . . . . . . . 11 ((𝑌 ∈ ℝ ∧ (2 · π) ∈ ℝ+) → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
40357, 253, 402sylancl 586 . . . . . . . . . 10 (𝜑 → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
404282, 403mpbid 231 . . . . . . . . 9 (𝜑 → (𝑌 / (2 · π)) ∈ ℤ)
4055nnzd 12567 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℤ)
406 2z 12576 . . . . . . . . . . . 12 2 ∈ ℤ
407406a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℤ)
408405, 407zmulcld 12654 . . . . . . . . . 10 (𝜑 → (𝑁 · 2) ∈ ℤ)
409408peano2zd 12651 . . . . . . . . 9 (𝜑 → ((𝑁 · 2) + 1) ∈ ℤ)
410404, 409zmulcld 12654 . . . . . . . 8 (𝜑 → ((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ∈ ℤ)
411 sinkpi 25960 . . . . . . . 8 (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ∈ ℤ → (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π)) = 0)
412410, 411syl 17 . . . . . . 7 (𝜑 → (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π)) = 0)
413383, 401, 4123eqtrd 2775 . . . . . 6 (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) = 0)
414 sincn 25885 . . . . . . . 8 sin ∈ (ℂ–cn→ℂ)
415414a1i 11 . . . . . . 7 (𝜑 → sin ∈ (ℂ–cn→ℂ))
416415, 286cnlimci 25335 . . . . . 6 (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) ∈ (sin lim ((𝑁 + (1 / 2)) · 𝑌)))
417413, 416eqeltrrd 2833 . . . . 5 (𝜑 → 0 ∈ (sin lim ((𝑁 + (1 / 2)) · 𝑌)))
418301, 376, 417limccog 44109 . . . 4 (𝜑 → 0 ∈ ((sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) lim 𝑌))
41914a1i 11 . . . . . . . . 9 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
420213fveq2d 6882 . . . . . . . . 9 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
421223sincld 16055 . . . . . . . . 9 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑤)) ∈ ℂ)
422419, 420, 214, 421fvmptd 6991 . . . . . . . 8 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹𝑤) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
423224fveq2d 6882 . . . . . . . 8 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
424422, 423eqtr4d 2774 . . . . . . 7 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹𝑤) = (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))
425424mpteq2dva 5241 . . . . . 6 (𝜑 → (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (𝐹𝑤)) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
42615feqmptd 6946 . . . . . 6 (𝜑𝐹 = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (𝐹𝑤)))
427 fcompt 7115 . . . . . . 7 ((sin:ℂ⟶ℂ ∧ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
428293, 373, 427sylancr 587 . . . . . 6 (𝜑 → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
429425, 426, 4283eqtr4rd 2782 . . . . 5 (𝜑 → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = 𝐹)
430429oveq1d 7408 . . . 4 (𝜑 → ((sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) lim 𝑌) = (𝐹 lim 𝑌))
431418, 430eleqtrd 2834 . . 3 (𝜑 → 0 ∈ (𝐹 lim 𝑌))
432 simpr 485 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → 𝑤 = 𝑌)
433432iftrued 4530 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = 0)
434263, 154, 156, 377, 379divdiv32d 11997 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑌 / 2) / (2 · π)) = ((𝑌 / (2 · π)) / 2))
435434oveq1d 7408 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑌 / 2) / (2 · π)) · (2 · π)) = (((𝑌 / (2 · π)) / 2) · (2 · π)))
436263halfcld 12439 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑌 / 2) ∈ ℂ)
437436, 156, 379divcan1d 11973 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑌 / 2) / (2 · π)) · (2 · π)) = (𝑌 / 2))
438384, 154, 156, 377div32d 11995 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑌 / (2 · π)) / 2) · (2 · π)) = ((𝑌 / (2 · π)) · ((2 · π) / 2)))
439155, 154, 377divcan3d 11977 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2 · π) / 2) = π)
440439oveq2d 7409 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑌 / (2 · π)) · ((2 · π) / 2)) = ((𝑌 / (2 · π)) · π))
441438, 440eqtrd 2771 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑌 / (2 · π)) / 2) · (2 · π)) = ((𝑌 / (2 · π)) · π))
442435, 437, 4413eqtr3d 2779 . . . . . . . . . . . . . . 15 (𝜑 → (𝑌 / 2) = ((𝑌 / (2 · π)) · π))
443442fveq2d 6882 . . . . . . . . . . . . . 14 (𝜑 → (sin‘(𝑌 / 2)) = (sin‘((𝑌 / (2 · π)) · π)))
444 sinkpi 25960 . . . . . . . . . . . . . . 15 ((𝑌 / (2 · π)) ∈ ℤ → (sin‘((𝑌 / (2 · π)) · π)) = 0)
445404, 444syl 17 . . . . . . . . . . . . . 14 (𝜑 → (sin‘((𝑌 / (2 · π)) · π)) = 0)
446443, 445eqtrd 2771 . . . . . . . . . . . . 13 (𝜑 → (sin‘(𝑌 / 2)) = 0)
447446oveq2d 7409 . . . . . . . . . . . 12 (𝜑 → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · 0))
448156mul01d 11395 . . . . . . . . . . . 12 (𝜑 → ((2 · π) · 0) = 0)
449447, 448eqtrd 2771 . . . . . . . . . . 11 (𝜑 → ((2 · π) · (sin‘(𝑌 / 2))) = 0)
450449eqcomd 2737 . . . . . . . . . 10 (𝜑 → 0 = ((2 · π) · (sin‘(𝑌 / 2))))
451450ad2antrr 724 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → 0 = ((2 · π) · (sin‘(𝑌 / 2))))
452 fvoveq1 7416 . . . . . . . . . . . 12 (𝑤 = 𝑌 → (sin‘(𝑤 / 2)) = (sin‘(𝑌 / 2)))
453452oveq2d 7409 . . . . . . . . . . 11 (𝑤 = 𝑌 → ((2 · π) · (sin‘(𝑤 / 2))) = ((2 · π) · (sin‘(𝑌 / 2))))
454453eqcomd 2737 . . . . . . . . . 10 (𝑤 = 𝑌 → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
455454adantl 482 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
456433, 451, 4553eqtrd 2775 . . . . . . . 8 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
457 iffalse 4531 . . . . . . . . . 10 𝑤 = 𝑌 → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = (𝐺𝑤))
458457adantl 482 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = (𝐺𝑤))
459 fvoveq1 7416 . . . . . . . . . . 11 (𝑦 = 𝑤 → (sin‘(𝑦 / 2)) = (sin‘(𝑤 / 2)))
460459oveq2d 7409 . . . . . . . . . 10 (𝑦 = 𝑤 → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
461120a1i 11 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (2 · π) ∈ ℂ)
462328halfcld 12439 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 / 2) ∈ ℂ)
463462sincld 16055 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (sin‘(𝑤 / 2)) ∈ ℂ)
464461, 463mulcld 11216 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ((2 · π) · (sin‘(𝑤 / 2))) ∈ ℂ)
465464adantr 481 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((2 · π) · (sin‘(𝑤 / 2))) ∈ ℂ)
46623, 460, 324, 465fvmptd3 7007 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐺𝑤) = ((2 · π) · (sin‘(𝑤 / 2))))
467458, 466eqtrd 2771 . . . . . . . 8 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
468456, 467pm2.61dan 811 . . . . . . 7 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
469468mpteq2dva 5241 . . . . . 6 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))))
470 eqid 2731 . . . . . . . . . . 11 (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2)))) = (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2))))
47175, 156, 75constcncfg 44361 . . . . . . . . . . . 12 (𝜑 → (𝑤 ∈ ℂ ↦ (2 · π)) ∈ (ℂ–cn→ℂ))
472 id 22 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ → 𝑤 ∈ ℂ)
473 2cnd 12272 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ → 2 ∈ ℂ)
474134a1i 11 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ → 2 ≠ 0)
475472, 473, 474divrec2d 11976 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℂ → (𝑤 / 2) = ((1 / 2) · 𝑤))
476475mpteq2ia 5244 . . . . . . . . . . . . . . 15 (𝑤 ∈ ℂ ↦ (𝑤 / 2)) = (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤))
477 eqid 2731 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) = (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤))
478477mulc1cncf 24350 . . . . . . . . . . . . . . . 16 ((1 / 2) ∈ ℂ → (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) ∈ (ℂ–cn→ℂ))
47939, 478ax-mp 5 . . . . . . . . . . . . . . 15 (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) ∈ (ℂ–cn→ℂ)
480476, 479eqeltri 2828 . . . . . . . . . . . . . 14 (𝑤 ∈ ℂ ↦ (𝑤 / 2)) ∈ (ℂ–cn→ℂ)
481480a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ∈ ℂ ↦ (𝑤 / 2)) ∈ (ℂ–cn→ℂ))
482415, 481cncfmpt1f 24359 . . . . . . . . . . . 12 (𝜑 → (𝑤 ∈ ℂ ↦ (sin‘(𝑤 / 2))) ∈ (ℂ–cn→ℂ))
483471, 482mulcncf 24892 . . . . . . . . . . 11 (𝜑 → (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ (ℂ–cn→ℂ))
484470, 483, 349, 75, 464cncfmptssg 44360 . . . . . . . . . 10 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
485 eqid 2731 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
48651, 485, 345cncfcn 24355 . . . . . . . . . . 11 (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
487349, 74, 486sylancl 586 . . . . . . . . . 10 (𝜑 → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
488484, 487eleqtrd 2834 . . . . . . . . 9 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
489 cncnp 22713 . . . . . . . . . 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 586 . . . . . . . . 9 (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ↔ ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))))
491488, 490mpbid 231 . . . . . . . 8 (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦)))
492491simprd 496 . . . . . . 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 3608 . . . . . . 7 ((∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
495492, 27, 494syl2anc 584 . . . . . 6 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
496469, 495eqeltrd 2832 . . . . 5 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
497307mpteq1d 5236 . . . . 5 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))))
498366eqcomd 2737 . . . . . . 7 (𝜑 → ((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
499498oveq1d 7408 . . . . . 6 (𝜑 → (((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld)))
500499fveq1d 6880 . . . . 5 (𝜑 → ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌) = ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
501496, 497, 5003eltr4d 2847 . . . 4 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
502 eqid 2731 . . . . 5 (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤)))
50311, 124syldan 591 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
504503, 23fmptd 7098 . . . . 5 (𝜑𝐺:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
505371, 51, 502, 504, 374, 263ellimc 25319 . . . 4 (𝜑 → (0 ∈ (𝐺 lim 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌)))
506501, 505mpbird 256 . . 3 (𝜑 → 0 ∈ (𝐺 lim 𝑌))
507256nrexdv 3148 . . . 4 (𝜑 → ¬ ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0)
508504ffund 6708 . . . . . 6 (𝜑 → Fun 𝐺)
509 fvelima 6944 . . . . . 6 ((Fun 𝐺 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺𝑦) = 0)
510508, 509sylan 580 . . . . 5 ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺𝑦) = 0)
511 2cnd 12272 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ∈ ℂ)
512119a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ∈ ℂ)
513134a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ≠ 0)
514238a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ≠ 0)
515105, 511, 512, 513, 514divdiv1d 12003 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
516515eqcomd 2737 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
517516adantr 481 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
518 2cnd 12272 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → 2 ∈ ℂ)
519119a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → π ∈ ℂ)
520518, 519mulcld 11216 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (2 · π) ∈ ℂ)
521232adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → 𝑦 ∈ ℂ)
522521halfcld 12439 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (𝑦 / 2) ∈ ℂ)
523522sincld 16055 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (sin‘(𝑦 / 2)) ∈ ℂ)
524520, 523mulcld 11216 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
52523fvmpt2 6995 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ) → (𝐺𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
526524, 525syldan 591 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (𝐺𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
527526eqcomd 2737 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) = (𝐺𝑦))
528 simpr 485 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (𝐺𝑦) = 0)
529527, 528eqtrd 2771 . . . . . . . . . . . . . 14 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) = 0)
530120a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (2 · π) ∈ ℂ)
531232halfcld 12439 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (𝑦 / 2) ∈ ℂ)
532531sincld 16055 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (sin‘(𝑦 / 2)) ∈ ℂ)
533530, 532mul0ord 11846 . . . . . . . . . . . . . . 15 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (((2 · π) · (sin‘(𝑦 / 2))) = 0 ↔ ((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0)))
534533adantr 481 . . . . . . . . . . . . . 14 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (((2 · π) · (sin‘(𝑦 / 2))) = 0 ↔ ((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0)))
535529, 534mpbid 231 . . . . . . . . . . . . 13 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → ((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0))
536 2cnne0 12404 . . . . . . . . . . . . . . 15 (2 ∈ ℂ ∧ 2 ≠ 0)
537119, 238pm3.2i 471 . . . . . . . . . . . . . . 15 (π ∈ ℂ ∧ π ≠ 0)
538 mulne0 11838 . . . . . . . . . . . . . . 15 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → (2 · π) ≠ 0)
539536, 537, 538mp2an 690 . . . . . . . . . . . . . 14 (2 · π) ≠ 0
540539neii 2941 . . . . . . . . . . . . 13 ¬ (2 · π) = 0
541 pm2.53 849 . . . . . . . . . . . . 13 (((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0) → (¬ (2 · π) = 0 → (sin‘(𝑦 / 2)) = 0))
542535, 540, 541mpisyl 21 . . . . . . . . . . . 12 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (sin‘(𝑦 / 2)) = 0)
543542adantll 712 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → (sin‘(𝑦 / 2)) = 0)
544105adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → 𝑦 ∈ ℂ)
545544halfcld 12439 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → (𝑦 / 2) ∈ ℂ)
546545, 246syl 17 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
547543, 546mpbid 231 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → ((𝑦 / 2) / π) ∈ ℤ)
548517, 547eqeltrd 2832 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → (𝑦 / (2 · π)) ∈ ℤ)
54911adantr 481 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → 𝑦 ∈ ℝ)
550549, 253, 254sylancl 586 . . . . . . . . 9 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
551548, 550mpbird 256 . . . . . . . 8 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → (𝑦 mod (2 · π)) = 0)
552551ex 413 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐺𝑦) = 0 → (𝑦 mod (2 · π)) = 0))
553552reximdva 3167 . . . . . 6 (𝜑 → (∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺𝑦) = 0 → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0))
554553adantr 481 . . . . 5 ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → (∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺𝑦) = 0 → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0))
555510, 554mpd 15 . . . 4 ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0)
556507, 555mtand 814 . . 3 (𝜑 → ¬ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌})))
557 simpr 485 . . . . . . . . 9 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
558111fvmpt2 6995 . . . . . . . . 9 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (π · (cos‘(𝑦 / 2))) ∈ ℂ) → (𝐼𝑦) = (π · (cos‘(𝑦 / 2))))
559557, 201, 558syl2anc 584 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐼𝑦) = (π · (cos‘(𝑦 / 2))))
560531coscld 16056 . . . . . . . . . 10 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (cos‘(𝑦 / 2)) ∈ ℂ)
561560adantl 482 . . . . . . . . 9 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ∈ ℂ)
562 dirkercncflem2.11 . . . . . . . . 9 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0)
563512, 561, 514, 562mulne0d 11848 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (π · (cos‘(𝑦 / 2))) ≠ 0)
564559, 563eqnetrd 3007 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐼𝑦) ≠ 0)
565564neneqd 2944 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝐼𝑦) = 0)
566565nrexdv 3148 . . . . 5 (𝜑 → ¬ ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼𝑦) = 0)
567201, 111fmptd 7098 . . . . . . 7 (𝜑𝐼:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
568567ffund 6708 . . . . . 6 (𝜑 → Fun 𝐼)
569 fvelima 6944 . . . . . 6 ((Fun 𝐼 ∧ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼𝑦) = 0)
570568, 569sylan 580 . . . . 5 ((𝜑 ∧ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼𝑦) = 0)
571566, 570mtand 814 . . . 4 (𝜑 → ¬ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌})))
572199imaeq1d 6048 . . . 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 44583 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑌 ∈ ℝ) → ((𝐷𝑁)‘𝑌) = if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))))
5765, 57, 575syl2anc 584 . . . 4 (𝜑 → ((𝐷𝑁)‘𝑌) = if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))))
577282iftrued 4530 . . . . 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 4528 . . . . . . . . . . . . . 14 (𝑤 = 𝑌 → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)) = (((2 · 𝑁) + 1) / (2 · π)))
581580adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)) = (((2 · 𝑁) + 1) / (2 · π)))
582154, 38mulcld 11216 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2 · 𝑁) ∈ ℂ)
583582, 397addcld 11215 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2 · 𝑁) + 1) ∈ ℂ)
584583, 154, 155, 377, 378divdiv1d 12003 . . . . . . . . . . . . . . . 16 (𝜑 → ((((2 · 𝑁) + 1) / 2) / π) = (((2 · 𝑁) + 1) / (2 · π)))
585584eqcomd 2737 . . . . . . . . . . . . . . 15 (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) = ((((2 · 𝑁) + 1) / 2) / π))
586582, 397, 154, 377divdird 12010 . . . . . . . . . . . . . . . . 17 (𝜑 → (((2 · 𝑁) + 1) / 2) = (((2 · 𝑁) / 2) + (1 / 2)))
58738, 154, 377divcan3d 11977 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2 · 𝑁) / 2) = 𝑁)
588587oveq1d 7408 . . . . . . . . . . . . . . . . 17 (𝜑 → (((2 · 𝑁) / 2) + (1 / 2)) = (𝑁 + (1 / 2)))
589586, 588eqtrd 2771 . . . . . . . . . . . . . . . 16 (𝜑 → (((2 · 𝑁) + 1) / 2) = (𝑁 + (1 / 2)))
590589oveq1d 7408 . . . . . . . . . . . . . . 15 (𝜑 → ((((2 · 𝑁) + 1) / 2) / π) = ((𝑁 + (1 / 2)) / π))
591585, 590eqtrd 2771 . . . . . . . . . . . . . 14 (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) = ((𝑁 + (1 / 2)) / π))
592591ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((2 · 𝑁) + 1) / (2 · π)) = ((𝑁 + (1 / 2)) / π))
593310fveq2d 6882 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑌 → (cos‘((𝑁 + (1 / 2)) · 𝑤)) = (cos‘((𝑁 + (1 / 2)) · 𝑌)))
594593oveq2d 7409 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑌 → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))))
595 fvoveq1 7416 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑌 → (cos‘(𝑤 / 2)) = (cos‘(𝑌 / 2)))
596595oveq2d 7409 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑌 → (π · (cos‘(𝑤 / 2))) = (π · (cos‘(𝑌 / 2))))
597594, 596oveq12d 7411 . . . . . . . . . . . . . . 15 (𝑤 = 𝑌 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))))
598597adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))))
59938, 40, 263adddird 11221 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑁 · 𝑌) + ((1 / 2) · 𝑌)))
600397, 154, 263, 377div32d 11995 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((1 / 2) · 𝑌) = (1 · (𝑌 / 2)))
601436mullidd 11214 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 · (𝑌 / 2)) = (𝑌 / 2))
602600, 601eqtrd 2771 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1 / 2) · 𝑌) = (𝑌 / 2))
603602oveq2d 7409 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑁 · 𝑌) + ((1 / 2) · 𝑌)) = ((𝑁 · 𝑌) + (𝑌 / 2)))
60438, 263mulcld 11216 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑁 · 𝑌) ∈ ℂ)
605604, 436addcomd 11398 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑁 · 𝑌) + (𝑌 / 2)) = ((𝑌 / 2) + (𝑁 · 𝑌)))
606599, 603, 6053eqtrd 2775 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑌 / 2) + (𝑁 · 𝑌)))
607606fveq2d 6882 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (cos‘((𝑁 + (1 / 2)) · 𝑌)) = (cos‘((𝑌 / 2) + (𝑁 · 𝑌))))
608604, 156, 379divcan1d 11973 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑁 · 𝑌) / (2 · π)) · (2 · π)) = (𝑁 · 𝑌))
609608eqcomd 2737 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑁 · 𝑌) = (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))
610609oveq2d 7409 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑌 / 2) + (𝑁 · 𝑌)) = ((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π))))
611610fveq2d 6882 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (cos‘((𝑌 / 2) + (𝑁 · 𝑌))) = (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))))
61238, 263, 156, 379divassd 12007 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑁 · 𝑌) / (2 · π)) = (𝑁 · (𝑌 / (2 · π))))
613405, 404zmulcld 12654 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑁 · (𝑌 / (2 · π))) ∈ ℤ)
614612, 613eqeltrd 2832 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑁 · 𝑌) / (2 · π)) ∈ ℤ)
615 cosper 25921 . . . . . . . . . . . . . . . . . . . 20 (((𝑌 / 2) ∈ ℂ ∧ ((𝑁 · 𝑌) / (2 · π)) ∈ ℤ) → (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))) = (cos‘(𝑌 / 2)))
616436, 614, 615syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))) = (cos‘(𝑌 / 2)))
617607, 611, 6163eqtrd 2775 . . . . . . . . . . . . . . . . . 18 (𝜑 → (cos‘((𝑁 + (1 / 2)) · 𝑌)) = (cos‘(𝑌 / 2)))
618617oveq2d 7409 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) = ((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))))
619618oveq1d 7408 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = (((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))) / (π · (cos‘(𝑌 / 2)))))
620436coscld 16056 . . . . . . . . . . . . . . . . 17 (𝜑 → (cos‘(𝑌 / 2)) ∈ ℂ)
621263, 154, 155, 377, 378divdiv1d 12003 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑌 / 2) / π) = (𝑌 / (2 · π)))
622621, 404eqeltrd 2832 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑌 / 2) / π) ∈ ℤ)
623622zred 12648 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑌 / 2) / π) ∈ ℝ)
624623, 272ltaddrpd 13031 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑌 / 2) / π) < (((𝑌 / 2) / π) + (1 / 2)))
625 halflt1 12412 . . . . . . . . . . . . . . . . . . . . . 22 (1 / 2) < 1
626625a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (1 / 2) < 1)
627268, 267, 623, 626ltadd2dd 11355 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝑌 / 2) / π) + (1 / 2)) < (((𝑌 / 2) / π) + 1))
628 btwnnz 12620 . . . . . . . . . . . . . . . . . . . 20 ((((𝑌 / 2) / π) ∈ ℤ ∧ ((𝑌 / 2) / π) < (((𝑌 / 2) / π) + (1 / 2)) ∧ (((𝑌 / 2) / π) + (1 / 2)) < (((𝑌 / 2) / π) + 1)) → ¬ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ)
629622, 624, 627, 628syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ)
630 coseq0 44353 . . . . . . . . . . . . . . . . . . . 20 ((𝑌 / 2) ∈ ℂ → ((cos‘(𝑌 / 2)) = 0 ↔ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ))
631436, 630syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((cos‘(𝑌 / 2)) = 0 ↔ (((𝑌 / 2) / π) + (1 / 2)) ∈ ℤ))
632629, 631mtbird 324 . . . . . . . . . . . . . . . . . 18 (𝜑 → ¬ (cos‘(𝑌 / 2)) = 0)
633632neqned 2946 . . . . . . . . . . . . . . . . 17 (𝜑 → (cos‘(𝑌 / 2)) ≠ 0)
63441, 155, 620, 378, 633divcan5rd 11999 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
635619, 634eqtrd 2771 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
636635ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
637598, 636eqtr2d 2772 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) / π) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))))
638581, 592, 6373eqtrrd 2776 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)))
639 iffalse 4531 . . . . . . . . . . . . . 14 𝑤 = 𝑌 → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))
640639adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))
641 eqidd 2732 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))))
642 fveq2 6878 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑤 → (𝐻𝑦) = (𝐻𝑤))
643 fveq2 6878 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑤 → (𝐼𝑦) = (𝐼𝑤))
644642, 643oveq12d 7411 . . . . . . . . . . . . . . 15 (𝑦 = 𝑤 → ((𝐻𝑦) / (𝐼𝑦)) = ((𝐻𝑤) / (𝐼𝑤)))
645644adantl 482 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝐻𝑦) / (𝐼𝑦)) = ((𝐻𝑤) / (𝐼𝑤)))
646106, 100fmptd 7098 . . . . . . . . . . . . . . . . 17 (𝜑𝐻:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
647646ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐻:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
648647, 324ffvelcdmd 7072 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐻𝑤) ∈ ℂ)
649567ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐼:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
650649, 324ffvelcdmd 7072 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼𝑤) ∈ ℂ)
651111a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
652 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
653652fvoveq1d 7415 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (cos‘(𝑦 / 2)) = (cos‘(𝑤 / 2)))
654653oveq2d 7409 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (π · (cos‘(𝑦 / 2))) = (π · (cos‘(𝑤 / 2))))
655119a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (𝐴(,)𝐵) → π ∈ ℂ)
656327halfcld 12439 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝐴(,)𝐵) → (𝑤 / 2) ∈ ℂ)
657656coscld 16056 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (𝐴(,)𝐵) → (cos‘(𝑤 / 2)) ∈ ℂ)
658655, 657mulcld 11216 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (𝐴(,)𝐵) → (π · (cos‘(𝑤 / 2))) ∈ ℂ)
659658ad2antlr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π · (cos‘(𝑤 / 2))) ∈ ℂ)
660651, 654, 324, 659fvmptd 6991 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼𝑤) = (π · (cos‘(𝑤 / 2))))
661537a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π ∈ ℂ ∧ π ≠ 0))
662657ad2antlr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ∈ ℂ)
663 simpll 765 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝜑)
664 fvoveq1 7416 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑤 → (cos‘(𝑦 / 2)) = (cos‘(𝑤 / 2)))
665664neeq1d 2999 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑤 → ((cos‘(𝑦 / 2)) ≠ 0 ↔ (cos‘(𝑤 / 2)) ≠ 0))
666226, 665imbi12d 344 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑤 → (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0) ↔ ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑤 / 2)) ≠ 0)))
667666, 562chvarvv 2002 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑤 / 2)) ≠ 0)
668663, 324, 667syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
669 mulne0 11838 . . . . . . . . . . . . . . . . 17 (((π ∈ ℂ ∧ π ≠ 0) ∧ ((cos‘(𝑤 / 2)) ∈ ℂ ∧ (cos‘(𝑤 / 2)) ≠ 0)) → (π · (cos‘(𝑤 / 2))) ≠ 0)
670661, 662, 668, 669syl12anc 835 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π · (cos‘(𝑤 / 2))) ≠ 0)
671660, 670eqnetrd 3007 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼𝑤) ≠ 0)
672648, 650, 671divcld 11972 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝐻𝑤) / (𝐼𝑤)) ∈ ℂ)
673641, 645, 324, 672fvmptd 6991 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤) = ((𝐻𝑤) / (𝐼𝑤)))
674100a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
675317fveq2d 6882 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (cos‘((𝑁 + (1 / 2)) · 𝑦)) = (cos‘((𝑁 + (1 / 2)) · 𝑤)))
676675oveq2d 7409 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))))
677329coscld 16056 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (cos‘((𝑁 + (1 / 2)) · 𝑤)) ∈ ℂ)
678325, 677mulcld 11216 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ℂ)
679678adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ℂ)
680674, 676, 324, 679fvmptd 6991 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐻𝑤) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))))
681680, 660oveq12d 7411 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝐻𝑤) / (𝐼𝑤)) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))))
682640, 673, 6813eqtrrd 2776 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)))
683638, 682pm2.61dan 811 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)))
684683mpteq2dva 5241 . . . . . . . . . 10 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))))
685579, 684eqtr2d 2772 . . . . . . . . 9 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) = 𝐿)
686349, 41, 75constcncfg 44361 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
687 cosf 16050 . . . . . . . . . . . . . . . . . . 19 cos:ℂ⟶ℂ
688231, 44sylan2 593 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
689 eqid 2731 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))
690688, 689fmptd 7098 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)):(𝐴(,)𝐵)⟶ℂ)
691 fcompt 7115 . . . . . . . . . . . . . . . . . . 19 ((cos:ℂ⟶ℂ ∧ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)):(𝐴(,)𝐵)⟶ℂ) → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
692687, 690, 691sylancr 587 . . . . . . . . . . . . . . . . . 18 (𝜑 → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
693 eqidd 2732 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
694316adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
695 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → 𝑤 ∈ (𝐴(,)𝐵))
696693, 694, 695, 329fvmptd 6991 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
697696fveq2d 6882 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = (cos‘((𝑁 + (1 / 2)) · 𝑤)))
698697mpteq2dva 5241 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))))
699692, 698eqtr2d 2772 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))) = (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))))
700349, 41, 75constcncfg 44361 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
701349, 75idcncfg 44362 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 𝑦) ∈ ((𝐴(,)𝐵)–cn→ℂ))
702700, 701mulcncf 24892 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
703 coscn 25886 . . . . . . . . . . . . . . . . . . 19 cos ∈ (ℂ–cn→ℂ)
704703a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → cos ∈ (ℂ–cn→ℂ))
705702, 704cncfco 24352 . . . . . . . . . . . . . . . . 17 (𝜑 → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
706699, 705eqeltrd 2832 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
707686, 706mulcncf 24892 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
708 eqid 2731 . . . . . . . . . . . . . . . 16 (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2))))
709349, 155, 75constcncfg 44361 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ π) ∈ ((𝐴(,)𝐵)–cn→ℂ))
710 2cnd 12272 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ)
711134a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → 2 ≠ 0)
712328, 710, 711divrecd 11975 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 / 2) = (𝑤 · (1 / 2)))
713712mpteq2dva 5241 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 / 2)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 · (1 / 2))))
714 eqid 2731 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2))) = (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2)))
715 cncfmptid 24358 . . . . . . . . . . . . . . . . . . . . . . 23 ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ))
71674, 74, 715mp2an 690 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ)
717716a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ))
71874a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 / 2) ∈ ℂ → ℂ ⊆ ℂ)
719 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 / 2) ∈ ℂ → (1 / 2) ∈ ℂ)
720718, 719, 718constcncfg 44361 . . . . . . . . . . . . . . . . . . . . . 22 ((1 / 2) ∈ ℂ → (𝑤 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
72139, 720mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑤 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
722717, 721mulcncf 24892 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2))) ∈ (ℂ–cn→ℂ))
723712, 462eqeltrrd 2833 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 · (1 / 2)) ∈ ℂ)
724714, 722, 349, 75, 723cncfmptssg 44360 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 · (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
725713, 724eqeltrd 2832 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 / 2)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
726704, 725cncfmpt1f 24359 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑤 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
727709, 726mulcncf 24892 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
728 ssid 4000 . . . . . . . . . . . . . . . . 17 (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)
729728a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵))
730 difssd 4128 . . . . . . . . . . . . . . . 16 (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
731658adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ∈ ℂ)
732119a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → π ∈ ℂ)
733657adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (cos‘(𝑤 / 2)) ∈ ℂ)
734238a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → π ≠ 0)
735595adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤 = 𝑌) → (cos‘(𝑤 / 2)) = (cos‘(𝑌 / 2)))
736633adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤 = 𝑌) → (cos‘(𝑌 / 2)) ≠ 0)
737735, 736eqnetrd 3007 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
738737adantlr 713 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
739738, 668pm2.61dan 811 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (cos‘(𝑤 / 2)) ≠ 0)
740732, 733, 734, 739mulne0d 11848 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ≠ 0)
741740neneqd 2944 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ¬ (π · (cos‘(𝑤 / 2))) = 0)
742 elsng 4636 . . . . . . . . . . . . . . . . . . 19 ((π · (cos‘(𝑤 / 2))) ∈ ℂ → ((π · (cos‘(𝑤 / 2))) ∈ {0} ↔ (π · (cos‘(𝑤 / 2))) = 0))
743731, 742syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ((π · (cos‘(𝑤 / 2))) ∈ {0} ↔ (π · (cos‘(𝑤 / 2))) = 0))
744741, 743mtbird 324 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ¬ (π · (cos‘(𝑤 / 2))) ∈ {0})
745731, 744eldifd 3955 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ∈ (ℂ ∖ {0}))
746708, 727, 729, 730, 745cncfmptssg 44360 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→(ℂ ∖ {0})))
747707, 746divcncf 24893 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
748747, 487eleqtrd 2834 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
749579, 748eqeltrd 2832 . . . . . . . . . . . 12 (𝜑𝐿 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
750 cncnp 22713 . . . . . . . . . . . . 13 ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → (𝐿 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))))
751355, 353, 750sylancl 586 . . . . . . . . . . . 12 (𝜑 → (𝐿 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))))
752749, 751mpbid 231 . . . . . . . . . . 11 (𝜑 → (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦)))
753752simprd 496 . . . . . . . . . 10 (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦))
754360eleq2d 2818 . . . . . . . . . . 11 (𝑦 = 𝑌 → (𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ↔ 𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌)))
755754rspccva 3608 . . . . . . . . . 10 ((∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → 𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
756753, 27, 755syl2anc 584 . . . . . . . . 9 (𝜑𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
757685, 756eqeltrd 2832 . . . . . . . 8 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
758307mpteq1d 5236 . . . . . . . 8 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))))
759757, 758, 5003eltr4d 2847 . . . . . . 7 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
760 eqid 2731 . . . . . . . 8 (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)))
761100fvmpt2 6995 . . . . . . . . . . . 12 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ) → (𝐻𝑦) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
762557, 106, 761syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐻𝑦) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
763762, 559oveq12d 7411 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐻𝑦) / (𝐼𝑦)) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) / (π · (cos‘(𝑦 / 2)))))
764106, 201, 563divcld 11972 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) / (π · (cos‘(𝑦 / 2)))) ∈ ℂ)
765763, 764eqeltrd 2832 . . . . . . . . 9 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐻𝑦) / (𝐼𝑦)) ∈ ℂ)
766 eqid 2731 . . . . . . . . 9 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))
767765, 766fmptd 7098 . . . . . . . 8 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
768371, 51, 760, 767, 374, 263ellimc 25319 . . . . . . 7 (𝜑 → ((((2 · 𝑁) + 1) / (2 · π)) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) lim 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌)))
769759, 768mpbird 256 . . . . . 6 (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) lim 𝑌))
770103eqcomd 2737 . . . . . . . . . 10 (𝜑𝐻 = (ℝ D 𝐹))
771770fveq1d 6880 . . . . . . . . 9 (𝜑 → (𝐻𝑦) = ((ℝ D 𝐹)‘𝑦))
772199eqcomd 2737 . . . . . . . . . 10 (𝜑𝐼 = (ℝ D 𝐺))
773772fveq1d 6880 . . . . . . . . 9 (𝜑 → (𝐼𝑦) = ((ℝ D 𝐺)‘𝑦))
774771, 773oveq12d 7411 . . . . . . . 8 (𝜑 → ((𝐻𝑦) / (𝐼𝑦)) = (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)))
775774mpteq2dv 5243 . . . . . . 7 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))))
776775oveq1d 7408 . . . . . 6 (𝜑 → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) lim 𝑌) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim 𝑌))
777769, 776eleqtrd 2834 . . . . 5 (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim 𝑌))
778577, 777eqeltrd 2832 . . . 4 (𝜑 → if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim 𝑌))
779576, 778eqeltrd 2832 . . 3 (𝜑 → ((𝐷𝑁)‘𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim 𝑌))
7804, 15, 24, 26, 27, 28, 110, 205, 431, 506, 556, 573, 779lhop 25462 . 2 (𝜑 → ((𝐷𝑁)‘𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹𝑦) / (𝐺𝑦))) lim 𝑌))
781574dirkerval 44580 . . . . . 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 5972 . . . 4 (𝜑 → ((𝐷𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
7844resmptd 6030 . . . 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 4533 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
78613recnd 11224 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
78714fvmpt2 6995 . . . . . . . 8 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ) → (𝐹𝑦) = (sin‘((𝑁 + (1 / 2)) · 𝑦)))
788557, 786, 787syl2anc 584 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹𝑦) = (sin‘((𝑁 + (1 / 2)) · 𝑦)))
789557, 503, 525syl2anc 584 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐺𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
790788, 789oveq12d 7411 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐹𝑦) / (𝐺𝑦)) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
791785, 790eqtr4d 2774 . . . . 5 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((𝐹𝑦) / (𝐺𝑦)))
792791mpteq2dva 5241 . . . 4 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹𝑦) / (𝐺𝑦))))
793783, 784, 7923eqtrrd 2776 . . 3 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹𝑦) / (𝐺𝑦))) = ((𝐷𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
794793oveq1d 7408 . 2 (𝜑 → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹𝑦) / (𝐺𝑦))) lim 𝑌) = (((𝐷𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) lim 𝑌))
795780, 794eleqtrd 2834 1 (𝜑 → ((𝐷𝑁)‘𝑌) ∈ (((𝐷𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) lim 𝑌))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845   = wceq 1541  wcel 2106  wne 2939  wral 3060  wrex 3069  cdif 3941  cun 3942  wss 3944  ifcif 4522  {csn 4622  {cpr 4624   class class class wbr 5141  cmpt 5224  dom cdm 5669  ran crn 5670  cres 5671  cima 5672  ccom 5673  Fun wfun 6526   Fn wfn 6527  wf 6528  cfv 6532  (class class class)co 7393  cc 11090  cr 11091  0cc0 11092  1c1 11093   + caddc 11095   · cmul 11097   < clt 11230   / cdiv 11853  cn 12194  2c2 12249  cz 12540  +crp 12956  (,)cioo 13306   mod cmo 13816  sincsin 15989  cosccos 15990  πcpi 15992  t crest 17348  TopOpenctopn 17349  topGenctg 17365  fldccnfld 20878  Topctop 22324  TopOnctopon 22341  Clsdccld 22449  intcnt 22450   Cn ccn 22657   CnP ccnp 22658  Hauscha 22741  cnccncf 24321   lim climc 25308   D cdv 25309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-inf2 9618  ax-cnex 11148  ax-resscn 11149  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-addrcl 11153  ax-mulcl 11154  ax-mulrcl 11155  ax-mulcom 11156  ax-addass 11157  ax-mulass 11158  ax-distr 11159  ax-i2m1 11160  ax-1ne0 11161  ax-1rid 11162  ax-rnegex 11163  ax-rrecex 11164  ax-cnre 11165  ax-pre-lttri 11166  ax-pre-lttrn 11167  ax-pre-ltadd 11168  ax-pre-mulgt0 11169  ax-pre-sup 11170  ax-addf 11171  ax-mulf 11172
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-tp 4627  df-op 4629  df-uni 4902  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-isom 6541  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-of 7653  df-om 7839  df-1st 7957  df-2nd 7958  df-supp 8129  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-1o 8448  df-2o 8449  df-er 8686  df-map 8805  df-pm 8806  df-ixp 8875  df-en 8923  df-dom 8924  df-sdom 8925  df-fin 8926  df-fsupp 9345  df-fi 9388  df-sup 9419  df-inf 9420  df-oi 9487  df-card 9916  df-pnf 11232  df-mnf 11233  df-xr 11234  df-ltxr 11235  df-le 11236  df-sub 11428  df-neg 11429  df-div 11854  df-nn 12195  df-2 12257  df-3 12258  df-4 12259  df-5 12260  df-6 12261  df-7 12262  df-8 12263  df-9 12264  df-n0 12455  df-z 12541  df-dec 12660  df-uz 12805  df-q 12915  df-rp 12957  df-xneg 13074  df-xadd 13075  df-xmul 13076  df-ioo 13310  df-ioc 13311  df-ico 13312  df-icc 13313  df-fz 13467  df-fzo 13610  df-fl 13739  df-mod 13817  df-seq 13949  df-exp 14010  df-fac 14216  df-bc 14245  df-hash 14273  df-shft 14996  df-cj 15028  df-re 15029  df-im 15030  df-sqrt 15164  df-abs 15165  df-limsup 15397  df-clim 15414  df-rlim 15415  df-sum 15615  df-ef 15993  df-sin 15995  df-cos 15996  df-pi 15998  df-struct 17062  df-sets 17079  df-slot 17097  df-ndx 17109  df-base 17127  df-ress 17156  df-plusg 17192  df-mulr 17193  df-starv 17194  df-sca 17195  df-vsca 17196  df-ip 17197  df-tset 17198  df-ple 17199  df-ds 17201  df-unif 17202  df-hom 17203  df-cco 17204  df-rest 17350  df-topn 17351  df-0g 17369  df-gsum 17370  df-topgen 17371  df-pt 17372  df-prds 17375  df-xrs 17430  df-qtop 17435  df-imas 17436  df-xps 17438  df-mre 17512  df-mrc 17513  df-acs 17515  df-mgm 18543  df-sgrp 18592  df-mnd 18603  df-submnd 18648  df-mulg 18923  df-cntz 19147  df-cmn 19614  df-psmet 20870  df-xmet 20871  df-met 20872  df-bl 20873  df-mopn 20874  df-fbas 20875  df-fg 20876  df-cnfld 20879  df-top 22325  df-topon 22342  df-topsp 22364  df-bases 22378  df-cld 22452  df-ntr 22453  df-cls 22454  df-nei 22531  df-lp 22569  df-perf 22570  df-cn 22660  df-cnp 22661  df-t1 22747  df-haus 22748  df-cmp 22820  df-tx 22995  df-hmeo 23188  df-fil 23279  df-fm 23371  df-flim 23372  df-flf 23373  df-xms 23755  df-ms 23756  df-tms 23757  df-cncf 24323  df-limc 25312  df-dv 25313
This theorem is referenced by:  dirkercncflem3  44594
  Copyright terms: Public domain W3C validator