Theorem knoppndvlem17

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

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

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem17.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		knoppndvlem17.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		knoppndvlem17.w	$$⊢W=\left(w\in ℝ⟼\sum _{i\in {\mathbb{N}}_0}F\left(w\right)\left(i\right)\right)$$
4		knoppndvlem17.a	$$⊢A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
5		knoppndvlem17.b	$$⊢B=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)$$
6		knoppndvlem17.c	$$⊢\phi \to C\in \left(-1,1\right)$$
7		knoppndvlem17.j	$$⊢\phi \to J\in {\mathbb{N}}_0$$
8		knoppndvlem17.m	$$⊢\phi \to M\in \mathbb{Z}$$
9		knoppndvlem17.n	$$⊢\phi \to N\in \mathbb{N}$$
10		knoppndvlem17.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	20	recnd	$$⊢\phi \to \frac{{\left|C\right|}^J}{2}\in ℂ$$
22		1red	$$⊢\phi \to 1\in ℝ$$
23	9	nnred	$$⊢\phi \to N\in ℝ$$
24	17 23	remulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
25	24 14	remulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|\in ℝ$$
26	25 22	resubcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1\in ℝ$$
27		0red	$$⊢\phi \to 0\in ℝ$$
28		0lt1	$$⊢0<1$$
29	28	a1i	$$⊢\phi \to 0<1$$
30	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)$$
31	30	simprd	$$⊢\phi \to 1<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1$$
32	27 22 26 29 31	lttrd	$$⊢\phi \to 0<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1$$
33	26 32	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)$$
34		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$$
35	33 34	syl	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1\ne 0$$
36	22 26 35	redivcld	$$⊢\phi \to \frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\in ℝ$$
37	22 36	resubcld	$$⊢\phi \to 1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\in ℝ$$
38	37	recnd	$$⊢\phi \to 1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\in ℂ$$
39	21 38	mulcomd	$$⊢\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(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)$$
40	39	oveq1d	$$⊢\phi \to \frac{\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)}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}=\frac{\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)}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}$$
41		2rp	$$⊢2\in {ℝ}^{+}$$
42	41	a1i	$$⊢\phi \to 2\in {ℝ}^{+}$$
43	9	nnrpd	$$⊢\phi \to N\in {ℝ}^{+}$$
44	42 43	rpmulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {ℝ}^{+}$$
45	7	nn0zd	$$⊢\phi \to J\in \mathbb{Z}$$
46	45	znegcld	$$⊢\phi \to -J\in \mathbb{Z}$$
47	44 46	rpexpcld	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}\in {ℝ}^{+}$$
48	47	rphalfcld	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\in {ℝ}^{+}$$
49	48	rpcnd	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\in ℂ$$
50	48	rpne0d	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\ne 0$$
51	38 21 49 50	divassd	$$⊢\phi \to \frac{\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)}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}=\left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)\left(\frac{\frac{{\left|C\right|}^J}{2}}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}\right)$$
52	21 49 50	divcld	$$⊢\phi \to \frac{\frac{{\left|C\right|}^J}{2}}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}\in ℂ$$
53	38 52	mulcomd	$$⊢\phi \to \left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)\left(\frac{\frac{{\left|C\right|}^J}{2}}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}\right)=\left(\frac{\frac{{\left|C\right|}^J}{2}}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}\right)\left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)$$
54	15	recnd	$$⊢\phi \to {\left|C\right|}^J\in ℂ$$
55	47	rpcnd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}\in ℂ$$
56	17	recnd	$$⊢\phi \to 2\in ℂ$$
57	47	rpne0d	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}\ne 0$$
58	54 55 56 57 19	divcan7d	$$⊢\phi \to \frac{\frac{{\left|C\right|}^J}{2}}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}=\frac{{\left|C\right|}^J}{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}$$
59	24	recnd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
60	44	rpne0d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0$$
61	59 60 45	expnegd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}=\frac{1}{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J}$$
62	61	oveq2d	$$⊢\phi \to \frac{{\left|C\right|}^J}{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}=\frac{{\left|C\right|}^J}{\frac{1}{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J}}$$
63		1cnd	$$⊢\phi \to 1\in ℂ$$
64	59 7	expcld	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\in ℂ$$
65	27 29	gtned	$$⊢\phi \to 1\ne 0$$
66	59 60 45	expne0d	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\ne 0$$
67	54 63 64 65 66	divdiv2d	$$⊢\phi \to \frac{{\left|C\right|}^J}{\frac{1}{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J}}=\frac{{\left|C\right|}^J{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J}{1}$$
68	54 64	mulcld	$$⊢\phi \to {\left|C\right|}^J{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\in ℂ$$
69	68	div1d	$$⊢\phi \to \frac{{\left|C\right|}^J{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J}{1}={\left|C\right|}^J{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J$$
70	54 64	mulcomd	$$⊢\phi \to {\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$$
71	59 60	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)$$
72	14	recnd	$$⊢\phi \to \left|C\right|\in ℂ$$
73	6 9 10	knoppndvlem13	$$⊢\phi \to C\ne 0$$
74	13 73	absne0d	$$⊢\phi \to \left|C\right|\ne 0$$
75	72 74	jca	$$⊢\phi \to \left(\left|C\right|\in ℂ\wedge \left|C\right|\ne 0\right)$$
76	71 75 45	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)$$
77		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$$
78	76 77	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$$
79	78	eqcomd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J{\left|C\right|}^J={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J$$
80	69 70 79	3eqtrd	$$⊢\phi \to \frac{{\left|C\right|}^J{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J}{1}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J$$
81	62 67 80	3eqtrd	$$⊢\phi \to \frac{{\left|C\right|}^J}{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J$$
82	58 81	eqtrd	$$⊢\phi \to \frac{\frac{{\left|C\right|}^J}{2}}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J$$
83	82	oveq1d	$$⊢\phi \to \left(\frac{\frac{{\left|C\right|}^J}{2}}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}\right)\left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J\left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)$$
84	53 83	eqtrd	$$⊢\phi \to \left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)\left(\frac{\frac{{\left|C\right|}^J}{2}}{\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(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)$$
85	40 51 84	3eqtrd	$$⊢\phi \to \frac{\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)}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J\left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)$$
86	85	eqcomd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J\left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)=\frac{\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)}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}$$
87	20 37	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 ℝ$$
88	5	a1i	$$⊢\phi \to B=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)$$
89	8	peano2zd	$$⊢\phi \to M+1\in \mathbb{Z}$$
90	9 45 89	knoppndvlem1	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)\in ℝ$$
91	88 90	eqeltrd	$$⊢\phi \to B\in ℝ$$
92	11	simprd	$$⊢\phi \to \left|C\right|<1$$
93	1 2 3 91 9 12 92	knoppcld	$$⊢\phi \to W\left(B\right)\in ℂ$$
94	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>}$$
95	9 45 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 ℝ$$
96	94 95	eqeltrd	$$⊢\phi \to A\in ℝ$$
97	1 2 3 96 9 12 92	knoppcld	$$⊢\phi \to W\left(A\right)\in ℂ$$
98	93 97	subcld	$$⊢\phi \to W\left(B\right)-W\left(A\right)\in ℂ$$
99	98	abscld	$$⊢\phi \to \left|W\left(B\right)-W\left(A\right)\right|\in ℝ$$
100	1 2 3 4 5 6 7 8 9 10	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|$$
101	87 99 48 100	lediv1dd	$$⊢\phi \to \frac{\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)}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}\le \frac{\left|W\left(B\right)-W\left(A\right)\right|}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}$$
102	86 101	eqbrtrd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J\left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)\le \frac{\left|W\left(B\right)-W\left(A\right)\right|}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}$$
103	4 5 7 8 9	knoppndvlem16	$$⊢\phi \to B-A=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}$$
104	103	eqcomd	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}=B-A$$
105	104	oveq2d	$$⊢\phi \to \frac{\left|W\left(B\right)-W\left(A\right)\right|}{\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}}=\frac{\left|W\left(B\right)-W\left(A\right)\right|}{B-A}$$
106	102 105	breqtrd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^J\left(1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\right)\le \frac{\left|W\left(B\right)-W\left(A\right)\right|}{B-A}$$