knoppndvlem6

	Ref	Expression
Hypotheses	knoppndvlem6.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
	knoppndvlem6.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
	knoppndvlem6.w	$⊢ W = (w \in ℝ ⟼ \sum_{i \in ℕ_{0}} F (w) (i))$
	knoppndvlem6.a	$⊢ A = (\frac{{2 \cdot N}^{- J}}{2}) \cdot M$
	knoppndvlem6.c	$⊢ φ \to C \in (- 1, 1)$
	knoppndvlem6.j	$⊢ φ \to J \in ℕ_{0}$
	knoppndvlem6.m	$⊢ φ \to M \in ℤ$
	knoppndvlem6.n	$⊢ φ \to N \in ℕ$
Assertion	knoppndvlem6	$⊢ φ \to W (A) = \sum_{i = 0}^{J} F (A) (i)$

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem6.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
2		knoppndvlem6.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
3		knoppndvlem6.w	$⊢ W = (w \in ℝ ⟼ \sum_{i \in ℕ_{0}} F (w) (i))$
4		knoppndvlem6.a	$⊢ A = (\frac{{2 \cdot N}^{- J}}{2}) \cdot M$
5		knoppndvlem6.c	$⊢ φ \to C \in (- 1, 1)$
6		knoppndvlem6.j	$⊢ φ \to J \in ℕ_{0}$
7		knoppndvlem6.m	$⊢ φ \to M \in ℤ$
8		knoppndvlem6.n	$⊢ φ \to N \in ℕ$
9		fveq2	$⊢ w = A \to F (w) = F (A)$
10	9	fveq1d	$⊢ w = A \to F (w) (i) = F (A) (i)$
11	10	sumeq2sdv	$⊢ w = A \to \sum_{i \in ℕ_{0}} F (w) (i) = \sum_{i \in ℕ_{0}} F (A) (i)$
12	4	a1i	$⊢ φ \to A = (\frac{{2 \cdot N}^{- J}}{2}) \cdot M$
13	6	nn0zd	$⊢ φ \to J \in ℤ$
14	8 13 7	knoppndvlem1	$⊢ φ \to (\frac{{2 \cdot N}^{- J}}{2}) \cdot M \in ℝ$
15	12 14	eqeltrd	$⊢ φ \to A \in ℝ$
16		sumex	$⊢ \sum_{i \in ℕ_{0}} F (A) (i) \in V$
17	16	a1i	$⊢ φ \to \sum_{i \in ℕ_{0}} F (A) (i) \in V$
18	3 11 15 17	fvmptd3	$⊢ φ \to W (A) = \sum_{i \in ℕ_{0}} F (A) (i)$
19		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
20		eqid	$⊢ ℤ_{\geq (J + 1)} = ℤ_{\geq (J + 1)}$
21		peano2nn0	$⊢ J \in ℕ_{0} \to J + 1 \in ℕ_{0}$
22	6 21	syl	$⊢ φ \to J + 1 \in ℕ_{0}$
23		eqidd	$⊢ (φ \land i \in ℕ_{0}) \to F (A) (i) = F (A) (i)$
24	8	adantr	$⊢ (φ \land i \in ℕ_{0}) \to N \in ℕ$
25	5	knoppndvlem3	$⊢ φ \to (C \in ℝ \land \|C\| < 1)$
26	25	simpld	$⊢ φ \to C \in ℝ$
27	26	adantr	$⊢ (φ \land i \in ℕ_{0}) \to C \in ℝ$
28	15	adantr	$⊢ (φ \land i \in ℕ_{0}) \to A \in ℝ$
29		simpr	$⊢ (φ \land i \in ℕ_{0}) \to i \in ℕ_{0}$
30	1 2 24 27 28 29	knoppcnlem3	$⊢ (φ \land i \in ℕ_{0}) \to F (A) (i) \in ℝ$
31	30	recnd	$⊢ (φ \land i \in ℕ_{0}) \to F (A) (i) \in ℂ$
32	1 2 3 15 5 8	knoppndvlem4	$⊢ φ \to seq 0 (+ F (A)) ⇝ W (A)$
33		seqex	$⊢ seq 0 (+ F (A)) \in V$
34		fvex	$⊢ W (A) \in V$
35	33 34	breldm	$⊢ seq 0 (+ F (A)) ⇝ W (A) \to seq 0 (+ F (A)) \in dom ⇝$
36	32 35	syl	$⊢ φ \to seq 0 (+ F (A)) \in dom ⇝$
37	19 20 22 23 31 36	isumsplit	$⊢ φ \to \sum_{i \in ℕ_{0}} F (A) (i) = \sum_{i = 0}^{J + 1 - 1} F (A) (i) + \sum_{i \in ℤ_{\geq (J + 1)}} F (A) (i)$
38	6	nn0cnd	$⊢ φ \to J \in ℂ$
39		1cnd	$⊢ φ \to 1 \in ℂ$
40	38 39	pncand	$⊢ φ \to J + 1 - 1 = J$
41	40	oveq2d	$⊢ φ \to (0 \dots J + 1 - 1) = (0 \dots J)$
42	41	sumeq1d	$⊢ φ \to \sum_{i = 0}^{J + 1 - 1} F (A) (i) = \sum_{i = 0}^{J} F (A) (i)$
43	42	oveq1d	$⊢ φ \to \sum_{i = 0}^{J + 1 - 1} F (A) (i) + \sum_{i \in ℤ_{\geq (J + 1)}} F (A) (i) = \sum_{i = 0}^{J} F (A) (i) + \sum_{i \in ℤ_{\geq (J + 1)}} F (A) (i)$
44	18 37 43	3eqtrd	$⊢ φ \to W (A) = \sum_{i = 0}^{J} F (A) (i) + \sum_{i \in ℤ_{\geq (J + 1)}} F (A) (i)$
45	15	adantr	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to A \in ℝ$
46		eluznn0	$⊢ (J + 1 \in ℕ_{0} \land i \in ℤ_{\geq (J + 1)}) \to i \in ℕ_{0}$
47	22 46	sylan	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to i \in ℕ_{0}$
48	2 45 47	knoppcnlem1	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to F (A) (i) = C^{i} T ({2 \cdot N}^{i} A)$
49	4	a1i	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to A = (\frac{{2 \cdot N}^{- J}}{2}) \cdot M$
50	49	oveq2d	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to {2 \cdot N}^{i} A = {2 \cdot N}^{i} (\frac{{2 \cdot N}^{- J}}{2}) \cdot M$
51	8	adantr	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to N \in ℕ$
52	47	nn0zd	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to i \in ℤ$
53	13	adantr	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to J \in ℤ$
54	7	adantr	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to M \in ℤ$
55		eluzle	$⊢ i \in ℤ_{\geq (J + 1)} \to J + 1 \leq i$
56	55	adantl	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to J + 1 \leq i$
57	53 52	jca	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to (J \in ℤ \land i \in ℤ)$
58		zltp1le	$⊢ (J \in ℤ \land i \in ℤ) \to (J < i \leftrightarrow J + 1 \leq i)$
59	57 58	syl	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to (J < i \leftrightarrow J + 1 \leq i)$
60	56 59	mpbird	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to J < i$
61	51 52 53 54 60	knoppndvlem2	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to {2 \cdot N}^{i} (\frac{{2 \cdot N}^{- J}}{2}) \cdot M \in ℤ$
62	50 61	eqeltrd	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to {2 \cdot N}^{i} A \in ℤ$
63	1 62	dnizeq0	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to T ({2 \cdot N}^{i} A) = 0$
64	63	oveq2d	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to C^{i} T ({2 \cdot N}^{i} A) = C^{i} \cdot 0$
65	26	recnd	$⊢ φ \to C \in ℂ$
66	65	adantr	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to C \in ℂ$
67	66 47	expcld	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to C^{i} \in ℂ$
68	67	mul01d	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to C^{i} \cdot 0 = 0$
69	48 64 68	3eqtrd	$⊢ (φ \land i \in ℤ_{\geq (J + 1)}) \to F (A) (i) = 0$
70	69	sumeq2dv	$⊢ φ \to \sum_{i \in ℤ_{\geq (J + 1)}} F (A) (i) = \sum_{i \in ℤ_{\geq (J + 1)}} 0$
71		ssidd	$⊢ φ \to ℤ_{\geq (J + 1)} \subseteq ℤ_{\geq (J + 1)}$
72	71	orcd	$⊢ φ \to (ℤ_{\geq (J + 1)} \subseteq ℤ_{\geq (J + 1)} \lor ℤ_{\geq (J + 1)} \in Fin)$
73		sumz	$⊢ (ℤ_{\geq (J + 1)} \subseteq ℤ_{\geq (J + 1)} \lor ℤ_{\geq (J + 1)} \in Fin) \to \sum_{i \in ℤ_{\geq (J + 1)}} 0 = 0$
74	72 73	syl	$⊢ φ \to \sum_{i \in ℤ_{\geq (J + 1)}} 0 = 0$
75	70 74	eqtrd	$⊢ φ \to \sum_{i \in ℤ_{\geq (J + 1)}} F (A) (i) = 0$
76	75	oveq2d	$⊢ φ \to \sum_{i = 0}^{J} F (A) (i) + \sum_{i \in ℤ_{\geq (J + 1)}} F (A) (i) = \sum_{i = 0}^{J} F (A) (i) + 0$
77	1 2 15 26 8	knoppndvlem5	$⊢ φ \to \sum_{i = 0}^{J} F (A) (i) \in ℝ$
78	77	recnd	$⊢ φ \to \sum_{i = 0}^{J} F (A) (i) \in ℂ$
79	78	addid1d	$⊢ φ \to \sum_{i = 0}^{J} F (A) (i) + 0 = \sum_{i = 0}^{J} F (A) (i)$
80	76 79	eqtrd	$⊢ φ \to \sum_{i = 0}^{J} F (A) (i) + \sum_{i \in ℤ_{\geq (J + 1)}} F (A) (i) = \sum_{i = 0}^{J} F (A) (i)$
81	44 80	eqtrd	$⊢ φ \to W (A) = \sum_{i = 0}^{J} F (A) (i)$

Metamath Proof Explorer

Theorem knoppndvlem6

Proof