Step | Hyp | Ref
| Expression |
1 | | dirkercncf.d |
. . . 4
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0,
(((2 · 𝑛) + 1) / (2
· π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) ·
(sin‘(𝑦 /
2))))))) |
2 | 1 | dirkerf 43638 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁):ℝ⟶ℝ) |
3 | | ax-resscn 10928 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
4 | 3 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ℝ
⊆ ℂ) |
5 | 2, 4 | fssd 6618 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁):ℝ⟶ℂ) |
6 | 5 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ (𝐷‘𝑁):ℝ⟶ℂ) |
7 | | oveq1 7282 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 → (𝑦 mod (2 · π)) = (𝑤 mod (2 · π))) |
8 | 7 | eqeq1d 2740 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑤 → ((𝑦 mod (2 · π)) = 0 ↔ (𝑤 mod (2 · π)) =
0)) |
9 | | oveq2 7283 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑤 → ((𝑛 + (1 / 2)) · 𝑦) = ((𝑛 + (1 / 2)) · 𝑤)) |
10 | 9 | fveq2d 6778 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 → (sin‘((𝑛 + (1 / 2)) · 𝑦)) = (sin‘((𝑛 + (1 / 2)) · 𝑤))) |
11 | | oveq1 7282 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑤 → (𝑦 / 2) = (𝑤 / 2)) |
12 | 11 | fveq2d 6778 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑤 → (sin‘(𝑦 / 2)) = (sin‘(𝑤 / 2))) |
13 | 12 | oveq2d 7291 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 → ((2 · π) ·
(sin‘(𝑦 / 2))) = ((2
· π) · (sin‘(𝑤 / 2)))) |
14 | 10, 13 | oveq12d 7293 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑤 → ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) ·
(sin‘(𝑦 / 2)))) =
((sin‘((𝑛 + (1 / 2))
· 𝑤)) / ((2 ·
π) · (sin‘(𝑤 / 2))))) |
15 | 8, 14 | ifbieq2d 4485 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → 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)))))) |
16 | 15 | cbvmptv 5187 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ ↦
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)))))) |
17 | 16 | mpteq2i 5179 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦
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))))))) |
18 | 1, 17 | eqtri 2766 |
. . . . . . . . 9
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑤 ∈ ℝ ↦ if((𝑤 mod (2 · π)) = 0,
(((2 · 𝑛) + 1) / (2
· π)), ((sin‘((𝑛 + (1 / 2)) · 𝑤)) / ((2 · π) ·
(sin‘(𝑤 /
2))))))) |
19 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑦 − π) = (𝑦 − π) |
20 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑦 + π) = (𝑦 + π) |
21 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑤 ∈ ((𝑦 − π)(,)(𝑦 + π)) ↦ ((sin‘((𝑛 + (1 / 2)) · 𝑤)) / ((2 · π) ·
(sin‘(𝑤 / 2))))) =
(𝑤 ∈ ((𝑦 − π)(,)(𝑦 + π)) ↦
((sin‘((𝑛 + (1 / 2))
· 𝑤)) / ((2 ·
π) · (sin‘(𝑤 / 2))))) |
22 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑤 ∈ ((𝑦 − π)(,)(𝑦 + π)) ↦ ((2 · π) ·
(sin‘(𝑤 / 2)))) =
(𝑤 ∈ ((𝑦 − π)(,)(𝑦 + π)) ↦ ((2 ·
π) · (sin‘(𝑤 / 2)))) |
23 | | simpll 764 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ 𝑁 ∈
ℕ) |
24 | | simplr 766 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ 𝑦 ∈
ℝ) |
25 | | simpr 485 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ (𝑦 mod (2 ·
π)) = 0) |
26 | 18, 19, 20, 21, 22, 23, 24, 25 | dirkercncflem3 43646 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ ((𝐷‘𝑁)‘𝑦) ∈ ((𝐷‘𝑁) limℂ 𝑦)) |
27 | 3 | jctl 524 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → (ℝ
⊆ ℂ ∧ 𝑦
∈ ℝ)) |
28 | 27 | ad2antlr 724 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ (ℝ ⊆ ℂ ∧ 𝑦 ∈ ℝ)) |
29 | | eqid 2738 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
30 | 29 | tgioo2 23966 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
31 | 29, 30 | cnplimc 25051 |
. . . . . . . . 9
⊢ ((ℝ
⊆ ℂ ∧ 𝑦
∈ ℝ) → ((𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP
(TopOpen‘ℂfld))‘𝑦) ↔ ((𝐷‘𝑁):ℝ⟶ℂ ∧ ((𝐷‘𝑁)‘𝑦) ∈ ((𝐷‘𝑁) limℂ 𝑦)))) |
32 | 28, 31 | syl 17 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ ((𝐷‘𝑁) ∈ (((topGen‘ran
(,)) CnP (TopOpen‘ℂfld))‘𝑦) ↔ ((𝐷‘𝑁):ℝ⟶ℂ ∧ ((𝐷‘𝑁)‘𝑦) ∈ ((𝐷‘𝑁) limℂ 𝑦)))) |
33 | 6, 26, 32 | mpbir2and 710 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ (𝐷‘𝑁) ∈ (((topGen‘ran
(,)) CnP (TopOpen‘ℂfld))‘𝑦)) |
34 | 29 | cnfldtop 23947 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) ∈ Top |
35 | 34 | a1i 11 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ (TopOpen‘ℂfld) ∈ Top) |
36 | 2 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ (𝐷‘𝑁):ℝ⟶ℝ) |
37 | 3 | a1i 11 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ ℝ ⊆ ℂ) |
38 | | retopon 23927 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
39 | 38 | toponunii 22065 |
. . . . . . . . 9
⊢ ℝ =
∪ (topGen‘ran (,)) |
40 | 29 | cnfldtopon 23946 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
41 | 40 | toponunii 22065 |
. . . . . . . . 9
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
42 | 39, 41 | cnprest2 22441 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝐷‘𝑁):ℝ⟶ℝ ∧ ℝ
⊆ ℂ) → ((𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP
(TopOpen‘ℂfld))‘𝑦) ↔ (𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP
((TopOpen‘ℂfld) ↾t
ℝ))‘𝑦))) |
43 | 35, 36, 37, 42 | syl3anc 1370 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ ((𝐷‘𝑁) ∈ (((topGen‘ran
(,)) CnP (TopOpen‘ℂfld))‘𝑦) ↔ (𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP
((TopOpen‘ℂfld) ↾t
ℝ))‘𝑦))) |
44 | 33, 43 | mpbid 231 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ (𝐷‘𝑁) ∈ (((topGen‘ran
(,)) CnP ((TopOpen‘ℂfld) ↾t
ℝ))‘𝑦)) |
45 | 30 | eqcomi 2747 |
. . . . . . . . 9
⊢
((TopOpen‘ℂfld) ↾t ℝ) =
(topGen‘ran (,)) |
46 | 45 | a1i 11 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ ((TopOpen‘ℂfld) ↾t ℝ) =
(topGen‘ran (,))) |
47 | 46 | oveq2d 7291 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ ((topGen‘ran (,)) CnP ((TopOpen‘ℂfld)
↾t ℝ)) = ((topGen‘ran (,)) CnP (topGen‘ran
(,)))) |
48 | 47 | fveq1d 6776 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ (((topGen‘ran (,)) CnP ((TopOpen‘ℂfld)
↾t ℝ))‘𝑦) = (((topGen‘ran (,)) CnP
(topGen‘ran (,)))‘𝑦)) |
49 | 44, 48 | eleqtrd 2841 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ (𝑦 mod (2 · π)) = 0)
→ (𝐷‘𝑁) ∈ (((topGen‘ran
(,)) CnP (topGen‘ran (,)))‘𝑦)) |
50 | | simpll 764 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ ¬
(𝑦 mod (2 · π)) =
0) → 𝑁 ∈
ℕ) |
51 | | simplr 766 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ ¬
(𝑦 mod (2 · π)) =
0) → 𝑦 ∈
ℝ) |
52 | | neqne 2951 |
. . . . . . 7
⊢ (¬
(𝑦 mod (2 · π)) =
0 → (𝑦 mod (2 ·
π)) ≠ 0) |
53 | 52 | adantl 482 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ ¬
(𝑦 mod (2 · π)) =
0) → (𝑦 mod (2
· π)) ≠ 0) |
54 | | eqid 2738 |
. . . . . 6
⊢
(⌊‘(𝑦 /
(2 · π))) = (⌊‘(𝑦 / (2 · π))) |
55 | | eqid 2738 |
. . . . . 6
⊢
((⌊‘(𝑦 /
(2 · π))) + 1) = ((⌊‘(𝑦 / (2 · π))) + 1) |
56 | | eqid 2738 |
. . . . . 6
⊢
((⌊‘(𝑦 /
(2 · π))) · (2 · π)) = ((⌊‘(𝑦 / (2 · π))) ·
(2 · π)) |
57 | | eqid 2738 |
. . . . . 6
⊢
(((⌊‘(𝑦
/ (2 · π))) + 1) · (2 · π)) =
(((⌊‘(𝑦 / (2
· π))) + 1) · (2 · π)) |
58 | 18, 50, 51, 53, 54, 55, 56, 57 | dirkercncflem4 43647 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) ∧ ¬
(𝑦 mod (2 · π)) =
0) → (𝐷‘𝑁) ∈ (((topGen‘ran
(,)) CnP (topGen‘ran (,)))‘𝑦)) |
59 | 49, 58 | pm2.61dan 810 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ) → (𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP
(topGen‘ran (,)))‘𝑦)) |
60 | 59 | ralrimiva 3103 |
. . 3
⊢ (𝑁 ∈ ℕ →
∀𝑦 ∈ ℝ
(𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP
(topGen‘ran (,)))‘𝑦)) |
61 | | cncnp 22431 |
. . . 4
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧
(topGen‘ran (,)) ∈ (TopOn‘ℝ)) → ((𝐷‘𝑁) ∈ ((topGen‘ran (,)) Cn
(topGen‘ran (,))) ↔ ((𝐷‘𝑁):ℝ⟶ℝ ∧ ∀𝑦 ∈ ℝ (𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP
(topGen‘ran (,)))‘𝑦)))) |
62 | 38, 38, 61 | mp2an 689 |
. . 3
⊢ ((𝐷‘𝑁) ∈ ((topGen‘ran (,)) Cn
(topGen‘ran (,))) ↔ ((𝐷‘𝑁):ℝ⟶ℝ ∧ ∀𝑦 ∈ ℝ (𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP
(topGen‘ran (,)))‘𝑦))) |
63 | 2, 60, 62 | sylanbrc 583 |
. 2
⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) ∈ ((topGen‘ran (,)) Cn
(topGen‘ran (,)))) |
64 | 29, 30, 30 | cncfcn 24073 |
. . 3
⊢ ((ℝ
⊆ ℂ ∧ ℝ ⊆ ℂ) → (ℝ–cn→ℝ) = ((topGen‘ran (,)) Cn
(topGen‘ran (,)))) |
65 | 3, 3, 64 | mp2an 689 |
. 2
⊢
(ℝ–cn→ℝ) =
((topGen‘ran (,)) Cn (topGen‘ran (,))) |
66 | 63, 65 | eleqtrrdi 2850 |
1
⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) ∈ (ℝ–cn→ℝ)) |