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