Proof of Theorem dirkercncflem2
Step | Hyp | Ref
| Expression |
1 | | difss 4020 |
. . . . 5
⊢ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ (𝐴(,)𝐵) |
2 | | ioossre 12875 |
. . . . 5
⊢ (𝐴(,)𝐵) ⊆ ℝ |
3 | 1, 2 | sstri 3884 |
. . . 4
⊢ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ |
4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ) |
5 | | dirkercncflem2.n |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
6 | 5 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℕ) |
7 | 6 | nnred 11724 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℝ) |
8 | | halfre 11923 |
. . . . . . . 8
⊢ (1 / 2)
∈ ℝ |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈
ℝ) |
10 | 7, 9 | readdcld 10741 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑁 + (1 / 2)) ∈ ℝ) |
11 | 4 | sselda 3875 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℝ) |
12 | 10, 11 | remulcld 10742 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℝ) |
13 | 12 | resincld 15581 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℝ) |
14 | | dirkercncflem2.f |
. . . 4
⊢ 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) |
15 | 13, 14 | fmptd 6882 |
. . 3
⊢ (𝜑 → 𝐹:((𝐴(,)𝐵) ∖ {𝑌})⟶ℝ) |
16 | | 2re 11783 |
. . . . . . 7
⊢ 2 ∈
ℝ |
17 | | pire 25195 |
. . . . . . 7
⊢ π
∈ ℝ |
18 | 16, 17 | remulcli 10728 |
. . . . . 6
⊢ (2
· π) ∈ ℝ |
19 | 18 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (2 · π) ∈
ℝ) |
20 | 11 | rehalfcld 11956 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℝ) |
21 | 20 | resincld 15581 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ∈ ℝ) |
22 | 19, 21 | remulcld 10742 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((2 · π) ·
(sin‘(𝑦 / 2))) ∈
ℝ) |
23 | | dirkercncflem2.g |
. . . 4
⊢ 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 /
2)))) |
24 | 22, 23 | fmptd 6882 |
. . 3
⊢ (𝜑 → 𝐺:((𝐴(,)𝐵) ∖ {𝑌})⟶ℝ) |
25 | | iooretop 23511 |
. . . 4
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) |
26 | 25 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran
(,))) |
27 | | dirkercncflem2.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ (𝐴(,)𝐵)) |
28 | | eqid 2738 |
. . 3
⊢ ((𝐴(,)𝐵) ∖ {𝑌}) = ((𝐴(,)𝐵) ∖ {𝑌}) |
29 | 14 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) |
30 | 29 | oveq2d 7180 |
. . . . . . 7
⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))) |
31 | | resmpt 5873 |
. . . . . . . . . . . 12
⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) ↾
((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) |
32 | 3, 31 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) ↾
((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) |
33 | 32 | eqcomi 2747 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) |
34 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) |
35 | 34 | oveq2d 7180 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) = (ℝ D ((𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))) |
36 | | ax-resscn 10665 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
37 | 36 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ⊆
ℂ) |
38 | 5 | nncnd 11725 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℂ) |
39 | | halfcn 11924 |
. . . . . . . . . . . . . . 15
⊢ (1 / 2)
∈ ℂ |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 / 2) ∈
ℂ) |
41 | 38, 40 | addcld 10731 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ) |
42 | 41 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑁 + (1 / 2)) ∈ ℂ) |
43 | 37 | sselda 3875 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
44 | 42, 43 | mulcld 10732 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ) |
45 | 44 | sincld 15568 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈
ℂ) |
46 | | eqid 2738 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) = (𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) |
47 | 45, 46 | fmptd 6882 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℝ⟶ℂ) |
48 | | ssid 3897 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℝ |
49 | 48, 3 | pm3.2i 474 |
. . . . . . . . . 10
⊢ (ℝ
⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ) |
50 | 49 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ ⊆ ℝ
∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)) |
51 | | eqid 2738 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
52 | 51 | tgioo2 23548 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
53 | 51, 52 | dvres 24655 |
. . . . . . . . 9
⊢
(((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℝ⟶ℂ)
∧ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)) → (ℝ D
((𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) ↾
((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})))) |
54 | 37, 47, 50, 53 | syl21anc 837 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) ↾
((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})))) |
55 | | retop 23507 |
. . . . . . . . . . 11
⊢
(topGen‘ran (,)) ∈ Top |
56 | | rehaus 23544 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) ∈ Haus |
57 | 27 | elioored 42611 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ∈ ℝ) |
58 | | uniretop 23508 |
. . . . . . . . . . . . . 14
⊢ ℝ =
∪ (topGen‘ran (,)) |
59 | 58 | sncld 22115 |
. . . . . . . . . . . . 13
⊢
(((topGen‘ran (,)) ∈ Haus ∧ 𝑌 ∈ ℝ) → {𝑌} ∈ (Clsd‘(topGen‘ran
(,)))) |
60 | 56, 57, 59 | sylancr 590 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑌} ∈ (Clsd‘(topGen‘ran
(,)))) |
61 | 58 | difopn 21778 |
. . . . . . . . . . . 12
⊢ (((𝐴(,)𝐵) ∈ (topGen‘ran (,)) ∧ {𝑌} ∈
(Clsd‘(topGen‘ran (,)))) → ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran
(,))) |
62 | 25, 60, 61 | sylancr 590 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran
(,))) |
63 | | isopn3i 21826 |
. . . . . . . . . . 11
⊢
(((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ∈ (topGen‘ran (,))) →
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})) = ((𝐴(,)𝐵) ∖ {𝑌})) |
64 | 55, 62, 63 | sylancr 590 |
. . . . . . . . . 10
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})) = ((𝐴(,)𝐵) ∖ {𝑌})) |
65 | 64 | reseq2d 5819 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) ↾
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) |
66 | | reelprrecn 10700 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ {ℝ, ℂ} |
67 | 66 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
68 | 41 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑁 + (1 / 2)) ∈ ℂ) |
69 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ) |
70 | 68, 69 | mulcld 10732 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ) |
71 | 70 | sincld 15568 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈
ℂ) |
72 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) = (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) |
73 | 71, 72 | fmptd 6882 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℂ⟶ℂ) |
74 | | ssid 3897 |
. . . . . . . . . . . . 13
⊢ ℂ
⊆ ℂ |
75 | 74 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂ ⊆
ℂ) |
76 | | dvsinax 42980 |
. . . . . . . . . . . . . . . 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 5742 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) = dom (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑦))))) |
79 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑦)))) = (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑦)))) |
80 | 70 | coscld 15569 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘((𝑁 + (1 / 2)) · 𝑦)) ∈
ℂ) |
81 | 68, 80 | mulcld 10732 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈
ℂ) |
82 | 79, 81 | dmmptd 6476 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = ℂ) |
83 | 78, 82 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) =
ℂ) |
84 | 36, 83 | sseqtrrid 3928 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ⊆ dom
(ℂ D (𝑦 ∈
ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))) |
85 | | dvres3 24657 |
. . . . . . . . . . . 12
⊢
(((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))):ℂ⟶ℂ)
∧ (ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))))) →
(ℝ D ((𝑦 ∈
ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) ↾
ℝ)) |
86 | 67, 73, 75, 84, 85 | syl22anc 838 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) ↾
ℝ)) = ((ℂ D (𝑦
∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ)) |
87 | | resmpt 5873 |
. . . . . . . . . . . . 13
⊢ (ℝ
⊆ ℂ → ((𝑦
∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) |
88 | 36, 87 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) |
89 | 88 | oveq2d 7180 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦))) ↾
ℝ)) = (ℝ D (𝑦
∈ ℝ ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦))))) |
90 | 77 | reseq1d 5818 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) ↾
ℝ) = ((𝑦 ∈
ℂ ↦ ((𝑁 + (1 /
2)) · (cos‘((𝑁
+ (1 / 2)) · 𝑦))))
↾ ℝ)) |
91 | | resmpt 5873 |
. . . . . . . . . . . . 13
⊢ (ℝ
⊆ ℂ → ((𝑦
∈ ℂ ↦ ((𝑁
+ (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))) |
92 | 36, 91 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℂ ↦ ((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑦)))) ↾
ℝ) = (𝑦 ∈
ℝ ↦ ((𝑁 + (1 /
2)) · (cos‘((𝑁
+ (1 / 2)) · 𝑦)))) |
93 | 90, 92 | eqtrdi 2789 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) ↾
ℝ) = (𝑦 ∈
ℝ ↦ ((𝑁 + (1 /
2)) · (cos‘((𝑁
+ (1 / 2)) · 𝑦))))) |
94 | 86, 89, 93 | 3eqtr3d 2781 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) = (𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑦))))) |
95 | 94 | reseq1d 5818 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) ↾
((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) |
96 | | resmpt 5873 |
. . . . . . . . . 10
⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑦)))) ↾
((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))) |
97 | 3, 96 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))) |
98 | 65, 95, 97 | 3eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦
(sin‘((𝑁 + (1 / 2))
· 𝑦)))) ↾
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))) |
99 | 35, 54, 98 | 3eqtrd 2777 |
. . . . . . 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 2744 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) = 𝐻) |
103 | 30, 99, 102 | 3eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → (ℝ D 𝐹) = 𝐻) |
104 | 103 | dmeqd 5742 |
. . . . 5
⊢ (𝜑 → dom (ℝ D 𝐹) = dom 𝐻) |
105 | 11 | recnd 10740 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ℂ) |
106 | 105, 81 | syldan 594 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈
ℂ) |
107 | 100, 106 | dmmptd 6476 |
. . . . 5
⊢ (𝜑 → dom 𝐻 = ((𝐴(,)𝐵) ∖ {𝑌})) |
108 | 104, 107 | eqtr2d 2774 |
. . . 4
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐹)) |
109 | | eqimss 3931 |
. . . 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 5873 |
. . . . . . . . . . . . 13
⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 /
2))))) |
114 | 3, 113 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 /
2)))) |
115 | 114 | eqcomi 2747 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 / 2)))) =
((𝑦 ∈ ℝ ↦
((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) |
116 | 115 | oveq2i 7175 |
. . . . . . . . . 10
⊢ (ℝ
D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 / 2))))) =
(ℝ D ((𝑦 ∈
ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) |
117 | 116 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 / 2))))) =
(ℝ D ((𝑦 ∈
ℝ ↦ ((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})))) |
118 | | 2cn 11784 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
119 | | picn 25196 |
. . . . . . . . . . . . . 14
⊢ π
∈ ℂ |
120 | 118, 119 | mulcli 10719 |
. . . . . . . . . . . . 13
⊢ (2
· π) ∈ ℂ |
121 | 120 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (2 · π)
∈ ℂ) |
122 | 43 | halfcld 11954 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 / 2) ∈ ℂ) |
123 | 122 | sincld 15568 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (sin‘(𝑦 / 2)) ∈
ℂ) |
124 | 121, 123 | mulcld 10732 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((2 · π)
· (sin‘(𝑦 /
2))) ∈ ℂ) |
125 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2)))) = (𝑦 ∈ ℝ ↦ ((2 · π)
· (sin‘(𝑦 /
2)))) |
126 | 124, 125 | fmptd 6882 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ ((2 · π)
· (sin‘(𝑦 /
2)))):ℝ⟶ℂ) |
127 | 51, 52 | dvres 24655 |
. . . . . . . . . 10
⊢
(((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ ((2 · π)
· (sin‘(𝑦 /
2)))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℝ)) → (ℝ D
((𝑦 ∈ ℝ ↦
((2 · π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π)
· (sin‘(𝑦 /
2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})))) |
128 | 37, 126, 50, 127 | syl21anc 837 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2)))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π)
· (sin‘(𝑦 /
2))))) ↾ ((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌})))) |
129 | 64 | reseq2d 5819 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2))))) ↾
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((2 · π)
· (sin‘(𝑦 /
2))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) |
130 | 36 | sseli 3871 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
131 | | 1cnd 10707 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℂ → 1 ∈
ℂ) |
132 | | 2cnd 11787 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℂ → 2 ∈
ℂ) |
133 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
134 | | 2ne0 11813 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ≠
0 |
135 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℂ → 2 ≠
0) |
136 | 131, 132,
133, 135 | div13d 11511 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℂ → ((1 / 2)
· 𝑦) = ((𝑦 / 2) ·
1)) |
137 | | halfcl 11934 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℂ → (𝑦 / 2) ∈
ℂ) |
138 | 137 | mulid1d 10729 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℂ → ((𝑦 / 2) · 1) = (𝑦 / 2)) |
139 | 136, 138 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℂ → ((1 / 2)
· 𝑦) = (𝑦 / 2)) |
140 | 139 | fveq2d 6672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℂ →
(sin‘((1 / 2) · 𝑦)) = (sin‘(𝑦 / 2))) |
141 | 140 | oveq2d 7180 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℂ → ((2
· π) · (sin‘((1 / 2) · 𝑦))) = ((2 · π) ·
(sin‘(𝑦 /
2)))) |
142 | 141 | eqcomd 2744 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℂ → ((2
· π) · (sin‘(𝑦 / 2))) = ((2 · π) ·
(sin‘((1 / 2) · 𝑦)))) |
143 | 130, 142 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ → ((2
· π) · (sin‘(𝑦 / 2))) = ((2 · π) ·
(sin‘((1 / 2) · 𝑦)))) |
144 | 143 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((2 · π)
· (sin‘(𝑦 /
2))) = ((2 · π) · (sin‘((1 / 2) · 𝑦)))) |
145 | 144 | mpteq2dva 5122 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ ((2 · π)
· (sin‘(𝑦 /
2)))) = (𝑦 ∈ ℝ
↦ ((2 · π) · (sin‘((1 / 2) · 𝑦))))) |
146 | 145 | oveq2d 7180 |
. . . . . . . . . . . 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 10732 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((1 / 2) ·
𝑦) ∈
ℂ) |
150 | 149 | sincld 15568 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (sin‘((1 / 2)
· 𝑦)) ∈
ℂ) |
151 | 147, 150 | mulcld 10732 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · π)
· (sin‘((1 / 2) · 𝑦))) ∈ ℂ) |
152 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦)))) = (𝑦 ∈ ℂ ↦ ((2 · π)
· (sin‘((1 / 2) · 𝑦)))) |
153 | 151, 152 | fmptd 6882 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ ((2 · π)
· (sin‘((1 / 2) · 𝑦)))):ℂ⟶ℂ) |
154 | | 2cnd 11787 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 2 ∈
ℂ) |
155 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → π ∈
ℂ) |
156 | 154, 155 | mulcld 10732 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (2 · π) ∈
ℂ) |
157 | | dvasinbx 42987 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((2
· π) ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D
(𝑦 ∈ ℂ ↦
((2 · π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (((2 · π)
· (1 / 2)) · (cos‘((1 / 2) · 𝑦))))) |
158 | 156, 39, 157 | sylancl 589 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (((2 · π)
· (1 / 2)) · (cos‘((1 / 2) · 𝑦))))) |
159 | | 2cnd 11787 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 2 ∈
ℂ) |
160 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → π ∈
ℂ) |
161 | 159, 160,
148 | mul32d 10921 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · π)
· (1 / 2)) = ((2 · (1 / 2)) · π)) |
162 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 2 ≠
0) |
163 | 159, 162 | recidd 11482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (2 · (1 / 2))
= 1) |
164 | 163 | oveq1d 7179 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · (1 / 2))
· π) = (1 · π)) |
165 | 160 | mulid2d 10730 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (1 · π) =
π) |
166 | 161, 164,
165 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((2 · π)
· (1 / 2)) = π) |
167 | 139 | fveq2d 6672 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ℂ →
(cos‘((1 / 2) · 𝑦)) = (cos‘(𝑦 / 2))) |
168 | 167 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘((1 / 2)
· 𝑦)) =
(cos‘(𝑦 /
2))) |
169 | 166, 168 | oveq12d 7182 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((2 · π)
· (1 / 2)) · (cos‘((1 / 2) · 𝑦))) = (π · (cos‘(𝑦 / 2)))) |
170 | 169 | mpteq2dva 5122 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (((2 · π)
· (1 / 2)) · (cos‘((1 / 2) · 𝑦)))) = (𝑦 ∈ ℂ ↦ (π ·
(cos‘(𝑦 /
2))))) |
171 | 158, 170 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℂ ↦ (π ·
(cos‘(𝑦 /
2))))) |
172 | 171 | dmeqd 5742 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) = dom (𝑦 ∈ ℂ ↦ (π ·
(cos‘(𝑦 /
2))))) |
173 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℂ ↦ (π
· (cos‘(𝑦 /
2)))) = (𝑦 ∈ ℂ
↦ (π · (cos‘(𝑦 / 2)))) |
174 | 69 | halfcld 11954 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑦 / 2) ∈ ℂ) |
175 | 174 | coscld 15569 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘(𝑦 / 2)) ∈
ℂ) |
176 | 160, 175 | mulcld 10732 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (π ·
(cos‘(𝑦 / 2))) ∈
ℂ) |
177 | 173, 176 | dmmptd 6476 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (𝑦 ∈ ℂ ↦ (π ·
(cos‘(𝑦 / 2)))) =
ℂ) |
178 | 172, 177 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) = ℂ) |
179 | 36, 178 | sseqtrrid 3928 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ℝ ⊆ dom
(ℂ D (𝑦 ∈
ℂ ↦ ((2 · π) · (sin‘((1 / 2) · 𝑦)))))) |
180 | | dvres3 24657 |
. . . . . . . . . . . . . . 15
⊢
(((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ ((2 · π)
· (sin‘((1 / 2) · 𝑦)))):ℂ⟶ℂ) ∧ (ℂ
⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ ((2 · π)
· (sin‘((1 / 2) · 𝑦))))))) → (ℝ D ((𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ)) |
181 | 67, 153, 75, 179, 180 | syl22anc 838 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ)) |
182 | | resmpt 5873 |
. . . . . . . . . . . . . . . 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 7180 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦)))) ↾ ℝ)) = (ℝ D (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦)))))) |
185 | 171 | reseq1d 5818 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) ↾ ℝ) = ((𝑦 ∈ ℂ ↦ (π ·
(cos‘(𝑦 / 2))))
↾ ℝ)) |
186 | 181, 184,
185 | 3eqtr3d 2781 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) = ((𝑦 ∈ ℂ ↦ (π ·
(cos‘(𝑦 / 2))))
↾ ℝ)) |
187 | | resmpt 5873 |
. . . . . . . . . . . . . 14
⊢ (ℝ
⊆ ℂ → ((𝑦
∈ ℂ ↦ (π · (cos‘(𝑦 / 2)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (π
· (cos‘(𝑦 /
2))))) |
188 | 36, 187 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℂ ↦ (π
· (cos‘(𝑦 /
2)))) ↾ ℝ) = (𝑦
∈ ℝ ↦ (π · (cos‘(𝑦 / 2)))) |
189 | 186, 188 | eqtrdi 2789 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘((1 / 2) · 𝑦))))) = (𝑦 ∈ ℝ ↦ (π ·
(cos‘(𝑦 /
2))))) |
190 | 146, 189 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2))))) = (𝑦 ∈ ℝ ↦ (π ·
(cos‘(𝑦 /
2))))) |
191 | 190 | reseq1d 5818 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2))))) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ (π ·
(cos‘(𝑦 / 2))))
↾ ((𝐴(,)𝐵) ∖ {𝑌}))) |
192 | 4 | resmptd 5876 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (π ·
(cos‘(𝑦 / 2))))
↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2))))) |
193 | 129, 191,
192 | 3eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ ((2
· π) · (sin‘(𝑦 / 2))))) ↾
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∖ {𝑌}))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2))))) |
194 | 117, 128,
193 | 3eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 / 2))))) =
(𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2))))) |
195 | 194 | eqcomd 2744 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2)))) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 /
2)))))) |
196 | 23 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 /
2))))) |
197 | 196 | oveq2d 7180 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐺) = (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 /
2)))))) |
198 | 197 | eqcomd 2744 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) ·
(sin‘(𝑦 / 2))))) =
(ℝ D 𝐺)) |
199 | 112, 195,
198 | 3eqtrrd 2778 |
. . . . . 6
⊢ (𝜑 → (ℝ D 𝐺) = 𝐼) |
200 | 199 | dmeqd 5742 |
. . . . 5
⊢ (𝜑 → dom (ℝ D 𝐺) = dom 𝐼) |
201 | 105, 176 | syldan 594 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (π · (cos‘(𝑦 / 2))) ∈
ℂ) |
202 | 111, 201 | dmmptd 6476 |
. . . . 5
⊢ (𝜑 → dom 𝐼 = ((𝐴(,)𝐵) ∖ {𝑌})) |
203 | 200, 202 | eqtr2d 2774 |
. . . 4
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐺)) |
204 | | eqimss 3931 |
. . . 4
⊢ (((𝐴(,)𝐵) ∖ {𝑌}) = dom (ℝ D 𝐺) → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐺)) |
205 | 203, 204 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ dom (ℝ D 𝐺)) |
206 | 105, 70 | syldan 594 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ) |
207 | 206 | ralrimiva 3096 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ) |
208 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) |
209 | 208 | fnmpt 6471 |
. . . . . . 7
⊢
(∀𝑦 ∈
((𝐴(,)𝐵) ∖ {𝑌})((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌})) |
210 | 207, 209 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌})) |
211 | | eqidd 2739 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) |
212 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤) |
213 | 212 | oveq2d 7180 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤)) |
214 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) |
215 | 38 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑁 ∈ ℂ) |
216 | | 1cnd 10707 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 1 ∈
ℂ) |
217 | 216 | halfcld 11954 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (1 / 2) ∈
ℂ) |
218 | 215, 217 | addcld 10731 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑁 + (1 / 2)) ∈ ℂ) |
219 | | eldifi 4015 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ (𝐴(,)𝐵)) |
220 | 219 | elioored 42611 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ ℝ) |
221 | 220 | recnd 10740 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑤 ∈ ℂ) |
222 | 221 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑤 ∈ ℂ) |
223 | 218, 222 | mulcld 10732 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ) |
224 | 211, 213,
214, 223 | fvmptd 6776 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤)) |
225 | | eleq1w 2815 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑤 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↔ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}))) |
226 | 225 | anbi2d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑤 → ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ↔ (𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})))) |
227 | | oveq1 7171 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑤 → (𝑦 mod (2 · π)) = (𝑤 mod (2 · π))) |
228 | 227 | neeq1d 2993 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑤 → ((𝑦 mod (2 · π)) ≠ 0 ↔ (𝑤 mod (2 · π)) ≠
0)) |
229 | 226, 228 | imbi12d 348 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 → (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 mod (2 · π)) ≠ 0) ↔
((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑤 mod (2 · π)) ≠
0))) |
230 | | eldifi 4015 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ (𝐴(,)𝐵)) |
231 | | elioore 12844 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ (𝐴(,)𝐵) → 𝑦 ∈ ℝ) |
232 | 230, 231,
130 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 𝑦 ∈ ℂ) |
233 | | 2cnd 11787 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 2 ∈ ℂ) |
234 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → π ∈
ℂ) |
235 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → 2 ≠ 0) |
236 | | 0re 10714 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℝ |
237 | | pipos 25197 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 <
π |
238 | 236, 237 | gtneii 10823 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ π ≠
0 |
239 | 238 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → π ≠ 0) |
240 | 232, 233,
234, 235, 239 | divdiv1d 11518 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → ((𝑦 / 2) / π) = (𝑦 / (2 · π))) |
241 | 240 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π)) |
242 | 241 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π)) |
243 | | dirkercncflem2.yne0 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ≠ 0) |
244 | 243 | neneqd 2939 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (sin‘(𝑦 / 2)) = 0) |
245 | 105 | halfcld 11954 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / 2) ∈ ℂ) |
246 | | sineq0 25260 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 / 2) ∈ ℂ →
((sin‘(𝑦 / 2)) = 0
↔ ((𝑦 / 2) / π)
∈ ℤ)) |
247 | 245, 246 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈
ℤ)) |
248 | 244, 247 | mtbid 327 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑦 / 2) / π) ∈
ℤ) |
249 | 242, 248 | eqneltrd 2852 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 / (2 · π)) ∈
ℤ) |
250 | | 2rp 12470 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ+ |
251 | | pirp 25198 |
. . . . . . . . . . . . . . . . . 18
⊢ π
∈ ℝ+ |
252 | | rpmulcl 12488 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℝ+ ∧ π ∈ ℝ+) → (2
· π) ∈ ℝ+) |
253 | 250, 251,
252 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (2
· π) ∈ ℝ+ |
254 | | mod0 13328 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ ∧ (2
· π) ∈ ℝ+) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈
ℤ)) |
255 | 11, 253, 254 | sylancl 589 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈
ℤ)) |
256 | 249, 255 | mtbird 328 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑦 mod (2 · π)) = 0) |
257 | 256 | neqned 2941 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 mod (2 · π)) ≠
0) |
258 | 229, 257 | chvarvv 2009 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑤 mod (2 · π)) ≠
0) |
259 | 258 | neneqd 2939 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝑤 mod (2 · π)) = 0) |
260 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝜑) |
261 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) |
262 | 221 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑤 ∈ ℂ) |
263 | 57 | recnd 10740 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑌 ∈ ℂ) |
264 | 263 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑌 ∈ ℂ) |
265 | | 0red 10715 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ∈
ℝ) |
266 | 5 | nnred 11724 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℝ) |
267 | | 1red 10713 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ∈
ℝ) |
268 | 267 | rehalfcld 11956 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
269 | 266, 268 | readdcld 10741 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ) |
270 | 5 | nngt0d 11758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 < 𝑁) |
271 | 250 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 2 ∈
ℝ+) |
272 | 271 | rpreccld 12517 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 / 2) ∈
ℝ+) |
273 | 266, 272 | ltaddrpd 12540 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 < (𝑁 + (1 / 2))) |
274 | 265, 266,
269, 270, 273 | lttrd 10872 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 < (𝑁 + (1 / 2))) |
275 | 274 | gt0ne0d 11275 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 + (1 / 2)) ≠ 0) |
276 | 41, 275 | jca 515 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠
0)) |
277 | 276 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → ((𝑁 + (1 / 2)) ∈ ℂ ∧ (𝑁 + (1 / 2)) ≠
0)) |
278 | | mulcan 11348 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ ((𝑁 + (1 / 2)) ∈ ℂ ∧
(𝑁 + (1 / 2)) ≠ 0))
→ (((𝑁 + (1 / 2))
· 𝑤) = ((𝑁 + (1 / 2)) · 𝑌) ↔ 𝑤 = 𝑌)) |
279 | 262, 264,
277, 278 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → (((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌) ↔ 𝑤 = 𝑌)) |
280 | 261, 279 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → 𝑤 = 𝑌) |
281 | | oveq1 7171 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑌 → (𝑤 mod (2 · π)) = (𝑌 mod (2 · π))) |
282 | | dirkercncflem2.ymod |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 mod (2 · π)) =
0) |
283 | 281, 282 | sylan9eqr 2795 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (𝑤 mod (2 · π)) = 0) |
284 | 260, 280,
283 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) → (𝑤 mod (2 · π)) = 0) |
285 | 259, 284 | mtand 816 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) |
286 | 41, 263 | mulcld 10732 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ) |
287 | 286 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑌) ∈ ℂ) |
288 | | elsn2g 4551 |
. . . . . . . . . . . 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 328 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ ((𝑁 + (1 / 2)) · 𝑤) ∈ {((𝑁 + (1 / 2)) · 𝑌)}) |
291 | 223, 290 | eldifd 3852 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑁 + (1 / 2)) · 𝑤) ∈ (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)})) |
292 | 224, 291 | eqeltrd 2833 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)})) |
293 | | sinf 15562 |
. . . . . . . . . . . 12
⊢
sin:ℂ⟶ℂ |
294 | 293 | fdmi 6510 |
. . . . . . . . . . 11
⊢ dom sin =
ℂ |
295 | 294 | eqcomi 2747 |
. . . . . . . . . 10
⊢ ℂ =
dom sin |
296 | 295 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ℂ = dom
sin) |
297 | 296 | difeq1d 4010 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (ℂ ∖ {((𝑁 + (1 / 2)) · 𝑌)}) = (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) |
298 | 292, 297 | eleqtrd 2835 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) |
299 | 298 | ralrimiva 3096 |
. . . . . 6
⊢ (𝜑 → ∀𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) |
300 | | fnfvrnss 6888 |
. . . . . 6
⊢ (((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) Fn ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ∀𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) ∈ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) → ran (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ⊆ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) |
301 | 210, 299,
300 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → ran (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ⊆ (dom sin ∖ {((𝑁 + (1 / 2)) · 𝑌)})) |
302 | | uncom 4041 |
. . . . . . . . . 10
⊢ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) |
303 | 302 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌}))) |
304 | 27 | snssd 4694 |
. . . . . . . . . 10
⊢ (𝜑 → {𝑌} ⊆ (𝐴(,)𝐵)) |
305 | | undif 4368 |
. . . . . . . . . 10
⊢ ({𝑌} ⊆ (𝐴(,)𝐵) ↔ ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐴(,)𝐵)) |
306 | 304, 305 | sylib 221 |
. . . . . . . . 9
⊢ (𝜑 → ({𝑌} ∪ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐴(,)𝐵)) |
307 | 303, 306 | eqtrd 2773 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) = (𝐴(,)𝐵)) |
308 | 307 | mpteq1d 5116 |
. . . . . . 7
⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))) |
309 | | iftrue 4417 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑌)) |
310 | | oveq2 7172 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑌 → ((𝑁 + (1 / 2)) · 𝑤) = ((𝑁 + (1 / 2)) · 𝑌)) |
311 | 309, 310 | eqtr4d 2776 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤)) |
312 | 311 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤)) |
313 | | iffalse 4420 |
. . . . . . . . . . . . 13
⊢ (¬
𝑤 = 𝑌 → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) |
314 | 313 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) |
315 | | eqidd 2739 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) |
316 | | oveq2 7172 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤)) |
317 | 316 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤)) |
318 | | simpl 486 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ (𝐴(,)𝐵)) |
319 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑤 = 𝑌 → ¬ 𝑤 = 𝑌) |
320 | | velsn 4529 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ {𝑌} ↔ 𝑤 = 𝑌) |
321 | 319, 320 | sylnibr 332 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑤 = 𝑌 → ¬ 𝑤 ∈ {𝑌}) |
322 | 321 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → ¬ 𝑤 ∈ {𝑌}) |
323 | 318, 322 | eldifd 3852 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ (𝐴(,)𝐵) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) |
324 | 323 | adantll 714 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) |
325 | 41 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑁 + (1 / 2)) ∈ ℂ) |
326 | | elioore 12844 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ (𝐴(,)𝐵) → 𝑤 ∈ ℝ) |
327 | 326 | recnd 10740 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ (𝐴(,)𝐵) → 𝑤 ∈ ℂ) |
328 | 327 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 𝑤 ∈ ℂ) |
329 | 325, 328 | mulcld 10732 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ) |
330 | 329 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) · 𝑤) ∈ ℂ) |
331 | 315, 317,
324, 330 | fvmptd 6776 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤)) |
332 | 314, 331 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤)) |
333 | 312, 332 | pm2.61dan 813 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = ((𝑁 + (1 / 2)) · 𝑤)) |
334 | 333 | mpteq2dva 5122 |
. . . . . . . . 9
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤))) |
335 | | ioosscn 12876 |
. . . . . . . . . . . . . 14
⊢ (𝐴(,)𝐵) ⊆ ℂ |
336 | | resmpt 5873 |
. . . . . . . . . . . . . 14
⊢ ((𝐴(,)𝐵) ⊆ ℂ → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤))) |
337 | 335, 336 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) |
338 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) = (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) |
339 | 338 | mulc1cncf 23650 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 + (1 / 2)) ∈ ℂ
→ (𝑤 ∈ ℂ
↦ ((𝑁 + (1 / 2))
· 𝑤)) ∈
(ℂ–cn→ℂ)) |
340 | 41, 339 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈ (ℂ–cn→ℂ)) |
341 | 51 | cnfldtop 23529 |
. . . . . . . . . . . . . . . . . . 19
⊢
(TopOpen‘ℂfld) ∈ Top |
342 | | unicntop 23531 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
343 | 342 | restid 16803 |
. . . . . . . . . . . . . . . . . . 19
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
344 | 341, 343 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
345 | 344 | eqcomi 2747 |
. . . . . . . . . . . . . . . . 17
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
346 | 51, 345, 345 | cncfcn 23655 |
. . . . . . . . . . . . . . . 16
⊢ ((ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℂ) =
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
347 | 74, 75, 346 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℂ–cn→ℂ) =
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
348 | 340, 347 | eleqtrd 2835 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
349 | 2, 37 | sstrid 3886 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
350 | 342 | cnrest 22029 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) ∧ (𝐴(,)𝐵) ⊆ ℂ) → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
351 | 348, 349,
350 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑤 ∈ ℂ ↦ ((𝑁 + (1 / 2)) · 𝑤)) ↾ (𝐴(,)𝐵)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
352 | 337, 351 | eqeltrrid 2838 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
353 | 51 | cnfldtopon 23528 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
354 | | resttopon 21905 |
. . . . . . . . . . . . . 14
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (𝐴(,)𝐵) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵))) |
355 | 353, 349,
354 | sylancr 590 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵))) |
356 | | cncnp 22024 |
. . . . . . . . . . . . 13
⊢
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
↔ ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)))) |
357 | 355, 353,
356 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
↔ ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)))) |
358 | 352, 357 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)):(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦))) |
359 | 358 | simprd 499 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
360 | | fveq2 6668 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑌 →
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
361 | 360 | eleq2d 2818 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑌 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌))) |
362 | 361 | rspccva 3523 |
. . . . . . . . . 10
⊢
((∀𝑦 ∈
(𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
363 | 359, 27, 362 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑤)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
364 | 334, 363 | eqeltrd 2833 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
365 | 307 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,)𝐵) = (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) |
366 | 365 | oveq2d 7180 |
. . . . . . . . . 10
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld)
↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}))) |
367 | 366 | oveq1d 7179 |
. . . . . . . . 9
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld)) =
(((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))) |
368 | 367 | fveq1d 6670 |
. . . . . . . 8
⊢ (𝜑 →
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌) = ((((TopOpen‘ℂfld)
↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌)) |
369 | 364, 368 | eleqtrd 2835 |
. . . . . . 7
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌)) |
370 | 308, 369 | eqeltrd 2833 |
. . . . . 6
⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌)) |
371 | | eqid 2738 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) = ((TopOpen‘ℂfld)
↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) |
372 | | eqid 2738 |
. . . . . . 7
⊢ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) |
373 | 206, 208 | fmptd 6882 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) |
374 | 4, 36 | sstrdi 3887 |
. . . . . . 7
⊢ (𝜑 → ((𝐴(,)𝐵) ∖ {𝑌}) ⊆ ℂ) |
375 | 371, 51, 372, 373, 374, 263 | ellimc 24617 |
. . . . . 6
⊢ (𝜑 → (((𝑁 + (1 / 2)) · 𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)) limℂ 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, ((𝑁 + (1 / 2)) · 𝑌), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌))) |
376 | 370, 375 | mpbird 260 |
. . . . 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 11363 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · π) ≠
0) |
380 | 263, 156,
379 | divcan1d 11488 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 / (2 · π)) · (2 ·
π)) = 𝑌) |
381 | 380 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 = ((𝑌 / (2 · π)) · (2 ·
π))) |
382 | 381 | oveq2d 7180 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 ·
π)))) |
383 | 382 | fveq2d 6672 |
. . . . . . 7
⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) = (sin‘((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) ·
(2 · π))))) |
384 | 263, 156,
379 | divcld 11487 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 / (2 · π)) ∈
ℂ) |
385 | 41, 384, 156 | mul12d 10920 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 ·
π))) = ((𝑌 / (2 ·
π)) · ((𝑁 + (1 /
2)) · (2 · π)))) |
386 | 41, 154, 155 | mulassd 10735 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑁 + (1 / 2)) · 2) · π) =
((𝑁 + (1 / 2)) · (2
· π))) |
387 | 386 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 + (1 / 2)) · (2 · π)) =
(((𝑁 + (1 / 2)) · 2)
· π)) |
388 | 387 | oveq2d 7180 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 / (2 · π)) · ((𝑁 + (1 / 2)) · (2 ·
π))) = ((𝑌 / (2 ·
π)) · (((𝑁 + (1 /
2)) · 2) · π))) |
389 | 38, 40, 154 | adddird 10737 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 2) = ((𝑁 · 2) + ((1 / 2) ·
2))) |
390 | 154, 377 | recid2d 11483 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((1 / 2) · 2) =
1) |
391 | 390 | oveq2d 7180 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 · 2) + ((1 / 2) · 2)) =
((𝑁 · 2) +
1)) |
392 | 389, 391 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 2) = ((𝑁 · 2) +
1)) |
393 | 392 | oveq1d 7179 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 + (1 / 2)) · 2) · π) =
(((𝑁 · 2) + 1)
· π)) |
394 | 393 | oveq2d 7180 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 / (2 · π)) · (((𝑁 + (1 / 2)) · 2) ·
π)) = ((𝑌 / (2 ·
π)) · (((𝑁
· 2) + 1) · π))) |
395 | 385, 388,
394 | 3eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 ·
π))) = ((𝑌 / (2 ·
π)) · (((𝑁
· 2) + 1) · π))) |
396 | 38, 154 | mulcld 10732 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 · 2) ∈
ℂ) |
397 | | 1cnd 10707 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℂ) |
398 | 396, 397 | addcld 10731 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 · 2) + 1) ∈
ℂ) |
399 | 384, 398,
155 | mulassd 10735 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ·
π) = ((𝑌 / (2 ·
π)) · (((𝑁
· 2) + 1) · π))) |
400 | 395, 399 | eqtr4d 2776 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) · (2 ·
π))) = (((𝑌 / (2
· π)) · ((𝑁 · 2) + 1)) ·
π)) |
401 | 400 | fveq2d 6672 |
. . . . . . 7
⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · ((𝑌 / (2 · π)) ·
(2 · π)))) = (sin‘(((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ·
π))) |
402 | | mod0 13328 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ ℝ ∧ (2
· π) ∈ ℝ+) → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈
ℤ)) |
403 | 57, 253, 402 | sylancl 589 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 mod (2 · π)) = 0 ↔ (𝑌 / (2 · π)) ∈
ℤ)) |
404 | 282, 403 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 / (2 · π)) ∈
ℤ) |
405 | 5 | nnzd 12160 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℤ) |
406 | | 2z 12088 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
407 | 406 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℤ) |
408 | 405, 407 | zmulcld 12167 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 · 2) ∈
ℤ) |
409 | 408 | peano2zd 12164 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 · 2) + 1) ∈
ℤ) |
410 | 404, 409 | zmulcld 12167 |
. . . . . . . 8
⊢ (𝜑 → ((𝑌 / (2 · π)) · ((𝑁 · 2) + 1)) ∈
ℤ) |
411 | | sinkpi 25258 |
. . . . . . . 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 2777 |
. . . . . 6
⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) = 0) |
414 | | sincn 25183 |
. . . . . . . 8
⊢ sin
∈ (ℂ–cn→ℂ) |
415 | 414 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → sin ∈
(ℂ–cn→ℂ)) |
416 | 415, 286 | cnlimci 24633 |
. . . . . 6
⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝑌)) ∈ (sin
limℂ ((𝑁 +
(1 / 2)) · 𝑌))) |
417 | 413, 416 | eqeltrrd 2834 |
. . . . 5
⊢ (𝜑 → 0 ∈ (sin
limℂ ((𝑁 +
(1 / 2)) · 𝑌))) |
418 | 301, 376,
417 | limccog 42687 |
. . . 4
⊢ (𝜑 → 0 ∈ ((sin ∘
(𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) limℂ 𝑌)) |
419 | 14 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))) |
420 | 213 | fveq2d 6672 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ 𝑦 = 𝑤) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) = (sin‘((𝑁 + (1 / 2)) · 𝑤))) |
421 | 223 | sincld 15568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑤)) ∈ ℂ) |
422 | 419, 420,
214, 421 | fvmptd 6776 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹‘𝑤) = (sin‘((𝑁 + (1 / 2)) · 𝑤))) |
423 | 224 | fveq2d 6672 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = (sin‘((𝑁 + (1 / 2)) · 𝑤))) |
424 | 422, 423 | eqtr4d 2776 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹‘𝑤) = (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) |
425 | 424 | mpteq2dva 5122 |
. . . . . 6
⊢ (𝜑 → (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (𝐹‘𝑤)) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))) |
426 | 15 | feqmptd 6731 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (𝐹‘𝑤))) |
427 | | fcompt 6899 |
. . . . . . 7
⊢
((sin:ℂ⟶ℂ ∧ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦)):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) → (sin ∘
(𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))) |
428 | 293, 373,
427 | sylancr 590 |
. . . . . 6
⊢ (𝜑 → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))) |
429 | 425, 426,
428 | 3eqtr4rd 2784 |
. . . . 5
⊢ (𝜑 → (sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = 𝐹) |
430 | 429 | oveq1d 7179 |
. . . 4
⊢ (𝜑 → ((sin ∘ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · 𝑦))) limℂ 𝑌) = (𝐹 limℂ 𝑌)) |
431 | 418, 430 | eleqtrd 2835 |
. . 3
⊢ (𝜑 → 0 ∈ (𝐹 limℂ 𝑌)) |
432 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → 𝑤 = 𝑌) |
433 | 432 | iftrued 4419 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = 0) |
434 | 263, 154,
156, 377, 379 | divdiv32d 11512 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑌 / 2) / (2 · π)) = ((𝑌 / (2 · π)) /
2)) |
435 | 434 | oveq1d 7179 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑌 / 2) / (2 · π)) · (2
· π)) = (((𝑌 / (2
· π)) / 2) · (2 · π))) |
436 | 263 | halfcld 11954 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑌 / 2) ∈ ℂ) |
437 | 436, 156,
379 | divcan1d 11488 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑌 / 2) / (2 · π)) · (2
· π)) = (𝑌 /
2)) |
438 | 384, 154,
156, 377 | div32d 11510 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑌 / (2 · π)) / 2) · (2
· π)) = ((𝑌 / (2
· π)) · ((2 · π) / 2))) |
439 | 155, 154,
377 | divcan3d 11492 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2 · π) / 2) =
π) |
440 | 439 | oveq2d 7180 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑌 / (2 · π)) · ((2 ·
π) / 2)) = ((𝑌 / (2
· π)) · π)) |
441 | 438, 440 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑌 / (2 · π)) / 2) · (2
· π)) = ((𝑌 / (2
· π)) · π)) |
442 | 435, 437,
441 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑌 / 2) = ((𝑌 / (2 · π)) ·
π)) |
443 | 442 | fveq2d 6672 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (sin‘(𝑌 / 2)) = (sin‘((𝑌 / (2 · π)) ·
π))) |
444 | | sinkpi 25258 |
. . . . . . . . . . . . . . 15
⊢ ((𝑌 / (2 · π)) ∈
ℤ → (sin‘((𝑌 / (2 · π)) · π)) =
0) |
445 | 404, 444 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (sin‘((𝑌 / (2 · π)) ·
π)) = 0) |
446 | 443, 445 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (sin‘(𝑌 / 2)) = 0) |
447 | 446 | oveq2d 7180 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · π)
· (sin‘(𝑌 /
2))) = ((2 · π) · 0)) |
448 | 156 | mul01d 10910 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · π)
· 0) = 0) |
449 | 447, 448 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · π)
· (sin‘(𝑌 /
2))) = 0) |
450 | 449 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (𝜑 → 0 = ((2 · π)
· (sin‘(𝑌 /
2)))) |
451 | 450 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → 0 = ((2 · π) ·
(sin‘(𝑌 /
2)))) |
452 | | fvoveq1 7187 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑌 → (sin‘(𝑤 / 2)) = (sin‘(𝑌 / 2))) |
453 | 452 | oveq2d 7180 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑌 → ((2 · π) ·
(sin‘(𝑤 / 2))) = ((2
· π) · (sin‘(𝑌 / 2)))) |
454 | 453 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑌 → ((2 · π) ·
(sin‘(𝑌 / 2))) = ((2
· π) · (sin‘(𝑤 / 2)))) |
455 | 454 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → ((2 · π) ·
(sin‘(𝑌 / 2))) = ((2
· π) · (sin‘(𝑤 / 2)))) |
456 | 433, 451,
455 | 3eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = ((2 · π) ·
(sin‘(𝑤 /
2)))) |
457 | | iffalse 4420 |
. . . . . . . . . 10
⊢ (¬
𝑤 = 𝑌 → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = (𝐺‘𝑤)) |
458 | 457 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = (𝐺‘𝑤)) |
459 | | fvoveq1 7187 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → (sin‘(𝑦 / 2)) = (sin‘(𝑤 / 2))) |
460 | 459 | oveq2d 7180 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑤 → ((2 · π) ·
(sin‘(𝑦 / 2))) = ((2
· π) · (sin‘(𝑤 / 2)))) |
461 | 120 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (2 · π) ∈
ℂ) |
462 | 328 | halfcld 11954 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 / 2) ∈ ℂ) |
463 | 462 | sincld 15568 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (sin‘(𝑤 / 2)) ∈ ℂ) |
464 | 461, 463 | mulcld 10732 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((2 · π) ·
(sin‘(𝑤 / 2))) ∈
ℂ) |
465 | 464 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((2 · π) ·
(sin‘(𝑤 / 2))) ∈
ℂ) |
466 | 23, 460, 324, 465 | fvmptd3 6792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐺‘𝑤) = ((2 · π) ·
(sin‘(𝑤 /
2)))) |
467 | 458, 466 | eqtrd 2773 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = ((2 · π) ·
(sin‘(𝑤 /
2)))) |
468 | 456, 467 | pm2.61dan 813 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → if(𝑤 = 𝑌, 0, (𝐺‘𝑤)) = ((2 · π) ·
(sin‘(𝑤 /
2)))) |
469 | 468 | mpteq2dva 5122 |
. . . . . 6
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 /
2))))) |
470 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℂ ↦ ((2
· π) · (sin‘(𝑤 / 2)))) = (𝑤 ∈ ℂ ↦ ((2 · π)
· (sin‘(𝑤 /
2)))) |
471 | 75, 156, 75 | constcncfg 42939 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (2 · π))
∈ (ℂ–cn→ℂ)) |
472 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ → 𝑤 ∈
ℂ) |
473 | | 2cnd 11787 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ → 2 ∈
ℂ) |
474 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ → 2 ≠
0) |
475 | 472, 473,
474 | divrec2d 11491 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℂ → (𝑤 / 2) = ((1 / 2) · 𝑤)) |
476 | 475 | mpteq2ia 5118 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℂ ↦ (𝑤 / 2)) = (𝑤 ∈ ℂ ↦ ((1 / 2) ·
𝑤)) |
477 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℂ ↦ ((1 / 2)
· 𝑤)) = (𝑤 ∈ ℂ ↦ ((1 / 2)
· 𝑤)) |
478 | 477 | mulc1cncf 23650 |
. . . . . . . . . . . . . . . 16
⊢ ((1 / 2)
∈ ℂ → (𝑤
∈ ℂ ↦ ((1 / 2) · 𝑤)) ∈ (ℂ–cn→ℂ)) |
479 | 39, 478 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℂ ↦ ((1 / 2)
· 𝑤)) ∈
(ℂ–cn→ℂ) |
480 | 476, 479 | eqeltri 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℂ ↦ (𝑤 / 2)) ∈
(ℂ–cn→ℂ) |
481 | 480 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (𝑤 / 2)) ∈ (ℂ–cn→ℂ)) |
482 | 415, 481 | cncfmpt1f 23659 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (sin‘(𝑤 / 2))) ∈
(ℂ–cn→ℂ)) |
483 | 471, 482 | mulcncf 24191 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ ((2 · π)
· (sin‘(𝑤 /
2)))) ∈ (ℂ–cn→ℂ)) |
484 | 470, 483,
349, 75, 464 | cncfmptssg 42938 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((𝐴(,)𝐵)–cn→ℂ)) |
485 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) |
486 | 51, 485, 345 | cncfcn 23655 |
. . . . . . . . . . 11
⊢ (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
487 | 349, 74, 486 | sylancl 589 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
488 | 484, 487 | eleqtrd 2835 |
. . . . . . . . 9
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
489 | | cncnp 22024 |
. . . . . . . . . 10
⊢
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
↔ ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 /
2)))):(𝐴(,)𝐵)⟶ℂ ∧
∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)))) |
490 | 355, 353,
489 | sylancl 589 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
↔ ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 /
2)))):(𝐴(,)𝐵)⟶ℂ ∧
∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)))) |
491 | 488, 490 | mpbid 235 |
. . . . . . . 8
⊢ (𝜑 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 /
2)))):(𝐴(,)𝐵)⟶ℂ ∧
∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦))) |
492 | 491 | simprd 499 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
493 | 360 | eleq2d 2818 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → ((𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) ↔ (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌))) |
494 | 493 | rspccva 3523 |
. . . . . . 7
⊢
((∀𝑦 ∈
(𝐴(,)𝐵)(𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
495 | 492, 27, 494 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((2 · π) ·
(sin‘(𝑤 / 2))))
∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
496 | 469, 495 | eqeltrd 2833 |
. . . . 5
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
497 | 307 | mpteq1d 5116 |
. . . . 5
⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤)))) |
498 | 366 | eqcomd 2744 |
. . . . . . 7
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) = ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵))) |
499 | 498 | oveq1d 7179 |
. . . . . 6
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld)) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))) |
500 | 499 | fveq1d 6670 |
. . . . 5
⊢ (𝜑 →
((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌) = ((((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
501 | 496, 497,
500 | 3eltr4d 2848 |
. . . 4
⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌)) |
502 | | eqid 2738 |
. . . . 5
⊢ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) |
503 | 11, 124 | syldan 594 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((2 · π) ·
(sin‘(𝑦 / 2))) ∈
ℂ) |
504 | 503, 23 | fmptd 6882 |
. . . . 5
⊢ (𝜑 → 𝐺:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) |
505 | 371, 51, 502, 504, 374, 263 | ellimc 24617 |
. . . 4
⊢ (𝜑 → (0 ∈ (𝐺 limℂ 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, 0, (𝐺‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌))) |
506 | 501, 505 | mpbird 260 |
. . 3
⊢ (𝜑 → 0 ∈ (𝐺 limℂ 𝑌)) |
507 | 256 | nrexdv 3179 |
. . . 4
⊢ (𝜑 → ¬ ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0) |
508 | 504 | ffund 6502 |
. . . . . 6
⊢ (𝜑 → Fun 𝐺) |
509 | | fvelima 6729 |
. . . . . 6
⊢ ((Fun
𝐺 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0) |
510 | 508, 509 | sylan 583 |
. . . . 5
⊢ ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0) |
511 | | 2cnd 11787 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ∈
ℂ) |
512 | 119 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ∈
ℂ) |
513 | 134 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 2 ≠ 0) |
514 | 238 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → π ≠ 0) |
515 | 105, 511,
512, 513, 514 | divdiv1d 11518 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝑦 / 2) / π) = (𝑦 / (2 · π))) |
516 | 515 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π)) |
517 | 516 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 / (2 · π)) = ((𝑦 / 2) / π)) |
518 | | 2cnd 11787 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → 2 ∈
ℂ) |
519 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → π ∈
ℂ) |
520 | 518, 519 | mulcld 10732 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (2 · π) ∈
ℂ) |
521 | 232 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → 𝑦 ∈ ℂ) |
522 | 521 | halfcld 11954 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (𝑦 / 2) ∈ ℂ) |
523 | 522 | sincld 15568 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (sin‘(𝑦 / 2)) ∈ ℂ) |
524 | 520, 523 | mulcld 10732 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) ·
(sin‘(𝑦 / 2))) ∈
ℂ) |
525 | 23 | fvmpt2 6780 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ((2 · π) ·
(sin‘(𝑦 / 2))) ∈
ℂ) → (𝐺‘𝑦) = ((2 · π) ·
(sin‘(𝑦 /
2)))) |
526 | 524, 525 | syldan 594 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (𝐺‘𝑦) = ((2 · π) ·
(sin‘(𝑦 /
2)))) |
527 | 526 | eqcomd 2744 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) ·
(sin‘(𝑦 / 2))) =
(𝐺‘𝑦)) |
528 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (𝐺‘𝑦) = 0) |
529 | 527, 528 | eqtrd 2773 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) ·
(sin‘(𝑦 / 2))) =
0) |
530 | 120 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (2 · π) ∈
ℂ) |
531 | 232 | halfcld 11954 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (𝑦 / 2) ∈ ℂ) |
532 | 531 | sincld 15568 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (sin‘(𝑦 / 2)) ∈ ℂ) |
533 | 530, 532 | mul0ord 11361 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (((2 · π) ·
(sin‘(𝑦 / 2))) = 0
↔ ((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0))) |
534 | 533 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (((2 · π) ·
(sin‘(𝑦 / 2))) = 0
↔ ((2 · π) = 0 ∨ (sin‘(𝑦 / 2)) = 0))) |
535 | 529, 534 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → ((2 · π) = 0 ∨
(sin‘(𝑦 / 2)) =
0)) |
536 | | 2cnne0 11919 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
537 | 119, 238 | pm3.2i 474 |
. . . . . . . . . . . . . . 15
⊢ (π
∈ ℂ ∧ π ≠ 0) |
538 | | mulne0 11353 |
. . . . . . . . . . . . . . 15
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0))
→ (2 · π) ≠ 0) |
539 | 536, 537,
538 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (2
· π) ≠ 0 |
540 | 539 | neii 2936 |
. . . . . . . . . . . . 13
⊢ ¬ (2
· π) = 0 |
541 | | pm2.53 850 |
. . . . . . . . . . . . 13
⊢ (((2
· π) = 0 ∨ (sin‘(𝑦 / 2)) = 0) → (¬ (2 · π) =
0 → (sin‘(𝑦 /
2)) = 0)) |
542 | 535, 540,
541 | mpisyl 21 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (𝐺‘𝑦) = 0) → (sin‘(𝑦 / 2)) = 0) |
543 | 542 | adantll 714 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (sin‘(𝑦 / 2)) = 0) |
544 | 105 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → 𝑦 ∈ ℂ) |
545 | 544 | halfcld 11954 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 / 2) ∈ ℂ) |
546 | 545, 246 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → ((sin‘(𝑦 / 2)) = 0 ↔ ((𝑦 / 2) / π) ∈
ℤ)) |
547 | 543, 546 | mpbid 235 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → ((𝑦 / 2) / π) ∈
ℤ) |
548 | 517, 547 | eqeltrd 2833 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 / (2 · π)) ∈
ℤ) |
549 | 11 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → 𝑦 ∈ ℝ) |
550 | 549, 253,
254 | sylancl 589 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → ((𝑦 mod (2 · π)) = 0 ↔ (𝑦 / (2 · π)) ∈
ℤ)) |
551 | 548, 550 | mpbird 260 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) ∧ (𝐺‘𝑦) = 0) → (𝑦 mod (2 · π)) = 0) |
552 | 551 | ex 416 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐺‘𝑦) = 0 → (𝑦 mod (2 · π)) =
0)) |
553 | 552 | reximdva 3183 |
. . . . . 6
⊢ (𝜑 → (∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0 → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) =
0)) |
554 | 553 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → (∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐺‘𝑦) = 0 → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) =
0)) |
555 | 510, 554 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝑦 mod (2 · π)) = 0) |
556 | 507, 555 | mtand 816 |
. . 3
⊢ (𝜑 → ¬ 0 ∈ (𝐺 “ ((𝐴(,)𝐵) ∖ {𝑌}))) |
557 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) |
558 | 111 | fvmpt2 6780 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (π · (cos‘(𝑦 / 2))) ∈ ℂ) →
(𝐼‘𝑦) = (π · (cos‘(𝑦 / 2)))) |
559 | 557, 201,
558 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐼‘𝑦) = (π · (cos‘(𝑦 / 2)))) |
560 | 531 | coscld 15569 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) → (cos‘(𝑦 / 2)) ∈ ℂ) |
561 | 560 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ∈ ℂ) |
562 | | dirkercncflem2.11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0) |
563 | 512, 561,
514, 562 | mulne0d 11363 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (π · (cos‘(𝑦 / 2))) ≠ 0) |
564 | 559, 563 | eqnetrd 3001 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐼‘𝑦) ≠ 0) |
565 | 564 | neneqd 2939 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ¬ (𝐼‘𝑦) = 0) |
566 | 565 | nrexdv 3179 |
. . . . 5
⊢ (𝜑 → ¬ ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼‘𝑦) = 0) |
567 | 201, 111 | fmptd 6882 |
. . . . . . 7
⊢ (𝜑 → 𝐼:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) |
568 | 567 | ffund 6502 |
. . . . . 6
⊢ (𝜑 → Fun 𝐼) |
569 | | fvelima 6729 |
. . . . . 6
⊢ ((Fun
𝐼 ∧ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼‘𝑦) = 0) |
570 | 568, 569 | sylan 583 |
. . . . 5
⊢ ((𝜑 ∧ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) → ∃𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})(𝐼‘𝑦) = 0) |
571 | 566, 570 | mtand 816 |
. . . 4
⊢ (𝜑 → ¬ 0 ∈ (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) |
572 | 199 | imaeq1d 5896 |
. . . 4
⊢ (𝜑 → ((ℝ D 𝐺) “ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝐼 “ ((𝐴(,)𝐵) ∖ {𝑌}))) |
573 | 571, 572 | neleqtrrd 2855 |
. . 3
⊢ (𝜑 → ¬ 0 ∈ ((ℝ D
𝐺) “ ((𝐴(,)𝐵) ∖ {𝑌}))) |
574 | | dirkercncflem2.d |
. . . . . 6
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0,
(((2 · 𝑛) + 1) / (2
· π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) ·
(sin‘(𝑦 /
2))))))) |
575 | 574 | dirkerval2 43161 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ ℝ) → ((𝐷‘𝑁)‘𝑌) = if((𝑌 mod (2 · π)) = 0, (((2 ·
𝑁) + 1) / (2 ·
π)), ((sin‘((𝑁 +
(1 / 2)) · 𝑌)) / ((2
· π) · (sin‘(𝑌 / 2)))))) |
576 | 5, 57, 575 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) = if((𝑌 mod (2 · π)) = 0, (((2 ·
𝑁) + 1) / (2 ·
π)), ((sin‘((𝑁 +
(1 / 2)) · 𝑌)) / ((2
· π) · (sin‘(𝑌 / 2)))))) |
577 | 282 | iftrued 4419 |
. . . . 5
⊢ (𝜑 → if((𝑌 mod (2 · π)) = 0, (((2 ·
𝑁) + 1) / (2 ·
π)), ((sin‘((𝑁 +
(1 / 2)) · 𝑌)) / ((2
· π) · (sin‘(𝑌 / 2))))) = (((2 · 𝑁) + 1) / (2 ·
π))) |
578 | | dirkercncflem2.l |
. . . . . . . . . . 11
⊢ 𝐿 = (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 /
2))))) |
579 | 578 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 = (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 /
2)))))) |
580 | | iftrue 4417 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑌 → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = (((2 · 𝑁) + 1) / (2 ·
π))) |
581 | 580 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = (((2 · 𝑁) + 1) / (2 ·
π))) |
582 | 154, 38 | mulcld 10732 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) |
583 | 582, 397 | addcld 10731 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2 · 𝑁) + 1) ∈
ℂ) |
584 | 583, 154,
155, 377, 378 | divdiv1d 11518 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((((2 · 𝑁) + 1) / 2) / π) = (((2
· 𝑁) + 1) / (2
· π))) |
585 | 584 | eqcomd 2744 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) =
((((2 · 𝑁) + 1) / 2)
/ π)) |
586 | 582, 397,
154, 377 | divdird 11525 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((2 · 𝑁) + 1) / 2) = (((2 ·
𝑁) / 2) + (1 /
2))) |
587 | 38, 154, 377 | divcan3d 11492 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2 · 𝑁) / 2) = 𝑁) |
588 | 587 | oveq1d 7179 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((2 · 𝑁) / 2) + (1 / 2)) = (𝑁 + (1 / 2))) |
589 | 586, 588 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2 · 𝑁) + 1) / 2) = (𝑁 + (1 / 2))) |
590 | 589 | oveq1d 7179 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((2 · 𝑁) + 1) / 2) / π) = ((𝑁 + (1 / 2)) /
π)) |
591 | 585, 590 | eqtrd 2773 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π)) =
((𝑁 + (1 / 2)) /
π)) |
592 | 591 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((2 · 𝑁) + 1) / (2 · π)) = ((𝑁 + (1 / 2)) /
π)) |
593 | 310 | fveq2d 6672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑌 → (cos‘((𝑁 + (1 / 2)) · 𝑤)) = (cos‘((𝑁 + (1 / 2)) · 𝑌))) |
594 | 593 | oveq2d 7180 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑌 → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌)))) |
595 | | fvoveq1 7187 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑌 → (cos‘(𝑤 / 2)) = (cos‘(𝑌 / 2))) |
596 | 595 | oveq2d 7180 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑌 → (π · (cos‘(𝑤 / 2))) = (π ·
(cos‘(𝑌 /
2)))) |
597 | 594, 596 | oveq12d 7182 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑌 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 / 2)))) =
(((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑌))) / (π
· (cos‘(𝑌 /
2))))) |
598 | 597 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 / 2)))) =
(((𝑁 + (1 / 2)) ·
(cos‘((𝑁 + (1 / 2))
· 𝑌))) / (π
· (cos‘(𝑌 /
2))))) |
599 | 38, 40, 263 | adddird 10737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑁 · 𝑌) + ((1 / 2) · 𝑌))) |
600 | 397, 154,
263, 377 | div32d 11510 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((1 / 2) · 𝑌) = (1 · (𝑌 / 2))) |
601 | 436 | mulid2d 10730 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 · (𝑌 / 2)) = (𝑌 / 2)) |
602 | 600, 601 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1 / 2) · 𝑌) = (𝑌 / 2)) |
603 | 602 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑁 · 𝑌) + ((1 / 2) · 𝑌)) = ((𝑁 · 𝑌) + (𝑌 / 2))) |
604 | 38, 263 | mulcld 10732 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑁 · 𝑌) ∈ ℂ) |
605 | 604, 436 | addcomd 10913 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑁 · 𝑌) + (𝑌 / 2)) = ((𝑌 / 2) + (𝑁 · 𝑌))) |
606 | 599, 603,
605 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝑌) = ((𝑌 / 2) + (𝑁 · 𝑌))) |
607 | 606 | fveq2d 6672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (cos‘((𝑁 + (1 / 2)) · 𝑌)) = (cos‘((𝑌 / 2) + (𝑁 · 𝑌)))) |
608 | 604, 156,
379 | divcan1d 11488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((𝑁 · 𝑌) / (2 · π)) · (2 ·
π)) = (𝑁 · 𝑌)) |
609 | 608 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑁 · 𝑌) = (((𝑁 · 𝑌) / (2 · π)) · (2 ·
π))) |
610 | 609 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑌 / 2) + (𝑁 · 𝑌)) = ((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 ·
π)))) |
611 | 610 | fveq2d 6672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (cos‘((𝑌 / 2) + (𝑁 · 𝑌))) = (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 ·
π))))) |
612 | 38, 263, 156, 379 | divassd 11522 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑁 · 𝑌) / (2 · π)) = (𝑁 · (𝑌 / (2 · π)))) |
613 | 405, 404 | zmulcld 12167 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑁 · (𝑌 / (2 · π))) ∈
ℤ) |
614 | 612, 613 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑁 · 𝑌) / (2 · π)) ∈
ℤ) |
615 | | cosper 25219 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑌 / 2) ∈ ℂ ∧
((𝑁 · 𝑌) / (2 · π)) ∈
ℤ) → (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 ·
π)))) = (cos‘(𝑌 /
2))) |
616 | 436, 614,
615 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (cos‘((𝑌 / 2) + (((𝑁 · 𝑌) / (2 · π)) · (2 ·
π)))) = (cos‘(𝑌 /
2))) |
617 | 607, 611,
616 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (cos‘((𝑁 + (1 / 2)) · 𝑌)) = (cos‘(𝑌 / 2))) |
618 | 617 | oveq2d 7180 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) = ((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2)))) |
619 | 618 | oveq1d 7179 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π ·
(cos‘(𝑌 / 2)))) =
(((𝑁 + (1 / 2)) ·
(cos‘(𝑌 / 2))) /
(π · (cos‘(𝑌 / 2))))) |
620 | 436 | coscld 15569 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (cos‘(𝑌 / 2)) ∈
ℂ) |
621 | 263, 154,
155, 377, 378 | divdiv1d 11518 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑌 / 2) / π) = (𝑌 / (2 · π))) |
622 | 621, 404 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑌 / 2) / π) ∈
ℤ) |
623 | 622 | zred 12161 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑌 / 2) / π) ∈
ℝ) |
624 | 623, 272 | ltaddrpd 12540 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑌 / 2) / π) < (((𝑌 / 2) / π) + (1 / 2))) |
625 | | halflt1 11927 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 / 2)
< 1 |
626 | 625 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (1 / 2) <
1) |
627 | 268, 267,
623, 626 | ltadd2dd 10870 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝑌 / 2) / π) + (1 / 2)) < (((𝑌 / 2) / π) +
1)) |
628 | | btwnnz 12132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑌 / 2) / π) ∈ ℤ
∧ ((𝑌 / 2) / π) <
(((𝑌 / 2) / π) + (1 /
2)) ∧ (((𝑌 / 2) / π)
+ (1 / 2)) < (((𝑌 / 2) /
π) + 1)) → ¬ (((𝑌 / 2) / π) + (1 / 2)) ∈
ℤ) |
629 | 622, 624,
627, 628 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ (((𝑌 / 2) / π) + (1 / 2)) ∈
ℤ) |
630 | | coseq0 42931 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑌 / 2) ∈ ℂ →
((cos‘(𝑌 / 2)) = 0
↔ (((𝑌 / 2) / π) +
(1 / 2)) ∈ ℤ)) |
631 | 436, 630 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((cos‘(𝑌 / 2)) = 0 ↔ (((𝑌 / 2) / π) + (1 / 2)) ∈
ℤ)) |
632 | 629, 631 | mtbird 328 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ¬ (cos‘(𝑌 / 2)) = 0) |
633 | 632 | neqned 2941 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (cos‘(𝑌 / 2)) ≠ 0) |
634 | 41, 155, 620, 378, 633 | divcan5rd 11514 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑁 + (1 / 2)) · (cos‘(𝑌 / 2))) / (π ·
(cos‘(𝑌 / 2)))) =
((𝑁 + (1 / 2)) /
π)) |
635 | 619, 634 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π ·
(cos‘(𝑌 / 2)))) =
((𝑁 + (1 / 2)) /
π)) |
636 | 635 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑌))) / (π ·
(cos‘(𝑌 / 2)))) =
((𝑁 + (1 / 2)) /
π)) |
637 | 598, 636 | eqtr2d 2774 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) / π) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 /
2))))) |
638 | 581, 592,
637 | 3eqtrrd 2778 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 / 2)))) =
if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) |
639 | | iffalse 4420 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑤 = 𝑌 → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) |
640 | 639 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)) |
641 | | eqidd 2739 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))) |
642 | | fveq2 6668 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑤 → (𝐻‘𝑦) = (𝐻‘𝑤)) |
643 | | fveq2 6668 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑤 → (𝐼‘𝑦) = (𝐼‘𝑤)) |
644 | 642, 643 | oveq12d 7182 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑤 → ((𝐻‘𝑦) / (𝐼‘𝑦)) = ((𝐻‘𝑤) / (𝐼‘𝑤))) |
645 | 644 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝐻‘𝑦) / (𝐼‘𝑦)) = ((𝐻‘𝑤) / (𝐼‘𝑤))) |
646 | 106, 100 | fmptd 6882 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐻:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) |
647 | 646 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐻:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) |
648 | 647, 324 | ffvelrnd 6856 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐻‘𝑤) ∈ ℂ) |
649 | 567 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐼:((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) |
650 | 649, 324 | ffvelrnd 6856 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼‘𝑤) ∈ ℂ) |
651 | 111 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2))))) |
652 | | simpr 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤) |
653 | 652 | fvoveq1d 7186 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (cos‘(𝑦 / 2)) = (cos‘(𝑤 / 2))) |
654 | 653 | oveq2d 7180 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (π · (cos‘(𝑦 / 2))) = (π ·
(cos‘(𝑤 /
2)))) |
655 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ (𝐴(,)𝐵) → π ∈
ℂ) |
656 | 327 | halfcld 11954 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ (𝐴(,)𝐵) → (𝑤 / 2) ∈ ℂ) |
657 | 656 | coscld 15569 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ (𝐴(,)𝐵) → (cos‘(𝑤 / 2)) ∈ ℂ) |
658 | 655, 657 | mulcld 10732 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ (𝐴(,)𝐵) → (π · (cos‘(𝑤 / 2))) ∈
ℂ) |
659 | 658 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π · (cos‘(𝑤 / 2))) ∈
ℂ) |
660 | 651, 654,
324, 659 | fvmptd 6776 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼‘𝑤) = (π · (cos‘(𝑤 / 2)))) |
661 | 537 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π ∈ ℂ ∧ π
≠ 0)) |
662 | 657 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ∈ ℂ) |
663 | | simpll 767 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝜑) |
664 | | fvoveq1 7187 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑤 → (cos‘(𝑦 / 2)) = (cos‘(𝑤 / 2))) |
665 | 664 | neeq1d 2993 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑤 → ((cos‘(𝑦 / 2)) ≠ 0 ↔ (cos‘(𝑤 / 2)) ≠ 0)) |
666 | 226, 665 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑤 → (((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0) ↔ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑤 / 2)) ≠ 0))) |
667 | 666, 562 | chvarvv 2009 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑤 / 2)) ≠ 0) |
668 | 663, 324,
667 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0) |
669 | | mulne0 11353 |
. . . . . . . . . . . . . . . . 17
⊢ (((π
∈ ℂ ∧ π ≠ 0) ∧ ((cos‘(𝑤 / 2)) ∈ ℂ ∧ (cos‘(𝑤 / 2)) ≠ 0)) → (π
· (cos‘(𝑤 /
2))) ≠ 0) |
670 | 661, 662,
668, 669 | syl12anc 836 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (π · (cos‘(𝑤 / 2))) ≠ 0) |
671 | 660, 670 | eqnetrd 3001 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐼‘𝑤) ≠ 0) |
672 | 648, 650,
671 | divcld 11487 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝐻‘𝑤) / (𝐼‘𝑤)) ∈ ℂ) |
673 | 641, 645,
324, 672 | fvmptd 6776 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤) = ((𝐻‘𝑤) / (𝐼‘𝑤))) |
674 | 100 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → 𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))) |
675 | 317 | fveq2d 6672 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → (cos‘((𝑁 + (1 / 2)) · 𝑦)) = (cos‘((𝑁 + (1 / 2)) · 𝑤))) |
676 | 675 | oveq2d 7180 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤)))) |
677 | 329 | coscld 15569 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘((𝑁 + (1 / 2)) · 𝑤)) ∈ ℂ) |
678 | 325, 677 | mulcld 10732 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈
ℂ) |
679 | 678 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈
ℂ) |
680 | 674, 676,
324, 679 | fvmptd 6776 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (𝐻‘𝑤) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤)))) |
681 | 680, 660 | oveq12d 7182 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → ((𝐻‘𝑤) / (𝐼‘𝑤)) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 /
2))))) |
682 | 640, 673,
681 | 3eqtrrd 2778 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑤 = 𝑌) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 / 2)))) =
if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) |
683 | 638, 682 | pm2.61dan 813 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 / 2)))) =
if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) |
684 | 683 | mpteq2dva 5122 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 / 2))))) =
(𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)))) |
685 | 579, 684 | eqtr2d 2774 |
. . . . . . . . 9
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) = 𝐿) |
686 | 349, 41, 75 | constcncfg 42939 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
687 | | cosf 15563 |
. . . . . . . . . . . . . . . . . . 19
⊢
cos:ℂ⟶ℂ |
688 | 231, 44 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑦) ∈ ℂ) |
689 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) |
690 | 688, 689 | fmptd 6882 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)):(𝐴(,)𝐵)⟶ℂ) |
691 | | fcompt 6899 |
. . . . . . . . . . . . . . . . . . 19
⊢
((cos:ℂ⟶ℂ ∧ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)):(𝐴(,)𝐵)⟶ℂ) → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))) |
692 | 687, 690,
691 | sylancr 590 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)))) |
693 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) |
694 | 316 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑦 = 𝑤) → ((𝑁 + (1 / 2)) · 𝑦) = ((𝑁 + (1 / 2)) · 𝑤)) |
695 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 𝑤 ∈ (𝐴(,)𝐵)) |
696 | 693, 694,
695, 329 | fvmptd 6776 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤) = ((𝑁 + (1 / 2)) · 𝑤)) |
697 | 696 | fveq2d 6672 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤)) = (cos‘((𝑁 + (1 / 2)) · 𝑤))) |
698 | 697 | mpteq2dva 5122 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤)))) |
699 | 692, 698 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))) = (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)))) |
700 | 349, 41, 75 | constcncfg 42939 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
701 | 349, 75 | idcncfg 42940 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 𝑦) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
702 | 700, 701 | mulcncf 24191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
703 | | coscn 25184 |
. . . . . . . . . . . . . . . . . . 19
⊢ cos
∈ (ℂ–cn→ℂ) |
704 | 703 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → cos ∈
(ℂ–cn→ℂ)) |
705 | 702, 704 | cncfco 23652 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (cos ∘ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑦))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
706 | 699, 705 | eqeltrd 2833 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘((𝑁 + (1 / 2)) · 𝑤))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
707 | 686, 706 | mulcncf 24191 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤)))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
708 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) |
709 | 349, 155,
75 | constcncfg 42939 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ π) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
710 | | 2cnd 11787 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ) |
711 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → 2 ≠ 0) |
712 | 328, 710,
711 | divrecd 11490 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 / 2) = (𝑤 · (1 / 2))) |
713 | 712 | mpteq2dva 5122 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 / 2)) = (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 · (1 / 2)))) |
714 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2))) = (𝑤 ∈ ℂ ↦ (𝑤 · (1 /
2))) |
715 | | cncfmptid 23658 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ)) |
716 | 74, 74, 715 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ) |
717 | 716 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ 𝑤) ∈ (ℂ–cn→ℂ)) |
718 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1 / 2)
∈ ℂ → ℂ ⊆ ℂ) |
719 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1 / 2)
∈ ℂ → (1 / 2) ∈ ℂ) |
720 | 718, 719,
718 | constcncfg 42939 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1 / 2)
∈ ℂ → (𝑤
∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ)) |
721 | 39, 720 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (1 / 2)) ∈
(ℂ–cn→ℂ)) |
722 | 717, 721 | mulcncf 24191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑤 ∈ ℂ ↦ (𝑤 · (1 / 2))) ∈
(ℂ–cn→ℂ)) |
723 | 712, 462 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (𝑤 · (1 / 2)) ∈
ℂ) |
724 | 714, 722,
349, 75, 723 | cncfmptssg 42938 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 · (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
725 | 713, 724 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (𝑤 / 2)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
726 | 704, 725 | cncfmpt1f 23659 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑤 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
727 | 709, 726 | mulcncf 24191 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
728 | | ssid 3897 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵) |
729 | 728 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)) |
730 | | difssd 4021 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℂ ∖ {0})
⊆ ℂ) |
731 | 658 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ∈
ℂ) |
732 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → π ∈
ℂ) |
733 | 657 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘(𝑤 / 2)) ∈ ℂ) |
734 | 238 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → π ≠ 0) |
735 | 595 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) = (cos‘(𝑌 / 2))) |
736 | 633 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (cos‘(𝑌 / 2)) ≠ 0) |
737 | 735, 736 | eqnetrd 3001 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0) |
738 | 737 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) ∧ 𝑤 = 𝑌) → (cos‘(𝑤 / 2)) ≠ 0) |
739 | 738, 668 | pm2.61dan 813 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (cos‘(𝑤 / 2)) ≠ 0) |
740 | 732, 733,
734, 739 | mulne0d 11363 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ≠ 0) |
741 | 740 | neneqd 2939 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ¬ (π ·
(cos‘(𝑤 / 2))) =
0) |
742 | | elsng 4527 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((π
· (cos‘(𝑤 /
2))) ∈ ℂ → ((π · (cos‘(𝑤 / 2))) ∈ {0} ↔ (π ·
(cos‘(𝑤 / 2))) =
0)) |
743 | 731, 742 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ((π · (cos‘(𝑤 / 2))) ∈ {0} ↔ (π
· (cos‘(𝑤 /
2))) = 0)) |
744 | 741, 743 | mtbird 328 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → ¬ (π ·
(cos‘(𝑤 / 2))) ∈
{0}) |
745 | 731, 744 | eldifd 3852 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴(,)𝐵)) → (π · (cos‘(𝑤 / 2))) ∈ (ℂ ∖
{0})) |
746 | 708, 727,
729, 730, 745 | cncfmptssg 42938 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (π · (cos‘(𝑤 / 2)))) ∈ ((𝐴(,)𝐵)–cn→(ℂ ∖ {0}))) |
747 | 707, 746 | divcncf 24192 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 / 2)))))
∈ ((𝐴(,)𝐵)–cn→ℂ)) |
748 | 747, 487 | eleqtrd 2835 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π ·
(cos‘(𝑤 / 2)))))
∈ (((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
749 | 579, 748 | eqeltrd 2833 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐿 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
750 | | cncnp 22024 |
. . . . . . . . . . . . 13
⊢
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) ∈ (TopOn‘(𝐴(,)𝐵)) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
(𝐿 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
↔ (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)))) |
751 | 355, 353,
750 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
↔ (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)))) |
752 | 749, 751 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐿:(𝐴(,)𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦))) |
753 | 752 | simprd 499 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
754 | 360 | eleq2d 2818 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑌 → (𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) ↔ 𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌))) |
755 | 754 | rspccva 3523 |
. . . . . . . . . 10
⊢
((∀𝑦 ∈
(𝐴(,)𝐵)𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) ∧ 𝑌 ∈ (𝐴(,)𝐵)) → 𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
756 | 753, 27, 755 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
757 | 685, 756 | eqeltrd 2833 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑌)) |
758 | 307 | mpteq1d 5116 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) = (𝑤 ∈ (𝐴(,)𝐵) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤)))) |
759 | 757, 758,
500 | 3eltr4d 2848 |
. . . . . . 7
⊢ (𝜑 → (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌)) |
760 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) = (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) |
761 | 100 | fvmpt2 6780 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) ∈ ℂ) →
(𝐻‘𝑦) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) |
762 | 557, 106,
761 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐻‘𝑦) = ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦)))) |
763 | 762, 559 | oveq12d 7182 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐻‘𝑦) / (𝐼‘𝑦)) = (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) / (π ·
(cos‘(𝑦 /
2))))) |
764 | 106, 201,
563 | divcld 11487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))) / (π ·
(cos‘(𝑦 / 2))))
∈ ℂ) |
765 | 763, 764 | eqeltrd 2833 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐻‘𝑦) / (𝐼‘𝑦)) ∈ ℂ) |
766 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) |
767 | 765, 766 | fmptd 6882 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))):((𝐴(,)𝐵) ∖ {𝑌})⟶ℂ) |
768 | 371, 51, 760, 767, 374, 263 | ellimc 24617 |
. . . . . . 7
⊢ (𝜑 → ((((2 · 𝑁) + 1) / (2 · π))
∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) limℂ 𝑌) ↔ (𝑤 ∈ (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌}) ↦ if(𝑤 = 𝑌, (((2 · 𝑁) + 1) / (2 · π)), ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦)))‘𝑤))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐴(,)𝐵) ∖ {𝑌}) ∪ {𝑌})) CnP
(TopOpen‘ℂfld))‘𝑌))) |
769 | 759, 768 | mpbird 260 |
. . . . . 6
⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π))
∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) limℂ 𝑌)) |
770 | 103 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 = (ℝ D 𝐹)) |
771 | 770 | fveq1d 6670 |
. . . . . . . . 9
⊢ (𝜑 → (𝐻‘𝑦) = ((ℝ D 𝐹)‘𝑦)) |
772 | 199 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 = (ℝ D 𝐺)) |
773 | 772 | fveq1d 6670 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼‘𝑦) = ((ℝ D 𝐺)‘𝑦)) |
774 | 771, 773 | oveq12d 7182 |
. . . . . . . 8
⊢ (𝜑 → ((𝐻‘𝑦) / (𝐼‘𝑦)) = (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) |
775 | 774 | mpteq2dv 5123 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦)))) |
776 | 775 | oveq1d 7179 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐻‘𝑦) / (𝐼‘𝑦))) limℂ 𝑌) = ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) limℂ 𝑌)) |
777 | 769, 776 | eleqtrd 2835 |
. . . . 5
⊢ (𝜑 → (((2 · 𝑁) + 1) / (2 · π))
∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) limℂ 𝑌)) |
778 | 577, 777 | eqeltrd 2833 |
. . . 4
⊢ (𝜑 → if((𝑌 mod (2 · π)) = 0, (((2 ·
𝑁) + 1) / (2 ·
π)), ((sin‘((𝑁 +
(1 / 2)) · 𝑌)) / ((2
· π) · (sin‘(𝑌 / 2))))) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) limℂ 𝑌)) |
779 | 576, 778 | eqeltrd 2833 |
. . 3
⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (((ℝ D 𝐹)‘𝑦) / ((ℝ D 𝐺)‘𝑦))) limℂ 𝑌)) |
780 | 4, 15, 24, 26, 27, 28, 110, 205, 431, 506, 556, 573, 779 | lhop 24760 |
. 2
⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))) limℂ 𝑌)) |
781 | 574 | dirkerval 43158 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) = (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0,
(((2 · 𝑁) + 1) / (2
· π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) ·
(sin‘(𝑦 /
2))))))) |
782 | 5, 781 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐷‘𝑁) = (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0,
(((2 · 𝑁) + 1) / (2
· π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) ·
(sin‘(𝑦 /
2))))))) |
783 | 782 | reseq1d 5818 |
. . . 4
⊢ (𝜑 → ((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) = ((𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0,
(((2 · 𝑁) + 1) / (2
· π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) ·
(sin‘(𝑦 / 2))))))
↾ ((𝐴(,)𝐵) ∖ {𝑌}))) |
784 | 4 | resmptd 5876 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0,
(((2 · 𝑁) + 1) / (2
· π)), ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) ·
(sin‘(𝑦 / 2))))))
↾ ((𝐴(,)𝐵) ∖ {𝑌})) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ if((𝑦 mod (2 · π)) = 0, (((2 ·
𝑁) + 1) / (2 ·
π)), ((sin‘((𝑁 +
(1 / 2)) · 𝑦)) / ((2
· π) · (sin‘(𝑦 / 2))))))) |
785 | 256 | iffalsed 4422 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → if((𝑦 mod (2 · π)) = 0, (((2 ·
𝑁) + 1) / (2 ·
π)), ((sin‘((𝑁 +
(1 / 2)) · 𝑦)) / ((2
· π) · (sin‘(𝑦 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) ·
(sin‘(𝑦 /
2))))) |
786 | 13 | recnd 10740 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ) |
787 | 14 | fvmpt2 6780 |
. . . . . . . 8
⊢ ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ∧ (sin‘((𝑁 + (1 / 2)) · 𝑦)) ∈ ℂ) → (𝐹‘𝑦) = (sin‘((𝑁 + (1 / 2)) · 𝑦))) |
788 | 557, 786,
787 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐹‘𝑦) = (sin‘((𝑁 + (1 / 2)) · 𝑦))) |
789 | 557, 503,
525 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (𝐺‘𝑦) = ((2 · π) ·
(sin‘(𝑦 /
2)))) |
790 | 788, 789 | oveq12d 7182 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → ((𝐹‘𝑦) / (𝐺‘𝑦)) = ((sin‘((𝑁 + (1 / 2)) · 𝑦)) / ((2 · π) ·
(sin‘(𝑦 /
2))))) |
791 | 785, 790 | eqtr4d 2776 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → if((𝑦 mod (2 · π)) = 0, (((2 ·
𝑁) + 1) / (2 ·
π)), ((sin‘((𝑁 +
(1 / 2)) · 𝑦)) / ((2
· π) · (sin‘(𝑦 / 2))))) = ((𝐹‘𝑦) / (𝐺‘𝑦))) |
792 | 791 | mpteq2dva 5122 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ if((𝑦 mod (2 · π)) = 0, (((2 ·
𝑁) + 1) / (2 ·
π)), ((sin‘((𝑁 +
(1 / 2)) · 𝑦)) / ((2
· π) · (sin‘(𝑦 / 2)))))) = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦)))) |
793 | 783, 784,
792 | 3eqtrrd 2778 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))) = ((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌}))) |
794 | 793 | oveq1d 7179 |
. 2
⊢ (𝜑 → ((𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝐹‘𝑦) / (𝐺‘𝑦))) limℂ 𝑌) = (((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) limℂ 𝑌)) |
795 | 780, 794 | eleqtrd 2835 |
1
⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ (((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) limℂ 𝑌)) |