Metamath Proof Explorer


Theorem knoppcnlem7

Description: Lemma for knoppcn . (Contributed by Asger C. Ipsen, 4-Apr-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

Ref Expression
Hypotheses knoppcnlem7.t 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
knoppcnlem7.f 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
knoppcnlem7.n ( 𝜑𝑁 ∈ ℕ )
knoppcnlem7.1 ( 𝜑𝐶 ∈ ℝ )
knoppcnlem7.2 ( 𝜑𝑀 ∈ ℕ0 )
Assertion knoppcnlem7 ( 𝜑 → ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑀 ) = ( 𝑤 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹𝑤 ) ) ‘ 𝑀 ) ) )

Proof

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 ( + , ( 𝐹𝑤 ) ) ‘ 𝑀 ) ) )