Step | Hyp | Ref
| Expression |
1 | | knoppcnlem8.t |
. . . . 5
⊢ 𝑇 = (𝑥 ∈ ℝ ↦
(abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) |
2 | | knoppcnlem8.f |
. . . . 5
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) |
3 | | knoppcnlem8.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
4 | 3 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑁 ∈
ℕ) |
5 | | knoppcnlem8.1 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) |
6 | 5 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈
ℝ) |
7 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
8 | 1, 2, 4, 6, 7 | knoppcnlem7 32489 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘) = (𝑤 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑤))‘𝑘))) |
9 | | simplr 792 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) → 𝑘 ∈
ℕ0) |
10 | | nn0uz 11722 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
11 | 9, 10 | syl6eleq 2711 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) → 𝑘 ∈
(ℤ≥‘0)) |
12 | 4 | ad2antrr 762 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑎 ∈ (0...𝑘)) → 𝑁 ∈ ℕ) |
13 | 6 | ad2antrr 762 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑎 ∈ (0...𝑘)) → 𝐶 ∈ ℝ) |
14 | | simplr 792 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑎 ∈ (0...𝑘)) → 𝑤 ∈ ℝ) |
15 | | elfznn0 12433 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (0...𝑘) → 𝑎 ∈ ℕ0) |
16 | 15 | adantl 482 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑎 ∈ (0...𝑘)) → 𝑎 ∈ ℕ0) |
17 | 1, 2, 12, 13, 14, 16 | knoppcnlem3 32485 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑎 ∈ (0...𝑘)) → ((𝐹‘𝑤)‘𝑎) ∈ ℝ) |
18 | 17 | recnd 10068 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ 𝑎 ∈ (0...𝑘)) → ((𝐹‘𝑤)‘𝑎) ∈ ℂ) |
19 | | addcl 10018 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 + 𝑏) ∈ ℂ) |
20 | 19 | adantl 482 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) ∧ (𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ)) → (𝑎 + 𝑏) ∈ ℂ) |
21 | 11, 18, 20 | seqcl 12821 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑤 ∈ ℝ) → (seq0( +
, (𝐹‘𝑤))‘𝑘) ∈ ℂ) |
22 | | eqid 2622 |
. . . . . 6
⊢ (𝑤 ∈ ℝ ↦ (seq0( +
, (𝐹‘𝑤))‘𝑘)) = (𝑤 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑤))‘𝑘)) |
23 | 21, 22 | fmptd 6385 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑤 ∈ ℝ ↦ (seq0( +
, (𝐹‘𝑤))‘𝑘)):ℝ⟶ℂ) |
24 | | cnex 10017 |
. . . . . . 7
⊢ ℂ
∈ V |
25 | | reex 10027 |
. . . . . . 7
⊢ ℝ
∈ V |
26 | 24, 25 | pm3.2i 471 |
. . . . . 6
⊢ (ℂ
∈ V ∧ ℝ ∈ V) |
27 | | elmapg 7870 |
. . . . . 6
⊢ ((ℂ
∈ V ∧ ℝ ∈ V) → ((𝑤 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑤))‘𝑘)) ∈ (ℂ ↑𝑚
ℝ) ↔ (𝑤 ∈
ℝ ↦ (seq0( + , (𝐹‘𝑤))‘𝑘)):ℝ⟶ℂ)) |
28 | 26, 27 | ax-mp 5 |
. . . . 5
⊢ ((𝑤 ∈ ℝ ↦ (seq0( +
, (𝐹‘𝑤))‘𝑘)) ∈ (ℂ ↑𝑚
ℝ) ↔ (𝑤 ∈
ℝ ↦ (seq0( + , (𝐹‘𝑤))‘𝑘)):ℝ⟶ℂ) |
29 | 23, 28 | sylibr 224 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑤 ∈ ℝ ↦ (seq0( +
, (𝐹‘𝑤))‘𝑘)) ∈ (ℂ ↑𝑚
ℝ)) |
30 | 8, 29 | eqeltrd 2701 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘) ∈ (ℂ ↑𝑚
ℝ)) |
31 | | eqid 2622 |
. . 3
⊢ (𝑘 ∈ ℕ0
↦ (seq0( ∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)) = (𝑘 ∈ ℕ0 ↦ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)) |
32 | 30, 31 | fmptd 6385 |
. 2
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)):ℕ0⟶(ℂ
↑𝑚 ℝ)) |
33 | | 0z 11388 |
. . . . . 6
⊢ 0 ∈
ℤ |
34 | | seqfn 12813 |
. . . . . 6
⊢ (0 ∈
ℤ → seq0( ∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn
(ℤ≥‘0)) |
35 | 33, 34 | ax-mp 5 |
. . . . 5
⊢ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn
(ℤ≥‘0) |
36 | 10 | fneq2i 5986 |
. . . . 5
⊢ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn ℕ0 ↔ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn
(ℤ≥‘0)) |
37 | 35, 36 | mpbir 221 |
. . . 4
⊢ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn ℕ0 |
38 | | dffn5 6241 |
. . . 4
⊢ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) Fn ℕ0 ↔ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) = (𝑘 ∈ ℕ0 ↦ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘))) |
39 | 37, 38 | mpbi 220 |
. . 3
⊢ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) = (𝑘 ∈ ℕ0 ↦ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)) |
40 | 39 | feq1i 6036 |
. 2
⊢ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))):ℕ0⟶(ℂ
↑𝑚 ℝ) ↔ (𝑘 ∈ ℕ0 ↦ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)):ℕ0⟶(ℂ
↑𝑚 ℝ)) |
41 | 32, 40 | sylibr 224 |
1
⊢ (𝜑 → seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))):ℕ0⟶(ℂ
↑𝑚 ℝ)) |