knoppndvlem11

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

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem11.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
2		knoppndvlem11.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
3		knoppndvlem11.a	$⊢ φ \to A \in ℝ$
4		knoppndvlem11.b	$⊢ φ \to B \in ℝ$
5		knoppndvlem11.c	$⊢ φ \to C \in (- 1, 1)$
6		knoppndvlem11.j	$⊢ φ \to J \in ℕ_{0}$
7		knoppndvlem11.n	$⊢ φ \to N \in ℕ$
8		fzfid	$⊢ φ \to (0 \dots J - 1) \in Fin$
9	7	adantr	$⊢ (φ \land i \in (0 \dots J - 1)) \to N \in ℕ$
10	5	knoppndvlem3	$⊢ φ \to (C \in ℝ \land \|C\| < 1)$
11	10	simpld	$⊢ φ \to C \in ℝ$
12	11	adantr	$⊢ (φ \land i \in (0 \dots J - 1)) \to C \in ℝ$
13	4	adantr	$⊢ (φ \land i \in (0 \dots J - 1)) \to B \in ℝ$
14		elfznn0	$⊢ i \in (0 \dots J - 1) \to i \in ℕ_{0}$
15	14	adantl	$⊢ (φ \land i \in (0 \dots J - 1)) \to i \in ℕ_{0}$
16	1 2 9 12 13 15	knoppcnlem3	$⊢ (φ \land i \in (0 \dots J - 1)) \to F (B) (i) \in ℝ$
17	16	recnd	$⊢ (φ \land i \in (0 \dots J - 1)) \to F (B) (i) \in ℂ$
18	3	adantr	$⊢ (φ \land i \in (0 \dots J - 1)) \to A \in ℝ$
19	1 2 9 12 18 15	knoppcnlem3	$⊢ (φ \land i \in (0 \dots J - 1)) \to F (A) (i) \in ℝ$
20	19	recnd	$⊢ (φ \land i \in (0 \dots J - 1)) \to F (A) (i) \in ℂ$
21	8 17 20	fsumsub	$⊢ φ \to \sum_{i = 0}^{J - 1} (F (B) (i) - F (A) (i)) = \sum_{i = 0}^{J - 1} F (B) (i) - \sum_{i = 0}^{J - 1} F (A) (i)$
22	21	eqcomd	$⊢ φ \to \sum_{i = 0}^{J - 1} F (B) (i) - \sum_{i = 0}^{J - 1} F (A) (i) = \sum_{i = 0}^{J - 1} (F (B) (i) - F (A) (i))$
23	22	fveq2d	$⊢ φ \to \|\sum_{i = 0}^{J - 1} F (B) (i) - \sum_{i = 0}^{J - 1} F (A) (i)\| = \|\sum_{i = 0}^{J - 1} (F (B) (i) - F (A) (i))\|$
24	17 20	subcld	$⊢ (φ \land i \in (0 \dots J - 1)) \to F (B) (i) - F (A) (i) \in ℂ$
25	8 24	fsumcl	$⊢ φ \to \sum_{i = 0}^{J - 1} (F (B) (i) - F (A) (i)) \in ℂ$
26	25	abscld	$⊢ φ \to \|\sum_{i = 0}^{J - 1} (F (B) (i) - F (A) (i))\| \in ℝ$
27	24	abscld	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|F (B) (i) - F (A) (i)\| \in ℝ$
28	8 27	fsumrecl	$⊢ φ \to \sum_{i = 0}^{J - 1} \|F (B) (i) - F (A) (i)\| \in ℝ$
29	4 3	resubcld	$⊢ φ \to B - A \in ℝ$
30	29	recnd	$⊢ φ \to B - A \in ℂ$
31	30	abscld	$⊢ φ \to \|B - A\| \in ℝ$
32		2re	$⊢ 2 \in ℝ$
33	32	a1i	$⊢ φ \to 2 \in ℝ$
34		nnre	$⊢ N \in ℕ \to N \in ℝ$
35	7 34	syl	$⊢ φ \to N \in ℝ$
36	33 35	remulcld	$⊢ φ \to 2 \cdot N \in ℝ$
37	11	recnd	$⊢ φ \to C \in ℂ$
38	37	abscld	$⊢ φ \to \|C\| \in ℝ$
39	36 38	remulcld	$⊢ φ \to 2 \cdot N \|C\| \in ℝ$
40	39	adantr	$⊢ (φ \land i \in (0 \dots J - 1)) \to 2 \cdot N \|C\| \in ℝ$
41	40 15	reexpcld	$⊢ (φ \land i \in (0 \dots J - 1)) \to {2 \cdot N \|C\|}^{i} \in ℝ$
42	8 41	fsumrecl	$⊢ φ \to \sum_{i = 0}^{J - 1} {2 \cdot N \|C\|}^{i} \in ℝ$
43	31 42	remulcld	$⊢ φ \to \|B - A\| \sum_{i = 0}^{J - 1} {2 \cdot N \|C\|}^{i} \in ℝ$
44	8 24	fsumabs	$⊢ φ \to \|\sum_{i = 0}^{J - 1} (F (B) (i) - F (A) (i))\| \leq \sum_{i = 0}^{J - 1} \|F (B) (i) - F (A) (i)\|$
45	31	adantr	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|B - A\| \in ℝ$
46	45 41	remulcld	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|B - A\| {2 \cdot N \|C\|}^{i} \in ℝ$
47	2 13 15	knoppcnlem1	$⊢ (φ \land i \in (0 \dots J - 1)) \to F (B) (i) = C^{i} T ({2 \cdot N}^{i} B)$
48	2 18 15	knoppcnlem1	$⊢ (φ \land i \in (0 \dots J - 1)) \to F (A) (i) = C^{i} T ({2 \cdot N}^{i} A)$
49	47 48	oveq12d	$⊢ (φ \land i \in (0 \dots J - 1)) \to F (B) (i) - F (A) (i) = C^{i} T ({2 \cdot N}^{i} B) - C^{i} T ({2 \cdot N}^{i} A)$
50	12 15	reexpcld	$⊢ (φ \land i \in (0 \dots J - 1)) \to C^{i} \in ℝ$
51	50	recnd	$⊢ (φ \land i \in (0 \dots J - 1)) \to C^{i} \in ℂ$
52	36	adantr	$⊢ (φ \land i \in (0 \dots J - 1)) \to 2 \cdot N \in ℝ$
53	52 15	reexpcld	$⊢ (φ \land i \in (0 \dots J - 1)) \to {2 \cdot N}^{i} \in ℝ$
54	53 13	remulcld	$⊢ (φ \land i \in (0 \dots J - 1)) \to {2 \cdot N}^{i} B \in ℝ$
55	1 54	dnicld2	$⊢ (φ \land i \in (0 \dots J - 1)) \to T ({2 \cdot N}^{i} B) \in ℝ$
56	55	recnd	$⊢ (φ \land i \in (0 \dots J - 1)) \to T ({2 \cdot N}^{i} B) \in ℂ$
57	53 18	remulcld	$⊢ (φ \land i \in (0 \dots J - 1)) \to {2 \cdot N}^{i} A \in ℝ$
58	1 57	dnicld2	$⊢ (φ \land i \in (0 \dots J - 1)) \to T ({2 \cdot N}^{i} A) \in ℝ$
59	58	recnd	$⊢ (φ \land i \in (0 \dots J - 1)) \to T ({2 \cdot N}^{i} A) \in ℂ$
60	51 56 59	subdid	$⊢ (φ \land i \in (0 \dots J - 1)) \to C^{i} (T ({2 \cdot N}^{i} B) - T ({2 \cdot N}^{i} A)) = C^{i} T ({2 \cdot N}^{i} B) - C^{i} T ({2 \cdot N}^{i} A)$
61	60	eqcomd	$⊢ (φ \land i \in (0 \dots J - 1)) \to C^{i} T ({2 \cdot N}^{i} B) - C^{i} T ({2 \cdot N}^{i} A) = C^{i} (T ({2 \cdot N}^{i} B) - T ({2 \cdot N}^{i} A))$
62	49 61	eqtrd	$⊢ (φ \land i \in (0 \dots J - 1)) \to F (B) (i) - F (A) (i) = C^{i} (T ({2 \cdot N}^{i} B) - T ({2 \cdot N}^{i} A))$
63	62	fveq2d	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|F (B) (i) - F (A) (i)\| = \|C^{i} (T ({2 \cdot N}^{i} B) - T ({2 \cdot N}^{i} A))\|$
64	56 59	subcld	$⊢ (φ \land i \in (0 \dots J - 1)) \to T ({2 \cdot N}^{i} B) - T ({2 \cdot N}^{i} A) \in ℂ$
65	51 64	absmuld	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|C^{i} (T ({2 \cdot N}^{i} B) - T ({2 \cdot N}^{i} A))\| = \|C^{i}\| \|T ({2 \cdot N}^{i} B) - T ({2 \cdot N}^{i} A)\|$
66	37	adantr	$⊢ (φ \land i \in (0 \dots J - 1)) \to C \in ℂ$
67	66 15	absexpd	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|C^{i}\| = {\|C\|}^{i}$
68	67	oveq1d	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|C^{i}\| \|T ({2 \cdot N}^{i} B) - T ({2 \cdot N}^{i} A)\| = {\|C\|}^{i} \|T ({2 \cdot N}^{i} B) - T ({2 \cdot N}^{i} A)\|$
69	65 68	eqtrd	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|C^{i} (T ({2 \cdot N}^{i} B) - T ({2 \cdot N}^{i} A))\| = {\|C\|}^{i} \|T ({2 \cdot N}^{i} B) - T ({2 \cdot N}^{i} A)\|$
70	63 69	eqtrd	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|F (B) (i) - F (A) (i)\| = {\|C\|}^{i} \|T ({2 \cdot N}^{i} B) - T ({2 \cdot N}^{i} A)\|$
71	64	abscld	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|T ({2 \cdot N}^{i} B) - T ({2 \cdot N}^{i} A)\| \in ℝ$
72	54 57	resubcld	$⊢ (φ \land i \in (0 \dots J - 1)) \to {2 \cdot N}^{i} B - {2 \cdot N}^{i} A \in ℝ$
73	72	recnd	$⊢ (φ \land i \in (0 \dots J - 1)) \to {2 \cdot N}^{i} B - {2 \cdot N}^{i} A \in ℂ$
74	73	abscld	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|{2 \cdot N}^{i} B - {2 \cdot N}^{i} A\| \in ℝ$
75	38	adantr	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|C\| \in ℝ$
76	75 15	reexpcld	$⊢ (φ \land i \in (0 \dots J - 1)) \to {\|C\|}^{i} \in ℝ$
77	66	absge0d	$⊢ (φ \land i \in (0 \dots J - 1)) \to 0 \leq \|C\|$
78	75 15 77	expge0d	$⊢ (φ \land i \in (0 \dots J - 1)) \to 0 \leq {\|C\|}^{i}$
79	1 57 54	dnibnd	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|T ({2 \cdot N}^{i} B) - T ({2 \cdot N}^{i} A)\| \leq \|{2 \cdot N}^{i} B - {2 \cdot N}^{i} A\|$
80	71 74 76 78 79	lemul2ad	$⊢ (φ \land i \in (0 \dots J - 1)) \to {\|C\|}^{i} \|T ({2 \cdot N}^{i} B) - T ({2 \cdot N}^{i} A)\| \leq {\|C\|}^{i} \|{2 \cdot N}^{i} B - {2 \cdot N}^{i} A\|$
81	53	recnd	$⊢ (φ \land i \in (0 \dots J - 1)) \to {2 \cdot N}^{i} \in ℂ$
82	13	recnd	$⊢ (φ \land i \in (0 \dots J - 1)) \to B \in ℂ$
83	18	recnd	$⊢ (φ \land i \in (0 \dots J - 1)) \to A \in ℂ$
84	81 82 83	subdid	$⊢ (φ \land i \in (0 \dots J - 1)) \to {2 \cdot N}^{i} (B - A) = {2 \cdot N}^{i} B - {2 \cdot N}^{i} A$
85	84	eqcomd	$⊢ (φ \land i \in (0 \dots J - 1)) \to {2 \cdot N}^{i} B - {2 \cdot N}^{i} A = {2 \cdot N}^{i} (B - A)$
86	85	fveq2d	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|{2 \cdot N}^{i} B - {2 \cdot N}^{i} A\| = \|{2 \cdot N}^{i} (B - A)\|$
87	30	adantr	$⊢ (φ \land i \in (0 \dots J - 1)) \to B - A \in ℂ$
88	81 87	absmuld	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|{2 \cdot N}^{i} (B - A)\| = \|{2 \cdot N}^{i}\| \|B - A\|$
89	52	recnd	$⊢ (φ \land i \in (0 \dots J - 1)) \to 2 \cdot N \in ℂ$
90	89 15	absexpd	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|{2 \cdot N}^{i}\| = {\|2 \cdot N\|}^{i}$
91	33	recnd	$⊢ φ \to 2 \in ℂ$
92	35	recnd	$⊢ φ \to N \in ℂ$
93	91 92	absmuld	$⊢ φ \to \|2 \cdot N\| = \|2\| \|N\|$
94		0le2	$⊢ 0 \leq 2$
95	32	absidi	$⊢ 0 \leq 2 \to \|2\| = 2$
96	94 95	ax-mp	$⊢ \|2\| = 2$
97	96	a1i	$⊢ φ \to \|2\| = 2$
98		0red	$⊢ φ \to 0 \in ℝ$
99		1red	$⊢ φ \to 1 \in ℝ$
100		0le1	$⊢ 0 \leq 1$
101	100	a1i	$⊢ φ \to 0 \leq 1$
102		nnge1	$⊢ N \in ℕ \to 1 \leq N$
103	7 102	syl	$⊢ φ \to 1 \leq N$
104	98 99 35 101 103	letrd	$⊢ φ \to 0 \leq N$
105	35 104	absidd	$⊢ φ \to \|N\| = N$
106	97 105	oveq12d	$⊢ φ \to \|2\| \|N\| = 2 \cdot N$
107	93 106	eqtrd	$⊢ φ \to \|2 \cdot N\| = 2 \cdot N$
108	107	oveq1d	$⊢ φ \to {\|2 \cdot N\|}^{i} = {2 \cdot N}^{i}$
109	108	adantr	$⊢ (φ \land i \in (0 \dots J - 1)) \to {\|2 \cdot N\|}^{i} = {2 \cdot N}^{i}$
110	90 109	eqtrd	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|{2 \cdot N}^{i}\| = {2 \cdot N}^{i}$
111	110	oveq1d	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|{2 \cdot N}^{i}\| \|B - A\| = {2 \cdot N}^{i} \|B - A\|$
112	88 111	eqtrd	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|{2 \cdot N}^{i} (B - A)\| = {2 \cdot N}^{i} \|B - A\|$
113	86 112	eqtrd	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|{2 \cdot N}^{i} B - {2 \cdot N}^{i} A\| = {2 \cdot N}^{i} \|B - A\|$
114	113	oveq2d	$⊢ (φ \land i \in (0 \dots J - 1)) \to {\|C\|}^{i} \|{2 \cdot N}^{i} B - {2 \cdot N}^{i} A\| = {\|C\|}^{i} {2 \cdot N}^{i} \|B - A\|$
115	76	recnd	$⊢ (φ \land i \in (0 \dots J - 1)) \to {\|C\|}^{i} \in ℂ$
116	45	recnd	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|B - A\| \in ℂ$
117	115 81 116	mulassd	$⊢ (φ \land i \in (0 \dots J - 1)) \to {\|C\|}^{i} {2 \cdot N}^{i} \|B - A\| = {\|C\|}^{i} {2 \cdot N}^{i} \|B - A\|$
118	117	eqcomd	$⊢ (φ \land i \in (0 \dots J - 1)) \to {\|C\|}^{i} {2 \cdot N}^{i} \|B - A\| = {\|C\|}^{i} {2 \cdot N}^{i} \|B - A\|$
119	115 81	mulcld	$⊢ (φ \land i \in (0 \dots J - 1)) \to {\|C\|}^{i} {2 \cdot N}^{i} \in ℂ$
120	119 116	mulcomd	$⊢ (φ \land i \in (0 \dots J - 1)) \to {\|C\|}^{i} {2 \cdot N}^{i} \|B - A\| = \|B - A\| {\|C\|}^{i} {2 \cdot N}^{i}$
121	115 81	mulcomd	$⊢ (φ \land i \in (0 \dots J - 1)) \to {\|C\|}^{i} {2 \cdot N}^{i} = {2 \cdot N}^{i} {\|C\|}^{i}$
122	75	recnd	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|C\| \in ℂ$
123	89 122 15	mulexpd	$⊢ (φ \land i \in (0 \dots J - 1)) \to {2 \cdot N \|C\|}^{i} = {2 \cdot N}^{i} {\|C\|}^{i}$
124	123	eqcomd	$⊢ (φ \land i \in (0 \dots J - 1)) \to {2 \cdot N}^{i} {\|C\|}^{i} = {2 \cdot N \|C\|}^{i}$
125	121 124	eqtrd	$⊢ (φ \land i \in (0 \dots J - 1)) \to {\|C\|}^{i} {2 \cdot N}^{i} = {2 \cdot N \|C\|}^{i}$
126	125	oveq2d	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|B - A\| {\|C\|}^{i} {2 \cdot N}^{i} = \|B - A\| {2 \cdot N \|C\|}^{i}$
127	118 120 126	3eqtrd	$⊢ (φ \land i \in (0 \dots J - 1)) \to {\|C\|}^{i} {2 \cdot N}^{i} \|B - A\| = \|B - A\| {2 \cdot N \|C\|}^{i}$
128	114 127	eqtrd	$⊢ (φ \land i \in (0 \dots J - 1)) \to {\|C\|}^{i} \|{2 \cdot N}^{i} B - {2 \cdot N}^{i} A\| = \|B - A\| {2 \cdot N \|C\|}^{i}$
129	80 128	breqtrd	$⊢ (φ \land i \in (0 \dots J - 1)) \to {\|C\|}^{i} \|T ({2 \cdot N}^{i} B) - T ({2 \cdot N}^{i} A)\| \leq \|B - A\| {2 \cdot N \|C\|}^{i}$
130	70 129	eqbrtrd	$⊢ (φ \land i \in (0 \dots J - 1)) \to \|F (B) (i) - F (A) (i)\| \leq \|B - A\| {2 \cdot N \|C\|}^{i}$
131	8 27 46 130	fsumle	$⊢ φ \to \sum_{i = 0}^{J - 1} \|F (B) (i) - F (A) (i)\| \leq \sum_{i = 0}^{J - 1} \|B - A\| {2 \cdot N \|C\|}^{i}$
132	31	recnd	$⊢ φ \to \|B - A\| \in ℂ$
133	125 119	eqeltrrd	$⊢ (φ \land i \in (0 \dots J - 1)) \to {2 \cdot N \|C\|}^{i} \in ℂ$
134	8 132 133	fsummulc2	$⊢ φ \to \|B - A\| \sum_{i = 0}^{J - 1} {2 \cdot N \|C\|}^{i} = \sum_{i = 0}^{J - 1} \|B - A\| {2 \cdot N \|C\|}^{i}$
135	134	eqcomd	$⊢ φ \to \sum_{i = 0}^{J - 1} \|B - A\| {2 \cdot N \|C\|}^{i} = \|B - A\| \sum_{i = 0}^{J - 1} {2 \cdot N \|C\|}^{i}$
136	131 135	breqtrd	$⊢ φ \to \sum_{i = 0}^{J - 1} \|F (B) (i) - F (A) (i)\| \leq \|B - A\| \sum_{i = 0}^{J - 1} {2 \cdot N \|C\|}^{i}$
137	26 28 43 44 136	letrd	$⊢ φ \to \|\sum_{i = 0}^{J - 1} (F (B) (i) - F (A) (i))\| \leq \|B - A\| \sum_{i = 0}^{J - 1} {2 \cdot N \|C\|}^{i}$
138	23 137	eqbrtrd	$⊢ φ \to \|\sum_{i = 0}^{J - 1} F (B) (i) - \sum_{i = 0}^{J - 1} F (A) (i)\| \leq \|B - A\| \sum_{i = 0}^{J - 1} {2 \cdot N \|C\|}^{i}$

Metamath Proof Explorer

Theorem knoppndvlem11

Proof