Theorem knoppndvlem22

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

	Ref	Expression
Hypotheses	knoppndvlem22.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
	knoppndvlem22.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)$$
	knoppndvlem22.w	$$⊢W=\left(w\in ℝ⟼\sum _{i\in {\mathbb{N}}_0}F\left(w\right)\left(i\right)\right)$$
	knoppndvlem22.c	$$⊢\phi \to C\in \left(-1,1\right)$$
	knoppndvlem22.d	$$⊢\phi \to D\in {ℝ}^{+}$$
	knoppndvlem22.e	$$⊢\phi \to E\in {ℝ}^{+}$$
	knoppndvlem22.h	$$⊢\phi \to H\in ℝ$$
	knoppndvlem22.n	$$⊢\phi \to N\in \mathbb{N}$$
	knoppndvlem22.1	$$⊢\phi \to 1<N\left|C\right|$$
Assertion	knoppndvlem22	$$⊢\phi \to \exists a\in ℝ\exists b\in ℝ\left(\left(a\le H\wedge H\le b\right)\wedge \left(b-a<D\wedge a\ne b\right)\wedge E\le \frac{\left|W\left(b\right)-W\left(a\right)\right|}{b-a}\right)$$

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem22.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		knoppndvlem22.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		knoppndvlem22.w	$$⊢W=\left(w\in ℝ⟼\sum _{i\in {\mathbb{N}}_0}F\left(w\right)\left(i\right)\right)$$
4		knoppndvlem22.c	$$⊢\phi \to C\in \left(-1,1\right)$$
5		knoppndvlem22.d	$$⊢\phi \to D\in {ℝ}^{+}$$
6		knoppndvlem22.e	$$⊢\phi \to E\in {ℝ}^{+}$$
7		knoppndvlem22.h	$$⊢\phi \to H\in ℝ$$
8		knoppndvlem22.n	$$⊢\phi \to N\in \mathbb{N}$$
9		knoppndvlem22.1	$$⊢\phi \to 1<N\left|C\right|$$
10	4 8 9	knoppndvlem20	$$⊢\phi \to 1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)\in {ℝ}^{+}$$
11	4 8 5 6 10 9	knoppndvlem18	$$⊢\phi \to \exists j\in {\mathbb{N}}_0\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {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)\right)$$
12		eqid	$$⊢1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)=1-\left(\frac{1}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|-1}\right)$$
13	4	adantr	$$⊢\left(\phi \wedge \left(j\in {\mathbb{N}}_0\wedge \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {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)\right)\right)\right)\to C\in \left(-1,1\right)$$
14	5	adantr	$$⊢\left(\phi \wedge \left(j\in {\mathbb{N}}_0\wedge \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {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)\right)\right)\right)\to D\in {ℝ}^{+}$$
15	6	adantr	$$⊢\left(\phi \wedge \left(j\in {\mathbb{N}}_0\wedge \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {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)\right)\right)\right)\to E\in {ℝ}^{+}$$
16	7	adantr	$$⊢\left(\phi \wedge \left(j\in {\mathbb{N}}_0\wedge \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {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)\right)\right)\right)\to H\in ℝ$$
17		simprl	$$⊢\left(\phi \wedge \left(j\in {\mathbb{N}}_0\wedge \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {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)\right)\right)\right)\to j\in {\mathbb{N}}_0$$
18	8	adantr	$$⊢\left(\phi \wedge \left(j\in {\mathbb{N}}_0\wedge \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {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)\right)\right)\right)\to N\in \mathbb{N}$$
19	9	adantr	$$⊢\left(\phi \wedge \left(j\in {\mathbb{N}}_0\wedge \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {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)\right)\right)\right)\to 1<N\left|C\right|$$
20		simprrl	$$⊢\left(\phi \wedge \left(j\in {\mathbb{N}}_0\wedge \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {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)\right)\right)\right)\to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D$$
21		simprrr	$$⊢\left(\phi \wedge \left(j\in {\mathbb{N}}_0\wedge \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {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)\right)\right)\right)\to E\le {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)$$
22	1 2 3 12 13 14 15 16 17 18 19 20 21	knoppndvlem21	$$⊢\left(\phi \wedge \left(j\in {\mathbb{N}}_0\wedge \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {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)\right)\right)\right)\to \exists a\in ℝ\exists b\in ℝ\left(\left(a\le H\wedge H\le b\right)\wedge \left(b-a<D\wedge a\ne b\right)\wedge E\le \frac{\left|W\left(b\right)-W\left(a\right)\right|}{b-a}\right)$$
23	11 22	rexlimddv	$$⊢\phi \to \exists a\in ℝ\exists b\in ℝ\left(\left(a\le H\wedge H\le b\right)\wedge \left(b-a<D\wedge a\ne b\right)\wedge E\le \frac{\left|W\left(b\right)-W\left(a\right)\right|}{b-a}\right)$$