Step | Hyp | Ref
| Expression |
1 | | knoppcnlem11.t |
. . . . . 6
⊢ 𝑇 = (𝑥 ∈ ℝ ↦
(abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) |
2 | | knoppcnlem11.f |
. . . . . 6
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) |
3 | | knoppcnlem11.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑁 ∈
ℕ) |
5 | | knoppcnlem11.1 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℝ) |
6 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈
ℝ) |
7 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
8 | 1, 2, 4, 6, 7 | knoppcnlem7 31659 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘) = (𝑤 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑤))‘𝑘))) |
9 | | eqidd 2611 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑙 ∈ (0...𝑘)) → ((𝐹‘𝑤)‘𝑙) = ((𝐹‘𝑤)‘𝑙)) |
10 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) → 𝑘 ∈
ℕ0) |
11 | | elnn0uz 11601 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
↔ 𝑘 ∈
(ℤ≥‘0)) |
12 | 10, 11 | sylib 207 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) → 𝑘 ∈
(ℤ≥‘0)) |
13 | 4 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑙 ∈ (0...𝑘)) → 𝑁 ∈ ℕ) |
14 | 6 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑙 ∈ (0...𝑘)) → 𝐶 ∈ ℝ) |
15 | | simplr 788 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑙 ∈ (0...𝑘)) → 𝑤 ∈ ℝ) |
16 | | elfzuz 12209 |
. . . . . . . . . . . 12
⊢ (𝑙 ∈ (0...𝑘) → 𝑙 ∈
(ℤ≥‘0)) |
17 | | nn0uz 11598 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
18 | 16, 17 | syl6eleqr 2699 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ (0...𝑘) → 𝑙 ∈ ℕ0) |
19 | 18 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑙 ∈ (0...𝑘)) → 𝑙 ∈ ℕ0) |
20 | 1, 2, 13, 14, 15, 19 | knoppcnlem3 31655 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑙 ∈ (0...𝑘)) → ((𝐹‘𝑤)‘𝑙) ∈ ℝ) |
21 | 20 | recnd 9947 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑙 ∈ (0...𝑘)) → ((𝐹‘𝑤)‘𝑙) ∈ ℂ) |
22 | 9, 12, 21 | fsumser 14308 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) →
Σ𝑙 ∈ (0...𝑘)((𝐹‘𝑤)‘𝑙) = (seq0( + , (𝐹‘𝑤))‘𝑘)) |
23 | 22 | eqcomd 2616 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) → (seq0( +
, (𝐹‘𝑤))‘𝑘) = Σ𝑙 ∈ (0...𝑘)((𝐹‘𝑤)‘𝑙)) |
24 | 23 | mpteq2dva 4672 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑤 ∈ ℝ ↦ (seq0( +
, (𝐹‘𝑤))‘𝑘)) = (𝑤 ∈ ℝ ↦ Σ𝑙 ∈ (0...𝑘)((𝐹‘𝑤)‘𝑙))) |
25 | 8, 24 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘) = (𝑤 ∈ ℝ ↦ Σ𝑙 ∈ (0...𝑘)((𝐹‘𝑤)‘𝑙))) |
26 | | eqid 2610 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
27 | | retopon 22377 |
. . . . . . 7
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
28 | 27 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(topGen‘ran (,)) ∈ (TopOn‘ℝ)) |
29 | | fzfid 12634 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(0...𝑘) ∈
Fin) |
30 | 4 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑘)) → 𝑁 ∈ ℕ) |
31 | 6 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑘)) → 𝐶 ∈ ℝ) |
32 | 18 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑘)) → 𝑙 ∈ ℕ0) |
33 | 1, 2, 30, 31, 32 | knoppcnlem10 31662 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑘)) → (𝑤 ∈ ℝ ↦ ((𝐹‘𝑤)‘𝑙)) ∈ ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld))) |
34 | 26, 28, 29, 33 | fsumcn 22481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑤 ∈ ℝ ↦
Σ𝑙 ∈ (0...𝑘)((𝐹‘𝑤)‘𝑙)) ∈ ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld))) |
35 | | ax-resscn 9872 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
36 | | ssid 3587 |
. . . . . . 7
⊢ ℂ
⊆ ℂ |
37 | 35, 36 | pm3.2i 470 |
. . . . . 6
⊢ (ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) |
38 | 26 | tgioo2 22414 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
39 | | fvex 6113 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) ∈ V |
40 | 26 | cnfldtopon 22396 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
41 | 40 | toponunii 20547 |
. . . . . . . . . 10
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
42 | 41 | restid 15917 |
. . . . . . . . 9
⊢
((TopOpen‘ℂfld) ∈ V →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
43 | 39, 42 | ax-mp 5 |
. . . . . . . 8
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
44 | 43 | eqcomi 2619 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
45 | 26, 38, 44 | cncfcn 22520 |
. . . . . 6
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℝ–cn→ℂ) = ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld))) |
46 | 37, 45 | ax-mp 5 |
. . . . 5
⊢
(ℝ–cn→ℂ) =
((topGen‘ran (,)) Cn
(TopOpen‘ℂfld)) |
47 | 34, 46 | syl6eleqr 2699 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑤 ∈ ℝ ↦
Σ𝑙 ∈ (0...𝑘)((𝐹‘𝑤)‘𝑙)) ∈ (ℝ–cn→ℂ)) |
48 | 25, 47 | eqeltrd 2688 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘) ∈ (ℝ–cn→ℂ)) |
49 | | eqid 2610 |
. . 3
⊢ (𝑘 ∈ ℕ0
↦ (seq0( ∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)) = (𝑘 ∈ ℕ0 ↦ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)) |
50 | 48, 49 | fmptd 6292 |
. 2
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)):ℕ0⟶(ℝ–cn→ℂ)) |
51 | | 0z 11265 |
. . . . . 6
⊢ 0 ∈
ℤ |
52 | | seqfn 12675 |
. . . . . 6
⊢ (0 ∈
ℤ → seq0( ∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn
(ℤ≥‘0)) |
53 | 51, 52 | ax-mp 5 |
. . . . 5
⊢ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn
(ℤ≥‘0) |
54 | 17 | fneq2i 5900 |
. . . . 5
⊢ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn ℕ0 ↔ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn
(ℤ≥‘0)) |
55 | 53, 54 | mpbir 220 |
. . . 4
⊢ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn ℕ0 |
56 | | dffn5 6151 |
. . . 4
⊢ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn ℕ0 ↔ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) = (𝑘 ∈ ℕ0 ↦ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘))) |
57 | 55, 56 | mpbi 219 |
. . 3
⊢ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) = (𝑘 ∈ ℕ0 ↦ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)) |
58 | 57 | feq1i 5949 |
. 2
⊢ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))):ℕ0⟶(ℝ–cn→ℂ) ↔ (𝑘 ∈ ℕ0 ↦ (seq0(
∘𝑓 + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)):ℕ0⟶(ℝ–cn→ℂ)) |
59 | 50, 58 | sylibr 223 |
1
⊢ (𝜑 → seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))):ℕ0⟶(ℝ–cn→ℂ)) |