knoppcnlem9

	Ref	Expression
Hypotheses	knoppcnlem9.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
	knoppcnlem9.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
	knoppcnlem9.w	$⊢ W = (w \in ℝ ⟼ \sum_{i \in ℕ_{0}} F (w) (i))$
	knoppcnlem9.n	$⊢ φ \to N \in ℕ$
	knoppcnlem9.1	$⊢ φ \to C \in ℝ$
	knoppcnlem9.2	$⊢ φ \to \|C\| < 1$
Assertion	knoppcnlem9	$⊢ φ \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) W$

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem9.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
2		knoppcnlem9.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
3		knoppcnlem9.w	$⊢ W = (w \in ℝ ⟼ \sum_{i \in ℕ_{0}} F (w) (i))$
4		knoppcnlem9.n	$⊢ φ \to N \in ℕ$
5		knoppcnlem9.1	$⊢ φ \to C \in ℝ$
6		knoppcnlem9.2	$⊢ φ \to \|C\| < 1$
7	1 2 4 5 6	knoppcnlem6	$⊢ φ \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \in dom \underset{u}{⇝} (ℝ)$
8		seqex	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \in V$
9	8	eldm	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \in dom \underset{u}{⇝} (ℝ) \leftrightarrow \exists f seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f$
10	7 9	sylib	$⊢ φ \to \exists f seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f$
11		simpr	$⊢ (φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f$
12		ulmcl	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f \to f : ℝ ⟶ ℂ$
13	12	feqmptd	$⊢ seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f \to f = (w \in ℝ ⟼ f (w))$
14	13	adantl	$⊢ (φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \to f = (w \in ℝ ⟼ f (w))$
15		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
16		0zd	$⊢ ((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \to 0 \in ℤ$
17		eqidd	$⊢ (((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \land i \in ℕ_{0}) \to F (w) (i) = F (w) (i)$
18	4	ad2antrr	$⊢ ((φ \land w \in ℝ) \land i \in ℕ_{0}) \to N \in ℕ$
19	5	ad2antrr	$⊢ ((φ \land w \in ℝ) \land i \in ℕ_{0}) \to C \in ℝ$
20		simplr	$⊢ ((φ \land w \in ℝ) \land i \in ℕ_{0}) \to w \in ℝ$
21		simpr	$⊢ ((φ \land w \in ℝ) \land i \in ℕ_{0}) \to i \in ℕ_{0}$
22	1 2 18 19 20 21	knoppcnlem3	$⊢ ((φ \land w \in ℝ) \land i \in ℕ_{0}) \to F (w) (i) \in ℝ$
23	22	adantllr	$⊢ (((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \land i \in ℕ_{0}) \to F (w) (i) \in ℝ$
24	23	recnd	$⊢ (((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \land i \in ℕ_{0}) \to F (w) (i) \in ℂ$
25	1 2 4 5	knoppcnlem8	$⊢ φ \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) : ℕ_{0} ⟶ ℂ^{ℝ}$
26	25	ad2antrr	$⊢ ((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) : ℕ_{0} ⟶ ℂ^{ℝ}$
27		simpr	$⊢ ((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \to w \in ℝ$
28		seqex	$⊢ seq 0 (+ F (w)) \in V$
29	28	a1i	$⊢ ((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \to seq 0 (+ F (w)) \in V$
30	4	ad2antrr	$⊢ ((φ \land w \in ℝ) \land k \in ℕ_{0}) \to N \in ℕ$
31	5	ad2antrr	$⊢ ((φ \land w \in ℝ) \land k \in ℕ_{0}) \to C \in ℝ$
32		simpr	$⊢ ((φ \land w \in ℝ) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
33	1 2 30 31 32	knoppcnlem7	$⊢ ((φ \land w \in ℝ) \land k \in ℕ_{0}) \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) (k) = (v \in ℝ ⟼ seq 0 (+ F (v)) (k))$
34	33	adantllr	$⊢ (((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \land k \in ℕ_{0}) \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) (k) = (v \in ℝ ⟼ seq 0 (+ F (v)) (k))$
35	34	fveq1d	$⊢ (((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \land k \in ℕ_{0}) \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) (k) (w) = (v \in ℝ ⟼ seq 0 (+ F (v)) (k)) (w)$
36		eqid	$⊢ (v \in ℝ ⟼ seq 0 (+ F (v)) (k)) = (v \in ℝ ⟼ seq 0 (+ F (v)) (k))$
37		fveq2	$⊢ v = w \to F (v) = F (w)$
38	37	seqeq3d	$⊢ v = w \to seq 0 (+ F (v)) = seq 0 (+ F (w))$
39	38	fveq1d	$⊢ v = w \to seq 0 (+ F (v)) (k) = seq 0 (+ F (w)) (k)$
40	27	adantr	$⊢ (((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \land k \in ℕ_{0}) \to w \in ℝ$
41		fvexd	$⊢ (((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \land k \in ℕ_{0}) \to seq 0 (+ F (w)) (k) \in V$
42	36 39 40 41	fvmptd3	$⊢ (((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \land k \in ℕ_{0}) \to (v \in ℝ ⟼ seq 0 (+ F (v)) (k)) (w) = seq 0 (+ F (w)) (k)$
43	35 42	eqtrd	$⊢ (((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \land k \in ℕ_{0}) \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) (k) (w) = seq 0 (+ F (w)) (k)$
44		simplr	$⊢ ((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f$
45	15 16 26 27 29 43 44	ulmclm	$⊢ ((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \to seq 0 (+ F (w)) ⇝ f (w)$
46	15 16 17 24 45	isumclim	$⊢ ((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \to \sum_{i \in ℕ_{0}} F (w) (i) = f (w)$
47	46	eqcomd	$⊢ ((φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \land w \in ℝ) \to f (w) = \sum_{i \in ℕ_{0}} F (w) (i)$
48	47	mpteq2dva	$⊢ (φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \to (w \in ℝ ⟼ f (w)) = (w \in ℝ ⟼ \sum_{i \in ℕ_{0}} F (w) (i))$
49	3	a1i	$⊢ (φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \to W = (w \in ℝ ⟼ \sum_{i \in ℕ_{0}} F (w) (i))$
50	49	eqcomd	$⊢ (φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \to (w \in ℝ ⟼ \sum_{i \in ℕ_{0}} F (w) (i)) = W$
51	14 48 50	3eqtrd	$⊢ (φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \to f = W$
52	11 51	breqtrd	$⊢ (φ \land seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f) \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) W$
53	52	ex	$⊢ φ \to (seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) W)$
54	53	exlimdv	$⊢ φ \to (\exists f seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) f \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) W)$
55	10 54	mpd	$⊢ φ \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \underset{u}{⇝} (ℝ) W$

Metamath Proof Explorer

Theorem knoppcnlem9

Proof