Step |
Hyp |
Ref |
Expression |
1 |
|
knoppcnlem7.t |
⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) ) |
2 |
|
knoppcnlem7.f |
⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) ) |
3 |
|
knoppcnlem7.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
4 |
|
knoppcnlem7.1 |
⊢ ( 𝜑 → 𝐶 ∈ ℝ ) |
5 |
|
knoppcnlem7.2 |
⊢ ( 𝜑 → 𝑀 ∈ ℕ0 ) |
6 |
|
reex |
⊢ ℝ ∈ V |
7 |
6
|
a1i |
⊢ ( 𝜑 → ℝ ∈ V ) |
8 |
|
elnn0uz |
⊢ ( 𝑀 ∈ ℕ0 ↔ 𝑀 ∈ ( ℤ≥ ‘ 0 ) ) |
9 |
5 8
|
sylib |
⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) ) |
10 |
|
eqid |
⊢ ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) |
11 |
10
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) |
12 |
|
fveq2 |
⊢ ( 𝑧 = 𝑤 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) |
13 |
12
|
fveq1d |
⊢ ( 𝑧 = 𝑤 → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑚 ) ) |
14 |
13
|
cbvmptv |
⊢ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) = ( 𝑤 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑚 ) ) |
15 |
14
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑚 = 𝑘 ) → ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) = ( 𝑤 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑚 ) ) ) |
16 |
|
fveq2 |
⊢ ( 𝑚 = 𝑘 → ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑚 ) = ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑘 ) ) |
17 |
16
|
mpteq2dv |
⊢ ( 𝑚 = 𝑘 → ( 𝑤 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑚 ) ) = ( 𝑤 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑘 ) ) ) |
18 |
17
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑚 = 𝑘 ) → ( 𝑤 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑚 ) ) = ( 𝑤 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑘 ) ) ) |
19 |
15 18
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑚 = 𝑘 ) → ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) = ( 𝑤 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑘 ) ) ) |
20 |
|
elfznn0 |
⊢ ( 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ℕ0 ) |
21 |
20
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ℕ0 ) |
22 |
6
|
mptex |
⊢ ( 𝑤 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑘 ) ) ∈ V |
23 |
22
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑤 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑘 ) ) ∈ V ) |
24 |
11 19 21 23
|
fvmptd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( 𝑤 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑘 ) ) ) |
25 |
7 9 24
|
seqof |
⊢ ( 𝜑 → ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑀 ) = ( 𝑤 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ‘ 𝑀 ) ) ) |