Step | Hyp | Ref
| Expression |
1 | | knoppcnlem11.t |
. . . . . 6
⊢ 𝑇 = (𝑥 ∈ ℝ ↦
(abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) |
2 | | knoppcnlem11.f |
. . . . . 6
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) |
3 | | knoppcnlem11.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
4 | 3 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑁 ∈
ℕ) |
5 | | knoppcnlem11.1 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℝ) |
6 | 5 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈
ℝ) |
7 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
8 | 1, 2, 4, 6, 7 | knoppcnlem7 34416 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘) = (𝑤 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑤))‘𝑘))) |
9 | | eqidd 2738 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑙 ∈ (0...𝑘)) → ((𝐹‘𝑤)‘𝑙) = ((𝐹‘𝑤)‘𝑙)) |
10 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) → 𝑘 ∈
ℕ0) |
11 | | elnn0uz 12479 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
↔ 𝑘 ∈
(ℤ≥‘0)) |
12 | 10, 11 | sylib 221 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) → 𝑘 ∈
(ℤ≥‘0)) |
13 | 4 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑙 ∈ (0...𝑘)) → 𝑁 ∈ ℕ) |
14 | 6 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑙 ∈ (0...𝑘)) → 𝐶 ∈ ℝ) |
15 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑙 ∈ (0...𝑘)) → 𝑤 ∈ ℝ) |
16 | | elfzuz 13108 |
. . . . . . . . . . . 12
⊢ (𝑙 ∈ (0...𝑘) → 𝑙 ∈
(ℤ≥‘0)) |
17 | | nn0uz 12476 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
18 | 16, 17 | eleqtrrdi 2849 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ (0...𝑘) → 𝑙 ∈ ℕ0) |
19 | 18 | adantl 485 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑙 ∈ (0...𝑘)) → 𝑙 ∈ ℕ0) |
20 | 1, 2, 13, 14, 15, 19 | knoppcnlem3 34412 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑙 ∈ (0...𝑘)) → ((𝐹‘𝑤)‘𝑙) ∈ ℝ) |
21 | 20 | recnd 10861 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑙 ∈ (0...𝑘)) → ((𝐹‘𝑤)‘𝑙) ∈ ℂ) |
22 | 9, 12, 21 | fsumser 15294 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) →
Σ𝑙 ∈ (0...𝑘)((𝐹‘𝑤)‘𝑙) = (seq0( + , (𝐹‘𝑤))‘𝑘)) |
23 | 22 | eqcomd 2743 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) → (seq0( +
, (𝐹‘𝑤))‘𝑘) = Σ𝑙 ∈ (0...𝑘)((𝐹‘𝑤)‘𝑙)) |
24 | 23 | mpteq2dva 5150 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑤 ∈ ℝ ↦ (seq0( +
, (𝐹‘𝑤))‘𝑘)) = (𝑤 ∈ ℝ ↦ Σ𝑙 ∈ (0...𝑘)((𝐹‘𝑤)‘𝑙))) |
25 | 8, 24 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘) = (𝑤 ∈ ℝ ↦ Σ𝑙 ∈ (0...𝑘)((𝐹‘𝑤)‘𝑙))) |
26 | | eqid 2737 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
27 | | retopon 23661 |
. . . . . . 7
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
28 | 27 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(topGen‘ran (,)) ∈ (TopOn‘ℝ)) |
29 | | fzfid 13546 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(0...𝑘) ∈
Fin) |
30 | 4 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑘)) → 𝑁 ∈ ℕ) |
31 | 6 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑘)) → 𝐶 ∈ ℝ) |
32 | 18 | adantl 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑘)) → 𝑙 ∈ ℕ0) |
33 | 1, 2, 30, 31, 32 | knoppcnlem10 34419 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑙 ∈ (0...𝑘)) → (𝑤 ∈ ℝ ↦ ((𝐹‘𝑤)‘𝑙)) ∈ ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld))) |
34 | 26, 28, 29, 33 | fsumcn 23767 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑤 ∈ ℝ ↦
Σ𝑙 ∈ (0...𝑘)((𝐹‘𝑤)‘𝑙)) ∈ ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld))) |
35 | | ax-resscn 10786 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
36 | | ssid 3923 |
. . . . . . 7
⊢ ℂ
⊆ ℂ |
37 | 35, 36 | pm3.2i 474 |
. . . . . 6
⊢ (ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) |
38 | 26 | tgioo2 23700 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
39 | 26 | cnfldtopon 23680 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
40 | 39 | toponrestid 21818 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
41 | 26, 38, 40 | cncfcn 23807 |
. . . . . 6
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℝ–cn→ℂ) = ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld))) |
42 | 37, 41 | ax-mp 5 |
. . . . 5
⊢
(ℝ–cn→ℂ) =
((topGen‘ran (,)) Cn
(TopOpen‘ℂfld)) |
43 | 34, 42 | eleqtrrdi 2849 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑤 ∈ ℝ ↦
Σ𝑙 ∈ (0...𝑘)((𝐹‘𝑤)‘𝑙)) ∈ (ℝ–cn→ℂ)) |
44 | 25, 43 | eqeltrd 2838 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘) ∈ (ℝ–cn→ℂ)) |
45 | 44 | fmpttd 6932 |
. 2
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)):ℕ0⟶(ℝ–cn→ℂ)) |
46 | | 0z 12187 |
. . . . . 6
⊢ 0 ∈
ℤ |
47 | | seqfn 13586 |
. . . . . 6
⊢ (0 ∈
ℤ → seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn
(ℤ≥‘0)) |
48 | 46, 47 | ax-mp 5 |
. . . . 5
⊢ seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn
(ℤ≥‘0) |
49 | 17 | fneq2i 6477 |
. . . . 5
⊢ (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn ℕ0 ↔ seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn
(ℤ≥‘0)) |
50 | 48, 49 | mpbir 234 |
. . . 4
⊢ seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn ℕ0 |
51 | | dffn5 6771 |
. . . 4
⊢ (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn ℕ0 ↔ seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) = (𝑘 ∈ ℕ0 ↦ (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘))) |
52 | 50, 51 | mpbi 233 |
. . 3
⊢ seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) = (𝑘 ∈ ℕ0 ↦ (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)) |
53 | 52 | feq1i 6536 |
. 2
⊢ (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))):ℕ0⟶(ℝ–cn→ℂ) ↔ (𝑘 ∈ ℕ0 ↦ (seq0(
∘f + , (𝑚 ∈
ℕ0 ↦ (𝑧
∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)):ℕ0⟶(ℝ–cn→ℂ)) |
54 | 45, 53 | sylibr 237 |
1
⊢ (𝜑 → seq0( ∘f
+ , (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))):ℕ0⟶(ℝ–cn→ℂ)) |