knoppcnlem11

	Ref	Expression
Hypotheses	knoppcnlem11.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
	knoppcnlem11.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
	knoppcnlem11.n	$⊢ φ \to N \in ℕ$
	knoppcnlem11.1	$⊢ φ \to C \in ℝ$
Assertion	knoppcnlem11	$⊢ φ \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) : ℕ_{0} ⟶ ℝ \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem11.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
2		knoppcnlem11.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
3		knoppcnlem11.n	$⊢ φ \to N \in ℕ$
4		knoppcnlem11.1	$⊢ φ \to C \in ℝ$
5	3	adantr	$⊢ (φ \land k \in ℕ_{0}) \to N \in ℕ$
6	4	adantr	$⊢ (φ \land k \in ℕ_{0}) \to C \in ℝ$
7		simpr	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
8	1 2 5 6 7	knoppcnlem7	$⊢ (φ \land k \in ℕ_{0}) \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) (k) = (w \in ℝ ⟼ seq 0 (+ F (w)) (k))$
9		eqidd	$⊢ (((φ \land k \in ℕ_{0}) \land w \in ℝ) \land l \in (0 \dots k)) \to F (w) (l) = F (w) (l)$
10		simplr	$⊢ ((φ \land k \in ℕ_{0}) \land w \in ℝ) \to k \in ℕ_{0}$
11		elnn0uz	$⊢ k \in ℕ_{0} \leftrightarrow k \in ℤ_{\geq 0}$
12	10 11	sylib	$⊢ ((φ \land k \in ℕ_{0}) \land w \in ℝ) \to k \in ℤ_{\geq 0}$
13	5	ad2antrr	$⊢ (((φ \land k \in ℕ_{0}) \land w \in ℝ) \land l \in (0 \dots k)) \to N \in ℕ$
14	6	ad2antrr	$⊢ (((φ \land k \in ℕ_{0}) \land w \in ℝ) \land l \in (0 \dots k)) \to C \in ℝ$
15		simplr	$⊢ (((φ \land k \in ℕ_{0}) \land w \in ℝ) \land l \in (0 \dots k)) \to w \in ℝ$
16		elfzuz	$⊢ l \in (0 \dots k) \to l \in ℤ_{\geq 0}$
17		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
18	16 17	eleqtrrdi	$⊢ l \in (0 \dots k) \to l \in ℕ_{0}$
19	18	adantl	$⊢ (((φ \land k \in ℕ_{0}) \land w \in ℝ) \land l \in (0 \dots k)) \to l \in ℕ_{0}$
20	1 2 13 14 15 19	knoppcnlem3	$⊢ (((φ \land k \in ℕ_{0}) \land w \in ℝ) \land l \in (0 \dots k)) \to F (w) (l) \in ℝ$
21	20	recnd	$⊢ (((φ \land k \in ℕ_{0}) \land w \in ℝ) \land l \in (0 \dots k)) \to F (w) (l) \in ℂ$
22	9 12 21	fsumser	$⊢ ((φ \land k \in ℕ_{0}) \land w \in ℝ) \to \sum_{l = 0}^{k} F (w) (l) = seq 0 (+ F (w)) (k)$
23	22	eqcomd	$⊢ ((φ \land k \in ℕ_{0}) \land w \in ℝ) \to seq 0 (+ F (w)) (k) = \sum_{l = 0}^{k} F (w) (l)$
24	23	mpteq2dva	$⊢ (φ \land k \in ℕ_{0}) \to (w \in ℝ ⟼ seq 0 (+ F (w)) (k)) = (w \in ℝ ⟼ \sum_{l = 0}^{k} F (w) (l))$
25	8 24	eqtrd	$⊢ (φ \land k \in ℕ_{0}) \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) (k) = (w \in ℝ ⟼ \sum_{l = 0}^{k} F (w) (l))$
26		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
27		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
28	27	a1i	$⊢ (φ \land k \in ℕ_{0}) \to topGen (ran (.)) \in TopOn (ℝ)$
29		fzfid	$⊢ (φ \land k \in ℕ_{0}) \to (0 \dots k) \in Fin$
30	5	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land l \in (0 \dots k)) \to N \in ℕ$
31	6	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land l \in (0 \dots k)) \to C \in ℝ$
32	18	adantl	$⊢ ((φ \land k \in ℕ_{0}) \land l \in (0 \dots k)) \to l \in ℕ_{0}$
33	1 2 30 31 32	knoppcnlem10	$⊢ ((φ \land k \in ℕ_{0}) \land l \in (0 \dots k)) \to (w \in ℝ ⟼ F (w) (l)) \in (topGen (ran (.)) Cn TopOpen (ℂ_{fld}))$
34	26 28 29 33	fsumcn	$⊢ (φ \land k \in ℕ_{0}) \to (w \in ℝ ⟼ \sum_{l = 0}^{k} F (w) (l)) \in (topGen (ran (.)) Cn TopOpen (ℂ_{fld}))$
35		ax-resscn	$⊢ ℝ \subseteq ℂ$
36		ssid	$⊢ ℂ \subseteq ℂ$
37	35 36	pm3.2i	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ)$
38	26	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
39	26	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
40	39	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
41	26 38 40	cncfcn	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to ℝ \underset{cn}{⟶} ℂ = topGen (ran (.)) Cn TopOpen (ℂ_{fld})$
42	37 41	ax-mp	$⊢ ℝ \underset{cn}{⟶} ℂ = topGen (ran (.)) Cn TopOpen (ℂ_{fld})$
43	34 42	eleqtrrdi	$⊢ (φ \land k \in ℕ_{0}) \to (w \in ℝ ⟼ \sum_{l = 0}^{k} F (w) (l)) : ℝ \underset{cn}{⟶} ℂ$
44	25 43	eqeltrd	$⊢ (φ \land k \in ℕ_{0}) \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) (k) : ℝ \underset{cn}{⟶} ℂ$
45	44	fmpttd	$⊢ φ \to (k \in ℕ_{0} ⟼ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) (k)) : ℕ_{0} ⟶ ℝ \underset{cn}{⟶} ℂ$
46		0z	$⊢ 0 \in ℤ$
47		seqfn	$⊢ 0 \in ℤ \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) Fn ℤ_{\geq 0}$
48	46 47	ax-mp	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) Fn ℤ_{\geq 0}$
49	17	fneq2i	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) Fn ℕ_{0} \leftrightarrow seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) Fn ℤ_{\geq 0}$
50	48 49	mpbir	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) Fn ℕ_{0}$
51		dffn5	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) Fn ℕ_{0} \leftrightarrow seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) = (k \in ℕ_{0} ⟼ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) (k))$
52	50 51	mpbi	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) = (k \in ℕ_{0} ⟼ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) (k))$
53	52	feq1i	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) : ℕ_{0} ⟶ ℝ \underset{cn}{⟶} ℂ \leftrightarrow (k \in ℕ_{0} ⟼ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) (k)) : ℕ_{0} ⟶ ℝ \underset{cn}{⟶} ℂ$
54	45 53	sylibr	$⊢ φ \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) : ℕ_{0} ⟶ ℝ \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem knoppcnlem11

Proof