knoppcnlem6

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

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem6.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
2		knoppcnlem6.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
3		knoppcnlem6.n	$⊢ φ \to N \in ℕ$
4		knoppcnlem6.1	$⊢ φ \to C \in ℝ$
5		knoppcnlem6.2	$⊢ φ \to \|C\| < 1$
6		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
7		0zd	$⊢ φ \to 0 \in ℤ$
8		reex	$⊢ ℝ \in V$
9	8	a1i	$⊢ φ \to ℝ \in V$
10	1 2 3 4	knoppcnlem5	$⊢ φ \to (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m))) : ℕ_{0} ⟶ ℂ^{ℝ}$
11		nn0ex	$⊢ ℕ_{0} \in V$
12	11	mptex	$⊢ (m \in ℕ_{0} ⟼ {\|C\|}^{m}) \in V$
13	12	a1i	$⊢ φ \to (m \in ℕ_{0} ⟼ {\|C\|}^{m}) \in V$
14		eqid	$⊢ (m \in ℕ_{0} ⟼ {\|C\|}^{m}) = (m \in ℕ_{0} ⟼ {\|C\|}^{m})$
15	14	a1i	$⊢ (φ \land k \in ℕ_{0}) \to (m \in ℕ_{0} ⟼ {\|C\|}^{m}) = (m \in ℕ_{0} ⟼ {\|C\|}^{m})$
16		simpr	$⊢ ((φ \land k \in ℕ_{0}) \land m = k) \to m = k$
17	16	oveq2d	$⊢ ((φ \land k \in ℕ_{0}) \land m = k) \to {\|C\|}^{m} = {\|C\|}^{k}$
18		simpr	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
19		ovexd	$⊢ (φ \land k \in ℕ_{0}) \to {\|C\|}^{k} \in V$
20	15 17 18 19	fvmptd	$⊢ (φ \land k \in ℕ_{0}) \to (m \in ℕ_{0} ⟼ {\|C\|}^{m}) (k) = {\|C\|}^{k}$
21	4	recnd	$⊢ φ \to C \in ℂ$
22	21	abscld	$⊢ φ \to \|C\| \in ℝ$
23	22	adantr	$⊢ (φ \land k \in ℕ_{0}) \to \|C\| \in ℝ$
24	23 18	reexpcld	$⊢ (φ \land k \in ℕ_{0}) \to {\|C\|}^{k} \in ℝ$
25	20 24	eqeltrd	$⊢ (φ \land k \in ℕ_{0}) \to (m \in ℕ_{0} ⟼ {\|C\|}^{m}) (k) \in ℝ$
26		eqid	$⊢ (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m))) = (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))$
27	26	a1i	$⊢ (φ \land (k \in ℕ_{0} \land w \in ℝ)) \to (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m))) = (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))$
28		simpr	$⊢ ((φ \land (k \in ℕ_{0} \land w \in ℝ)) \land m = k) \to m = k$
29	28	fveq2d	$⊢ ((φ \land (k \in ℕ_{0} \land w \in ℝ)) \land m = k) \to F (z) (m) = F (z) (k)$
30	29	mpteq2dv	$⊢ ((φ \land (k \in ℕ_{0} \land w \in ℝ)) \land m = k) \to (z \in ℝ ⟼ F (z) (m)) = (z \in ℝ ⟼ F (z) (k))$
31	18	adantrr	$⊢ (φ \land (k \in ℕ_{0} \land w \in ℝ)) \to k \in ℕ_{0}$
32	8	mptex	$⊢ (z \in ℝ ⟼ F (z) (k)) \in V$
33	32	a1i	$⊢ (φ \land (k \in ℕ_{0} \land w \in ℝ)) \to (z \in ℝ ⟼ F (z) (k)) \in V$
34	27 30 31 33	fvmptd	$⊢ (φ \land (k \in ℕ_{0} \land w \in ℝ)) \to (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m))) (k) = (z \in ℝ ⟼ F (z) (k))$
35		simpr	$⊢ ((φ \land (k \in ℕ_{0} \land w \in ℝ)) \land z = w) \to z = w$
36	35	fveq2d	$⊢ ((φ \land (k \in ℕ_{0} \land w \in ℝ)) \land z = w) \to F (z) = F (w)$
37	36	fveq1d	$⊢ ((φ \land (k \in ℕ_{0} \land w \in ℝ)) \land z = w) \to F (z) (k) = F (w) (k)$
38		simprr	$⊢ (φ \land (k \in ℕ_{0} \land w \in ℝ)) \to w \in ℝ$
39		fvexd	$⊢ (φ \land (k \in ℕ_{0} \land w \in ℝ)) \to F (w) (k) \in V$
40	34 37 38 39	fvmptd	$⊢ (φ \land (k \in ℕ_{0} \land w \in ℝ)) \to (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m))) (k) (w) = F (w) (k)$
41	40	fveq2d	$⊢ (φ \land (k \in ℕ_{0} \land w \in ℝ)) \to \|(m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m))) (k) (w)\| = \|F (w) (k)\|$
42	3	adantr	$⊢ (φ \land (k \in ℕ_{0} \land w \in ℝ)) \to N \in ℕ$
43	4	adantr	$⊢ (φ \land (k \in ℕ_{0} \land w \in ℝ)) \to C \in ℝ$
44	1 2 42 43 38 31	knoppcnlem4	$⊢ (φ \land (k \in ℕ_{0} \land w \in ℝ)) \to \|F (w) (k)\| \leq (m \in ℕ_{0} ⟼ {\|C\|}^{m}) (k)$
45	41 44	eqbrtrd	$⊢ (φ \land (k \in ℕ_{0} \land w \in ℝ)) \to \|(m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m))) (k) (w)\| \leq (m \in ℕ_{0} ⟼ {\|C\|}^{m}) (k)$
46	22	recnd	$⊢ φ \to \|C\| \in ℂ$
47		absidm	$⊢ C \in ℂ \to \|\|C\|\| = \|C\|$
48	21 47	syl	$⊢ φ \to \|\|C\|\| = \|C\|$
49	48 5	eqbrtrd	$⊢ φ \to \|\|C\|\| < 1$
50	46 49 20	geolim	$⊢ φ \to seq 0 (+ (m \in ℕ_{0} ⟼ {\|C\|}^{m})) ⇝ (\frac{1}{1 - \|C\|})$
51		seqex	$⊢ seq 0 (+ (m \in ℕ_{0} ⟼ {\|C\|}^{m})) \in V$
52		ovex	$⊢ \frac{1}{1 - \|C\|} \in V$
53	51 52	breldm	$⊢ seq 0 (+ (m \in ℕ_{0} ⟼ {\|C\|}^{m})) ⇝ (\frac{1}{1 - \|C\|}) \to seq 0 (+ (m \in ℕ_{0} ⟼ {\|C\|}^{m})) \in dom ⇝$
54	50 53	syl	$⊢ φ \to seq 0 (+ (m \in ℕ_{0} ⟼ {\|C\|}^{m})) \in dom ⇝$
55	6 7 9 10 13 25 45 54	mtest	$⊢ φ \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) \in dom \underset{u}{⇝} (ℝ)$

Metamath Proof Explorer

Theorem knoppcnlem6

Proof