Theorem knoppndvlem14

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 1-Jul-2021) (Revised by Asger C. Ipsen, 7-Jul-2021)

	Ref	Expression
Hypotheses	knoppndvlem14.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
	knoppndvlem14.f	$$⊢F=\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}y\right)\right)\right)$$
	knoppndvlem14.a	$$⊢A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
	knoppndvlem14.b	$$⊢B=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)$$
	knoppndvlem14.c	$$⊢\phi \to C\in \left(-1,1\right)$$
	knoppndvlem14.j	$$⊢\phi \to J\in {\mathbb{N}}_0$$
	knoppndvlem14.m	$$⊢\phi \to M\in \mathbb{Z}$$
	knoppndvlem14.n	$$⊢\phi \to N\in \mathbb{N}$$
	knoppndvlem14.1	$$⊢\phi \to 1<N\left|C\right|$$
Assertion	knoppndvlem14	$$⊢\phi \to \left|\sum _{i=0}^{J-1}F\left(B\right)\left(i\right)-\sum _{i=0}^{J-1}F\left(A\right)\left(i\right)\right|\le \left(\frac{{\left|C\right|}^J}{2}\right)\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem14.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		knoppndvlem14.f	$$⊢F=\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}y\right)\right)\right)$$
3		knoppndvlem14.a	$$⊢A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
4		knoppndvlem14.b	$$⊢B=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)$$
5		knoppndvlem14.c	$$⊢\phi \to C\in \left(-1,1\right)$$
6		knoppndvlem14.j	$$⊢\phi \to J\in {\mathbb{N}}_0$$
7		knoppndvlem14.m	$$⊢\phi \to M\in \mathbb{Z}$$
8		knoppndvlem14.n	$$⊢\phi \to N\in \mathbb{N}$$
9		knoppndvlem14.1	$$⊢\phi \to 1<N\left|C\right|$$
10	4	a1i	$$⊢\phi \to B=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)$$
11	6	nn0zd	$$⊢\phi \to J\in \mathbb{Z}$$
12	7	peano2zd	$$⊢\phi \to M+1\in \mathbb{Z}$$
13	8 11 12	knoppndvlem1	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)\in ℝ$$
14	10 13	eqeltrd	$$⊢\phi \to B\in ℝ$$
15	5	knoppndvlem3	$$⊢\phi \to \left(C\in ℝ\wedge \left|C\right|<1\right)$$
16	15	simpld	$$⊢\phi \to C\in ℝ$$
17	1 2 14 16 8	knoppndvlem5	$$⊢\phi \to \sum _{i=0}^{J-1}F\left(B\right)\left(i\right)\in ℝ$$
18	3	a1i	$$⊢\phi \to A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
19	8 11 7	knoppndvlem1	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℝ$$
20	18 19	eqeltrd	$$⊢\phi \to A\in ℝ$$
21	1 2 20 16 8	knoppndvlem5	$$⊢\phi \to \sum _{i=0}^{J-1}F\left(A\right)\left(i\right)\in ℝ$$
22	17 21	resubcld	$$⊢\phi \to \sum _{i=0}^{J-1}F\left(B\right)\left(i\right)-\sum _{i=0}^{J-1}F\left(A\right)\left(i\right)\in ℝ$$
23	22	recnd	$$⊢\phi \to \sum _{i=0}^{J-1}F\left(B\right)\left(i\right)-\sum _{i=0}^{J-1}F\left(A\right)\left(i\right)\in ℂ$$
24	23	abscld	$$⊢\phi \to \left|\sum _{i=0}^{J-1}F\left(B\right)\left(i\right)-\sum _{i=0}^{J-1}F\left(A\right)\left(i\right)\right|\in ℝ$$
25	14 20	resubcld	$$⊢\phi \to B-A\in ℝ$$
26	25	recnd	$$⊢\phi \to B-A\in ℂ$$
27	26	abscld	$$⊢\phi \to \left|B-A\right|\in ℝ$$
28		fzfid	$$⊢\phi \to \left(0\dots J-1\right)\in \mathrm{Fin}$$
29		2re	$$⊢2\in ℝ$$
30	29	a1i	$$⊢\phi \to 2\in ℝ$$
31		nnre	$$⊢N\in \mathbb{N}\to N\in ℝ$$
32	8 31	syl	$$⊢\phi \to N\in ℝ$$
33	30 32	remulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
34	16	recnd	$$⊢\phi \to C\in ℂ$$
35	34	abscld	$$⊢\phi \to \left|C\right|\in ℝ$$
36	33 35	remulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|\in ℝ$$
37	36	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots J-1\right)\right)\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|\in ℝ$$
38		elfznn0	$$⊢i\in \left(0\dots J-1\right)\to i\in {\mathbb{N}}_0$$
39	38	adantl	$$⊢\left(\phi \wedge i\in \left(0\dots J-1\right)\right)\to i\in {\mathbb{N}}_0$$
40	37 39	reexpcld	$$⊢\left(\phi \wedge i\in \left(0\dots J-1\right)\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^i\in ℝ$$
41	28 40	fsumrecl	$$⊢\phi \to \sum _{i=0}^{J-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^i\in ℝ$$
42	27 41	remulcld	$$⊢\phi \to \left|B-A\right|\sum _{i=0}^{J-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^i\in ℝ$$
43	35 6	reexpcld	$$⊢\phi \to {\left|C\right|}^J\in ℝ$$
44		2ne0	$$⊢2\ne 0$$
45	44	a1i	$$⊢\phi \to 2\ne 0$$
46	43 30 45	redivcld	$$⊢\phi \to \frac{{\left|C\right|}^J}{2}\in ℝ$$
47		1red	$$⊢\phi \to 1\in ℝ$$
48	36 47	resubcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1\in ℝ$$
49		0red	$$⊢\phi \to 0\in ℝ$$
50		0lt1	$$⊢0<1$$
51	50	a1i	$$⊢\phi \to 0<1$$
52	5 8 9	knoppndvlem12	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|\ne 1\wedge 1<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1\right)$$
53	52	simprd	$$⊢\phi \to 1<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1$$
54	49 47 48 51 53	lttrd	$$⊢\phi \to 0<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1$$
55	49 54	jca	$$⊢\phi \to \left(0\in ℝ\wedge 0<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1\right)$$
56		ltne	$$⊢\left(0\in ℝ\wedge 0<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1\right)\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1\ne 0$$
57	55 56	syl	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1\ne 0$$
58	47 48 57	redivcld	$$⊢\phi \to \frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\in ℝ$$
59	46 58	remulcld	$$⊢\phi \to \left(\frac{{\left|C\right|}^J}{2}\right)\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\in ℝ$$
60	1 2 20 14 5 6 8	knoppndvlem11	$$⊢\phi \to \left|\sum _{i=0}^{J-1}F\left(B\right)\left(i\right)-\sum _{i=0}^{J-1}F\left(A\right)\left(i\right)\right|\le \left|B-A\right|\sum _{i=0}^{J-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^i$$
61	10 18	oveq12d	$$⊢\phi \to B-A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)-\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
62	30	recnd	$$⊢\phi \to 2\in ℂ$$
63	32	recnd	$$⊢\phi \to N\in ℂ$$
64		nnge1	$$⊢N\in \mathbb{N}\to 1\le N$$
65	8 64	syl	$$⊢\phi \to 1\le N$$
66	49 47 32 51 65	ltletrd	$$⊢\phi \to 0<N$$
67	49 66	jca	$$⊢\phi \to \left(0\in ℝ\wedge 0<N\right)$$
68		ltne	$$⊢\left(0\in ℝ\wedge 0<N\right)\to N\ne 0$$
69	67 68	syl	$$⊢\phi \to N\ne 0$$
70	62 63 45 69	mulne0d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0$$
71	11	znegcld	$$⊢\phi \to -J\in \mathbb{Z}$$
72	33 70 71	reexpclzd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}\in ℝ$$
73	72 30 45	redivcld	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\in ℝ$$
74	73	recnd	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\in ℂ$$
75	12	zcnd	$$⊢\phi \to M+1\in ℂ$$
76	7	zcnd	$$⊢\phi \to M\in ℂ$$
77	74 75 76	subdid	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1-M\right)=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)-\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
78	77	eqcomd	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)-\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1-M\right)$$
79		1cnd	$$⊢\phi \to 1\in ℂ$$
80	76 79	pncan2d	$$⊢\phi \to M+1-M=1$$
81	80	oveq2d	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1-M\right)=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot 1$$
82	74	mulridd	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot 1=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}$$
83	78 81 82	3eqtrd	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)-\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}$$
84	61 83	eqtrd	$$⊢\phi \to B-A=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}$$
85	84	fveq2d	$$⊢\phi \to \left|B-A\right|=\left|\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right|$$
86	72	recnd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}\in ℂ$$
87	86 62 45	absdivd	$$⊢\phi \to \left|\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right|=\frac{\left|{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}\right|}{\left|2\right|}$$
88	62 63	mulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
89	88 70 71	3jca	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0\wedge -J\in \mathbb{Z}\right)$$
90		absexpz	$$⊢\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0\wedge -J\in \mathbb{Z}\right)\to \left|{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}\right|={\left|2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right|}^{-J}$$
91	89 90	syl	$$⊢\phi \to \left|{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}\right|={\left|2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right|}^{-J}$$
92	62 63	absmuld	$$⊢\phi \to \left|2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right|=\left|2\right|\left|N\right|$$
93		0le2	$$⊢0\le 2$$
94	29 93	pm3.2i	$$⊢\left(2\in ℝ\wedge 0\le 2\right)$$
95		absid	$$⊢\left(2\in ℝ\wedge 0\le 2\right)\to \left|2\right|=2$$
96	94 95	ax-mp	$$⊢\left|2\right|=2$$
97	96	a1i	$$⊢\phi \to \left|2\right|=2$$
98	49 32 66	ltled	$$⊢\phi \to 0\le N$$
99	32 98	absidd	$$⊢\phi \to \left|N\right|=N$$
100	97 99	oveq12d	$$⊢\phi \to \left|2\right|\left|N\right|=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
101	92 100	eqtrd	$$⊢\phi \to \left|2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right|=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
102	101	oveq1d	$$⊢\phi \to {\left|2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right|}^{-J}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}$$
103	91 102	eqtrd	$$⊢\phi \to \left|{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}\right|={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}$$
104	103 97	oveq12d	$$⊢\phi \to \frac{\left|{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}\right|}{\left|2\right|}=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}$$
105	87 104	eqtrd	$$⊢\phi \to \left|\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right|=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}$$
106	85 105	eqtrd	$$⊢\phi \to \left|B-A\right|=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}$$
107	36	recnd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|\in ℂ$$
108	52	simpld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|\ne 1$$
109	107 108 6	geoser	$$⊢\phi \to \sum _{i=0}^{J-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^i=\frac{1-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J}{1-2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}$$
110	107 6	expcld	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J\in ℂ$$
111	108	necomd	$$⊢\phi \to 1\ne 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|$$
112	79 110 79 107 111	div2subd	$$⊢\phi \to \frac{1-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J}{1-2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}$$
113	109 112	eqtrd	$$⊢\phi \to \sum _{i=0}^{J-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^i=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}$$
114	106 113	oveq12d	$$⊢\phi \to \left|B-A\right|\sum _{i=0}^{J-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^i=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)$$
115	113 41	eqeltrrd	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\in ℝ$$
116	36 6	reexpcld	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J\in ℝ$$
117	116 48 57	redivcld	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\in ℝ$$
118		2rp	$$⊢2\in {ℝ}^{+}$$
119	118	a1i	$$⊢\phi \to 2\in {ℝ}^{+}$$
120	119	rpgt0d	$$⊢\phi \to 0<2$$
121	30 32 120 66	mulgt0d	$$⊢\phi \to 0<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
122	33 71 121	3jca	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ\wedge -J\in \mathbb{Z}\wedge 0<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
123		expgt0	$$⊢\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ\wedge -J\in \mathbb{Z}\wedge 0<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\to 0<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}$$
124	122 123	syl	$$⊢\phi \to 0<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}$$
125	49 72 124	ltled	$$⊢\phi \to 0\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}$$
126	72 119 125	divge0d	$$⊢\phi \to 0\le \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}$$
127	116 47	resubcld	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J-1\in ℝ$$
128	48 54	elrpd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1\in {ℝ}^{+}$$
129	116	lem1d	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J-1\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J$$
130	127 116 128 129	lediv1dd	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\le \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}$$
131	115 117 73 126 130	lemul2ad	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\le \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)$$
132	48	recnd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1\in ℂ$$
133	110 132 57	divrecd	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)$$
134	133	oveq2d	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right){2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)$$
135	58	recnd	$$⊢\phi \to \frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\in ℂ$$
136	74 110 135	mulassd	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right){2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right){2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)$$
137	136	eqcomd	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right){2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right){2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)$$
138	86 110 62 45	div23d	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J}{2}=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right){2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J$$
139	138	eqcomd	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right){2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J}{2}$$
140	88 70	jca	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0\right)$$
141	35	recnd	$$⊢\phi \to \left|C\right|\in ℂ$$
142	5 8 9	knoppndvlem13	$$⊢\phi \to C\ne 0$$
143	34 142	absne0d	$$⊢\phi \to \left|C\right|\ne 0$$
144	141 143	jca	$$⊢\phi \to \left(\left|C\right|\in ℂ\wedge \left|C\right|\ne 0\right)$$
145	140 144 11	3jca	$$⊢\phi \to \left(\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0\right)\wedge \left(\left|C\right|\in ℂ\wedge \left|C\right|\ne 0\right)\wedge J\in \mathbb{Z}\right)$$
146		mulexpz	$$⊢\left(\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0\right)\wedge \left(\left|C\right|\in ℂ\wedge \left|C\right|\ne 0\right)\wedge J\in \mathbb{Z}\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J{\left|C\right|}^J$$
147	145 146	syl	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J{\left|C\right|}^J$$
148	147	oveq2d	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J{\left|C\right|}^J$$
149	88 6	expcld	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\in ℂ$$
150	43	recnd	$$⊢\phi \to {\left|C\right|}^J\in ℂ$$
151	86 149 150	mulassd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J{\left|C\right|}^J={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J{\left|C\right|}^J$$
152	151	eqcomd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J{\left|C\right|}^J={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J{\left|C\right|}^J$$
153	140 71 11	jca32	$$⊢\phi \to \left(\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0\right)\wedge \left(-J\in \mathbb{Z}\wedge J\in \mathbb{Z}\right)\right)$$
154		expaddz	$$⊢\left(\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0\right)\wedge \left(-J\in \mathbb{Z}\wedge J\in \mathbb{Z}\right)\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J+J}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J$$
155	153 154	syl	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J+J}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J$$
156	155	eqcomd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J+J}$$
157	71	zcnd	$$⊢\phi \to -J\in ℂ$$
158	6	nn0cnd	$$⊢\phi \to J\in ℂ$$
159	157 158	addcomd	$$⊢\phi \to -J+J=J+\mathrm{-<mi\; mathcolor="\#808">J</mi>}$$
160	158	negidd	$$⊢\phi \to J+\mathrm{-<mi\; mathcolor="\#808">J</mi>}=0$$
161	159 160	eqtrd	$$⊢\phi \to -J+J=0$$
162	161	oveq2d	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J+J}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^0$$
163	88	exp0d	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^0=1$$
164	156 162 163	3eqtrd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J=1$$
165	164	oveq1d	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J{\left|C\right|}^J=1{\left|C\right|}^J$$
166	150	mullidd	$$⊢\phi \to 1{\left|C\right|}^J={\left|C\right|}^J$$
167	165 166	eqtrd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J{\left|C\right|}^J={\left|C\right|}^J$$
168	148 152 167	3eqtrd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J={\left|C\right|}^J$$
169	168	oveq1d	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J}{2}=\frac{{\left|C\right|}^J}{2}$$
170	139 169	eqtrd	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right){2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J=\frac{{\left|C\right|}^J}{2}$$
171	170	oveq1d	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right){2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)=\left(\frac{{\left|C\right|}^J}{2}\right)\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)$$
172	134 137 171	3eqtrd	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)=\left(\frac{{\left|C\right|}^J}{2}\right)\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)$$
173	131 172	breqtrd	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\le \left(\frac{{\left|C\right|}^J}{2}\right)\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)$$
174	114 173	eqbrtrd	$$⊢\phi \to \left|B-A\right|\sum _{i=0}^{J-1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^i\le \left(\frac{{\left|C\right|}^J}{2}\right)\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)$$
175	24 42 59 60 174	letrd	$$⊢\phi \to \left|\sum _{i=0}^{J-1}F\left(B\right)\left(i\right)-\sum _{i=0}^{J-1}F\left(A\right)\left(i\right)\right|\le \left(\frac{{\left|C\right|}^J}{2}\right)\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)$$