knoppcnlem8

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

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem8.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
2		knoppcnlem8.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
3		knoppcnlem8.n	$⊢ φ \to N \in ℕ$
4		knoppcnlem8.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		simplr	$⊢ ((φ \land k \in ℕ_{0}) \land w \in ℝ) \to k \in ℕ_{0}$
10		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
11	9 10	eleqtrdi	$⊢ ((φ \land k \in ℕ_{0}) \land w \in ℝ) \to k \in ℤ_{\geq 0}$
12	5	ad2antrr	$⊢ (((φ \land k \in ℕ_{0}) \land w \in ℝ) \land a \in (0 \dots k)) \to N \in ℕ$
13	6	ad2antrr	$⊢ (((φ \land k \in ℕ_{0}) \land w \in ℝ) \land a \in (0 \dots k)) \to C \in ℝ$
14		simplr	$⊢ (((φ \land k \in ℕ_{0}) \land w \in ℝ) \land a \in (0 \dots k)) \to w \in ℝ$
15		elfznn0	$⊢ a \in (0 \dots k) \to a \in ℕ_{0}$
16	15	adantl	$⊢ (((φ \land k \in ℕ_{0}) \land w \in ℝ) \land a \in (0 \dots k)) \to a \in ℕ_{0}$
17	1 2 12 13 14 16	knoppcnlem3	$⊢ (((φ \land k \in ℕ_{0}) \land w \in ℝ) \land a \in (0 \dots k)) \to F (w) (a) \in ℝ$
18	17	recnd	$⊢ (((φ \land k \in ℕ_{0}) \land w \in ℝ) \land a \in (0 \dots k)) \to F (w) (a) \in ℂ$
19		addcl	$⊢ (a \in ℂ \land b \in ℂ) \to a + b \in ℂ$
20	19	adantl	$⊢ (((φ \land k \in ℕ_{0}) \land w \in ℝ) \land (a \in ℂ \land b \in ℂ)) \to a + b \in ℂ$
21	11 18 20	seqcl	$⊢ ((φ \land k \in ℕ_{0}) \land w \in ℝ) \to seq 0 (+ F (w)) (k) \in ℂ$
22	21	fmpttd	$⊢ (φ \land k \in ℕ_{0}) \to (w \in ℝ ⟼ seq 0 (+ F (w)) (k)) : ℝ ⟶ ℂ$
23		cnex	$⊢ ℂ \in V$
24		reex	$⊢ ℝ \in V$
25	23 24	pm3.2i	$⊢ (ℂ \in V \land ℝ \in V)$
26		elmapg	$⊢ (ℂ \in V \land ℝ \in V) \to ((w \in ℝ ⟼ seq 0 (+ F (w)) (k)) \in (ℂ^{ℝ}) \leftrightarrow (w \in ℝ ⟼ seq 0 (+ F (w)) (k)) : ℝ ⟶ ℂ)$
27	25 26	ax-mp	$⊢ (w \in ℝ ⟼ seq 0 (+ F (w)) (k)) \in (ℂ^{ℝ}) \leftrightarrow (w \in ℝ ⟼ seq 0 (+ F (w)) (k)) : ℝ ⟶ ℂ$
28	22 27	sylibr	$⊢ (φ \land k \in ℕ_{0}) \to (w \in ℝ ⟼ seq 0 (+ F (w)) (k)) \in (ℂ^{ℝ})$
29	8 28	eqeltrd	$⊢ (φ \land k \in ℕ_{0}) \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) (k) \in (ℂ^{ℝ})$
30	29	fmpttd	$⊢ φ \to (k \in ℕ_{0} ⟼ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) (k)) : ℕ_{0} ⟶ ℂ^{ℝ}$
31		0z	$⊢ 0 \in ℤ$
32		seqfn	$⊢ 0 \in ℤ \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) Fn ℤ_{\geq 0}$
33	31 32	ax-mp	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) Fn ℤ_{\geq 0}$
34	10	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}$
35	33 34	mpbir	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) Fn ℕ_{0}$
36		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))$
37	35 36	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))$
38	37	feq1i	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) : ℕ_{0} ⟶ ℂ^{ℝ} \leftrightarrow (k \in ℕ_{0} ⟼ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) (k)) : ℕ_{0} ⟶ ℂ^{ℝ}$
39	30 38	sylibr	$⊢ φ \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) : ℕ_{0} ⟶ ℂ^{ℝ}$

Metamath Proof Explorer

Theorem knoppcnlem8

Proof