Theorem knoppcnlem8

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

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

Proof

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 ℝ ) )