Theorem knoppndvlem15

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

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

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem15.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		knoppndvlem15.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		knoppndvlem15.w	$$⊢W=\left(w\in ℝ⟼\sum _{i\in {\mathbb{N}}_0}F\left(w\right)\left(i\right)\right)$$
4		knoppndvlem15.a	$$⊢A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
5		knoppndvlem15.b	$$⊢B=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)$$
6		knoppndvlem15.c	$$⊢\phi \to C\in \left(-1,1\right)$$
7		knoppndvlem15.j	$$⊢\phi \to J\in {\mathbb{N}}_0$$
8		knoppndvlem15.m	$$⊢\phi \to M\in \mathbb{Z}$$
9		knoppndvlem15.n	$$⊢\phi \to N\in \mathbb{N}$$
10		knoppndvlem15.1	$$⊢\phi \to 1<N\left|C\right|$$
11	6	knoppndvlem3	$$⊢\phi \to \left(C\in ℝ\wedge \left|C\right|<1\right)$$
12	11	simpld	$$⊢\phi \to C\in ℝ$$
13	12	recnd	$$⊢\phi \to C\in ℂ$$
14	13	abscld	$$⊢\phi \to \left|C\right|\in ℝ$$
15	14 7	reexpcld	$$⊢\phi \to {\left|C\right|}^J\in ℝ$$
16		2re	$$⊢2\in ℝ$$
17	16	a1i	$$⊢\phi \to 2\in ℝ$$
18		2ne0	$$⊢2\ne 0$$
19	18	a1i	$$⊢\phi \to 2\ne 0$$
20	15 17 19	redivcld	$$⊢\phi \to \frac{{\left|C\right|}^J}{2}\in ℝ$$
21		1red	$$⊢\phi \to 1\in ℝ$$
22	9	nnred	$$⊢\phi \to N\in ℝ$$
23	17 22	remulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
24	23 14	remulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|\in ℝ$$
25	24 21	resubcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1\in ℝ$$
26		0red	$$⊢\phi \to 0\in ℝ$$
27		0lt1	$$⊢0<1$$
28	27	a1i	$$⊢\phi \to 0<1$$
29	6 9 10	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)$$
30	29	simprd	$$⊢\phi \to 1<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1$$
31	26 21 25 28 30	lttrd	$$⊢\phi \to 0<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1$$
32	25 31	jca	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1\in ℝ\wedge 0<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1\right)$$
33		gt0ne0	$$⊢\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1\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$$
34	32 33	syl	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1\ne 0$$
35	21 25 34	redivcld	$$⊢\phi \to \frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\in ℝ$$
36	21 35	resubcld	$$⊢\phi \to 1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\in ℝ$$
37	20 36	remulcld	$$⊢\phi \to \left(\frac{{\left|C\right|}^J}{2}\right)\left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)\in ℝ$$
38	4	a1i	$$⊢\phi \to A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
39	7	nn0zd	$$⊢\phi \to J\in \mathbb{Z}$$
40	9 39 8	knoppndvlem1	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℝ$$
41	38 40	eqeltrd	$$⊢\phi \to A\in ℝ$$
42	1 2 9 12 41 7	knoppcnlem3	$$⊢\phi \to F\left(A\right)\left(J\right)\in ℝ$$
43	42	recnd	$$⊢\phi \to F\left(A\right)\left(J\right)\in ℂ$$
44	5	a1i	$$⊢\phi \to B=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)$$
45	8	peano2zd	$$⊢\phi \to M+1\in \mathbb{Z}$$
46	9 39 45	knoppndvlem1	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)\in ℝ$$
47	44 46	eqeltrd	$$⊢\phi \to B\in ℝ$$
48	1 2 9 12 47 7	knoppcnlem3	$$⊢\phi \to F\left(B\right)\left(J\right)\in ℝ$$
49	48	recnd	$$⊢\phi \to F\left(B\right)\left(J\right)\in ℂ$$
50	43 49	subcld	$$⊢\phi \to F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\in ℂ$$
51	50	abscld	$$⊢\phi \to \left|F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\right|\in ℝ$$
52	1 2 47 12 9	knoppndvlem5	$$⊢\phi \to \sum _{i=0}^{J-1}F\left(B\right)\left(i\right)\in ℝ$$
53	52	recnd	$$⊢\phi \to \sum _{i=0}^{J-1}F\left(B\right)\left(i\right)\in ℂ$$
54	1 2 41 12 9	knoppndvlem5	$$⊢\phi \to \sum _{i=0}^{J-1}F\left(A\right)\left(i\right)\in ℝ$$
55	54	recnd	$$⊢\phi \to \sum _{i=0}^{J-1}F\left(A\right)\left(i\right)\in ℂ$$
56	53 55	subcld	$$⊢\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 ℂ$$
57	56	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 ℝ$$
58	51 57	resubcld	$$⊢\phi \to \left|F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\right|-\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 ℝ$$
59	50 56	subcld	$$⊢\phi \to F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)-\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 ℂ$$
60	59	abscld	$$⊢\phi \to \left|F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)-\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)\right|\in ℝ$$
61	20 35	jca	$$⊢\phi \to \left(\frac{{\left|C\right|}^J}{2}\in ℝ\wedge \frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\in ℝ\right)$$
62		remulcl	$$⊢\left(\frac{{\left|C\right|}^J}{2}\in ℝ\wedge \frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\in ℝ\right)\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 ℝ$$
63	61 62	syl	$$⊢\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 ℝ$$
64	20 63	jca	$$⊢\phi \to \left(\frac{{\left|C\right|}^J}{2}\in ℝ\wedge \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 ℝ\right)$$
65		resubcl	$$⊢\left(\frac{{\left|C\right|}^J}{2}\in ℝ\wedge \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 ℝ\right)\to \left(\frac{{\left|C\right|}^J}{2}\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)\in ℝ$$
66	64 65	syl	$$⊢\phi \to \left(\frac{{\left|C\right|}^J}{2}\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)\in ℝ$$
67	20	recnd	$$⊢\phi \to \frac{{\left|C\right|}^J}{2}\in ℂ$$
68		1cnd	$$⊢\phi \to 1\in ℂ$$
69	35	recnd	$$⊢\phi \to \frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\in ℂ$$
70	67 68 69	subdid	$$⊢\phi \to \left(\frac{{\left|C\right|}^J}{2}\right)\left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)=\left(\frac{{\left|C\right|}^J}{2}\right)\cdot 1-\left(\frac{{\left|C\right|}^J}{2}\right)\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)$$
71	67	mulridd	$$⊢\phi \to \left(\frac{{\left|C\right|}^J}{2}\right)\cdot 1=\frac{{\left|C\right|}^J}{2}$$
72	71	oveq1d	$$⊢\phi \to \left(\frac{{\left|C\right|}^J}{2}\right)\cdot 1-\left(\frac{{\left|C\right|}^J}{2}\right)\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{{\left|C\right|}^J}{2}\right)\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)$$
73	66	leidd	$$⊢\phi \to \left(\frac{{\left|C\right|}^J}{2}\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)\le \left(\frac{{\left|C\right|}^J}{2}\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)$$
74	72 73	eqbrtrd	$$⊢\phi \to \left(\frac{{\left|C\right|}^J}{2}\right)\cdot 1-\left(\frac{{\left|C\right|}^J}{2}\right)\left(\frac{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{{\left|C\right|}^J}{2}\right)\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)$$
75	70 74	eqbrtrd	$$⊢\phi \to \left(\frac{{\left|C\right|}^J}{2}\right)\left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)\le \left(\frac{{\left|C\right|}^J}{2}\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)$$
76	20 35	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 ℝ$$
77	20	leidd	$$⊢\phi \to \frac{{\left|C\right|}^J}{2}\le \frac{{\left|C\right|}^J}{2}$$
78	43 49	abssubd	$$⊢\phi \to \left|F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\right|=\left|F\left(B\right)\left(J\right)-F\left(A\right)\left(J\right)\right|$$
79	1 2 4 5 6 7 8 9	knoppndvlem10	$$⊢\phi \to \left|F\left(B\right)\left(J\right)-F\left(A\right)\left(J\right)\right|=\frac{{\left|C\right|}^J}{2}$$
80	78 79	eqtrd	$$⊢\phi \to \left|F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\right|=\frac{{\left|C\right|}^J}{2}$$
81	80	eqcomd	$$⊢\phi \to \frac{{\left|C\right|}^J}{2}=\left|F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\right|$$
82	77 81	breqtrd	$$⊢\phi \to \frac{{\left|C\right|}^J}{2}\le \left|F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\right|$$
83	1 2 4 5 6 7 8 9 10	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)$$
84	20 57 51 76 82 83	le2subd	$$⊢\phi \to \left(\frac{{\left|C\right|}^J}{2}\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)\le \left|F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\right|-\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|$$
85	37 66 58 75 84	letrd	$$⊢\phi \to \left(\frac{{\left|C\right|}^J}{2}\right)\left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)\le \left|F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\right|-\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|$$
86	50 56	abs2difd	$$⊢\phi \to \left|F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\right|-\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|F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)-\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)\right|$$
87	37 58 60 85 86	letrd	$$⊢\phi \to \left(\frac{{\left|C\right|}^J}{2}\right)\left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)\le \left|F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)-\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)\right|$$
88	50 56	abssubd	$$⊢\phi \to \left|F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)-\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)\right|=\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)-\left(F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\right)\right|$$
89	87 88	breqtrd	$$⊢\phi \to \left(\frac{{\left|C\right|}^J}{2}\right)\left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)\le \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)-\left(F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\right)\right|$$
90	1 2 3 5 6 7 45 9	knoppndvlem6	$$⊢\phi \to W\left(B\right)=\sum _{i=0}^{J}F\left(B\right)\left(i\right)$$
91		elnn0uz	$$⊢J\in {\mathbb{N}}_0\leftrightarrow J\in {\mathbb{Z}}_{\ge 0}$$
92	7 91	sylib	$$⊢\phi \to J\in {\mathbb{Z}}_{\ge 0}$$
93	9	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots J\right)\right)\to N\in \mathbb{N}$$
94	12	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots J\right)\right)\to C\in ℝ$$
95	47	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots J\right)\right)\to B\in ℝ$$
96		elfznn0	$$⊢i\in \left(0\dots J\right)\to i\in {\mathbb{N}}_0$$
97	96	adantl	$$⊢\left(\phi \wedge i\in \left(0\dots J\right)\right)\to i\in {\mathbb{N}}_0$$
98	1 2 93 94 95 97	knoppcnlem3	$$⊢\left(\phi \wedge i\in \left(0\dots J\right)\right)\to F\left(B\right)\left(i\right)\in ℝ$$
99	98	recnd	$$⊢\left(\phi \wedge i\in \left(0\dots J\right)\right)\to F\left(B\right)\left(i\right)\in ℂ$$
100		fveq2	$$⊢i=J\to F\left(B\right)\left(i\right)=F\left(B\right)\left(J\right)$$
101	92 99 100	fsumm1	$$⊢\phi \to \sum _{i=0}^{J}F\left(B\right)\left(i\right)=\sum _{i=0}^{J-1}F\left(B\right)\left(i\right)+F\left(B\right)\left(J\right)$$
102	90 101	eqtrd	$$⊢\phi \to W\left(B\right)=\sum _{i=0}^{J-1}F\left(B\right)\left(i\right)+F\left(B\right)\left(J\right)$$
103	1 2 3 4 6 7 8 9	knoppndvlem6	$$⊢\phi \to W\left(A\right)=\sum _{i=0}^{J}F\left(A\right)\left(i\right)$$
104	41	adantr	$$⊢\left(\phi \wedge i\in \left(0\dots J\right)\right)\to A\in ℝ$$
105	1 2 93 94 104 97	knoppcnlem3	$$⊢\left(\phi \wedge i\in \left(0\dots J\right)\right)\to F\left(A\right)\left(i\right)\in ℝ$$
106	105	recnd	$$⊢\left(\phi \wedge i\in \left(0\dots J\right)\right)\to F\left(A\right)\left(i\right)\in ℂ$$
107		fveq2	$$⊢i=J\to F\left(A\right)\left(i\right)=F\left(A\right)\left(J\right)$$
108	92 106 107	fsumm1	$$⊢\phi \to \sum _{i=0}^{J}F\left(A\right)\left(i\right)=\sum _{i=0}^{J-1}F\left(A\right)\left(i\right)+F\left(A\right)\left(J\right)$$
109	103 108	eqtrd	$$⊢\phi \to W\left(A\right)=\sum _{i=0}^{J-1}F\left(A\right)\left(i\right)+F\left(A\right)\left(J\right)$$
110	102 109	oveq12d	$$⊢\phi \to W\left(B\right)-W\left(A\right)=\sum _{i=0}^{J-1}F\left(B\right)\left(i\right)+F\left(B\right)\left(J\right)-\left(\sum _{i=0}^{J-1}F\left(A\right)\left(i\right)+F\left(A\right)\left(J\right)\right)$$
111	53 55 43 49	subadd4d	$$⊢\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)-\left(F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\right)=\sum _{i=0}^{J-1}F\left(B\right)\left(i\right)+F\left(B\right)\left(J\right)-\left(\sum _{i=0}^{J-1}F\left(A\right)\left(i\right)+F\left(A\right)\left(J\right)\right)$$
112	111	eqcomd	$$⊢\phi \to \sum _{i=0}^{J-1}F\left(B\right)\left(i\right)+F\left(B\right)\left(J\right)-\left(\sum _{i=0}^{J-1}F\left(A\right)\left(i\right)+F\left(A\right)\left(J\right)\right)=\sum _{i=0}^{J-1}F\left(B\right)\left(i\right)-\sum _{i=0}^{J-1}F\left(A\right)\left(i\right)-\left(F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\right)$$
113	110 112	eqtrd	$$⊢\phi \to W\left(B\right)-W\left(A\right)=\sum _{i=0}^{J-1}F\left(B\right)\left(i\right)-\sum _{i=0}^{J-1}F\left(A\right)\left(i\right)-\left(F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\right)$$
114	113	fveq2d	$$⊢\phi \to \left|W\left(B\right)-W\left(A\right)\right|=\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)-\left(F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\right)\right|$$
115	114	eqcomd	$$⊢\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)-\left(F\left(A\right)\left(J\right)-F\left(B\right)\left(J\right)\right)\right|=\left|W\left(B\right)-W\left(A\right)\right|$$
116	89 115	breqtrd	$$⊢\phi \to \left(\frac{{\left|C\right|}^J}{2}\right)\left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)\le \left|W\left(B\right)-W\left(A\right)\right|$$