Theorem knoppndvlem4

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 15-Jun-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

	Ref	Expression
Hypotheses	knoppndvlem4.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
	knoppndvlem4.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
	knoppndvlem4.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
	knoppndvlem4.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	knoppndvlem4.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
	knoppndvlem4.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	knoppndvlem4	⊢ ( 𝜑 → seq 0 ( + , ( 𝐹 ‘ 𝐴 ) ) ⇝ ( 𝑊 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem4.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		knoppndvlem4.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		knoppndvlem4.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
4		knoppndvlem4.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
5		knoppndvlem4.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
6		knoppndvlem4.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
8		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
9	5	knoppndvlem3	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( abs ‘ 𝐶 ) < 1 ) )
10	9	simpld	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
11	1 2 6 10	knoppcnlem8	⊢ ( 𝜑 → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) : ℕ0 ⟶ ( ℂ ↑m ℝ ) )
12		seqex	⊢ seq 0 ( + , ( 𝐹 ‘ 𝐴 ) ) ∈ V
13	12	a1i	⊢ ( 𝜑 → seq 0 ( + , ( 𝐹 ‘ 𝐴 ) ) ∈ V )
14	6	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ∈ ℕ )
15	10	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ ℝ )
16		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
17	1 2 14 15 16	knoppcnlem7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) = ( 𝑣 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹 ‘ 𝑣 ) ) ‘ 𝑘 ) ) )
18	17	fveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ‘ 𝐴 ) = ( ( 𝑣 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹 ‘ 𝑣 ) ) ‘ 𝑘 ) ) ‘ 𝐴 ) )
19		eqid	⊢ ( 𝑣 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹 ‘ 𝑣 ) ) ‘ 𝑘 ) ) = ( 𝑣 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹 ‘ 𝑣 ) ) ‘ 𝑘 ) )
20		fveq2	⊢ ( 𝑣 = 𝐴 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) )
21	20	seqeq3d	⊢ ( 𝑣 = 𝐴 → seq 0 ( + , ( 𝐹 ‘ 𝑣 ) ) = seq 0 ( + , ( 𝐹 ‘ 𝐴 ) ) )
22	21	fveq1d	⊢ ( 𝑣 = 𝐴 → ( seq 0 ( + , ( 𝐹 ‘ 𝑣 ) ) ‘ 𝑘 ) = ( seq 0 ( + , ( 𝐹 ‘ 𝐴 ) ) ‘ 𝑘 ) )
23		fvexd	⊢ ( 𝜑 → ( seq 0 ( + , ( 𝐹 ‘ 𝐴 ) ) ‘ 𝑘 ) ∈ V )
24	19 22 4 23	fvmptd3	⊢ ( 𝜑 → ( ( 𝑣 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹 ‘ 𝑣 ) ) ‘ 𝑘 ) ) ‘ 𝐴 ) = ( seq 0 ( + , ( 𝐹 ‘ 𝐴 ) ) ‘ 𝑘 ) )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑣 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹 ‘ 𝑣 ) ) ‘ 𝑘 ) ) ‘ 𝐴 ) = ( seq 0 ( + , ( 𝐹 ‘ 𝐴 ) ) ‘ 𝑘 ) )
26	18 25	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ‘ 𝐴 ) = ( seq 0 ( + , ( 𝐹 ‘ 𝐴 ) ) ‘ 𝑘 ) )
27	9	simprd	⊢ ( 𝜑 → ( abs ‘ 𝐶 ) < 1 )
28	1 2 3 6 10 27	knoppcnlem9	⊢ ( 𝜑 → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑊 )
29	7 8 11 4 13 26 28	ulmclm	⊢ ( 𝜑 → seq 0 ( + , ( 𝐹 ‘ 𝐴 ) ) ⇝ ( 𝑊 ‘ 𝐴 ) )