Theorem knoppcnlem11

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

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

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem11.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		knoppcnlem11.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		knoppcnlem11.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		knoppcnlem11.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		eqidd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) = ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) )
10		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) → 𝑘 ∈ ℕ0 )
11		elnn0uz	⊢ ( 𝑘 ∈ ℕ0 ↔ 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
12	10 11	sylib	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
13	5	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → 𝑁 ∈ ℕ )
14	6	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → 𝐶 ∈ ℝ )
15		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → 𝑤 ∈ ℝ )
16		elfzuz	⊢ ( 𝑙 ∈ ( 0 ... 𝑘 ) → 𝑙 ∈ ( ℤ≥ ‘ 0 ) )
17		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
18	16 17	eleqtrrdi	⊢ ( 𝑙 ∈ ( 0 ... 𝑘 ) → 𝑙 ∈ ℕ0 )
19	18	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → 𝑙 ∈ ℕ0 )
20	1 2 13 14 15 19	knoppcnlem3	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) ∈ ℝ )
21	20	recnd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) ∈ ℂ )
22	9 12 21	fsumser	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) → Σ 𝑙 ∈ ( 0 ... 𝑘 ) ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) = ( seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ‘ 𝑘 ) )
23	22	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) → ( seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ‘ 𝑘 ) = Σ 𝑙 ∈ ( 0 ... 𝑘 ) ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) )
24	23	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑤 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ‘ 𝑘 ) ) = ( 𝑤 ∈ ℝ ↦ Σ 𝑙 ∈ ( 0 ... 𝑘 ) ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) ) )
25	8 24	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) = ( 𝑤 ∈ ℝ ↦ Σ 𝑙 ∈ ( 0 ... 𝑘 ) ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) ) )
26		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
27		retopon	⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
28	27	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) )
29		fzfid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 0 ... 𝑘 ) ∈ Fin )
30	5	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → 𝑁 ∈ ℕ )
31	6	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → 𝐶 ∈ ℝ )
32	18	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → 𝑙 ∈ ℕ0 )
33	1 2 30 31 32	knoppcnlem10	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → ( 𝑤 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
34	26 28 29 33	fsumcn	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑤 ∈ ℝ ↦ Σ 𝑙 ∈ ( 0 ... 𝑘 ) ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
35		ax-resscn	⊢ ℝ ⊆ ℂ
36		ssid	⊢ ℂ ⊆ ℂ
37	35 36	pm3.2i	⊢ ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ )
38	26	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
39	26	cnfldtopon	⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
40	39	toponrestid	⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
41	26 38 40	cncfcn	⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℝ –cn→ ℂ ) = ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
42	37 41	ax-mp	⊢ ( ℝ –cn→ ℂ ) = ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) )
43	34 42	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑤 ∈ ℝ ↦ Σ 𝑙 ∈ ( 0 ... 𝑘 ) ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) ) ∈ ( ℝ –cn→ ℂ ) )
44	25 43	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ∈ ( ℝ –cn→ ℂ ) )
45	44	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ) : ℕ0 ⟶ ( ℝ –cn→ ℂ ) )
46		0z	⊢ 0 ∈ ℤ
47		seqfn	⊢ ( 0 ∈ ℤ → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) Fn ( ℤ≥ ‘ 0 ) )
48	46 47	ax-mp	⊢ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) Fn ( ℤ≥ ‘ 0 )
49	17	fneq2i	⊢ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) Fn ℕ0 ↔ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) Fn ( ℤ≥ ‘ 0 ) )
50	48 49	mpbir	⊢ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) Fn ℕ0
51		dffn5	⊢ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) Fn ℕ0 ↔ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ) )
52	50 51	mpbi	⊢ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) )
53	52	feq1i	⊢ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) : ℕ0 ⟶ ( ℝ –cn→ ℂ ) ↔ ( 𝑘 ∈ ℕ0 ↦ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ) : ℕ0 ⟶ ( ℝ –cn→ ℂ ) )
54	45 53	sylibr	⊢ ( 𝜑 → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) : ℕ0 ⟶ ( ℝ –cn→ ℂ ) )