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