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 44335
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 4091 . . . . 5 ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ (𝐴(,)𝐵)
2 ioossre 13325 . . . . 5 (𝐴(,)𝐵) ⊆ ℝ
31, 2sstri 3953 . . . 4 ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ
43a1i 11 . . 3 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)
5 dirkercncflem2.n . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
65adantr 481 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℕ)
76nnred 12168 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℝ)
8 halfre 12367 . . . . . . . 8 (1 / 2) ∈ ℝ
98a1i 11 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈ ℝ)
107, 9readdcld 11184 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑁 + (1 / 2)) ∈ ℝ)
114sselda 3944 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℝ)
1210, 11remulcld 11185 . . . . 5 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℝ)
1312resincld 16025 . . . 4 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℝ)
14 dirkercncflem2.f . . . 4 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
1513, 14fmptd 7062 . . 3 (𝜑𝐹:((𝐴(,)𝐵) ∖ {𝑌})⟶ℝ)
16 2re 12227 . . . . . . 7 2 ∈ ℝ
17 pire 25815 . . . . . . 7 π ∈ ℝ
1816, 17remulcli 11171 . . . . . 6 (2 · π) ∈ ℝ
1918a1i 11 . . . . 5 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈ ℝ)
2011rehalfcld 12400 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℝ)
2120resincld 16025 . . . . 5 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ∈ ℝ)
2219, 21remulcld 11185 . . . 4 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℝ)
23 dirkercncflem2.g . . . 4 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
2422, 23fmptd 7062 . . 3 (𝜑𝐺:((𝐴(,)𝐵) ∖ {𝑌})⟶ℝ)
25 iooretop 24129 . . . 4 (𝐴(,)𝐵) ∈ (topGen‘ran (,))
2625a1i 11 . . 3 (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran (,)))
27 dirkercncflem2.y . . 3 (𝜑𝑌 ∈ (𝐴(,)𝐵))
28 eqid 2736 . . 3 ((𝐴(,)𝐵) ∖ {𝑌}) = ((𝐴(,)𝐵) ∖ {𝑌})
2914a1i 11 . . . . . . . 8 (𝜑𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
3029oveq2d 7373 . . . . . . 7 (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
31 resmpt 5991 . . . . . . . . . . . 12 (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
323, 31ax-mp 5 . . . . . . . . . . 11 ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
3332eqcomi 2745 . . . . . . . . . 10 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))
3433a1i 11 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
3534oveq2d 7373 . . . . . . . 8 (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))))
36 ax-resscn 11108 . . . . . . . . . 10 ℝ ⊆ ℂ
3736a1i 11 . . . . . . . . 9 (𝜑 → ℝ ⊆ ℂ)
385nncnd 12169 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℂ)
39 halfcn 12368 . . . . . . . . . . . . . . 15 (1 / 2) ∈ ℂ
4039a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (1 / 2) ∈ ℂ)
4138, 40addcld 11174 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ)
4241adantr 481 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (𝑁 + (1 / 2)) ∈ ℂ)
4337sselda 3944 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
4442, 43mulcld 11175 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
4544sincld 16012 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
46 eqid 2736 . . . . . . . . . 10 (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
4745, 46fmptd 7062 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℝ⟶ℂ)
48 ssid 3966 . . . . . . . . . . 11 ℝ ⊆ ℝ
4948, 3pm3.2i 471 . . . . . . . . . 10 (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)
5049a1i 11 . . . . . . . . 9 (𝜑 → (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ))
51 eqid 2736 . . . . . . . . . 10 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
5251tgioo2 24166 . . . . . . . . . 10 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
5351, 52dvres 25275 . . . . . . . . 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 24125 . . . . . . . . . . 11 (topGen‘ran (,)) ∈ Top
56 rehaus 24162 . . . . . . . . . . . . 13 (topGen‘ran (,)) ∈ Haus
5727elioored 43777 . . . . . . . . . . . . 13 (𝜑𝑌 ∈ ℝ)
58 uniretop 24126 . . . . . . . . . . . . . 14 ℝ = (topGen‘ran (,))
5958sncld 22722 . . . . . . . . . . . . 13 (((topGen‘ran (,)) ∈ Haus ∧ 𝑌 ∈ ℝ) → {𝑌} ∈ (Clsd‘(topGen‘ran (,))))
6056, 57, 59sylancr 587 . . . . . . . . . . . 12 (𝜑 → {𝑌} ∈ (Clsd‘(topGen‘ran (,))))
6158difopn 22385 . . . . . . . . . . . 12 (((𝐴(,)𝐵) ∈ (topGen‘ran (,)) ∧ {𝑌} ∈ (Clsd‘(topGen‘ran (,)))) → ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,)))
6225, 60, 61sylancr 587 . . . . . . . . . . 11 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,)))
63 isopn3i 22433 . . . . . . . . . . 11 (((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})) = ((𝐴(,)𝐵) ∖ {𝑌}))
6455, 62, 63sylancr 587 . . . . . . . . . 10 (𝜑 → ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})) = ((𝐴(,)𝐵) ∖ {𝑌}))
6564reseq2d 5937 . . . . . . . . 9 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
66 reelprrecn 11143 . . . . . . . . . . . . 13 ℝ ∈ {ℝ, ℂ}
6766a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ {ℝ, ℂ})
6841adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℂ) → (𝑁 + (1 / 2)) ∈ ℂ)
69 simpr 485 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
7068, 69mulcld 11175 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℂ) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
7170sincld 16012 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℂ) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
72 eqid 2736 . . . . . . . . . . . . 13 (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))
7371, 72fmptd 7062 . . . . . . . . . . . 12 (𝜑 → (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℂ⟶ℂ)
74 ssid 3966 . . . . . . . . . . . . 13 ℂ ⊆ ℂ
7574a1i 11 . . . . . . . . . . . 12 (𝜑 → ℂ ⊆ ℂ)
76 dvsinax 44144 . . . . . . . . . . . . . . . 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 5861 . . . . . . . . . . . . . 14 (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = dom (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
79 eqid 2736 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
8070coscld 16013 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ℂ) → (cos‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
8168, 80mulcld 11175 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℂ) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ)
8279, 81dmmptd 6646 . . . . . . . . . . . . . 14 (𝜑 → dom (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = ℂ)
8378, 82eqtrd 2776 . . . . . . . . . . . . 13 (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = ℂ)
8436, 83sseqtrrid 3997 . . . . . . . . . . . 12 (𝜑 → ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
85 dvres3 25277 . . . . . . . . . . . 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 5991 . . . . . . . . . . . . 13 (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
8836, 87mp1i 13 . . . . . . . . . . . 12 (𝜑 → ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
8988oveq2d 7373 . . . . . . . . . . 11 (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))))
9077reseq1d 5936 . . . . . . . . . . . 12 (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = ((𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ))
91 resmpt 5991 . . . . . . . . . . . . 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 2792 . . . . . . . . . . 11 (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
9486, 89, 933eqtr3d 2784 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
9594reseq1d 5936 . . . . . . . . 9 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
96 resmpt 5991 . . . . . . . . . 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 2780 . . . . . . . 8 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
9935, 54, 983eqtrd 2780 . . . . . . 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 2742 . . . . . . 7 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = 𝐻)
10330, 99, 1023eqtrd 2780 . . . . . 6 (𝜑 → (ℝ D 𝐹) = 𝐻)
104103dmeqd 5861 . . . . 5 (𝜑 → dom (ℝ D 𝐹) = dom 𝐻)
10511recnd 11183 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℂ)
106105, 81syldan 591 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ)
107100, 106dmmptd 6646 . . . . 5 (𝜑 → dom 𝐻 = ((𝐴(,)𝐵) ∖ {𝑌}))
108104, 107eqtr2d 2777 . . . 4 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐹))
109 eqimss 4000 . . . 4 (((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐹) → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐹))
110108, 109syl 17 . . 3 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐹))
111 dirkercncflem2.i . . . . . . . 8 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2))))
112111a1i 11 . . . . . . 7 (𝜑𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
113 resmpt 5991 . . . . . . . . . . . . 13 (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))))
1143, 113ax-mp 5 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))
115114eqcomi 2745 . . . . . . . . . . 11 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))
116115oveq2i 7368 . . . . . . . . . 10 (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
117116a1i 11 . . . . . . . . 9 (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D ((𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))))
118 2cn 12228 . . . . . . . . . . . . . 14 2 ∈ ℂ
119 picn 25816 . . . . . . . . . . . . . 14 π ∈ ℂ
120118, 119mulcli 11162 . . . . . . . . . . . . 13 (2 · π) ∈ ℂ
121120a1i 11 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (2 · π) ∈ ℂ)
12243halfcld 12398 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → (𝑦 / 2) ∈ ℂ)
123122sincld 16012 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (sin‘(𝑦 / 2)) ∈ ℂ)
124121, 123mulcld 11175 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
125 eqid 2736 . . . . . . . . . . 11 (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))
126124, 125fmptd 7062 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))):ℝ⟶ℂ)
12751, 52dvres 25275 . . . . . . . . . 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 5937 . . . . . . . . . 10 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
13036sseli 3940 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
131 1cnd 11150 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → 1 ∈ ℂ)
132 2cnd 12231 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → 2 ∈ ℂ)
133 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
134 2ne0 12257 . . . . . . . . . . . . . . . . . . . . . 22 2 ≠ 0
135134a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → 2 ≠ 0)
136131, 132, 133, 135div13d 11955 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℂ → ((1 / 2) · 𝑦) = ((𝑦 / 2) · 1))
137 halfcl 12378 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℂ → (𝑦 / 2) ∈ ℂ)
138137mulid1d 11172 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℂ → ((𝑦 / 2) · 1) = (𝑦 / 2))
139136, 138eqtrd 2776 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℂ → ((1 / 2) · 𝑦) = (𝑦 / 2))
140139fveq2d 6846 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℂ → (sin‘((1 / 2) · 𝑦)) = (sin‘(𝑦 / 2)))
141140oveq2d 7373 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℂ → ((2 · π) · (sin‘((1 / 2) · 𝑦))) = ((2 · π) · (sin‘(𝑦 / 2))))
142141eqcomd 2742 . . . . . . . . . . . . . . . 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 5205 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))))
146145oveq2d 7373 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))
147120a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ℂ) → (2 · π) ∈ ℂ)
14839a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ℂ) → (1 / 2) ∈ ℂ)
149148, 69mulcld 11175 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℂ) → ((1 / 2) · 𝑦) ∈ ℂ)
150149sincld 16012 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ℂ) → (sin‘((1 / 2) · 𝑦)) ∈ ℂ)
151147, 150mulcld 11175 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ℂ) → ((2 · π) · (sin‘((1 / 2) · 𝑦))) ∈ ℂ)
152 eqid 2736 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))
153151, 152fmptd 7062 . . . . . . . . . . . . . . 15 (𝜑 → (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))):ℂ⟶ℂ)
154 2cnd 12231 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ∈ ℂ)
155119a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → π ∈ ℂ)
156154, 155mulcld 11175 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2 · π) ∈ ℂ)
157 dvasinbx 44151 . . . . . . . . . . . . . . . . . . . 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 12231 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ ℂ) → 2 ∈ ℂ)
160119a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ ℂ) → π ∈ ℂ)
161159, 160, 148mul32d 11365 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ ℂ) → ((2 · π) · (1 / 2)) = ((2 · (1 / 2)) · π))
162134a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ ℂ) → 2 ≠ 0)
163159, 162recidd 11926 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ ℂ) → (2 · (1 / 2)) = 1)
164163oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ ℂ) → ((2 · (1 / 2)) · π) = (1 · π))
165160mulid2d 11173 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ ℂ) → (1 · π) = π)
166161, 164, 1653eqtrd 2780 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ ℂ) → ((2 · π) · (1 / 2)) = π)
167139fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℂ → (cos‘((1 / 2) · 𝑦)) = (cos‘(𝑦 / 2)))
168167adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ ℂ) → (cos‘((1 / 2) · 𝑦)) = (cos‘(𝑦 / 2)))
169166, 168oveq12d 7375 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ ℂ) → (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦))) = (π · (cos‘(𝑦 / 2))))
170169mpteq2dva 5205 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ ℂ ↦ (((2 · π) · (1 / 2)) · (cos‘((1 / 2) · 𝑦)))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
171158, 170eqtrd 2776 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
172171dmeqd 5861 . . . . . . . . . . . . . . . . 17 (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = dom (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))))
173 eqid 2736 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) = (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2))))
17469halfcld 12398 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ ℂ) → (𝑦 / 2) ∈ ℂ)
175174coscld 16013 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ℂ) → (cos‘(𝑦 / 2)) ∈ ℂ)
176160, 175mulcld 11175 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℂ) → (π · (cos‘(𝑦 / 2))) ∈ ℂ)
177173, 176dmmptd 6646 . . . . . . . . . . . . . . . . 17 (𝜑 → dom (𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) = ℂ)
178172, 177eqtrd 2776 . . . . . . . . . . . . . . . 16 (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = ℂ)
17936, 178sseqtrrid 3997 . . . . . . . . . . . . . . 15 (𝜑 → ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))
180 dvres3 25277 . . . . . . . . . . . . . . 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 5991 . . . . . . . . . . . . . . . 16 (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))))
18336, 182mp1i 13 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))))
184183oveq2d 7373 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))))
185171reseq1d 5936 . . . . . . . . . . . . . 14 (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ) = ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ))
186181, 184, 1853eqtr3d 2784 . . . . . . . . . . . . 13 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ))
187 resmpt 5991 . . . . . . . . . . . . . 14 (ℝ ⊆ ℂ → ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
18836, 187ax-mp 5 . . . . . . . . . . . . 13 ((𝑦 ∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2))))
189186, 188eqtrdi 2792 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
190146, 189eqtrd 2776 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))))
191190reseq1d 5936 . . . . . . . . . 10 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
1924resmptd 5994 . . . . . . . . . 10 (𝜑 → ((𝑦 ∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
193129, 191, 1923eqtrd 2780 . . . . . . . . 9 (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
194117, 128, 1933eqtrd 2780 . . . . . . . 8 (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
195194eqcomd 2742 . . . . . . 7 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))))
19623a1i 11 . . . . . . . . 9 (𝜑𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2)))))
197196oveq2d 7373 . . . . . . . 8 (𝜑 → (ℝ D 𝐺) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))))
198197eqcomd 2742 . . . . . . 7 (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))) = (ℝ D 𝐺))
199112, 195, 1983eqtrrd 2781 . . . . . 6 (𝜑 → (ℝ D 𝐺) = 𝐼)
200199dmeqd 5861 . . . . 5 (𝜑 → dom (ℝ D 𝐺) = dom 𝐼)
201105, 176syldan 591 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (π · (cos‘(𝑦 / 2))) ∈ ℂ)
202111, 201dmmptd 6646 . . . . 5 (𝜑 → dom 𝐼 = ((𝐴(,)𝐵) ∖ {𝑌}))
203200, 202eqtr2d 2777 . . . 4 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐺))
204 eqimss 4000 . . . 4 (((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐺) → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐺))
205203, 204syl 17 . . 3 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐺))
206105, 70syldan 591 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
207206ralrimiva 3143 . . . . . . 7 (𝜑 → ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
208 eqid 2736 . . . . . . . 8 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))
209208fnmpt 6641 . . . . . . 7 (∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}))
210207, 209syl 17 . . . . . 6 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}))
211 eqidd 2737 . . . . . . . . . 10 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
212 simpr 485 . . . . . . . . . . 11 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
213212oveq2d 7373 . . . . . . . . . 10 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
214 simpr 485 . . . . . . . . . 10 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
21538adantr 481 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℂ)
216 1cnd 11150 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈ ℂ)
217216halfcld 12398 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈ ℂ)
218215, 217addcld 11174 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑁 + (1 / 2)) ∈ ℂ)
219 eldifi 4086 . . . . . . . . . . . . . 14 (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ (𝐴(,)𝐵))
220219elioored 43777 . . . . . . . . . . . . 13 (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ ℝ)
221220recnd 11183 . . . . . . . . . . . 12 (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ ℂ)
222221adantl 482 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑤 ∈ ℂ)
223218, 222mulcld 11175 . . . . . . . . . 10 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
224211, 213, 214, 223fvmptd 6955 . . . . . . . . 9 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
225 eleq1w 2820 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑤 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↔ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})))
226225anbi2d 629 . . . . . . . . . . . . . . 15 (𝑦 = 𝑤 → ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ↔ (𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))))
227 oveq1 7364 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑤 → (𝑦 mod (2 · π)) = (𝑤 mod (2 · π)))
228227neeq1d 3003 . . . . . . . . . . . . . . 15 (𝑦 = 𝑤 → ((𝑦 mod (2 · π)) ≠ 0 ↔ (𝑤 mod (2 · π)) ≠ 0))
229226, 228imbi12d 344 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 mod (2 · π)) ≠ 0) ↔ ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑤 mod (2 · π)) ≠ 0)))
230 eldifi 4086 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ (𝐴(,)𝐵))
231 elioore 13294 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝐴(,)𝐵) → 𝑦 ∈ ℝ)
232230, 231, 1303syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ ℂ)
233 2cnd 12231 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 2 ∈ ℂ)
234119a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → π ∈ ℂ)
235134a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 2 ≠ 0)
236 0re 11157 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℝ
237 pipos 25817 . . . . . . . . . . . . . . . . . . . . . 22 0 < π
238236, 237gtneii 11267 . . . . . . . . . . . . . . . . . . . . 21 π ≠ 0
239238a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → π ≠ 0)
240232, 233, 234, 235, 239divdiv1d 11962 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
241240eqcomd 2742 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
242241adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
243 dirkercncflem2.yne0 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ≠ 0)
244243neneqd 2948 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (sin‘(𝑦 / 2)) = 0)
245105halfcld 12398 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℂ)
246 sineq0 25880 . . . . . . . . . . . . . . . . . . 19 ((𝑦 / 2) ∈ ℂ → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
247245, 246syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
248244, 247mtbid 323 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / 2) / π) ∈ ℤ)
249242, 248eqneltrd 2857 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 / (2 · π)) ∈ ℤ)
250 2rp 12920 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ+
251 pirp 25818 . . . . . . . . . . . . . . . . . 18 π ∈ ℝ+
252 rpmulcl 12938 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℝ+ ∧ π ∈ ℝ+) → (2 · π) ∈ ℝ+)
253250, 251, 252mp2an 690 . . . . . . . . . . . . . . . . 17 (2 · π) ∈ ℝ+
254 mod0 13781 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℝ ∧ (2 · π) ∈ ℝ+) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
25511, 253, 254sylancl 586 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈ ℤ))
256249, 255mtbird 324 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 mod (2 · π)) = 0)
257256neqned 2950 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 mod (2 · π)) ≠ 0)
258229, 257chvarvv 2002 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑤 mod (2 · π)) ≠ 0)
259258neneqd 2948 . . . . . . . . . . . 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 11183 . . . . . . . . . . . . . . . 16 (𝜑𝑌 ∈ ℂ)
264263ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑌 ∈ ℂ)
265 0red 11158 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ∈ ℝ)
2665nnred 12168 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℝ)
267 1red 11156 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ∈ ℝ)
268267rehalfcld 12400 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 / 2) ∈ ℝ)
269266, 268readdcld 11184 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ)
2705nngt0d 12202 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 𝑁)
271250a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ∈ ℝ+)
272271rpreccld 12967 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 / 2) ∈ ℝ+)
273266, 272ltaddrpd 12990 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 < (𝑁 + (1 / 2)))
274265, 266, 269, 270, 273lttrd 11316 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 < (𝑁 + (1 / 2)))
275274gt0ne0d 11719 . . . . . . . . . . . . . . . . 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 11792 . . . . . . . . . . . . . . 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 7364 . . . . . . . . . . . . . 14 (𝑤 = 𝑌 → (𝑤 mod (2 · π)) = (𝑌 mod (2 · π)))
282 dirkercncflem2.ymod . . . . . . . . . . . . . 14 (𝜑 → (𝑌 mod (2 · π)) = 0)
283281, 282sylan9eqr 2798 . . . . . . . . . . . . 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 11175 . . . . . . . . . . . . 13 (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ)
287286adantr 481 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ)
288 elsn2g 4624 . . . . . . . . . . . 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 3921 . . . . . . . . 9 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑤) ∈ (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
292224, 291eqeltrd 2838 . . . . . . . 8 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
293 sinf 16006 . . . . . . . . . . . 12 sin:ℂ⟶ℂ
294293fdmi 6680 . . . . . . . . . . 11 dom sin = ℂ
295294eqcomi 2745 . . . . . . . . . 10 ℂ = dom sin
296295a1i 11 . . . . . . . . 9 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ℂ = dom sin)
297296difeq1d 4081 . . . . . . . 8 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}) = (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
298292, 297eleqtrd 2840 . . . . . . 7 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
299298ralrimiva 3143 . . . . . 6 (𝜑 → ∀𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)}))
300 fnfvrnss 7068 . . . . . 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 4113 . . . . . . . . . 10 (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌}))
303302a1i 11 . . . . . . . . 9 (𝜑 → (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})))
30427snssd 4769 . . . . . . . . . 10 (𝜑 → {𝑌} ⊆ (𝐴(,)𝐵))
305 undif 4441 . . . . . . . . . 10 ({𝑌} ⊆ (𝐴(,)𝐵) ↔ ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐴(,)𝐵))
306304, 305sylib 217 . . . . . . . . 9 (𝜑 → ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐴(,)𝐵))
307303, 306eqtrd 2776 . . . . . . . 8 (𝜑 → (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = (𝐴(,)𝐵))
308307mpteq1d 5200 . . . . . . 7 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
309 iftrue 4492 . . . . . . . . . . . . 13 (𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑌))
310 oveq2 7365 . . . . . . . . . . . . 13 (𝑤 = 𝑌 → ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))
311309, 310eqtr4d 2779 . . . . . . . . . . . 12 (𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
312311adantl 482 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
313 iffalse 4495 . . . . . . . . . . . . 13 𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))
314313adantl 482 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))
315 eqidd 2737 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
316 oveq2 7365 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
317316adantl 482 . . . . . . . . . . . . 13 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
318 simpl 483 . . . . . . . . . . . . . . 15 ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ (𝐴(,)𝐵))
319 id 22 . . . . . . . . . . . . . . . . 17 𝑤 = 𝑌 → ¬ 𝑤 = 𝑌)
320 velsn 4602 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ {𝑌} ↔ 𝑤 = 𝑌)
321319, 320sylnibr 328 . . . . . . . . . . . . . . . 16 𝑤 = 𝑌 → ¬ 𝑤 ∈ {𝑌})
322321adantl 482 . . . . . . . . . . . . . . 15 ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → ¬ 𝑤 ∈ {𝑌})
323318, 322eldifd 3921 . . . . . . . . . . . . . 14 ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
324323adantll 712 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))
32541adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (𝑁 + (1 / 2)) ∈ ℂ)
326 elioore 13294 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ (𝐴(,)𝐵) → 𝑤 ∈ ℝ)
327326recnd 11183 . . . . . . . . . . . . . . . 16 (𝑤 ∈ (𝐴(,)𝐵) → 𝑤 ∈ ℂ)
328327adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → 𝑤 ∈ ℂ)
329325, 328mulcld 11175 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
330329adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ)
331315, 317, 324, 330fvmptd 6955 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
332314, 331eqtrd 2776 . . . . . . . . . . 11 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
333312, 332pm2.61dan 811 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤))
334333mpteq2dva 5205 . . . . . . . . 9 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)))
335 ioosscn 13326 . . . . . . . . . . . . . 14 (𝐴(,)𝐵) ⊆ ℂ
336 resmpt 5991 . . . . . . . . . . . . . 14 ((𝐴(,)𝐵) ⊆ ℂ → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)))
337335, 336ax-mp 5 . . . . . . . . . . . . 13 ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤))
338 eqid 2736 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) = (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤))
339338mulc1cncf 24268 . . . . . . . . . . . . . . . 16 ((𝑁 + (1 / 2)) ∈ ℂ → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (ℂ–cn→ℂ))
34041, 339syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (ℂ–cn→ℂ))
34151cnfldtop 24147 . . . . . . . . . . . . . . . . . . 19 (TopOpen‘ℂfld) ∈ Top
342 unicntop 24149 . . . . . . . . . . . . . . . . . . . 20 ℂ = (TopOpen‘ℂfld)
343342restid 17315 . . . . . . . . . . . . . . . . . . 19 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
344341, 343ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
345344eqcomi 2745 . . . . . . . . . . . . . . . . 17 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
34651, 345, 345cncfcn 24273 . . . . . . . . . . . . . . . 16 ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℂ) = ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
34774, 75, 346sylancr 587 . . . . . . . . . . . . . . 15 (𝜑 → (ℂ–cn→ℂ) = ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
348340, 347eleqtrd 2840 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)))
3492, 37sstrid 3955 . . . . . . . . . . . . . 14 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
350342cnrest 22636 . . . . . . . . . . . . . 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 2843 . . . . . . . . . . . 12 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
35351cnfldtopon 24146 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
354 resttopon 22512 . . . . . . . . . . . . . 14 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)))
355353, 349, 354sylancr 587 . . . . . . . . . . . . 13 (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)))
356 cncnp 22631 . . . . . . . . . . . . 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 6842 . . . . . . . . . . . 12 (𝑦 = 𝑌 → ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
361360eleq2d 2823 . . . . . . . . . . 11 (𝑦 = 𝑌 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌)))
362361rspccva 3580 . . . . . . . . . 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 2838 . . . . . . . 8 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
365307eqcomd 2742 . . . . . . . . . . 11 (𝜑 → (𝐴(,)𝐵) = (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}))
366365oveq2d 7373 . . . . . . . . . 10 (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})))
367366oveq1d 7372 . . . . . . . . 9 (𝜑 → (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld)))
368367fveq1d 6844 . . . . . . . 8 (𝜑 → ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌) = ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
369364, 368eleqtrd 2840 . . . . . . 7 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
370308, 369eqeltrd 2838 . . . . . 6 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
371 eqid 2736 . . . . . . 7 ((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) = ((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}))
372 eqid 2736 . . . . . . 7 (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))
373206, 208fmptd 7062 . . . . . . 7 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
3744, 36sstrdi 3956 . . . . . . 7 (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℂ)
375371, 51, 372, 373, 374, 263ellimc 25237 . . . . . 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 11807 . . . . . . . . . . 11 (𝜑 → (2 · π) ≠ 0)
380263, 156, 379divcan1d 11932 . . . . . . . . . 10 (𝜑 → ((𝑌 / (2 · π)) · (2 · π)) = 𝑌)
381380eqcomd 2742 . . . . . . . . 9 (𝜑𝑌 = ((𝑌 / (2 · π)) · (2 · π)))
382381oveq2d 7373 . . . . . . . 8 (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))))
383382fveq2d 6846 . . . . . . 7 (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) = (sin‘((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π)))))
384263, 156, 379divcld 11931 . . . . . . . . . . 11 (𝜑 → (𝑌 / (2 · π)) ∈ ℂ)
38541, 384, 156mul12d 11364 . . . . . . . . . 10 (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = ((𝑌 / (2 · π)) · ((𝑁 + (1 / 2)) · (2 · π))))
38641, 154, 155mulassd 11178 . . . . . . . . . . . 12 (𝜑 → (((𝑁 + (1 / 2)) · 2) · π) = ((𝑁 + (1 / 2)) · (2 · π)))
387386eqcomd 2742 . . . . . . . . . . 11 (𝜑 → ((𝑁 + (1 / 2)) · (2 · π)) = (((𝑁 + (1 / 2)) · 2) · π))
388387oveq2d 7373 . . . . . . . . . 10 (𝜑 → ((𝑌 / (2 · π)) · ((𝑁 + (1 / 2)) · (2 · π))) = ((𝑌 / (2 · π)) · (((𝑁 + (1 / 2)) · 2) · π)))
38938, 40, 154adddird 11180 . . . . . . . . . . . . 13 (𝜑 → ((𝑁 + (1 / 2)) · 2) = ((𝑁 · 2) + ((1 / 2) · 2)))
390154, 377recid2d 11927 . . . . . . . . . . . . . 14 (𝜑 → ((1 / 2) · 2) = 1)
391390oveq2d 7373 . . . . . . . . . . . . 13 (𝜑 → ((𝑁 · 2) + ((1 / 2) · 2)) = ((𝑁 · 2) + 1))
392389, 391eqtrd 2776 . . . . . . . . . . . 12 (𝜑 → ((𝑁 + (1 / 2)) · 2) = ((𝑁 · 2) + 1))
393392oveq1d 7372 . . . . . . . . . . 11 (𝜑 → (((𝑁 + (1 / 2)) · 2) · π) = (((𝑁 · 2) + 1) · π))
394393oveq2d 7373 . . . . . . . . . 10 (𝜑 → ((𝑌 / (2 · π)) · (((𝑁 + (1 / 2)) · 2) · π)) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
395385, 388, 3943eqtrd 2780 . . . . . . . . 9 (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
39638, 154mulcld 11175 . . . . . . . . . . 11 (𝜑 → (𝑁 · 2) ∈ ℂ)
397 1cnd 11150 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
398396, 397addcld 11174 . . . . . . . . . 10 (𝜑 → ((𝑁 · 2) + 1) ∈ ℂ)
399384, 398, 155mulassd 11178 . . . . . . . . 9 (𝜑 → (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π) = ((𝑌 / (2 · π)) · (((𝑁 · 2) + 1) · π)))
400395, 399eqtr4d 2779 . . . . . . . 8 (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π))) = (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π))
401400fveq2d 6846 . . . . . . 7 (𝜑 → (sin‘((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 · π)))) = (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π)))
402 mod0 13781 . . . . . . . . . . 11 ((𝑌 ∈ ℝ ∧ (2 · π) ∈ ℝ+) → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
40357, 253, 402sylancl 586 . . . . . . . . . 10 (𝜑 → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈ ℤ))
404282, 403mpbid 231 . . . . . . . . 9 (𝜑 → (𝑌 / (2 · π)) ∈ ℤ)
4055nnzd 12526 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℤ)
406 2z 12535 . . . . . . . . . . . 12 2 ∈ ℤ
407406a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℤ)
408405, 407zmulcld 12613 . . . . . . . . . 10 (𝜑 → (𝑁 · 2) ∈ ℤ)
409408peano2zd 12610 . . . . . . . . 9 (𝜑 → ((𝑁 · 2) + 1) ∈ ℤ)
410404, 409zmulcld 12613 . . . . . . . 8 (𝜑 → ((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ∈ ℤ)
411 sinkpi 25878 . . . . . . . 8 (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ∈ ℤ → (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π)) = 0)
412410, 411syl 17 . . . . . . 7 (𝜑 → (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) · π)) = 0)
413383, 401, 4123eqtrd 2780 . . . . . 6 (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) = 0)
414 sincn 25803 . . . . . . . 8 sin ∈ (ℂ–cn→ℂ)
415414a1i 11 . . . . . . 7 (𝜑 → sin ∈ (ℂ–cn→ℂ))
416415, 286cnlimci 25253 . . . . . 6 (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) ∈ (sin lim ((𝑁 + (1 / 2)) · 𝑌)))
417413, 416eqeltrrd 2839 . . . . 5 (𝜑 → 0 ∈ (sin lim ((𝑁 + (1 / 2)) · 𝑌)))
418301, 376, 417limccog 43851 . . . 4 (𝜑 → 0 ∈ ((sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) lim 𝑌))
41914a1i 11 . . . . . . . . 9 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))
420213fveq2d 6846 . . . . . . . . 9 (((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
421223sincld 16012 . . . . . . . . 9 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑤)) ∈ ℂ)
422419, 420, 214, 421fvmptd 6955 . . . . . . . 8 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹𝑤) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
423224fveq2d 6846 . . . . . . . 8 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = (sin‘((𝑁 + (1 / 2)) · 𝑤)))
424422, 423eqtr4d 2779 . . . . . . 7 ((𝜑𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹𝑤) = (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))
425424mpteq2dva 5205 . . . . . 6 (𝜑 → (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (𝐹𝑤)) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
42615feqmptd 6910 . . . . . 6 (𝜑𝐹 = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (𝐹𝑤)))
427 fcompt 7079 . . . . . . 7 ((sin:ℂ⟶ℂ ∧ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
428293, 373, 427sylancr 587 . . . . . 6 (𝜑 → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
429425, 426, 4283eqtr4rd 2787 . . . . 5 (𝜑 → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = 𝐹)
430429oveq1d 7372 . . . 4 (𝜑 → ((sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) lim 𝑌) = (𝐹 lim 𝑌))
431418, 430eleqtrd 2840 . . 3 (𝜑 → 0 ∈ (𝐹 lim 𝑌))
432 simpr 485 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → 𝑤 = 𝑌)
433432iftrued 4494 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = 0)
434263, 154, 156, 377, 379divdiv32d 11956 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑌 / 2) / (2 · π)) = ((𝑌 / (2 · π)) / 2))
435434oveq1d 7372 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑌 / 2) / (2 · π)) · (2 · π)) = (((𝑌 / (2 · π)) / 2) · (2 · π)))
436263halfcld 12398 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑌 / 2) ∈ ℂ)
437436, 156, 379divcan1d 11932 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑌 / 2) / (2 · π)) · (2 · π)) = (𝑌 / 2))
438384, 154, 156, 377div32d 11954 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑌 / (2 · π)) / 2) · (2 · π)) = ((𝑌 / (2 · π)) · ((2 · π) / 2)))
439155, 154, 377divcan3d 11936 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2 · π) / 2) = π)
440439oveq2d 7373 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑌 / (2 · π)) · ((2 · π) / 2)) = ((𝑌 / (2 · π)) · π))
441438, 440eqtrd 2776 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑌 / (2 · π)) / 2) · (2 · π)) = ((𝑌 / (2 · π)) · π))
442435, 437, 4413eqtr3d 2784 . . . . . . . . . . . . . . 15 (𝜑 → (𝑌 / 2) = ((𝑌 / (2 · π)) · π))
443442fveq2d 6846 . . . . . . . . . . . . . 14 (𝜑 → (sin‘(𝑌 / 2)) = (sin‘((𝑌 / (2 · π)) · π)))
444 sinkpi 25878 . . . . . . . . . . . . . . 15 ((𝑌 / (2 · π)) ∈ ℤ → (sin‘((𝑌 / (2 · π)) · π)) = 0)
445404, 444syl 17 . . . . . . . . . . . . . 14 (𝜑 → (sin‘((𝑌 / (2 · π)) · π)) = 0)
446443, 445eqtrd 2776 . . . . . . . . . . . . 13 (𝜑 → (sin‘(𝑌 / 2)) = 0)
447446oveq2d 7373 . . . . . . . . . . . 12 (𝜑 → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · 0))
448156mul01d 11354 . . . . . . . . . . . 12 (𝜑 → ((2 · π) · 0) = 0)
449447, 448eqtrd 2776 . . . . . . . . . . 11 (𝜑 → ((2 · π) · (sin‘(𝑌 / 2))) = 0)
450449eqcomd 2742 . . . . . . . . . 10 (𝜑 → 0 = ((2 · π) · (sin‘(𝑌 / 2))))
451450ad2antrr 724 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → 0 = ((2 · π) · (sin‘(𝑌 / 2))))
452 fvoveq1 7380 . . . . . . . . . . . 12 (𝑤 = 𝑌 → (sin‘(𝑤 / 2)) = (sin‘(𝑌 / 2)))
453452oveq2d 7373 . . . . . . . . . . 11 (𝑤 = 𝑌 → ((2 · π) · (sin‘(𝑤 / 2))) = ((2 · π) · (sin‘(𝑌 / 2))))
454453eqcomd 2742 . . . . . . . . . 10 (𝑤 = 𝑌 → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
455454adantl 482 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → ((2 · π) · (sin‘(𝑌 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
456433, 451, 4553eqtrd 2780 . . . . . . . 8 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
457 iffalse 4495 . . . . . . . . . 10 𝑤 = 𝑌 → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = (𝐺𝑤))
458457adantl 482 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = (𝐺𝑤))
459 fvoveq1 7380 . . . . . . . . . . 11 (𝑦 = 𝑤 → (sin‘(𝑦 / 2)) = (sin‘(𝑤 / 2)))
460459oveq2d 7373 . . . . . . . . . 10 (𝑦 = 𝑤 → ((2 · π) · (sin‘(𝑦 / 2))) = ((2 · π) · (sin‘(𝑤 / 2))))
461120a1i 11 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (2 · π) ∈ ℂ)
462328halfcld 12398 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 / 2) ∈ ℂ)
463462sincld 16012 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (sin‘(𝑤 / 2)) ∈ ℂ)
464461, 463mulcld 11175 . . . . . . . . . . 11 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ((2 · π) · (sin‘(𝑤 / 2))) ∈ ℂ)
465464adantr 481 . . . . . . . . . 10 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((2 · π) · (sin‘(𝑤 / 2))) ∈ ℂ)
46623, 460, 324, 465fvmptd3 6971 . . . . . . . . 9 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐺𝑤) = ((2 · π) · (sin‘(𝑤 / 2))))
467458, 466eqtrd 2776 . . . . . . . 8 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
468456, 467pm2.61dan 811 . . . . . . 7 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → if(𝑤 = 𝑌, 0, (𝐺𝑤)) = ((2 · π) · (sin‘(𝑤 / 2))))
469468mpteq2dva 5205 . . . . . 6 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))))
470 eqid 2736 . . . . . . . . . . 11 (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2)))) = (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2))))
47175, 156, 75constcncfg 44103 . . . . . . . . . . . 12 (𝜑 → (𝑤 ∈ ℂ ↦ (2 · π)) ∈ (ℂ–cn→ℂ))
472 id 22 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ → 𝑤 ∈ ℂ)
473 2cnd 12231 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ → 2 ∈ ℂ)
474134a1i 11 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ → 2 ≠ 0)
475472, 473, 474divrec2d 11935 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℂ → (𝑤 / 2) = ((1 / 2) · 𝑤))
476475mpteq2ia 5208 . . . . . . . . . . . . . . 15 (𝑤 ∈ ℂ ↦ (𝑤 / 2)) = (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤))
477 eqid 2736 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) = (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤))
478477mulc1cncf 24268 . . . . . . . . . . . . . . . 16 ((1 / 2) ∈ ℂ → (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) ∈ (ℂ–cn→ℂ))
47939, 478ax-mp 5 . . . . . . . . . . . . . . 15 (𝑤 ∈ ℂ ↦ ((1 / 2) · 𝑤)) ∈ (ℂ–cn→ℂ)
480476, 479eqeltri 2834 . . . . . . . . . . . . . 14 (𝑤 ∈ ℂ ↦ (𝑤 / 2)) ∈ (ℂ–cn→ℂ)
481480a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ∈ ℂ ↦ (𝑤 / 2)) ∈ (ℂ–cn→ℂ))
482415, 481cncfmpt1f 24277 . . . . . . . . . . . 12 (𝜑 → (𝑤 ∈ ℂ ↦ (sin‘(𝑤 / 2))) ∈ (ℂ–cn→ℂ))
483471, 482mulcncf 24810 . . . . . . . . . . 11 (𝜑 → (𝑤 ∈ ℂ ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ (ℂ–cn→ℂ))
484470, 483, 349, 75, 464cncfmptssg 44102 . . . . . . . . . 10 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
485 eqid 2736 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))
48651, 485, 345cncfcn 24273 . . . . . . . . . . 11 (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
487349, 74, 486sylancl 586 . . . . . . . . . 10 (𝜑 → ((𝐴(,)𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
488484, 487eleqtrd 2840 . . . . . . . . 9 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
489 cncnp 22631 . . . . . . . . . 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 2823 . . . . . . . 8 (𝑦 = 𝑌 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑤 / 2)))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌)))
494493rspccva 3580 . . . . . . 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 2838 . . . . 5 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
497307mpteq1d 5200 . . . . 5 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))))
498366eqcomd 2742 . . . . . . 7 (𝜑 → ((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) = ((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)))
499498oveq1d 7372 . . . . . 6 (𝜑 → (((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld)))
500499fveq1d 6844 . . . . 5 (𝜑 → ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌) = ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
501496, 497, 5003eltr4d 2853 . . . 4 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
502 eqid 2736 . . . . 5 (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤)))
50311, 124syldan 591 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
504503, 23fmptd 7062 . . . . 5 (𝜑𝐺:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
505371, 51, 502, 504, 374, 263ellimc 25237 . . . 4 (𝜑 → (0 ∈ (𝐺 lim 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌)))
506501, 505mpbird 256 . . 3 (𝜑 → 0 ∈ (𝐺 lim 𝑌))
507256nrexdv 3146 . . . 4 (𝜑 → ¬ ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0)
508504ffund 6672 . . . . . 6 (𝜑 → Fun 𝐺)
509 fvelima 6908 . . . . . 6 ((Fun 𝐺 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺𝑦) = 0)
510508, 509sylan 580 . . . . 5 ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺𝑦) = 0)
511 2cnd 12231 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ∈ ℂ)
512119a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ∈ ℂ)
513134a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ≠ 0)
514238a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ≠ 0)
515105, 511, 512, 513, 514divdiv1d 11962 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / 2) / π) = (𝑦 / (2 · π)))
516515eqcomd 2742 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
517516adantr 481 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π))
518 2cnd 12231 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → 2 ∈ ℂ)
519119a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → π ∈ ℂ)
520518, 519mulcld 11175 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (2 · π) ∈ ℂ)
521232adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → 𝑦 ∈ ℂ)
522521halfcld 12398 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (𝑦 / 2) ∈ ℂ)
523522sincld 16012 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (sin‘(𝑦 / 2)) ∈ ℂ)
524520, 523mulcld 11175 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ)
52523fvmpt2 6959 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ((2 · π) · (sin‘(𝑦 / 2))) ∈ ℂ) → (𝐺𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
526524, 525syldan 591 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (𝐺𝑦) = ((2 · π) · (sin‘(𝑦 / 2))))
527526eqcomd 2742 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) = (𝐺𝑦))
528 simpr 485 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → (𝐺𝑦) = 0)
529527, 528eqtrd 2776 . . . . . . . . . . . . . 14 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺𝑦) = 0) → ((2 · π) · (sin‘(𝑦 / 2))) = 0)
530120a1i 11 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (2 · π) ∈ ℂ)
531232halfcld 12398 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (𝑦 / 2) ∈ ℂ)
532531sincld 16012 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (sin‘(𝑦 / 2)) ∈ ℂ)
533530, 532mul0ord 11805 . . . . . . . . . . . . . . 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 12363 . . . . . . . . . . . . . . 15 (2 ∈ ℂ ∧ 2 ≠ 0)
537119, 238pm3.2i 471 . . . . . . . . . . . . . . 15 (π ∈ ℂ ∧ π ≠ 0)
538 mulne0 11797 . . . . . . . . . . . . . . 15 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → (2 · π) ≠ 0)
539536, 537, 538mp2an 690 . . . . . . . . . . . . . 14 (2 · π) ≠ 0
540539neii 2945 . . . . . . . . . . . . 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 12398 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → (𝑦 / 2) ∈ ℂ)
546545, 246syl 17 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈ ℤ))
547543, 546mpbid 231 . . . . . . . . . 10 (((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺𝑦) = 0) → ((𝑦 / 2) / π) ∈ ℤ)
548517, 547eqeltrd 2838 . . . . . . . . 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 3165 . . . . . 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 6959 . . . . . . . . 9 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (π · (cos‘(𝑦 / 2))) ∈ ℂ) → (𝐼𝑦) = (π · (cos‘(𝑦 / 2))))
559557, 201, 558syl2anc 584 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐼𝑦) = (π · (cos‘(𝑦 / 2))))
560531coscld 16013 . . . . . . . . . 10 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (cos‘(𝑦 / 2)) ∈ ℂ)
561560adantl 482 . . . . . . . . 9 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ∈ ℂ)
562 dirkercncflem2.11 . . . . . . . . 9 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0)
563512, 561, 514, 562mulne0d 11807 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (π · (cos‘(𝑦 / 2))) ≠ 0)
564559, 563eqnetrd 3011 . . . . . . 7 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐼𝑦) ≠ 0)
565564neneqd 2948 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝐼𝑦) = 0)
566565nrexdv 3146 . . . . 5 (𝜑 → ¬ ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼𝑦) = 0)
567201, 111fmptd 7062 . . . . . . 7 (𝜑𝐼:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
568567ffund 6672 . . . . . 6 (𝜑 → Fun 𝐼)
569 fvelima 6908 . . . . . 6 ((Fun 𝐼 ∧ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼𝑦) = 0)
570568, 569sylan 580 . . . . 5 ((𝜑 ∧ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼𝑦) = 0)
571566, 570mtand 814 . . . 4 (𝜑 → ¬ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌})))
572199imaeq1d 6012 . . . 4 (𝜑 → ((ℝ D 𝐺) “ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌})))
573571, 572neleqtrrd 2860 . . 3 (𝜑 → ¬ 0 ∈ ((ℝ D 𝐺) “ ((𝐴(,)𝐵) ∖ {𝑌})))
574 dirkercncflem2.d . . . . . 6 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
575574dirkerval2 44325 . . . . 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 4494 . . . . 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 4492 . . . . . . . . . . . . . 14 (𝑤 = 𝑌 → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)) = (((2 · 𝑁) + 1) / (2 · π)))
581580adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)) = (((2 · 𝑁) + 1) / (2 · π)))
582154, 38mulcld 11175 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2 · 𝑁) ∈ ℂ)
583582, 397addcld 11174 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2 · 𝑁) + 1) ∈ ℂ)
584583, 154, 155, 377, 378divdiv1d 11962 . . . . . . . . . . . . . . . 16 (𝜑 → ((((2 · 𝑁) + 1) / 2) / π) = (((2 · 𝑁) + 1) / (2 · π)))
585584eqcomd 2742 . . . . . . . . . . . . . . 15 (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) = ((((2 · 𝑁) + 1) / 2) / π))
586582, 397, 154, 377divdird 11969 . . . . . . . . . . . . . . . . 17 (𝜑 → (((2 · 𝑁) + 1) / 2) = (((2 · 𝑁) / 2) + (1 / 2)))
58738, 154, 377divcan3d 11936 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2 · 𝑁) / 2) = 𝑁)
588587oveq1d 7372 . . . . . . . . . . . . . . . . 17 (𝜑 → (((2 · 𝑁) / 2) + (1 / 2)) = (𝑁 + (1 / 2)))
589586, 588eqtrd 2776 . . . . . . . . . . . . . . . 16 (𝜑 → (((2 · 𝑁) + 1) / 2) = (𝑁 + (1 / 2)))
590589oveq1d 7372 . . . . . . . . . . . . . . 15 (𝜑 → ((((2 · 𝑁) + 1) / 2) / π) = ((𝑁 + (1 / 2)) / π))
591585, 590eqtrd 2776 . . . . . . . . . . . . . 14 (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) = ((𝑁 + (1 / 2)) / π))
592591ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((2 · 𝑁) + 1) / (2 · π)) = ((𝑁 + (1 / 2)) / π))
593310fveq2d 6846 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑌 → (cos‘((𝑁 + (1 / 2)) · 𝑤)) = (cos‘((𝑁 + (1 / 2)) · 𝑌)))
594593oveq2d 7373 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑌 → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))))
595 fvoveq1 7380 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑌 → (cos‘(𝑤 / 2)) = (cos‘(𝑌 / 2)))
596595oveq2d 7373 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑌 → (π · (cos‘(𝑤 / 2))) = (π · (cos‘(𝑌 / 2))))
597594, 596oveq12d 7375 . . . . . . . . . . . . . . 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 11180 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑁 · 𝑌) + ((1 / 2) · 𝑌)))
600397, 154, 263, 377div32d 11954 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((1 / 2) · 𝑌) = (1 · (𝑌 / 2)))
601436mulid2d 11173 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 · (𝑌 / 2)) = (𝑌 / 2))
602600, 601eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1 / 2) · 𝑌) = (𝑌 / 2))
603602oveq2d 7373 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑁 · 𝑌) + ((1 / 2) · 𝑌)) = ((𝑁 · 𝑌) + (𝑌 / 2)))
60438, 263mulcld 11175 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑁 · 𝑌) ∈ ℂ)
605604, 436addcomd 11357 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑁 · 𝑌) + (𝑌 / 2)) = ((𝑌 / 2) + (𝑁 · 𝑌)))
606599, 603, 6053eqtrd 2780 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑌 / 2) + (𝑁 · 𝑌)))
607606fveq2d 6846 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (cos‘((𝑁 + (1 / 2)) · 𝑌)) = (cos‘((𝑌 / 2) + (𝑁 · 𝑌))))
608604, 156, 379divcan1d 11932 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑁 · 𝑌) / (2 · π)) · (2 · π)) = (𝑁 · 𝑌))
609608eqcomd 2742 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑁 · 𝑌) = (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))
610609oveq2d 7373 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑌 / 2) + (𝑁 · 𝑌)) = ((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π))))
611610fveq2d 6846 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (cos‘((𝑌 / 2) + (𝑁 · 𝑌))) = (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))))
61238, 263, 156, 379divassd 11966 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑁 · 𝑌) / (2 · π)) = (𝑁 · (𝑌 / (2 · π))))
613405, 404zmulcld 12613 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑁 · (𝑌 / (2 · π))) ∈ ℤ)
614612, 613eqeltrd 2838 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑁 · 𝑌) / (2 · π)) ∈ ℤ)
615 cosper 25839 . . . . . . . . . . . . . . . . . . . 20 (((𝑌 / 2) ∈ ℂ ∧ ((𝑁 · 𝑌) / (2 · π)) ∈ ℤ) → (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))) = (cos‘(𝑌 / 2)))
616436, 614, 615syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 · π)))) = (cos‘(𝑌 / 2)))
617607, 611, 6163eqtrd 2780 . . . . . . . . . . . . . . . . . 18 (𝜑 → (cos‘((𝑁 + (1 / 2)) · 𝑌)) = (cos‘(𝑌 / 2)))
618617oveq2d 7373 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) = ((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))))
619618oveq1d 7372 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = (((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))) / (π · (cos‘(𝑌 / 2)))))
620436coscld 16013 . . . . . . . . . . . . . . . . 17 (𝜑 → (cos‘(𝑌 / 2)) ∈ ℂ)
621263, 154, 155, 377, 378divdiv1d 11962 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑌 / 2) / π) = (𝑌 / (2 · π)))
622621, 404eqeltrd 2838 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑌 / 2) / π) ∈ ℤ)
623622zred 12607 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑌 / 2) / π) ∈ ℝ)
624623, 272ltaddrpd 12990 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑌 / 2) / π) < (((𝑌 / 2) / π) + (1 / 2)))
625 halflt1 12371 . . . . . . . . . . . . . . . . . . . . . 22 (1 / 2) < 1
626625a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (1 / 2) < 1)
627268, 267, 623, 626ltadd2dd 11314 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝑌 / 2) / π) + (1 / 2)) < (((𝑌 / 2) / π) + 1))
628 btwnnz 12579 . . . . . . . . . . . . . . . . . . . 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 44095 . . . . . . . . . . . . . . . . . . . 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 2950 . . . . . . . . . . . . . . . . 17 (𝜑 → (cos‘(𝑌 / 2)) ≠ 0)
63441, 155, 620, 378, 633divcan5rd 11958 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
635619, 634eqtrd 2776 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
636635ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π · (cos‘(𝑌 / 2)))) = ((𝑁 + (1 / 2)) / π))
637598, 636eqtr2d 2777 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) / π) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))))
638581, 592, 6373eqtrrd 2781 . . . . . . . . . . . 12 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))) = if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)))
639 iffalse 4495 . . . . . . . . . . . . . 14 𝑤 = 𝑌 → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))
640639adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))
641 eqidd 2737 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))))
642 fveq2 6842 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑤 → (𝐻𝑦) = (𝐻𝑤))
643 fveq2 6842 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑤 → (𝐼𝑦) = (𝐼𝑤))
644642, 643oveq12d 7375 . . . . . . . . . . . . . . 15 (𝑦 = 𝑤 → ((𝐻𝑦) / (𝐼𝑦)) = ((𝐻𝑤) / (𝐼𝑤)))
645644adantl 482 . . . . . . . . . . . . . 14 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝐻𝑦) / (𝐼𝑦)) = ((𝐻𝑤) / (𝐼𝑤)))
646106, 100fmptd 7062 . . . . . . . . . . . . . . . . 17 (𝜑𝐻:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
647646ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐻:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
648647, 324ffvelcdmd 7036 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐻𝑤) ∈ ℂ)
649567ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐼:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
650649, 324ffvelcdmd 7036 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼𝑤) ∈ ℂ)
651111a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))))
652 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
653652fvoveq1d 7379 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (cos‘(𝑦 / 2)) = (cos‘(𝑤 / 2)))
654653oveq2d 7373 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (π · (cos‘(𝑦 / 2))) = (π · (cos‘(𝑤 / 2))))
655119a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (𝐴(,)𝐵) → π ∈ ℂ)
656327halfcld 12398 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝐴(,)𝐵) → (𝑤 / 2) ∈ ℂ)
657656coscld 16013 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (𝐴(,)𝐵) → (cos‘(𝑤 / 2)) ∈ ℂ)
658655, 657mulcld 11175 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (𝐴(,)𝐵) → (π · (cos‘(𝑤 / 2))) ∈ ℂ)
659658ad2antlr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π · (cos‘(𝑤 / 2))) ∈ ℂ)
660651, 654, 324, 659fvmptd 6955 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼𝑤) = (π · (cos‘(𝑤 / 2))))
661537a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π ∈ ℂ ∧ π ≠ 0))
662657ad2antlr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ∈ ℂ)
663 simpll 765 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝜑)
664 fvoveq1 7380 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑤 → (cos‘(𝑦 / 2)) = (cos‘(𝑤 / 2)))
665664neeq1d 3003 . . . . . . . . . . . . . . . . . . . 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 11797 . . . . . . . . . . . . . . . . 17 (((π ∈ ℂ ∧ π ≠ 0) ∧ ((cos‘(𝑤 / 2)) ∈ ℂ ∧ (cos‘(𝑤 / 2)) ≠ 0)) → (π · (cos‘(𝑤 / 2))) ≠ 0)
670661, 662, 668, 669syl12anc 835 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π · (cos‘(𝑤 / 2))) ≠ 0)
671660, 670eqnetrd 3011 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼𝑤) ≠ 0)
672648, 650, 671divcld 11931 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝐻𝑤) / (𝐼𝑤)) ∈ ℂ)
673641, 645, 324, 672fvmptd 6955 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤) = ((𝐻𝑤) / (𝐼𝑤)))
674100a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))))
675317fveq2d 6846 . . . . . . . . . . . . . . . 16 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (cos‘((𝑁 + (1 / 2)) · 𝑦)) = (cos‘((𝑁 + (1 / 2)) · 𝑤)))
676675oveq2d 7373 . . . . . . . . . . . . . . 15 ((((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))))
677329coscld 16013 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (cos‘((𝑁 + (1 / 2)) · 𝑤)) ∈ ℂ)
678325, 677mulcld 11175 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ℂ)
679678adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ℂ)
680674, 676, 324, 679fvmptd 6955 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐻𝑤) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))))
681680, 660oveq12d 7375 . . . . . . . . . . . . 13 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝐻𝑤) / (𝐼𝑤)) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))))
682640, 673, 6813eqtrrd 2781 . . . . . . . . . . . 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 5205 . . . . . . . . . 10 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))))
685579, 684eqtr2d 2777 . . . . . . . . 9 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) = 𝐿)
686349, 41, 75constcncfg 44103 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
687 cosf 16007 . . . . . . . . . . . . . . . . . . 19 cos:ℂ⟶ℂ
688231, 44sylan2 593 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ)
689 eqid 2736 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))
690688, 689fmptd 7062 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)):(𝐴(,)𝐵)⟶ℂ)
691 fcompt 7079 . . . . . . . . . . . . . . . . . . 19 ((cos:ℂ⟶ℂ ∧ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)):(𝐴(,)𝐵)⟶ℂ) → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
692687, 690, 691sylancr 587 . . . . . . . . . . . . . . . . . 18 (𝜑 → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))))
693 eqidd 2737 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)))
694316adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤))
695 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → 𝑤 ∈ (𝐴(,)𝐵))
696693, 694, 695, 329fvmptd 6955 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤))
697696fveq2d 6846 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = (cos‘((𝑁 + (1 / 2)) · 𝑤)))
698697mpteq2dva 5205 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))))
699692, 698eqtr2d 2777 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))) = (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))))
700349, 41, 75constcncfg 44103 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
701349, 75idcncfg 44104 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 𝑦) ∈ ((𝐴(,)𝐵)–cn→ℂ))
702700, 701mulcncf 24810 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
703 coscn 25804 . . . . . . . . . . . . . . . . . . 19 cos ∈ (ℂ–cn→ℂ)
704703a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → cos ∈ (ℂ–cn→ℂ))
705702, 704cncfco 24270 . . . . . . . . . . . . . . . . 17 (𝜑 → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
706699, 705eqeltrd 2838 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
707686, 706mulcncf 24810 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
708 eqid 2736 . . . . . . . . . . . . . . . 16 (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2))))
709349, 155, 75constcncfg 44103 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ π) ∈ ((𝐴(,)𝐵)–cn→ℂ))
710 2cnd 12231 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ)
711134a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → 2 ≠ 0)
712328, 710, 711divrecd 11934 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 / 2) = (𝑤 · (1 / 2)))
713712mpteq2dva 5205 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 / 2)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 · (1 / 2))))
714 eqid 2736 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2))) = (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2)))
715 cncfmptid 24276 . . . . . . . . . . . . . . . . . . . . . . 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 44103 . . . . . . . . . . . . . . . . . . . . . 22 ((1 / 2) ∈ ℂ → (𝑤 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
72139, 720mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑤 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
722717, 721mulcncf 24810 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2))) ∈ (ℂ–cn→ℂ))
723712, 462eqeltrrd 2839 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 · (1 / 2)) ∈ ℂ)
724714, 722, 349, 75, 723cncfmptssg 44102 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 · (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
725713, 724eqeltrd 2838 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 / 2)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
726704, 725cncfmpt1f 24277 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑤 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
727709, 726mulcncf 24810 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
728 ssid 3966 . . . . . . . . . . . . . . . . 17 (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)
729728a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵))
730 difssd 4092 . . . . . . . . . . . . . . . 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 3011 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
738737adantlr 713 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0)
739738, 668pm2.61dan 811 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (cos‘(𝑤 / 2)) ≠ 0)
740732, 733, 734, 739mulne0d 11807 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ≠ 0)
741740neneqd 2948 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → ¬ (π · (cos‘(𝑤 / 2))) = 0)
742 elsng 4600 . . . . . . . . . . . . . . . . . . 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 3921 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ∈ (ℂ ∖ {0}))
746708, 727, 729, 730, 745cncfmptssg 44102 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→(ℂ ∖ {0})))
747707, 746divcncf 24811 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
748747, 487eleqtrd 2840 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2))))) ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
749579, 748eqeltrd 2838 . . . . . . . . . . . 12 (𝜑𝐿 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld)))
750 cncnp 22631 . . . . . . . . . . . . 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 2823 . . . . . . . . . . 11 (𝑦 = 𝑌 → (𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑦) ↔ 𝐿 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌)))
755754rspccva 3580 . . . . . . . . . 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 2838 . . . . . . . 8 (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP (TopOpen‘ℂfld))‘𝑌))
758307mpteq1d 5200 . . . . . . . 8 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))))
759757, 758, 5003eltr4d 2853 . . . . . . 7 (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌))
760 eqid 2736 . . . . . . . 8 (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤)))
761100fvmpt2 6959 . . . . . . . . . . . 12 ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ) → (𝐻𝑦) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
762557, 106, 761syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐻𝑦) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))
763762, 559oveq12d 7375 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐻𝑦) / (𝐼𝑦)) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) / (π · (cos‘(𝑦 / 2)))))
764106, 201, 563divcld 11931 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) / (π · (cos‘(𝑦 / 2)))) ∈ ℂ)
765763, 764eqeltrd 2838 . . . . . . . . 9 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐻𝑦) / (𝐼𝑦)) ∈ ℂ)
766 eqid 2736 . . . . . . . . 9 (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))
767765, 766fmptd 7062 . . . . . . . 8 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ)
768371, 51, 760, 767, 374, 263ellimc 25237 . . . . . . 7 (𝜑 → ((((2 · 𝑁) + 1) / (2 · π)) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) lim 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦)))‘𝑤))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP (TopOpen‘ℂfld))‘𝑌)))
769759, 768mpbird 256 . . . . . 6 (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) lim 𝑌))
770103eqcomd 2742 . . . . . . . . . 10 (𝜑𝐻 = (ℝ D 𝐹))
771770fveq1d 6844 . . . . . . . . 9 (𝜑 → (𝐻𝑦) = ((ℝ D 𝐹)‘𝑦))
772199eqcomd 2742 . . . . . . . . . 10 (𝜑𝐼 = (ℝ D 𝐺))
773772fveq1d 6844 . . . . . . . . 9 (𝜑 → (𝐼𝑦) = ((ℝ D 𝐺)‘𝑦))
774771, 773oveq12d 7375 . . . . . . . 8 (𝜑 → ((𝐻𝑦) / (𝐼𝑦)) = (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)))
775774mpteq2dv 5207 . . . . . . 7 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))))
776775oveq1d 7372 . . . . . 6 (𝜑 → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻𝑦) / (𝐼𝑦))) lim 𝑌) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim 𝑌))
777769, 776eleqtrd 2840 . . . . 5 (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim 𝑌))
778577, 777eqeltrd 2838 . . . 4 (𝜑 → if((𝑌 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑌)) / ((2 · π) · (sin‘(𝑌 / 2))))) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim 𝑌))
779576, 778eqeltrd 2838 . . 3 (𝜑 → ((𝐷𝑁)‘𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) lim 𝑌))
7804, 15, 24, 26, 27, 28, 110, 205, 431, 506, 556, 573, 779lhop 25380 . 2 (𝜑 → ((𝐷𝑁)‘𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹𝑦) / (𝐺𝑦))) lim 𝑌))
781574dirkerval 44322 . . . . . 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 5936 . . . 4 (𝜑 → ((𝐷𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
7844resmptd 5994 . . . 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 4497 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
78613recnd 11183 . . . . . . . 8 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ)
78714fvmpt2 6959 . . . . . . . 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 7375 . . . . . 6 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐹𝑦) / (𝐺𝑦)) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
791785, 790eqtr4d 2779 . . . . 5 ((𝜑𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = ((𝐹𝑦) / (𝐺𝑦)))
792791mpteq2dva 5205 . . . 4 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑁) + 1) / (2 · π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹𝑦) / (𝐺𝑦))))
793783, 784, 7923eqtrrd 2781 . . 3 (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹𝑦) / (𝐺𝑦))) = ((𝐷𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))
794793oveq1d 7372 . 2 (𝜑 → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹𝑦) / (𝐺𝑦))) lim 𝑌) = (((𝐷𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) lim 𝑌))
795780, 794eleqtrd 2840 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 2943  wral 3064  wrex 3073  cdif 3907  cun 3908  wss 3910  ifcif 4486  {csn 4586  {cpr 4588   class class class wbr 5105  cmpt 5188  dom cdm 5633  ran crn 5634  cres 5635  cima 5636  ccom 5637  Fun wfun 6490   Fn wfn 6491  wf 6492  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189   / cdiv 11812  cn 12153  2c2 12208  cz 12499  +crp 12915  (,)cioo 13264   mod cmo 13774  sincsin 15946  cosccos 15947  πcpi 15949  t crest 17302  TopOpenctopn 17303  topGenctg 17319  fldccnfld 20796  Topctop 22242  TopOnctopon 22259  Clsdccld 22367  intcnt 22368   Cn ccn 22575   CnP ccnp 22576  Hauscha 22659  cnccncf 24239   lim climc 25226   D cdv 25227
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 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ioc 13269  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-fac 14174  df-bc 14203  df-hash 14231  df-shft 14952  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-limsup 15353  df-clim 15370  df-rlim 15371  df-sum 15571  df-ef 15950  df-sin 15952  df-cos 15953  df-pi 15955  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-fbas 20793  df-fg 20794  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lp 22487  df-perf 22488  df-cn 22578  df-cnp 22579  df-t1 22665  df-haus 22666  df-cmp 22738  df-tx 22913  df-hmeo 23106  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291  df-xms 23673  df-ms 23674  df-tms 23675  df-cncf 24241  df-limc 25230  df-dv 25231
This theorem is referenced by:  dirkercncflem3  44336
  Copyright terms: Public domain W3C validator