Step | Hyp | Ref
| Expression |
1 | | knoppcnlem8.t |
. . . . 5
⊢ 𝑇 = (𝑥 ∈ ℝ ↦
(abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) |
2 | | knoppcnlem8.f |
. . . . 5
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) |
3 | | knoppcnlem8.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
4 | 3 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑁 ∈
ℕ) |
5 | | knoppcnlem8.1 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) |
6 | 5 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈
ℝ) |
7 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
8 | 1, 2, 4, 6, 7 | knoppcnlem7 34416 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘) = (𝑤 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑤))‘𝑘))) |
9 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) → 𝑘 ∈
ℕ0) |
10 | | nn0uz 12476 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
11 | 9, 10 | eleqtrdi 2848 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) → 𝑘 ∈
(ℤ≥‘0)) |
12 | 4 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑎 ∈ (0...𝑘)) → 𝑁 ∈ ℕ) |
13 | 6 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑎 ∈ (0...𝑘)) → 𝐶 ∈ ℝ) |
14 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑎 ∈ (0...𝑘)) → 𝑤 ∈ ℝ) |
15 | | elfznn0 13205 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (0...𝑘) → 𝑎 ∈ ℕ0) |
16 | 15 | adantl 485 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑎 ∈ (0...𝑘)) → 𝑎 ∈ ℕ0) |
17 | 1, 2, 12, 13, 14, 16 | knoppcnlem3 34412 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑎 ∈ (0...𝑘)) → ((𝐹‘𝑤)‘𝑎) ∈ ℝ) |
18 | 17 | recnd 10861 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑎 ∈ (0...𝑘)) → ((𝐹‘𝑤)‘𝑎) ∈ ℂ) |
19 | | addcl 10811 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 + 𝑏) ∈ ℂ) |
20 | 19 | adantl 485 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ (𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ)) → (𝑎 + 𝑏) ∈ ℂ) |
21 | 11, 18, 20 | seqcl 13596 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) → (seq0( +
, (𝐹‘𝑤))‘𝑘) ∈ ℂ) |
22 | 21 | fmpttd 6932 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑤 ∈ ℝ ↦ (seq0( +
, (𝐹‘𝑤))‘𝑘)):ℝ⟶ℂ) |
23 | | cnex 10810 |
. . . . . . 7
⊢ ℂ
∈ V |
24 | | reex 10820 |
. . . . . . 7
⊢ ℝ
∈ V |
25 | 23, 24 | pm3.2i 474 |
. . . . . 6
⊢ (ℂ
∈ V ∧ ℝ ∈ V) |
26 | | elmapg 8521 |
. . . . . 6
⊢ ((ℂ
∈ V ∧ ℝ ∈ V) → ((𝑤 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑤))‘𝑘)) ∈ (ℂ ↑m
ℝ) ↔ (𝑤 ∈
ℝ ↦ (seq0( + , (𝐹‘𝑤))‘𝑘)):ℝ⟶ℂ)) |
27 | 25, 26 | ax-mp 5 |
. . . . 5
⊢ ((𝑤 ∈ ℝ ↦ (seq0( +
, (𝐹‘𝑤))‘𝑘)) ∈ (ℂ ↑m
ℝ) ↔ (𝑤 ∈
ℝ ↦ (seq0( + , (𝐹‘𝑤))‘𝑘)):ℝ⟶ℂ) |
28 | 22, 27 | sylibr 237 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑤 ∈ ℝ ↦ (seq0( +
, (𝐹‘𝑤))‘𝑘)) ∈ (ℂ ↑m
ℝ)) |
29 | 8, 28 | eqeltrd 2838 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘) ∈ (ℂ ↑m
ℝ)) |
30 | 29 | fmpttd 6932 |
. 2
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)):ℕ0⟶(ℂ
↑m ℝ)) |
31 | | 0z 12187 |
. . . . . 6
⊢ 0 ∈
ℤ |
32 | | seqfn 13586 |
. . . . . 6
⊢ (0 ∈
ℤ → seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn
(ℤ≥‘0)) |
33 | 31, 32 | ax-mp 5 |
. . . . 5
⊢ seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn
(ℤ≥‘0) |
34 | 10 | fneq2i 6477 |
. . . . 5
⊢ (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn ℕ0 ↔ seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn
(ℤ≥‘0)) |
35 | 33, 34 | mpbir 234 |
. . . 4
⊢ seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn ℕ0 |
36 | | dffn5 6771 |
. . . 4
⊢ (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn ℕ0 ↔ seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) = (𝑘 ∈ ℕ0 ↦ (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘))) |
37 | 35, 36 | mpbi 233 |
. . 3
⊢ seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) = (𝑘 ∈ ℕ0 ↦ (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)) |
38 | 37 | feq1i 6536 |
. 2
⊢ (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))):ℕ0⟶(ℂ
↑m ℝ) ↔ (𝑘 ∈ ℕ0 ↦ (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)):ℕ0⟶(ℂ
↑m ℝ)) |
39 | 30, 38 | sylibr 237 |
1
⊢ (𝜑 → seq0( ∘f
+ , (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))):ℕ0⟶(ℂ
↑m ℝ)) |