Proof of Theorem dirkercncflem2
Step | Hyp | Ref
| Expression |
1 | | difss 3888 |
. . . . 5
⊢ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ (𝐴(,)𝐵) |
2 | | ioossre 12439 |
. . . . 5
⊢ (𝐴(,)𝐵) ⊆ ℝ |
3 | 1, 2 | sstri 3761 |
. . . 4
⊢ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ |
4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ) |
5 | | dirkercncflem2.n |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
6 | 5 | adantr 466 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℕ) |
7 | 6 | nnred 11240 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℝ) |
8 | | halfre 11452 |
. . . . . . . 8
⊢ (1 / 2)
∈ ℝ |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈
ℝ) |
10 | 7, 9 | readdcld 10274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑁 + (1 / 2)) ∈ ℝ) |
11 | 4 | sselda 3752 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℝ) |
12 | 10, 11 | remulcld 10275 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℝ) |
13 | 12 | resincld 15078 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℝ) |
14 | | dirkercncflem2.f |
. . . 4
⊢ 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) |
15 | 13, 14 | fmptd 6529 |
. . 3
⊢ (𝜑 → 𝐹:((𝐴(,)𝐵) ∖ {𝑌})⟶ℝ) |
16 | | 2re 11295 |
. . . . . . 7
⊢ 2 ∈
ℝ |
17 | | pire 24430 |
. . . . . . 7
⊢ π
∈ ℝ |
18 | 16, 17 | remulcli 10259 |
. . . . . 6
⊢ (2
· π) ∈ ℝ |
19 | 18 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈
ℝ) |
20 | 11 | rehalfcld 11485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℝ) |
21 | 20 | resincld 15078 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ∈ ℝ) |
22 | 19, 21 | remulcld 10275 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((2 · π) ·
(sin‘(𝑦 / 2))) ∈
ℝ) |
23 | | dirkercncflem2.g |
. . . 4
⊢ 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 /
2)))) |
24 | 22, 23 | fmptd 6529 |
. . 3
⊢ (𝜑 → 𝐺:((𝐴(,)𝐵) ∖ {𝑌})⟶ℝ) |
25 | | iooretop 22788 |
. . . 4
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) |
26 | 25 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran
(,))) |
27 | | dirkercncflem2.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ (𝐴(,)𝐵)) |
28 | | eqid 2771 |
. . 3
⊢ ((𝐴(,)𝐵) ∖ {𝑌}) = ((𝐴(,)𝐵) ∖ {𝑌}) |
29 | 14 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) |
30 | 29 | oveq2d 6811 |
. . . . . . 7
⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))) |
31 | | resmpt 5589 |
. . . . . . . . . . . 12
⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) ↾
((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) |
32 | 3, 31 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) ↾
((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) |
33 | 32 | eqcomi 2780 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) |
34 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) |
35 | 34 | oveq2d 6811 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))) |
36 | | ax-resscn 10198 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
37 | 36 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ⊆
ℂ) |
38 | 5 | nncnd 11241 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℂ) |
39 | | halfcn 11453 |
. . . . . . . . . . . . . . 15
⊢ (1 / 2)
∈ ℂ |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 / 2) ∈
ℂ) |
41 | 38, 40 | addcld 10264 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ) |
42 | 41 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑁 + (1 / 2)) ∈ ℂ) |
43 | 37 | sselda 3752 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
44 | 42, 43 | mulcld 10265 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ) |
45 | 44 | sincld 15065 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈
ℂ) |
46 | | eqid 2771 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) = (𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) |
47 | 45, 46 | fmptd 6529 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℝ⟶ℂ) |
48 | | ssid 3773 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℝ |
49 | 48, 3 | pm3.2i 456 |
. . . . . . . . . 10
⊢ (ℝ
⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ) |
50 | 49 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ ⊆ ℝ
∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)) |
51 | | eqid 2771 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
52 | 51 | tgioo2 22825 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
53 | 51, 52 | dvres 23894 |
. . . . . . . . 9
⊢
(((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℝ⟶ℂ)
∧ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)) → (ℝ D
((𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) ↾
((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})))) |
54 | 37, 47, 50, 53 | syl21anc 1475 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) ↾
((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})))) |
55 | | retop 22784 |
. . . . . . . . . . 11
⊢
(topGen‘ran (,)) ∈ Top |
56 | | rehaus 22821 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) ∈ Haus |
57 | 27 | elioored 40291 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ∈ ℝ) |
58 | | uniretop 22785 |
. . . . . . . . . . . . . 14
⊢ ℝ =
∪ (topGen‘ran (,)) |
59 | 58 | sncld 21395 |
. . . . . . . . . . . . 13
⊢
(((topGen‘ran (,)) ∈ Haus ∧ 𝑌 ∈ ℝ) → {𝑌} ∈ (Clsd‘(topGen‘ran
(,)))) |
60 | 56, 57, 59 | sylancr 575 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑌} ∈ (Clsd‘(topGen‘ran
(,)))) |
61 | 58 | difopn 21058 |
. . . . . . . . . . . 12
⊢ (((𝐴(,)𝐵) ∈ (topGen‘ran (,)) ∧ {𝑌} ∈
(Clsd‘(topGen‘ran (,)))) → ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran
(,))) |
62 | 25, 60, 61 | sylancr 575 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran
(,))) |
63 | | isopn3i 21106 |
. . . . . . . . . . 11
⊢
(((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,))) →
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})) = ((𝐴(,)𝐵) ∖ {𝑌})) |
64 | 55, 62, 63 | sylancr 575 |
. . . . . . . . . 10
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})) = ((𝐴(,)𝐵) ∖ {𝑌})) |
65 | 64 | reseq2d 5533 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) ↾
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) |
66 | | reelprrecn 10233 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ {ℝ, ℂ} |
67 | 66 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
68 | 41 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑁 + (1 / 2)) ∈ ℂ) |
69 | | simpr 471 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ) |
70 | 68, 69 | mulcld 10265 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ) |
71 | 70 | sincld 15065 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈
ℂ) |
72 | | eqid 2771 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) = (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) |
73 | 71, 72 | fmptd 6529 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℂ⟶ℂ) |
74 | | ssid 3773 |
. . . . . . . . . . . . 13
⊢ ℂ
⊆ ℂ |
75 | 74 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂ ⊆
ℂ) |
76 | | dvsinax 40642 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 + (1 / 2)) ∈ ℂ
→ (ℂ D (𝑦 ∈
ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))) |
77 | 41, 76 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) = (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑦))))) |
78 | 77 | dmeqd 5463 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) = dom (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑦))))) |
79 | | eqid 2771 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑦)))) = (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑦)))) |
80 | 70 | coscld 15066 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘((𝑁 + (1 / 2)) · 𝑦)) ∈
ℂ) |
81 | 68, 80 | mulcld 10265 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈
ℂ) |
82 | 79, 81 | dmmptd 6163 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = ℂ) |
83 | 78, 82 | eqtrd 2805 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) =
ℂ) |
84 | 36, 83 | syl5sseqr 3803 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ⊆ dom
(ℂ D (𝑦 ∈
ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))) |
85 | | dvres3 23896 |
. . . . . . . . . . . 12
⊢
(((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℂ⟶ℂ)
∧ (ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))))) →
(ℝ D ((𝑦 ∈
ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) ↾
ℝ)) |
86 | 67, 73, 75, 84, 85 | syl22anc 1477 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) ↾
ℝ)) = ((ℂ D (𝑦
∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ)) |
87 | | resmpt 5589 |
. . . . . . . . . . . . 13
⊢ (ℝ
⊆ ℂ → ((𝑦
∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) |
88 | 36, 87 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) |
89 | 88 | oveq2d 6811 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) ↾
ℝ)) = (ℝ D (𝑦
∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))) |
90 | 77 | reseq1d 5532 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) ↾
ℝ) = ((𝑦 ∈
ℂ ↦ ((𝑁 + (1 /
2)) · (cos‘((𝑁
+ (1 / 2)) · 𝑦))))
↾ ℝ)) |
91 | | resmpt 5589 |
. . . . . . . . . . . . 13
⊢ (ℝ
⊆ ℂ → ((𝑦
∈ ℂ ↦ ((𝑁
+ (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))) |
92 | 36, 91 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑦)))) ↾
ℝ) = (𝑦 ∈
ℝ ↦ ((𝑁 + (1 /
2)) · (cos‘((𝑁
+ (1 / 2)) · 𝑦)))) |
93 | 90, 92 | syl6eq 2821 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) ↾
ℝ) = (𝑦 ∈
ℝ ↦ ((𝑁 + (1 /
2)) · (cos‘((𝑁
+ (1 / 2)) · 𝑦))))) |
94 | 86, 89, 93 | 3eqtr3d 2813 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑦))))) |
95 | 94 | reseq1d 5532 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) ↾
((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) |
96 | | resmpt 5589 |
. . . . . . . . . 10
⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑦)))) ↾
((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))) |
97 | 3, 96 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))) |
98 | 65, 95, 97 | 3eqtrd 2809 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) ↾
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))) |
99 | 35, 54, 98 | 3eqtrd 2809 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))) |
100 | | dirkercncflem2.h |
. . . . . . . . 9
⊢ 𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) |
101 | 100 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))) |
102 | 101 | eqcomd 2777 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = 𝐻) |
103 | 30, 99, 102 | 3eqtrd 2809 |
. . . . . 6
⊢ (𝜑 → (ℝ D 𝐹) = 𝐻) |
104 | 103 | dmeqd 5463 |
. . . . 5
⊢ (𝜑 → dom (ℝ D 𝐹) = dom 𝐻) |
105 | 11 | recnd 10273 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℂ) |
106 | 105, 81 | syldan 579 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈
ℂ) |
107 | 100, 106 | dmmptd 6163 |
. . . . 5
⊢ (𝜑 → dom 𝐻 = ((𝐴(,)𝐵) ∖ {𝑌})) |
108 | 104, 107 | eqtr2d 2806 |
. . . 4
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐹)) |
109 | | eqimss 3806 |
. . . 4
⊢ (((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐹) → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐹)) |
110 | 108, 109 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐹)) |
111 | | dirkercncflem2.i |
. . . . . . . 8
⊢ 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))) |
112 | 111 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2))))) |
113 | | resmpt 5589 |
. . . . . . . . . . . . 13
⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 /
2))))) |
114 | 3, 113 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 /
2)))) |
115 | 114 | eqcomi 2780 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 / 2)))) =
((𝑦 ∈ ℝ ↦
((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) |
116 | 115 | oveq2i 6806 |
. . . . . . . . . 10
⊢ (ℝ
D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 / 2))))) =
(ℝ D ((𝑦 ∈
ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) |
117 | 116 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 / 2))))) =
(ℝ D ((𝑦 ∈
ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))) |
118 | | 2cn 11296 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
119 | | picn 24431 |
. . . . . . . . . . . . . 14
⊢ π
∈ ℂ |
120 | 118, 119 | mulcli 10250 |
. . . . . . . . . . . . 13
⊢ (2
· π) ∈ ℂ |
121 | 120 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (2 · π)
∈ ℂ) |
122 | 43 | halfcld 11483 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 / 2) ∈ ℂ) |
123 | 122 | sincld 15065 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (sin‘(𝑦 / 2)) ∈
ℂ) |
124 | 121, 123 | mulcld 10265 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((2 · π)
· (sin‘(𝑦 /
2))) ∈ ℂ) |
125 | | eqid 2771 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ ℝ ↦ ((2 · π)
· (sin‘(𝑦 /
2)))) |
126 | 124, 125 | fmptd 6529 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ ((2 · π)
· (sin‘(𝑦 /
2)))):ℝ⟶ℂ) |
127 | 51, 52 | dvres 23894 |
. . . . . . . . . 10
⊢
(((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ ((2 · π)
· (sin‘(𝑦 /
2)))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)) → (ℝ D
((𝑦 ∈ ℝ ↦
((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π)
· (sin‘(𝑦 /
2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})))) |
128 | 37, 126, 50, 127 | syl21anc 1475 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π)
· (sin‘(𝑦 /
2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})))) |
129 | 64 | reseq2d 5533 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2))))) ↾
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π)
· (sin‘(𝑦 /
2))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) |
130 | 36 | sseli 3748 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
131 | | 1cnd 10261 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℂ → 1 ∈
ℂ) |
132 | | 2cnd 11298 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℂ → 2 ∈
ℂ) |
133 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
134 | | 2ne0 11318 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ≠
0 |
135 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℂ → 2 ≠
0) |
136 | 131, 132,
133, 135 | div13d 11030 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℂ → ((1 / 2)
· 𝑦) = ((𝑦 / 2) ·
1)) |
137 | | halfcl 11463 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℂ → (𝑦 / 2) ∈
ℂ) |
138 | 137 | mulid1d 10262 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℂ → ((𝑦 / 2) · 1) = (𝑦 / 2)) |
139 | 136, 138 | eqtrd 2805 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℂ → ((1 / 2)
· 𝑦) = (𝑦 / 2)) |
140 | 139 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℂ →
(sin‘((1 / 2) · 𝑦)) = (sin‘(𝑦 / 2))) |
141 | 140 | oveq2d 6811 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℂ → ((2
· π) · (sin‘((1 / 2) · 𝑦))) = ((2 · π) ·
(sin‘(𝑦 /
2)))) |
142 | 141 | eqcomd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℂ → ((2
· π) · (sin‘(𝑦 / 2))) = ((2 · π) ·
(sin‘((1 / 2) · 𝑦)))) |
143 | 130, 142 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ → ((2
· π) · (sin‘(𝑦 / 2))) = ((2 · π) ·
(sin‘((1 / 2) · 𝑦)))) |
144 | 143 | adantl 467 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((2 · π)
· (sin‘(𝑦 /
2))) = ((2 · π) · (sin‘((1 / 2) · 𝑦)))) |
145 | 144 | mpteq2dva 4879 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ ((2 · π)
· (sin‘(𝑦 /
2)))) = (𝑦 ∈ ℝ
↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) |
146 | 145 | oveq2d 6811 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2))))) = (ℝ D (𝑦 ∈ ℝ ↦ ((2 · π)
· (sin‘((1 / 2) · 𝑦)))))) |
147 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (2 · π)
∈ ℂ) |
148 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (1 / 2) ∈
ℂ) |
149 | 148, 69 | mulcld 10265 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((1 / 2) ·
𝑦) ∈
ℂ) |
150 | 149 | sincld 15065 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (sin‘((1 / 2)
· 𝑦)) ∈
ℂ) |
151 | 147, 150 | mulcld 10265 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · π)
· (sin‘((1 / 2) · 𝑦))) ∈ ℂ) |
152 | | eqid 2771 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((2 · π)
· (sin‘((1 / 2) · 𝑦)))) |
153 | 151, 152 | fmptd 6529 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ ((2 · π)
· (sin‘((1 / 2) · 𝑦)))):ℂ⟶ℂ) |
154 | | 2cnd 11298 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 2 ∈
ℂ) |
155 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → π ∈
ℂ) |
156 | 154, 155 | mulcld 10265 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (2 · π) ∈
ℂ) |
157 | | dvasinbx 40650 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((2
· π) ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D
(𝑦 ∈ ℂ ↦
((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (((2 · π)
· (1 / 2)) · (cos‘((1 / 2) · 𝑦))))) |
158 | 156, 39, 157 | sylancl 574 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (((2 · π)
· (1 / 2)) · (cos‘((1 / 2) · 𝑦))))) |
159 | | 2cnd 11298 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 2 ∈
ℂ) |
160 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → π ∈
ℂ) |
161 | 159, 160,
148 | mul32d 10451 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · π)
· (1 / 2)) = ((2 · (1 / 2)) · π)) |
162 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 2 ≠
0) |
163 | 159, 162 | recidd 11001 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (2 · (1 / 2))
= 1) |
164 | 163 | oveq1d 6810 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · (1 / 2))
· π) = (1 · π)) |
165 | 160 | mulid2d 10263 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (1 · π) =
π) |
166 | 161, 164,
165 | 3eqtrd 2809 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · π)
· (1 / 2)) = π) |
167 | 139 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ℂ →
(cos‘((1 / 2) · 𝑦)) = (cos‘(𝑦 / 2))) |
168 | 167 | adantl 467 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘((1 / 2)
· 𝑦)) =
(cos‘(𝑦 /
2))) |
169 | 166, 168 | oveq12d 6813 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((2 · π)
· (1 / 2)) · (cos‘((1 / 2) · 𝑦))) = (π · (cos‘(𝑦 / 2)))) |
170 | 169 | mpteq2dva 4879 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (((2 · π)
· (1 / 2)) · (cos‘((1 / 2) · 𝑦)))) = (𝑦 ∈ ℂ ↦ (π ·
(cos‘(𝑦 /
2))))) |
171 | 158, 170 | eqtrd 2805 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (π ·
(cos‘(𝑦 /
2))))) |
172 | 171 | dmeqd 5463 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) = dom (𝑦 ∈ ℂ ↦ (π ·
(cos‘(𝑦 /
2))))) |
173 | | eqid 2771 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℂ ↦ (π
· (cos‘(𝑦 /
2)))) = (𝑦 ∈ ℂ
↦ (π · (cos‘(𝑦 / 2)))) |
174 | 69 | halfcld 11483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑦 / 2) ∈ ℂ) |
175 | 174 | coscld 15066 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘(𝑦 / 2)) ∈
ℂ) |
176 | 160, 175 | mulcld 10265 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (π ·
(cos‘(𝑦 / 2))) ∈
ℂ) |
177 | 173, 176 | dmmptd 6163 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (𝑦 ∈ ℂ ↦ (π ·
(cos‘(𝑦 / 2)))) =
ℂ) |
178 | 172, 177 | eqtrd 2805 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) = ℂ) |
179 | 36, 178 | syl5sseqr 3803 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ℝ ⊆ dom
(ℂ D (𝑦 ∈
ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))))) |
180 | | dvres3 23896 |
. . . . . . . . . . . . . . 15
⊢
(((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ ((2 · π)
· (sin‘((1 / 2) · 𝑦)))):ℂ⟶ℂ) ∧ (ℂ
⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π)
· (sin‘((1 / 2) · 𝑦))))))) → (ℝ D ((𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ)) |
181 | 67, 153, 75, 179, 180 | syl22anc 1477 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ)) |
182 | | resmpt 5589 |
. . . . . . . . . . . . . . . 16
⊢ (ℝ
⊆ ℂ → ((𝑦
∈ ℂ ↦ ((2 · π) · (sin‘((1 / 2) ·
𝑦)))) ↾ ℝ) =
(𝑦 ∈ ℝ ↦
((2 · π) · (sin‘((1 / 2) · 𝑦))))) |
183 | 36, 182 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ ((2 · π)
· (sin‘((1 / 2) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((2 · π)
· (sin‘((1 / 2) · 𝑦))))) |
184 | 183 | oveq2d 6811 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦)))))) |
185 | 171 | reseq1d 5532 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ) = ((𝑦 ∈ ℂ ↦ (π ·
(cos‘(𝑦 / 2))))
↾ ℝ)) |
186 | 181, 184,
185 | 3eqtr3d 2813 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) = ((𝑦 ∈ ℂ ↦ (π ·
(cos‘(𝑦 / 2))))
↾ ℝ)) |
187 | | resmpt 5589 |
. . . . . . . . . . . . . 14
⊢ (ℝ
⊆ ℂ → ((𝑦
∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (π
· (cos‘(𝑦 /
2))))) |
188 | 36, 187 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℂ ↦ (π
· (cos‘(𝑦 /
2)))) ↾ ℝ) = (𝑦
∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))) |
189 | 186, 188 | syl6eq 2821 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℝ ↦ (π ·
(cos‘(𝑦 /
2))))) |
190 | 146, 189 | eqtrd 2805 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ ℝ ↦ (π ·
(cos‘(𝑦 /
2))))) |
191 | 190 | reseq1d 5532 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ (π ·
(cos‘(𝑦 / 2))))
↾ ((𝐴(,)𝐵) ∖ {𝑌}))) |
192 | 4 | resmptd 5592 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (π ·
(cos‘(𝑦 / 2))))
↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2))))) |
193 | 129, 191,
192 | 3eqtrd 2809 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2))))) ↾
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2))))) |
194 | 117, 128,
193 | 3eqtrd 2809 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 / 2))))) =
(𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2))))) |
195 | 194 | eqcomd 2777 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 /
2)))))) |
196 | 23 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 /
2))))) |
197 | 196 | oveq2d 6811 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐺) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 /
2)))))) |
198 | 197 | eqcomd 2777 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 / 2))))) =
(ℝ D 𝐺)) |
199 | 112, 195,
198 | 3eqtrrd 2810 |
. . . . . 6
⊢ (𝜑 → (ℝ D 𝐺) = 𝐼) |
200 | 199 | dmeqd 5463 |
. . . . 5
⊢ (𝜑 → dom (ℝ D 𝐺) = dom 𝐼) |
201 | 105, 176 | syldan 579 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (π · (cos‘(𝑦 / 2))) ∈
ℂ) |
202 | 111, 201 | dmmptd 6163 |
. . . . 5
⊢ (𝜑 → dom 𝐼 = ((𝐴(,)𝐵) ∖ {𝑌})) |
203 | 200, 202 | eqtr2d 2806 |
. . . 4
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐺)) |
204 | | eqimss 3806 |
. . . 4
⊢ (((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐺) → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐺)) |
205 | 203, 204 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐺)) |
206 | 105, 70 | syldan 579 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ) |
207 | 206 | ralrimiva 3115 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ) |
208 | | eqid 2771 |
. . . . . . . 8
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) |
209 | 208 | fnmpt 6159 |
. . . . . . 7
⊢
(∀𝑦 ∈
((𝐴(,)𝐵) ∖ {𝑌})((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌})) |
210 | 207, 209 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌})) |
211 | | eqidd 2772 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) |
212 | | simpr 471 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤) |
213 | 212 | oveq2d 6811 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤)) |
214 | | simpr 471 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) |
215 | 38 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℂ) |
216 | | 1cnd 10261 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈
ℂ) |
217 | 216 | halfcld 11483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈
ℂ) |
218 | 215, 217 | addcld 10264 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑁 + (1 / 2)) ∈ ℂ) |
219 | | eldifi 3883 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ (𝐴(,)𝐵)) |
220 | 219 | elioored 40291 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ ℝ) |
221 | 220 | recnd 10273 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ ℂ) |
222 | 221 | adantl 467 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑤 ∈ ℂ) |
223 | 218, 222 | mulcld 10265 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ) |
224 | 211, 213,
214, 223 | fvmptd 6432 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤)) |
225 | | eleq1w 2833 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑤 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↔ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))) |
226 | 225 | anbi2d 614 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑤 → ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ↔ (𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})))) |
227 | | oveq1 6802 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑤 → (𝑦 mod (2 · π)) = (𝑤 mod (2 · π))) |
228 | 227 | neeq1d 3002 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑤 → ((𝑦 mod (2 · π)) ≠ 0 ↔ (𝑤 mod (2 · π)) ≠
0)) |
229 | 226, 228 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 → (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 mod (2 · π)) ≠ 0) ↔
((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑤 mod (2 · π)) ≠
0))) |
230 | | eldifi 3883 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ (𝐴(,)𝐵)) |
231 | | elioore 12409 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ (𝐴(,)𝐵) → 𝑦 ∈ ℝ) |
232 | 230, 231,
130 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ ℂ) |
233 | | 2cnd 11298 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 2 ∈ ℂ) |
234 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → π ∈
ℂ) |
235 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 2 ≠ 0) |
236 | | 0re 10245 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℝ |
237 | | pipos 24432 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 <
π |
238 | 236, 237 | gtneii 10354 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ π ≠
0 |
239 | 238 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → π ≠ 0) |
240 | 232, 233,
234, 235, 239 | divdiv1d 11037 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → ((𝑦 / 2) / π) = (𝑦 / (2 · π))) |
241 | 240 | eqcomd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π)) |
242 | 241 | adantl 467 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π)) |
243 | | dirkercncflem2.yne0 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ≠ 0) |
244 | 243 | neneqd 2948 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (sin‘(𝑦 / 2)) = 0) |
245 | 105 | halfcld 11483 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℂ) |
246 | | sineq0 24493 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 / 2) ∈ ℂ →
((sin‘(𝑦 / 2)) = 0
↔ ((𝑦 / 2) / π)
∈ ℤ)) |
247 | 245, 246 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈
ℤ)) |
248 | 244, 247 | mtbid 313 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / 2) / π) ∈
ℤ) |
249 | 242, 248 | eqneltrd 2869 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 / (2 · π)) ∈
ℤ) |
250 | | 2rp 12039 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ+ |
251 | | pirp 24433 |
. . . . . . . . . . . . . . . . . 18
⊢ π
∈ ℝ+ |
252 | | rpmulcl 12057 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℝ+ ∧ π ∈ ℝ+) → (2
· π) ∈ ℝ+) |
253 | 250, 251,
252 | mp2an 672 |
. . . . . . . . . . . . . . . . 17
⊢ (2
· π) ∈ ℝ+ |
254 | | mod0 12882 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ ∧ (2
· π) ∈ ℝ+) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈
ℤ)) |
255 | 11, 253, 254 | sylancl 574 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈
ℤ)) |
256 | 249, 255 | mtbird 314 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 mod (2 · π)) = 0) |
257 | 256 | neqned 2950 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 mod (2 · π)) ≠
0) |
258 | 229, 257 | chvarv 2425 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑤 mod (2 · π)) ≠
0) |
259 | 258 | neneqd 2948 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑤 mod (2 · π)) = 0) |
260 | | simpll 750 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝜑) |
261 | | simpr 471 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) |
262 | 221 | ad2antlr 706 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑤 ∈ ℂ) |
263 | 57 | recnd 10273 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑌 ∈ ℂ) |
264 | 263 | ad2antrr 705 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑌 ∈ ℂ) |
265 | | 0red 10246 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ∈
ℝ) |
266 | 5 | nnred 11240 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℝ) |
267 | | 1red 10260 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ∈
ℝ) |
268 | 267 | rehalfcld 11485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
269 | 266, 268 | readdcld 10274 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ) |
270 | 5 | nngt0d 11269 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 < 𝑁) |
271 | 250 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 2 ∈
ℝ+) |
272 | 271 | rpreccld 12084 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 / 2) ∈
ℝ+) |
273 | 266, 272 | ltaddrpd 12107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 < (𝑁 + (1 / 2))) |
274 | 265, 266,
269, 270, 273 | lttrd 10403 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 < (𝑁 + (1 / 2))) |
275 | 274 | gt0ne0d 10797 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 + (1 / 2)) ≠ 0) |
276 | 41, 275 | jca 501 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠
0)) |
277 | 276 | ad2antrr 705 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠
0)) |
278 | | mulcan 10869 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ ((𝑁 + (1 / 2)) ∈ ℂ ∧
(𝑁 + (1 / 2)) ≠ 0))
→ (((𝑁 + (1 / 2))
· 𝑤) = ((𝑁 + (1 / 2)) · 𝑌) ↔ 𝑤 = 𝑌)) |
279 | 262, 264,
277, 278 | syl3anc 1476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → (((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌) ↔ 𝑤 = 𝑌)) |
280 | 261, 279 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑤 = 𝑌) |
281 | | oveq1 6802 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑌 → (𝑤 mod (2 · π)) = (𝑌 mod (2 · π))) |
282 | | dirkercncflem2.ymod |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 mod (2 · π)) =
0) |
283 | 281, 282 | sylan9eqr 2827 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (𝑤 mod (2 · π)) = 0) |
284 | 260, 280,
283 | syl2anc 573 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → (𝑤 mod (2 · π)) = 0) |
285 | 259, 284 | mtand 817 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) |
286 | 41, 263 | mulcld 10265 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ) |
287 | 286 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ) |
288 | | elsn2g 4350 |
. . . . . . . . . . . 12
⊢ (((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ → (((𝑁 + (1 / 2)) · 𝑤) ∈ {((𝑁 + (1 / 2)) · 𝑌)} ↔ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))) |
289 | 287, 288 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑁 + (1 / 2)) · 𝑤) ∈ {((𝑁 + (1 / 2)) · 𝑌)} ↔ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌))) |
290 | 285, 289 | mtbird 314 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑁 + (1 / 2)) · 𝑤) ∈ {((𝑁 + (1 / 2)) · 𝑌)}) |
291 | 223, 290 | eldifd 3734 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑤) ∈ (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)})) |
292 | 224, 291 | eqeltrd 2850 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)})) |
293 | | sinf 15059 |
. . . . . . . . . . . 12
⊢
sin:ℂ⟶ℂ |
294 | 293 | fdmi 6194 |
. . . . . . . . . . 11
⊢ dom sin =
ℂ |
295 | 294 | eqcomi 2780 |
. . . . . . . . . 10
⊢ ℂ =
dom sin |
296 | 295 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ℂ = dom
sin) |
297 | 296 | difeq1d 3878 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}) = (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) |
298 | 292, 297 | eleqtrd 2852 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) |
299 | 298 | ralrimiva 3115 |
. . . . . 6
⊢ (𝜑 → ∀𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) |
300 | | fnfvrnss 6534 |
. . . . . 6
⊢ (((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ∀𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) → ran (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ⊆ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) |
301 | 210, 299,
300 | syl2anc 573 |
. . . . 5
⊢ (𝜑 → ran (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ⊆ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) |
302 | | uncom 3908 |
. . . . . . . . . 10
⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) |
303 | 302 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌}))) |
304 | 27 | snssd 4476 |
. . . . . . . . . 10
⊢ (𝜑 → {𝑌} ⊆ (𝐴(,)𝐵)) |
305 | | undif 4192 |
. . . . . . . . . 10
⊢ ({𝑌} ⊆ (𝐴(,)𝐵) ↔ ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐴(,)𝐵)) |
306 | 304, 305 | sylib 208 |
. . . . . . . . 9
⊢ (𝜑 → ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐴(,)𝐵)) |
307 | 303, 306 | eqtrd 2805 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = (𝐴(,)𝐵)) |
308 | 307 | mpteq1d 4873 |
. . . . . . 7
⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))) |
309 | | iftrue 4232 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑌)) |
310 | | oveq2 6803 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑌 → ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) |
311 | 309, 310 | eqtr4d 2808 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤)) |
312 | 311 | adantl 467 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤)) |
313 | | iffalse 4235 |
. . . . . . . . . . . . 13
⊢ (¬
𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) |
314 | 313 | adantl 467 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) |
315 | | eqidd 2772 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) |
316 | | oveq2 6803 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤)) |
317 | 316 | adantl 467 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤)) |
318 | | simpl 468 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ (𝐴(,)𝐵)) |
319 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑤 = 𝑌 → ¬ 𝑤 = 𝑌) |
320 | | velsn 4333 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ {𝑌} ↔ 𝑤 = 𝑌) |
321 | 319, 320 | sylnibr 318 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑤 = 𝑌 → ¬ 𝑤 ∈ {𝑌}) |
322 | 321 | adantl 467 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → ¬ 𝑤 ∈ {𝑌}) |
323 | 318, 322 | eldifd 3734 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) |
324 | 323 | adantll 693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) |
325 | 41 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑁 + (1 / 2)) ∈ ℂ) |
326 | | elioore 12409 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ (𝐴(,)𝐵) → 𝑤 ∈ ℝ) |
327 | 326 | recnd 10273 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ (𝐴(,)𝐵) → 𝑤 ∈ ℂ) |
328 | 327 | adantl 467 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 𝑤 ∈ ℂ) |
329 | 325, 328 | mulcld 10265 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ) |
330 | 329 | adantr 466 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ) |
331 | 315, 317,
324, 330 | fvmptd 6432 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤)) |
332 | 314, 331 | eqtrd 2805 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤)) |
333 | 312, 332 | pm2.61dan 814 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤)) |
334 | 333 | mpteq2dva 4879 |
. . . . . . . . 9
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤))) |
335 | | ioosscn 40234 |
. . . . . . . . . . . . . 14
⊢ (𝐴(,)𝐵) ⊆ ℂ |
336 | | resmpt 5589 |
. . . . . . . . . . . . . 14
⊢ ((𝐴(,)𝐵) ⊆ ℂ → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤))) |
337 | 335, 336 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) |
338 | | eqid 2771 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) = (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) |
339 | 338 | mulc1cncf 22927 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 + (1 / 2)) ∈ ℂ
→ (𝑤 ∈ ℂ
↦ ((𝑁 + (1 / 2))
· 𝑤)) ∈
(ℂ–cn→ℂ)) |
340 | 41, 339 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (ℂ–cn→ℂ)) |
341 | 51 | cnfldtop 22806 |
. . . . . . . . . . . . . . . . . . 19
⊢
(TopOpen‘ℂfld) ∈ Top |
342 | | unicntop 22808 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
343 | 342 | restid 16301 |
. . . . . . . . . . . . . . . . . . 19
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
344 | 341, 343 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
345 | 344 | eqcomi 2780 |
. . . . . . . . . . . . . . . . 17
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
346 | 51, 345, 345 | cncfcn 22931 |
. . . . . . . . . . . . . . . 16
⊢ ((ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℂ) =
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
347 | 74, 75, 346 | sylancr 575 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ–cn→ℂ) =
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
348 | 340, 347 | eleqtrd 2852 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
349 | 2, 37 | syl5ss 3763 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
350 | 342 | cnrest 21309 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
351 | 348, 349,
350 | syl2anc 573 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
352 | 337, 351 | syl5eqelr 2855 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
353 | 51 | cnfldtopon 22805 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
354 | | resttopon 21185 |
. . . . . . . . . . . . . 14
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (𝐴(,)𝐵) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵))) |
355 | 353, 349,
354 | sylancr 575 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵))) |
356 | | cncnp 21304 |
. . . . . . . . . . . . 13
⊢
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
↔ ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)))) |
357 | 355, 353,
356 | sylancl 574 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
↔ ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)))) |
358 | 352, 357 | mpbid 222 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦))) |
359 | 358 | simprd 483 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
360 | | fveq2 6333 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑌 →
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
361 | 360 | eleq2d 2836 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑌 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌))) |
362 | 361 | rspccva 3459 |
. . . . . . . . . 10
⊢
((∀𝑦 ∈
(𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
363 | 359, 27, 362 | syl2anc 573 |
. . . . . . . . 9
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
364 | 334, 363 | eqeltrd 2850 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
365 | 307 | eqcomd 2777 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,)𝐵) = (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) |
366 | 365 | oveq2d 6811 |
. . . . . . . . . 10
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld)
↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}))) |
367 | 366 | oveq1d 6810 |
. . . . . . . . 9
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld)) =
(((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))) |
368 | 367 | fveq1d 6335 |
. . . . . . . 8
⊢ (𝜑 →
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌) = ((((TopOpen‘ℂfld)
↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌)) |
369 | 364, 368 | eleqtrd 2852 |
. . . . . . 7
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌)) |
370 | 308, 369 | eqeltrd 2850 |
. . . . . 6
⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌)) |
371 | | eqid 2771 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) = ((TopOpen‘ℂfld)
↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) |
372 | | eqid 2771 |
. . . . . . 7
⊢ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) |
373 | 206, 208 | fmptd 6529 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) |
374 | 4, 36 | syl6ss 3764 |
. . . . . . 7
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℂ) |
375 | 371, 51, 372, 373, 374, 263 | ellimc 23856 |
. . . . . 6
⊢ (𝜑 → (((𝑁 + (1 / 2)) · 𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) limℂ 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌))) |
376 | 370, 375 | mpbird 247 |
. . . . 5
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) limℂ 𝑌)) |
377 | 134 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ≠ 0) |
378 | 238 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → π ≠
0) |
379 | 154, 155,
377, 378 | mulne0d 10884 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · π) ≠
0) |
380 | 263, 156,
379 | divcan1d 11007 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 / (2 · π)) · (2 ·
π)) = 𝑌) |
381 | 380 | eqcomd 2777 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 = ((𝑌 / (2 · π)) · (2 ·
π))) |
382 | 381 | oveq2d 6811 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 ·
π)))) |
383 | 382 | fveq2d 6337 |
. . . . . . 7
⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) = (sin‘((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) ·
(2 · π))))) |
384 | 263, 156,
379 | divcld 11006 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 / (2 · π)) ∈
ℂ) |
385 | 41, 384, 156 | mul12d 10450 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 ·
π))) = ((𝑌 / (2 ·
π)) · ((𝑁 + (1 /
2)) · (2 · π)))) |
386 | 41, 154, 155 | mulassd 10268 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑁 + (1 / 2)) · 2) · π) =
((𝑁 + (1 / 2)) · (2
· π))) |
387 | 386 | eqcomd 2777 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 + (1 / 2)) · (2 · π)) =
(((𝑁 + (1 / 2)) · 2)
· π)) |
388 | 387 | oveq2d 6811 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 / (2 · π)) · ((𝑁 + (1 / 2)) · (2 ·
π))) = ((𝑌 / (2 ·
π)) · (((𝑁 + (1 /
2)) · 2) · π))) |
389 | 38, 40, 154 | adddird 10270 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 2) = ((𝑁 · 2) + ((1 / 2) ·
2))) |
390 | 154, 377 | recid2d 11002 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((1 / 2) · 2) =
1) |
391 | 390 | oveq2d 6811 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 · 2) + ((1 / 2) · 2)) =
((𝑁 · 2) +
1)) |
392 | 389, 391 | eqtrd 2805 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 2) = ((𝑁 · 2) +
1)) |
393 | 392 | oveq1d 6810 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 + (1 / 2)) · 2) · π) =
(((𝑁 · 2) + 1)
· π)) |
394 | 393 | oveq2d 6811 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 / (2 · π)) · (((𝑁 + (1 / 2)) · 2) ·
π)) = ((𝑌 / (2 ·
π)) · (((𝑁
· 2) + 1) · π))) |
395 | 385, 388,
394 | 3eqtrd 2809 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 ·
π))) = ((𝑌 / (2 ·
π)) · (((𝑁
· 2) + 1) · π))) |
396 | 38, 154 | mulcld 10265 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 · 2) ∈
ℂ) |
397 | | 1cnd 10261 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℂ) |
398 | 396, 397 | addcld 10264 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 · 2) + 1) ∈
ℂ) |
399 | 384, 398,
155 | mulassd 10268 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ·
π) = ((𝑌 / (2 ·
π)) · (((𝑁
· 2) + 1) · π))) |
400 | 395, 399 | eqtr4d 2808 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 ·
π))) = (((𝑌 / (2
· π)) · ((𝑁 · 2) + 1)) ·
π)) |
401 | 400 | fveq2d 6337 |
. . . . . . 7
⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) ·
(2 · π)))) = (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ·
π))) |
402 | | mod0 12882 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ ℝ ∧ (2
· π) ∈ ℝ+) → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈
ℤ)) |
403 | 57, 253, 402 | sylancl 574 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈
ℤ)) |
404 | 282, 403 | mpbid 222 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 / (2 · π)) ∈
ℤ) |
405 | 5 | nnzd 11687 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℤ) |
406 | | 2z 11615 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
407 | 406 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℤ) |
408 | 405, 407 | zmulcld 11694 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 · 2) ∈
ℤ) |
409 | 408 | peano2zd 11691 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 · 2) + 1) ∈
ℤ) |
410 | 404, 409 | zmulcld 11694 |
. . . . . . . 8
⊢ (𝜑 → ((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ∈
ℤ) |
411 | | sinkpi 24491 |
. . . . . . . 8
⊢ (((𝑌 / (2 · π)) ·
((𝑁 · 2) + 1))
∈ ℤ → (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ·
π)) = 0) |
412 | 410, 411 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (sin‘(((𝑌 / (2 · π)) ·
((𝑁 · 2) + 1))
· π)) = 0) |
413 | 383, 401,
412 | 3eqtrd 2809 |
. . . . . 6
⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) = 0) |
414 | | sincn 24417 |
. . . . . . . 8
⊢ sin
∈ (ℂ–cn→ℂ) |
415 | 414 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → sin ∈
(ℂ–cn→ℂ)) |
416 | 415, 286 | cnlimci 23872 |
. . . . . 6
⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) ∈ (sin
limℂ ((𝑁 +
(1 / 2)) · 𝑌))) |
417 | 413, 416 | eqeltrrd 2851 |
. . . . 5
⊢ (𝜑 → 0 ∈ (sin
limℂ ((𝑁 +
(1 / 2)) · 𝑌))) |
418 | 301, 376,
417 | limccog 40367 |
. . . 4
⊢ (𝜑 → 0 ∈ ((sin ∘
(𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) limℂ 𝑌)) |
419 | 14 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) |
420 | 213 | fveq2d 6337 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) = (sin‘((𝑁 + (1 / 2)) · 𝑤))) |
421 | 223 | sincld 15065 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑤)) ∈ ℂ) |
422 | 419, 420,
214, 421 | fvmptd 6432 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹‘𝑤) = (sin‘((𝑁 + (1 / 2)) · 𝑤))) |
423 | 224 | fveq2d 6337 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = (sin‘((𝑁 + (1 / 2)) · 𝑤))) |
424 | 422, 423 | eqtr4d 2808 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹‘𝑤) = (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) |
425 | 424 | mpteq2dva 4879 |
. . . . . 6
⊢ (𝜑 → (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (𝐹‘𝑤)) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))) |
426 | 15 | feqmptd 6393 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (𝐹‘𝑤))) |
427 | | fcompt 6545 |
. . . . . . 7
⊢
((sin:ℂ⟶ℂ ∧ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) → (sin ∘
(𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))) |
428 | 293, 373,
427 | sylancr 575 |
. . . . . 6
⊢ (𝜑 → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))) |
429 | 425, 426,
428 | 3eqtr4rd 2816 |
. . . . 5
⊢ (𝜑 → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = 𝐹) |
430 | 429 | oveq1d 6810 |
. . . 4
⊢ (𝜑 → ((sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) limℂ 𝑌) = (𝐹 limℂ 𝑌)) |
431 | 418, 430 | eleqtrd 2852 |
. . 3
⊢ (𝜑 → 0 ∈ (𝐹 limℂ 𝑌)) |
432 | | simpr 471 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → 𝑤 = 𝑌) |
433 | 432 | iftrued 4234 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = 0) |
434 | 263, 154,
156, 377, 379 | divdiv32d 11031 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑌 / 2) / (2 · π)) = ((𝑌 / (2 · π)) /
2)) |
435 | 434 | oveq1d 6810 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑌 / 2) / (2 · π)) · (2
· π)) = (((𝑌 / (2
· π)) / 2) · (2 · π))) |
436 | 263 | halfcld 11483 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑌 / 2) ∈ ℂ) |
437 | 436, 156,
379 | divcan1d 11007 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑌 / 2) / (2 · π)) · (2
· π)) = (𝑌 /
2)) |
438 | 384, 154,
156, 377 | div32d 11029 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑌 / (2 · π)) / 2) · (2
· π)) = ((𝑌 / (2
· π)) · ((2 · π) / 2))) |
439 | 155, 154,
377 | divcan3d 11011 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2 · π) / 2) =
π) |
440 | 439 | oveq2d 6811 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑌 / (2 · π)) · ((2 ·
π) / 2)) = ((𝑌 / (2
· π)) · π)) |
441 | 438, 440 | eqtrd 2805 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑌 / (2 · π)) / 2) · (2
· π)) = ((𝑌 / (2
· π)) · π)) |
442 | 435, 437,
441 | 3eqtr3d 2813 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑌 / 2) = ((𝑌 / (2 · π)) ·
π)) |
443 | 442 | fveq2d 6337 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (sin‘(𝑌 / 2)) = (sin‘((𝑌 / (2 · π)) ·
π))) |
444 | | sinkpi 24491 |
. . . . . . . . . . . . . . 15
⊢ ((𝑌 / (2 · π)) ∈
ℤ → (sin‘((𝑌 / (2 · π)) · π)) =
0) |
445 | 404, 444 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (sin‘((𝑌 / (2 · π)) ·
π)) = 0) |
446 | 443, 445 | eqtrd 2805 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (sin‘(𝑌 / 2)) = 0) |
447 | 446 | oveq2d 6811 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · π)
· (sin‘(𝑌 /
2))) = ((2 · π) · 0)) |
448 | 156 | mul01d 10440 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · π)
· 0) = 0) |
449 | 447, 448 | eqtrd 2805 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · π)
· (sin‘(𝑌 /
2))) = 0) |
450 | 449 | eqcomd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → 0 = ((2 · π)
· (sin‘(𝑌 /
2)))) |
451 | 450 | ad2antrr 705 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → 0 = ((2 · π) ·
(sin‘(𝑌 /
2)))) |
452 | | fvoveq1 6818 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑌 → (sin‘(𝑤 / 2)) = (sin‘(𝑌 / 2))) |
453 | 452 | oveq2d 6811 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑌 → ((2 · π) ·
(sin‘(𝑤 / 2))) = ((2
· π) · (sin‘(𝑌 / 2)))) |
454 | 453 | eqcomd 2777 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑌 → ((2 · π) ·
(sin‘(𝑌 / 2))) = ((2
· π) · (sin‘(𝑤 / 2)))) |
455 | 454 | adantl 467 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → ((2 · π) ·
(sin‘(𝑌 / 2))) = ((2
· π) · (sin‘(𝑤 / 2)))) |
456 | 433, 451,
455 | 3eqtrd 2809 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = ((2 · π) ·
(sin‘(𝑤 /
2)))) |
457 | | iffalse 4235 |
. . . . . . . . . 10
⊢ (¬
𝑤 = 𝑌 → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = (𝐺‘𝑤)) |
458 | 457 | adantl 467 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = (𝐺‘𝑤)) |
459 | 23 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 /
2))))) |
460 | | fvoveq1 6818 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (sin‘(𝑦 / 2)) = (sin‘(𝑤 / 2))) |
461 | 460 | oveq2d 6811 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → ((2 · π) ·
(sin‘(𝑦 / 2))) = ((2
· π) · (sin‘(𝑤 / 2)))) |
462 | 461 | adantl 467 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((2 · π) ·
(sin‘(𝑦 / 2))) = ((2
· π) · (sin‘(𝑤 / 2)))) |
463 | 120 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (2 · π) ∈
ℂ) |
464 | 328 | halfcld 11483 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 / 2) ∈ ℂ) |
465 | 464 | sincld 15065 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (sin‘(𝑤 / 2)) ∈ ℂ) |
466 | 463, 465 | mulcld 10265 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((2 · π) ·
(sin‘(𝑤 / 2))) ∈
ℂ) |
467 | 466 | adantr 466 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((2 · π) ·
(sin‘(𝑤 / 2))) ∈
ℂ) |
468 | 459, 462,
324, 467 | fvmptd 6432 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐺‘𝑤) = ((2 · π) ·
(sin‘(𝑤 /
2)))) |
469 | 458, 468 | eqtrd 2805 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = ((2 · π) ·
(sin‘(𝑤 /
2)))) |
470 | 456, 469 | pm2.61dan 814 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = ((2 · π) ·
(sin‘(𝑤 /
2)))) |
471 | 470 | mpteq2dva 4879 |
. . . . . 6
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 /
2))))) |
472 | | eqid 2771 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℂ ↦ ((2
· π) · (sin‘(𝑤 / 2)))) = (𝑤 ∈ ℂ ↦ ((2 · π)
· (sin‘(𝑤 /
2)))) |
473 | 75, 156, 75 | constcncfg 40599 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (2 · π))
∈ (ℂ–cn→ℂ)) |
474 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ → 𝑤 ∈
ℂ) |
475 | | 2cnd 11298 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ → 2 ∈
ℂ) |
476 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ → 2 ≠
0) |
477 | 474, 475,
476 | divrec2d 11010 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℂ → (𝑤 / 2) = ((1 / 2) · 𝑤)) |
478 | 477 | mpteq2ia 4875 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℂ ↦ (𝑤 / 2)) = (𝑤 ∈ ℂ ↦ ((1 / 2) ·
𝑤)) |
479 | | eqid 2771 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ ↦ ((1 / 2)
· 𝑤)) = (𝑤 ∈ ℂ ↦ ((1 / 2)
· 𝑤)) |
480 | 479 | mulc1cncf 22927 |
. . . . . . . . . . . . . . . 16
⊢ ((1 / 2)
∈ ℂ → (𝑤
∈ ℂ ↦ ((1 / 2) · 𝑤)) ∈ (ℂ–cn→ℂ)) |
481 | 39, 480 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℂ ↦ ((1 / 2)
· 𝑤)) ∈
(ℂ–cn→ℂ) |
482 | 478, 481 | eqeltri 2846 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℂ ↦ (𝑤 / 2)) ∈
(ℂ–cn→ℂ) |
483 | 482 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (𝑤 / 2)) ∈ (ℂ–cn→ℂ)) |
484 | 415, 483 | cncfmpt1f 22935 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (sin‘(𝑤 / 2))) ∈
(ℂ–cn→ℂ)) |
485 | 473, 484 | mulcncf 23433 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ ((2 · π)
· (sin‘(𝑤 /
2)))) ∈ (ℂ–cn→ℂ)) |
486 | 472, 485,
349, 75, 466 | cncfmptssg 40598 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((𝐴(,)𝐵)–cn→ℂ)) |
487 | | eqid 2771 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) |
488 | 51, 487, 345 | cncfcn 22931 |
. . . . . . . . . . 11
⊢ (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
489 | 349, 74, 488 | sylancl 574 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
490 | 486, 489 | eleqtrd 2852 |
. . . . . . . . 9
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
491 | | cncnp 21304 |
. . . . . . . . . 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))‘𝑦)))) |
492 | 355, 353,
491 | sylancl 574 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
↔ ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 /
2)))):(𝐴(,)𝐵)⟶ℂ ∧
∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)))) |
493 | 490, 492 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 /
2)))):(𝐴(,)𝐵)⟶ℂ ∧
∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦))) |
494 | 493 | simprd 483 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
495 | 360 | eleq2d 2836 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌))) |
496 | 495 | rspccva 3459 |
. . . . . . 7
⊢
((∀𝑦 ∈
(𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
497 | 494, 27, 496 | syl2anc 573 |
. . . . . 6
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
498 | 471, 497 | eqeltrd 2850 |
. . . . 5
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
499 | 307 | mpteq1d 4873 |
. . . . 5
⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤)))) |
500 | 366 | eqcomd 2777 |
. . . . . . 7
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) = ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵))) |
501 | 500 | oveq1d 6810 |
. . . . . 6
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld)) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))) |
502 | 501 | fveq1d 6335 |
. . . . 5
⊢ (𝜑 →
((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌) = ((((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
503 | 498, 499,
502 | 3eltr4d 2865 |
. . . 4
⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌)) |
504 | | eqid 2771 |
. . . . 5
⊢ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) |
505 | 11, 124 | syldan 579 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((2 · π) ·
(sin‘(𝑦 / 2))) ∈
ℂ) |
506 | 505, 23 | fmptd 6529 |
. . . . 5
⊢ (𝜑 → 𝐺:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) |
507 | 371, 51, 504, 506, 374, 263 | ellimc 23856 |
. . . 4
⊢ (𝜑 → (0 ∈ (𝐺 limℂ 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌))) |
508 | 503, 507 | mpbird 247 |
. . 3
⊢ (𝜑 → 0 ∈ (𝐺 limℂ 𝑌)) |
509 | 256 | nrexdv 3149 |
. . . 4
⊢ (𝜑 → ¬ ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0) |
510 | 506 | ffund 6188 |
. . . . . 6
⊢ (𝜑 → Fun 𝐺) |
511 | | fvelima 6392 |
. . . . . 6
⊢ ((Fun
𝐺 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0) |
512 | 510, 511 | sylan 569 |
. . . . 5
⊢ ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0) |
513 | | 2cnd 11298 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ∈
ℂ) |
514 | 119 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ∈
ℂ) |
515 | 134 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ≠ 0) |
516 | 238 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ≠ 0) |
517 | 105, 513,
514, 515, 516 | divdiv1d 11037 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / 2) / π) = (𝑦 / (2 · π))) |
518 | 517 | eqcomd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π)) |
519 | 518 | adantr 466 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π)) |
520 | | 2cnd 11298 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → 2 ∈
ℂ) |
521 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → π ∈
ℂ) |
522 | 520, 521 | mulcld 10265 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (2 · π) ∈
ℂ) |
523 | 232 | adantr 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → 𝑦 ∈ ℂ) |
524 | 523 | halfcld 11483 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (𝑦 / 2) ∈ ℂ) |
525 | 524 | sincld 15065 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (sin‘(𝑦 / 2)) ∈ ℂ) |
526 | 522, 525 | mulcld 10265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) ·
(sin‘(𝑦 / 2))) ∈
ℂ) |
527 | 23 | fvmpt2 6435 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ((2 · π) ·
(sin‘(𝑦 / 2))) ∈
ℂ) → (𝐺‘𝑦) = ((2 · π) ·
(sin‘(𝑦 /
2)))) |
528 | 526, 527 | syldan 579 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (𝐺‘𝑦) = ((2 · π) ·
(sin‘(𝑦 /
2)))) |
529 | 528 | eqcomd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) ·
(sin‘(𝑦 / 2))) =
(𝐺‘𝑦)) |
530 | | simpr 471 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (𝐺‘𝑦) = 0) |
531 | 529, 530 | eqtrd 2805 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) ·
(sin‘(𝑦 / 2))) =
0) |
532 | 120 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (2 · π) ∈
ℂ) |
533 | 232 | halfcld 11483 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (𝑦 / 2) ∈ ℂ) |
534 | 533 | sincld 15065 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (sin‘(𝑦 / 2)) ∈ ℂ) |
535 | 532, 534 | mul0ord 10882 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (((2 · π) ·
(sin‘(𝑦 / 2))) = 0
↔ ((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0))) |
536 | 535 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (((2 · π) ·
(sin‘(𝑦 / 2))) = 0
↔ ((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0))) |
537 | 531, 536 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) = 0 ∨
(sin‘(𝑦 / 2)) =
0)) |
538 | | 2cnne0 11448 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
539 | 119, 238 | pm3.2i 456 |
. . . . . . . . . . . . . . 15
⊢ (π
∈ ℂ ∧ π ≠ 0) |
540 | | mulne0 10874 |
. . . . . . . . . . . . . . 15
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0))
→ (2 · π) ≠ 0) |
541 | 538, 539,
540 | mp2an 672 |
. . . . . . . . . . . . . 14
⊢ (2
· π) ≠ 0 |
542 | 541 | neii 2945 |
. . . . . . . . . . . . 13
⊢ ¬ (2
· π) = 0 |
543 | | pm2.53 840 |
. . . . . . . . . . . . 13
⊢ (((2
· π) = 0 ∨ (sin‘(𝑦 / 2)) = 0) → (¬ (2 · π) =
0 → (sin‘(𝑦 /
2)) = 0)) |
544 | 537, 542,
543 | mpisyl 21 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (sin‘(𝑦 / 2)) = 0) |
545 | 544 | adantll 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (sin‘(𝑦 / 2)) = 0) |
546 | 105 | adantr 466 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → 𝑦 ∈ ℂ) |
547 | 546 | halfcld 11483 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 / 2) ∈ ℂ) |
548 | 547, 246 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈
ℤ)) |
549 | 545, 548 | mpbid 222 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → ((𝑦 / 2) / π) ∈
ℤ) |
550 | 519, 549 | eqeltrd 2850 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 / (2 · π)) ∈
ℤ) |
551 | 11 | adantr 466 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → 𝑦 ∈ ℝ) |
552 | 551, 253,
254 | sylancl 574 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈
ℤ)) |
553 | 550, 552 | mpbird 247 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 mod (2 · π)) = 0) |
554 | 553 | ex 397 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐺‘𝑦) = 0 → (𝑦 mod (2 · π)) =
0)) |
555 | 554 | reximdva 3165 |
. . . . . 6
⊢ (𝜑 → (∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0 → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) =
0)) |
556 | 555 | adantr 466 |
. . . . 5
⊢ ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → (∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0 → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) =
0)) |
557 | 512, 556 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0) |
558 | 509, 557 | mtand 817 |
. . 3
⊢ (𝜑 → ¬ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) |
559 | | simpr 471 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) |
560 | 111 | fvmpt2 6435 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (π · (cos‘(𝑦 / 2))) ∈ ℂ) →
(𝐼‘𝑦) = (π · (cos‘(𝑦 / 2)))) |
561 | 559, 201,
560 | syl2anc 573 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐼‘𝑦) = (π · (cos‘(𝑦 / 2)))) |
562 | 533 | coscld 15066 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (cos‘(𝑦 / 2)) ∈ ℂ) |
563 | 562 | adantl 467 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ∈ ℂ) |
564 | | dirkercncflem2.11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0) |
565 | 514, 563,
516, 564 | mulne0d 10884 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (π · (cos‘(𝑦 / 2))) ≠ 0) |
566 | 561, 565 | eqnetrd 3010 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐼‘𝑦) ≠ 0) |
567 | 566 | neneqd 2948 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝐼‘𝑦) = 0) |
568 | 567 | nrexdv 3149 |
. . . . 5
⊢ (𝜑 → ¬ ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼‘𝑦) = 0) |
569 | 201, 111 | fmptd 6529 |
. . . . . . 7
⊢ (𝜑 → 𝐼:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) |
570 | 569 | ffund 6188 |
. . . . . 6
⊢ (𝜑 → Fun 𝐼) |
571 | | fvelima 6392 |
. . . . . 6
⊢ ((Fun
𝐼 ∧ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼‘𝑦) = 0) |
572 | 570, 571 | sylan 569 |
. . . . 5
⊢ ((𝜑 ∧ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼‘𝑦) = 0) |
573 | 568, 572 | mtand 817 |
. . . 4
⊢ (𝜑 → ¬ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) |
574 | 199 | imaeq1d 5605 |
. . . 4
⊢ (𝜑 → ((ℝ D 𝐺) “ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) |
575 | 573, 574 | neleqtrrd 2872 |
. . 3
⊢ (𝜑 → ¬ 0 ∈ ((ℝ D
𝐺) “ ((𝐴(,)𝐵) ∖ {𝑌}))) |
576 | | dirkercncflem2.d |
. . . . . 6
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0,
(((2 · 𝑛) + 1) / (2
· π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) ·
(sin‘(𝑦 /
2))))))) |
577 | 576 | dirkerval2 40825 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ ℝ) → ((𝐷‘𝑁)‘𝑌) = if((𝑌 mod (2 · π)) = 0, (((2 ·
𝑁) + 1) / (2 ·
π)), ((sin‘((𝑁 +
(1 / 2)) · 𝑌)) / ((2
· π) · (sin‘(𝑌 / 2)))))) |
578 | 5, 57, 577 | syl2anc 573 |
. . . 4
⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) = if((𝑌 mod (2 · π)) = 0, (((2 ·
𝑁) + 1) / (2 ·
π)), ((sin‘((𝑁 +
(1 / 2)) · 𝑌)) / ((2
· π) · (sin‘(𝑌 / 2)))))) |
579 | 282 | iftrued 4234 |
. . . . 5
⊢ (𝜑 → if((𝑌 mod (2 · π)) = 0, (((2 ·
𝑁) + 1) / (2 ·
π)), ((sin‘((𝑁 +
(1 / 2)) · 𝑌)) / ((2
· π) · (sin‘(𝑌 / 2))))) = (((2 · 𝑁) + 1) / (2 ·
π))) |
580 | | dirkercncflem2.l |
. . . . . . . . . . 11
⊢ 𝐿 = (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 /
2))))) |
581 | 580 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 = (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 /
2)))))) |
582 | | iftrue 4232 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑌 → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = (((2 · 𝑁) + 1) / (2 ·
π))) |
583 | 582 | adantl 467 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = (((2 · 𝑁) + 1) / (2 ·
π))) |
584 | 154, 38 | mulcld 10265 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) |
585 | 584, 397 | addcld 10264 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2 · 𝑁) + 1) ∈
ℂ) |
586 | 585, 154,
155, 377, 378 | divdiv1d 11037 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((((2 · 𝑁) + 1) / 2) / π) = (((2
· 𝑁) + 1) / (2
· π))) |
587 | 586 | eqcomd 2777 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) =
((((2 · 𝑁) + 1) / 2)
/ π)) |
588 | 584, 397,
154, 377 | divdird 11044 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((2 · 𝑁) + 1) / 2) = (((2 ·
𝑁) / 2) + (1 /
2))) |
589 | 38, 154, 377 | divcan3d 11011 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2 · 𝑁) / 2) = 𝑁) |
590 | 589 | oveq1d 6810 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((2 · 𝑁) / 2) + (1 / 2)) = (𝑁 + (1 / 2))) |
591 | 588, 590 | eqtrd 2805 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2 · 𝑁) + 1) / 2) = (𝑁 + (1 / 2))) |
592 | 591 | oveq1d 6810 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((2 · 𝑁) + 1) / 2) / π) = ((𝑁 + (1 / 2)) /
π)) |
593 | 587, 592 | eqtrd 2805 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) =
((𝑁 + (1 / 2)) /
π)) |
594 | 593 | ad2antrr 705 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((2 · 𝑁) + 1) / (2 · π)) = ((𝑁 + (1 / 2)) /
π)) |
595 | 310 | fveq2d 6337 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑌 → (cos‘((𝑁 + (1 / 2)) · 𝑤)) = (cos‘((𝑁 + (1 / 2)) · 𝑌))) |
596 | 595 | oveq2d 6811 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑌 → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌)))) |
597 | | fvoveq1 6818 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑌 → (cos‘(𝑤 / 2)) = (cos‘(𝑌 / 2))) |
598 | 597 | oveq2d 6811 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑌 → (π · (cos‘(𝑤 / 2))) = (π ·
(cos‘(𝑌 /
2)))) |
599 | 596, 598 | oveq12d 6813 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑌 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 / 2)))) =
(((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑌))) / (π
· (cos‘(𝑌 /
2))))) |
600 | 599 | adantl 467 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 / 2)))) =
(((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑌))) / (π
· (cos‘(𝑌 /
2))))) |
601 | 38, 40, 263 | adddird 10270 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑁 · 𝑌) + ((1 / 2) · 𝑌))) |
602 | 397, 154,
263, 377 | div32d 11029 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((1 / 2) · 𝑌) = (1 · (𝑌 / 2))) |
603 | 436 | mulid2d 10263 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 · (𝑌 / 2)) = (𝑌 / 2)) |
604 | 602, 603 | eqtrd 2805 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1 / 2) · 𝑌) = (𝑌 / 2)) |
605 | 604 | oveq2d 6811 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑁 · 𝑌) + ((1 / 2) · 𝑌)) = ((𝑁 · 𝑌) + (𝑌 / 2))) |
606 | 38, 263 | mulcld 10265 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑁 · 𝑌) ∈ ℂ) |
607 | 606, 436 | addcomd 10443 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑁 · 𝑌) + (𝑌 / 2)) = ((𝑌 / 2) + (𝑁 · 𝑌))) |
608 | 601, 605,
607 | 3eqtrd 2809 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑌 / 2) + (𝑁 · 𝑌))) |
609 | 608 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (cos‘((𝑁 + (1 / 2)) · 𝑌)) = (cos‘((𝑌 / 2) + (𝑁 · 𝑌)))) |
610 | 606, 156,
379 | divcan1d 11007 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((𝑁 · 𝑌) / (2 · π)) · (2 ·
π)) = (𝑁 · 𝑌)) |
611 | 610 | eqcomd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑁 · 𝑌) = (((𝑁 · 𝑌) / (2 · π)) · (2 ·
π))) |
612 | 611 | oveq2d 6811 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑌 / 2) + (𝑁 · 𝑌)) = ((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 ·
π)))) |
613 | 612 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (cos‘((𝑌 / 2) + (𝑁 · 𝑌))) = (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 ·
π))))) |
614 | 38, 263, 156, 379 | divassd 11041 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑁 · 𝑌) / (2 · π)) = (𝑁 · (𝑌 / (2 · π)))) |
615 | 405, 404 | zmulcld 11694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑁 · (𝑌 / (2 · π))) ∈
ℤ) |
616 | 614, 615 | eqeltrd 2850 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑁 · 𝑌) / (2 · π)) ∈
ℤ) |
617 | | cosper 24454 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑌 / 2) ∈ ℂ ∧
((𝑁 · 𝑌) / (2 · π)) ∈
ℤ) → (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 ·
π)))) = (cos‘(𝑌 /
2))) |
618 | 436, 616,
617 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 ·
π)))) = (cos‘(𝑌 /
2))) |
619 | 609, 613,
618 | 3eqtrd 2809 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (cos‘((𝑁 + (1 / 2)) · 𝑌)) = (cos‘(𝑌 / 2))) |
620 | 619 | oveq2d 6811 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) = ((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2)))) |
621 | 620 | oveq1d 6810 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π ·
(cos‘(𝑌 / 2)))) =
(((𝑁 + (1 / 2)) ·
(cos‘(𝑌 / 2))) /
(π · (cos‘(𝑌 / 2))))) |
622 | 436 | coscld 15066 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (cos‘(𝑌 / 2)) ∈
ℂ) |
623 | 263, 154,
155, 377, 378 | divdiv1d 11037 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑌 / 2) / π) = (𝑌 / (2 · π))) |
624 | 623, 404 | eqeltrd 2850 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑌 / 2) / π) ∈
ℤ) |
625 | 624 | zred 11688 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑌 / 2) / π) ∈
ℝ) |
626 | 625, 272 | ltaddrpd 12107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑌 / 2) / π) < (((𝑌 / 2) / π) + (1 / 2))) |
627 | | halflt1 11456 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 / 2)
< 1 |
628 | 627 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (1 / 2) <
1) |
629 | 268, 267,
625, 628 | ltadd2dd 10401 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝑌 / 2) / π) + (1 / 2)) < (((𝑌 / 2) / π) +
1)) |
630 | | btwnnz 11659 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑌 / 2) / π) ∈ ℤ
∧ ((𝑌 / 2) / π) <
(((𝑌 / 2) / π) + (1 /
2)) ∧ (((𝑌 / 2) / π)
+ (1 / 2)) < (((𝑌 / 2) /
π) + 1)) → ¬ (((𝑌 / 2) / π) + (1 / 2)) ∈
ℤ) |
631 | 624, 626,
629, 630 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ (((𝑌 / 2) / π) + (1 / 2)) ∈
ℤ) |
632 | | coseq0 40590 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑌 / 2) ∈ ℂ →
((cos‘(𝑌 / 2)) = 0
↔ (((𝑌 / 2) / π) +
(1 / 2)) ∈ ℤ)) |
633 | 436, 632 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((cos‘(𝑌 / 2)) = 0 ↔ (((𝑌 / 2) / π) + (1 / 2)) ∈
ℤ)) |
634 | 631, 633 | mtbird 314 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ¬ (cos‘(𝑌 / 2)) = 0) |
635 | 634 | neqned 2950 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (cos‘(𝑌 / 2)) ≠ 0) |
636 | 41, 155, 622, 378, 635 | divcan5rd 11033 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))) / (π ·
(cos‘(𝑌 / 2)))) =
((𝑁 + (1 / 2)) /
π)) |
637 | 621, 636 | eqtrd 2805 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π ·
(cos‘(𝑌 / 2)))) =
((𝑁 + (1 / 2)) /
π)) |
638 | 637 | ad2antrr 705 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π ·
(cos‘(𝑌 / 2)))) =
((𝑁 + (1 / 2)) /
π)) |
639 | 600, 638 | eqtr2d 2806 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) / π) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 /
2))))) |
640 | 583, 594,
639 | 3eqtrrd 2810 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 / 2)))) =
if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) |
641 | | iffalse 4235 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑤 = 𝑌 → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) |
642 | 641 | adantl 467 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) |
643 | | eqidd 2772 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))) |
644 | | fveq2 6333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑤 → (𝐻‘𝑦) = (𝐻‘𝑤)) |
645 | | fveq2 6333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑤 → (𝐼‘𝑦) = (𝐼‘𝑤)) |
646 | 644, 645 | oveq12d 6813 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑤 → ((𝐻‘𝑦) / (𝐼‘𝑦)) = ((𝐻‘𝑤) / (𝐼‘𝑤))) |
647 | 646 | adantl 467 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝐻‘𝑦) / (𝐼‘𝑦)) = ((𝐻‘𝑤) / (𝐼‘𝑤))) |
648 | 106, 100 | fmptd 6529 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐻:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) |
649 | 648 | ad2antrr 705 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐻:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) |
650 | 649, 324 | ffvelrnd 6505 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐻‘𝑤) ∈ ℂ) |
651 | 569 | ad2antrr 705 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐼:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) |
652 | 651, 324 | ffvelrnd 6505 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼‘𝑤) ∈ ℂ) |
653 | 111 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2))))) |
654 | | simpr 471 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤) |
655 | 654 | fvoveq1d 6817 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (cos‘(𝑦 / 2)) = (cos‘(𝑤 / 2))) |
656 | 655 | oveq2d 6811 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (π · (cos‘(𝑦 / 2))) = (π ·
(cos‘(𝑤 /
2)))) |
657 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ (𝐴(,)𝐵) → π ∈
ℂ) |
658 | 327 | halfcld 11483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ (𝐴(,)𝐵) → (𝑤 / 2) ∈ ℂ) |
659 | 658 | coscld 15066 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ (𝐴(,)𝐵) → (cos‘(𝑤 / 2)) ∈ ℂ) |
660 | 657, 659 | mulcld 10265 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ (𝐴(,)𝐵) → (π · (cos‘(𝑤 / 2))) ∈
ℂ) |
661 | 660 | ad2antlr 706 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π · (cos‘(𝑤 / 2))) ∈
ℂ) |
662 | 653, 656,
324, 661 | fvmptd 6432 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼‘𝑤) = (π · (cos‘(𝑤 / 2)))) |
663 | 539 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π ∈ ℂ ∧ π
≠ 0)) |
664 | 659 | ad2antlr 706 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ∈ ℂ) |
665 | | simpll 750 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝜑) |
666 | | fvoveq1 6818 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑤 → (cos‘(𝑦 / 2)) = (cos‘(𝑤 / 2))) |
667 | 666 | neeq1d 3002 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑤 → ((cos‘(𝑦 / 2)) ≠ 0 ↔ (cos‘(𝑤 / 2)) ≠ 0)) |
668 | 226, 667 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑤 → (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0) ↔ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑤 / 2)) ≠ 0))) |
669 | 668, 564 | chvarv 2425 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑤 / 2)) ≠ 0) |
670 | 665, 324,
669 | syl2anc 573 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0) |
671 | | mulne0 10874 |
. . . . . . . . . . . . . . . . 17
⊢ (((π
∈ ℂ ∧ π ≠ 0) ∧ ((cos‘(𝑤 / 2)) ∈ ℂ ∧ (cos‘(𝑤 / 2)) ≠ 0)) → (π
· (cos‘(𝑤 /
2))) ≠ 0) |
672 | 663, 664,
670, 671 | syl12anc 1474 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π · (cos‘(𝑤 / 2))) ≠ 0) |
673 | 662, 672 | eqnetrd 3010 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼‘𝑤) ≠ 0) |
674 | 650, 652,
673 | divcld 11006 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝐻‘𝑤) / (𝐼‘𝑤)) ∈ ℂ) |
675 | 643, 647,
324, 674 | fvmptd 6432 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤) = ((𝐻‘𝑤) / (𝐼‘𝑤))) |
676 | 100 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))) |
677 | 317 | fveq2d 6337 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (cos‘((𝑁 + (1 / 2)) · 𝑦)) = (cos‘((𝑁 + (1 / 2)) · 𝑤))) |
678 | 677 | oveq2d 6811 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤)))) |
679 | 329 | coscld 15066 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘((𝑁 + (1 / 2)) · 𝑤)) ∈ ℂ) |
680 | 325, 679 | mulcld 10265 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈
ℂ) |
681 | 680 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈
ℂ) |
682 | 676, 678,
324, 681 | fvmptd 6432 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐻‘𝑤) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤)))) |
683 | 682, 662 | oveq12d 6813 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝐻‘𝑤) / (𝐼‘𝑤)) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 /
2))))) |
684 | 642, 675,
683 | 3eqtrrd 2810 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 / 2)))) =
if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) |
685 | 640, 684 | pm2.61dan 814 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 / 2)))) =
if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) |
686 | 685 | mpteq2dva 4879 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 / 2))))) =
(𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)))) |
687 | 581, 686 | eqtr2d 2806 |
. . . . . . . . 9
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) = 𝐿) |
688 | 349, 41, 75 | constcncfg 40599 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
689 | | cosf 15060 |
. . . . . . . . . . . . . . . . . . 19
⊢
cos:ℂ⟶ℂ |
690 | 231, 44 | sylan2 580 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ) |
691 | | eqid 2771 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) |
692 | 690, 691 | fmptd 6529 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)):(𝐴(,)𝐵)⟶ℂ) |
693 | | fcompt 6545 |
. . . . . . . . . . . . . . . . . . 19
⊢
((cos:ℂ⟶ℂ ∧ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)):(𝐴(,)𝐵)⟶ℂ) → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))) |
694 | 689, 692,
693 | sylancr 575 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))) |
695 | | eqidd 2772 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) |
696 | 316 | adantl 467 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤)) |
697 | | simpr 471 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 𝑤 ∈ (𝐴(,)𝐵)) |
698 | 695, 696,
697, 329 | fvmptd 6432 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤)) |
699 | 698 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = (cos‘((𝑁 + (1 / 2)) · 𝑤))) |
700 | 699 | mpteq2dva 4879 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤)))) |
701 | 694, 700 | eqtr2d 2806 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))) = (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)))) |
702 | 349, 41, 75 | constcncfg 40599 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
703 | 349, 75 | idcncfg 40600 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 𝑦) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
704 | 702, 703 | mulcncf 23433 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
705 | | coscn 24418 |
. . . . . . . . . . . . . . . . . . 19
⊢ cos
∈ (ℂ–cn→ℂ) |
706 | 705 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → cos ∈
(ℂ–cn→ℂ)) |
707 | 704, 706 | cncfco 22929 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
708 | 701, 707 | eqeltrd 2850 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
709 | 688, 708 | mulcncf 23433 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤)))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
710 | | eqid 2771 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) |
711 | 349, 155,
75 | constcncfg 40599 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ π) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
712 | | 2cnd 11298 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ) |
713 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 2 ≠ 0) |
714 | 328, 712,
713 | divrecd 11009 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 / 2) = (𝑤 · (1 / 2))) |
715 | 714 | mpteq2dva 4879 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 / 2)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 · (1 / 2)))) |
716 | | eqid 2771 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2))) = (𝑤 ∈ ℂ ↦ (𝑤 · (1 /
2))) |
717 | | cncfmptid 22934 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ)) |
718 | 74, 74, 717 | mp2an 672 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ) |
719 | 718 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ)) |
720 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1 / 2)
∈ ℂ → ℂ ⊆ ℂ) |
721 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1 / 2)
∈ ℂ → (1 / 2) ∈ ℂ) |
722 | 720, 721,
720 | constcncfg 40599 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1 / 2)
∈ ℂ → (𝑤
∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ)) |
723 | 39, 722 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (1 / 2)) ∈
(ℂ–cn→ℂ)) |
724 | 719, 723 | mulcncf 23433 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2))) ∈
(ℂ–cn→ℂ)) |
725 | 714, 464 | eqeltrrd 2851 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 · (1 / 2)) ∈
ℂ) |
726 | 716, 724,
349, 75, 725 | cncfmptssg 40598 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 · (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
727 | 715, 726 | eqeltrd 2850 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 / 2)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
728 | 706, 727 | cncfmpt1f 22935 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑤 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
729 | 711, 728 | mulcncf 23433 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
730 | | ssid 3773 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵) |
731 | 730 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)) |
732 | | difssd 3889 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℂ ∖ {0})
⊆ ℂ) |
733 | 660 | adantl 467 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ∈
ℂ) |
734 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → π ∈
ℂ) |
735 | 659 | adantl 467 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘(𝑤 / 2)) ∈ ℂ) |
736 | 238 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → π ≠ 0) |
737 | 597 | adantl 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) = (cos‘(𝑌 / 2))) |
738 | 635 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (cos‘(𝑌 / 2)) ≠ 0) |
739 | 737, 738 | eqnetrd 3010 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0) |
740 | 739 | adantlr 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0) |
741 | 740, 670 | pm2.61dan 814 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘(𝑤 / 2)) ≠ 0) |
742 | 734, 735,
736, 741 | mulne0d 10884 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ≠ 0) |
743 | 742 | neneqd 2948 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ¬ (π ·
(cos‘(𝑤 / 2))) =
0) |
744 | | elsng 4331 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((π
· (cos‘(𝑤 /
2))) ∈ ℂ → ((π · (cos‘(𝑤 / 2))) ∈ {0} ↔ (π ·
(cos‘(𝑤 / 2))) =
0)) |
745 | 733, 744 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((π · (cos‘(𝑤 / 2))) ∈ {0} ↔ (π
· (cos‘(𝑤 /
2))) = 0)) |
746 | 743, 745 | mtbird 314 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ¬ (π ·
(cos‘(𝑤 / 2))) ∈
{0}) |
747 | 733, 746 | eldifd 3734 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ∈ (ℂ ∖
{0})) |
748 | 710, 729,
731, 732, 747 | cncfmptssg 40598 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→(ℂ ∖ {0}))) |
749 | 709, 748 | divcncf 23434 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 / 2)))))
∈ ((𝐴(,)𝐵)–cn→ℂ)) |
750 | 749, 489 | eleqtrd 2852 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 / 2)))))
∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
751 | 581, 750 | eqeltrd 2850 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐿 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
752 | | cncnp 21304 |
. . . . . . . . . . . . 13
⊢
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
(𝐿 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
↔ (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)))) |
753 | 355, 353,
752 | sylancl 574 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
↔ (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)))) |
754 | 751, 753 | mpbid 222 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦))) |
755 | 754 | simprd 483 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
756 | 360 | eleq2d 2836 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑌 → (𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) ↔ 𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌))) |
757 | 756 | rspccva 3459 |
. . . . . . . . . 10
⊢
((∀𝑦 ∈
(𝐴(,)𝐵)𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → 𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
758 | 755, 27, 757 | syl2anc 573 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
759 | 687, 758 | eqeltrd 2850 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
760 | 307 | mpteq1d 4873 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)))) |
761 | 759, 760,
502 | 3eltr4d 2865 |
. . . . . . 7
⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌)) |
762 | | eqid 2771 |
. . . . . . . 8
⊢ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) |
763 | 100 | fvmpt2 6435 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ) →
(𝐻‘𝑦) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) |
764 | 559, 106,
763 | syl2anc 573 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐻‘𝑦) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) |
765 | 764, 561 | oveq12d 6813 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐻‘𝑦) / (𝐼‘𝑦)) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) / (π ·
(cos‘(𝑦 /
2))))) |
766 | 106, 201,
565 | divcld 11006 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) / (π ·
(cos‘(𝑦 / 2))))
∈ ℂ) |
767 | 765, 766 | eqeltrd 2850 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐻‘𝑦) / (𝐼‘𝑦)) ∈ ℂ) |
768 | | eqid 2771 |
. . . . . . . . 9
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) |
769 | 767, 768 | fmptd 6529 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) |
770 | 371, 51, 762, 769, 374, 263 | ellimc 23856 |
. . . . . . 7
⊢ (𝜑 → ((((2 · 𝑁) + 1) / (2 · π))
∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) limℂ 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌))) |
771 | 761, 770 | mpbird 247 |
. . . . . 6
⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π))
∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) limℂ 𝑌)) |
772 | 103 | eqcomd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 = (ℝ D 𝐹)) |
773 | 772 | fveq1d 6335 |
. . . . . . . . 9
⊢ (𝜑 → (𝐻‘𝑦) = ((ℝ D 𝐹)‘𝑦)) |
774 | 199 | eqcomd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 = (ℝ D 𝐺)) |
775 | 774 | fveq1d 6335 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼‘𝑦) = ((ℝ D 𝐺)‘𝑦)) |
776 | 773, 775 | oveq12d 6813 |
. . . . . . . 8
⊢ (𝜑 → ((𝐻‘𝑦) / (𝐼‘𝑦)) = (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) |
777 | 776 | mpteq2dv 4880 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)))) |
778 | 777 | oveq1d 6810 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) limℂ 𝑌) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) limℂ 𝑌)) |
779 | 771, 778 | eleqtrd 2852 |
. . . . 5
⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π))
∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) limℂ 𝑌)) |
780 | 579, 779 | eqeltrd 2850 |
. . . 4
⊢ (𝜑 → if((𝑌 mod (2 · π)) = 0, (((2 ·
𝑁) + 1) / (2 ·
π)), ((sin‘((𝑁 +
(1 / 2)) · 𝑌)) / ((2
· π) · (sin‘(𝑌 / 2))))) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) limℂ 𝑌)) |
781 | 578, 780 | eqeltrd 2850 |
. . 3
⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) limℂ 𝑌)) |
782 | 4, 15, 24, 26, 27, 28, 110, 205, 431, 508, 558, 575, 781 | lhop 23998 |
. 2
⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))) limℂ 𝑌)) |
783 | 576 | dirkerval 40822 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) = (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0,
(((2 · 𝑁) + 1) / (2
· π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) ·
(sin‘(𝑦 /
2))))))) |
784 | 5, 783 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐷‘𝑁) = (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0,
(((2 · 𝑁) + 1) / (2
· π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) ·
(sin‘(𝑦 /
2))))))) |
785 | 784 | reseq1d 5532 |
. . . 4
⊢ (𝜑 → ((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0,
(((2 · 𝑁) + 1) / (2
· π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) ·
(sin‘(𝑦 / 2))))))
↾ ((𝐴(,)𝐵) ∖ {𝑌}))) |
786 | 4 | resmptd 5592 |
. . . 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))))))) |
787 | 256 | iffalsed 4237 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → if((𝑦 mod (2 · π)) = 0, (((2 ·
𝑁) + 1) / (2 ·
π)), ((sin‘((𝑁 +
(1 / 2)) · 𝑦)) / ((2
· π) · (sin‘(𝑦 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) ·
(sin‘(𝑦 /
2))))) |
788 | 13 | recnd 10273 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ) |
789 | 14 | fvmpt2 6435 |
. . . . . . . 8
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ) → (𝐹‘𝑦) = (sin‘((𝑁 + (1 / 2)) · 𝑦))) |
790 | 559, 788,
789 | syl2anc 573 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹‘𝑦) = (sin‘((𝑁 + (1 / 2)) · 𝑦))) |
791 | 559, 505,
527 | syl2anc 573 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐺‘𝑦) = ((2 · π) ·
(sin‘(𝑦 /
2)))) |
792 | 790, 791 | oveq12d 6813 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐹‘𝑦) / (𝐺‘𝑦)) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) ·
(sin‘(𝑦 /
2))))) |
793 | 787, 792 | eqtr4d 2808 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → if((𝑦 mod (2 · π)) = 0, (((2 ·
𝑁) + 1) / (2 ·
π)), ((sin‘((𝑁 +
(1 / 2)) · 𝑦)) / ((2
· π) · (sin‘(𝑦 / 2))))) = ((𝐹‘𝑦) / (𝐺‘𝑦))) |
794 | 793 | mpteq2dva 4879 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ if((𝑦 mod (2 · π)) = 0, (((2 ·
𝑁) + 1) / (2 ·
π)), ((sin‘((𝑁 +
(1 / 2)) · 𝑦)) / ((2
· π) · (sin‘(𝑦 / 2)))))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦)))) |
795 | 785, 786,
794 | 3eqtrrd 2810 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))) = ((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) |
796 | 795 | oveq1d 6810 |
. 2
⊢ (𝜑 → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))) limℂ 𝑌) = (((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) limℂ 𝑌)) |
797 | 782, 796 | eleqtrd 2852 |
1
⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ (((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) limℂ 𝑌)) |