# Metamath Proof Explorer

## 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 {ℕ}_{0}⟼{{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{y}\right)\right)\right)$
knoppndvlem17.w ${⊢}{W}=\left({w}\in ℝ⟼\sum _{{i}\in {ℕ}_{0}}{F}\left({w}\right)\left({i}\right)\right)$
knoppndvlem17.a ${⊢}{A}=\left(\frac{{2\cdot {N}}^{-{J}}}{2}\right)\cdot {M}$
knoppndvlem17.b ${⊢}{B}=\left(\frac{{2\cdot {N}}^{-{J}}}{2}\right)\left({M}+1\right)$
knoppndvlem17.c ${⊢}{\phi }\to {C}\in \left(-1,1\right)$
knoppndvlem17.j ${⊢}{\phi }\to {J}\in {ℕ}_{0}$
knoppndvlem17.m ${⊢}{\phi }\to {M}\in ℤ$
knoppndvlem17.n ${⊢}{\phi }\to {N}\in ℕ$
knoppndvlem17.1 ${⊢}{\phi }\to 1<{N}\left|{C}\right|$
Assertion knoppndvlem17 ${⊢}{\phi }\to {2\cdot {N}\left|{C}\right|}^{{J}}\left(1-\left(\frac{1}{2\cdot {N}\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 {ℕ}_{0}⟼{{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{y}\right)\right)\right)$
3 knoppndvlem17.w ${⊢}{W}=\left({w}\in ℝ⟼\sum _{{i}\in {ℕ}_{0}}{F}\left({w}\right)\left({i}\right)\right)$
4 knoppndvlem17.a ${⊢}{A}=\left(\frac{{2\cdot {N}}^{-{J}}}{2}\right)\cdot {M}$
5 knoppndvlem17.b ${⊢}{B}=\left(\frac{{2\cdot {N}}^{-{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 {ℕ}_{0}$
8 knoppndvlem17.m ${⊢}{\phi }\to {M}\in ℤ$
9 knoppndvlem17.n ${⊢}{\phi }\to {N}\in ℕ$
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 {N}\in ℝ$
25 24 14 remulcld ${⊢}{\phi }\to 2\cdot {N}\left|{C}\right|\in ℝ$
26 25 22 resubcld ${⊢}{\phi }\to 2\cdot {N}\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 {N}\left|{C}\right|\ne 1\wedge 1<2\cdot {N}\left|{C}\right|-1\right)$
31 30 simprd ${⊢}{\phi }\to 1<2\cdot {N}\left|{C}\right|-1$
32 27 22 26 29 31 lttrd ${⊢}{\phi }\to 0<2\cdot {N}\left|{C}\right|-1$
33 26 32 jca ${⊢}{\phi }\to \left(2\cdot {N}\left|{C}\right|-1\in ℝ\wedge 0<2\cdot {N}\left|{C}\right|-1\right)$
34 gt0ne0 ${⊢}\left(2\cdot {N}\left|{C}\right|-1\in ℝ\wedge 0<2\cdot {N}\left|{C}\right|-1\right)\to 2\cdot {N}\left|{C}\right|-1\ne 0$
35 33 34 syl ${⊢}{\phi }\to 2\cdot {N}\left|{C}\right|-1\ne 0$
36 22 26 35 redivcld ${⊢}{\phi }\to \frac{1}{2\cdot {N}\left|{C}\right|-1}\in ℝ$
37 22 36 resubcld ${⊢}{\phi }\to 1-\left(\frac{1}{2\cdot {N}\left|{C}\right|-1}\right)\in ℝ$
38 37 recnd ${⊢}{\phi }\to 1-\left(\frac{1}{2\cdot {N}\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 {N}\left|{C}\right|-1}\right)\right)=\left(1-\left(\frac{1}{2\cdot {N}\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 {N}\left|{C}\right|-1}\right)\right)}{\frac{{2\cdot {N}}^{-{J}}}{2}}=\frac{\left(1-\left(\frac{1}{2\cdot {N}\left|{C}\right|-1}\right)\right)\left(\frac{{\left|{C}\right|}^{{J}}}{2}\right)}{\frac{{2\cdot {N}}^{-{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 {N}\in {ℝ}^{+}$
45 7 nn0zd ${⊢}{\phi }\to {J}\in ℤ$
46 45 znegcld ${⊢}{\phi }\to -{J}\in ℤ$
47 44 46 rpexpcld ${⊢}{\phi }\to {2\cdot {N}}^{-{J}}\in {ℝ}^{+}$
48 47 rphalfcld ${⊢}{\phi }\to \frac{{2\cdot {N}}^{-{J}}}{2}\in {ℝ}^{+}$
49 48 rpcnd ${⊢}{\phi }\to \frac{{2\cdot {N}}^{-{J}}}{2}\in ℂ$
50 48 rpne0d ${⊢}{\phi }\to \frac{{2\cdot {N}}^{-{J}}}{2}\ne 0$
51 38 21 49 50 divassd ${⊢}{\phi }\to \frac{\left(1-\left(\frac{1}{2\cdot {N}\left|{C}\right|-1}\right)\right)\left(\frac{{\left|{C}\right|}^{{J}}}{2}\right)}{\frac{{2\cdot {N}}^{-{J}}}{2}}=\left(1-\left(\frac{1}{2\cdot {N}\left|{C}\right|-1}\right)\right)\left(\frac{\frac{{\left|{C}\right|}^{{J}}}{2}}{\frac{{2\cdot {N}}^{-{J}}}{2}}\right)$
52 21 49 50 divcld ${⊢}{\phi }\to \frac{\frac{{\left|{C}\right|}^{{J}}}{2}}{\frac{{2\cdot {N}}^{-{J}}}{2}}\in ℂ$
53 38 52 mulcomd ${⊢}{\phi }\to \left(1-\left(\frac{1}{2\cdot {N}\left|{C}\right|-1}\right)\right)\left(\frac{\frac{{\left|{C}\right|}^{{J}}}{2}}{\frac{{2\cdot {N}}^{-{J}}}{2}}\right)=\left(\frac{\frac{{\left|{C}\right|}^{{J}}}{2}}{\frac{{2\cdot {N}}^{-{J}}}{2}}\right)\left(1-\left(\frac{1}{2\cdot {N}\left|{C}\right|-1}\right)\right)$
54 15 recnd ${⊢}{\phi }\to {\left|{C}\right|}^{{J}}\in ℂ$
55 47 rpcnd ${⊢}{\phi }\to {2\cdot {N}}^{-{J}}\in ℂ$
56 17 recnd ${⊢}{\phi }\to 2\in ℂ$
57 47 rpne0d ${⊢}{\phi }\to {2\cdot {N}}^{-{J}}\ne 0$
58 54 55 56 57 19 divcan7d ${⊢}{\phi }\to \frac{\frac{{\left|{C}\right|}^{{J}}}{2}}{\frac{{2\cdot {N}}^{-{J}}}{2}}=\frac{{\left|{C}\right|}^{{J}}}{{2\cdot {N}}^{-{J}}}$
59 24 recnd ${⊢}{\phi }\to 2\cdot {N}\in ℂ$
60 44 rpne0d ${⊢}{\phi }\to 2\cdot {N}\ne 0$
61 59 60 45 expnegd ${⊢}{\phi }\to {2\cdot {N}}^{-{J}}=\frac{1}{{2\cdot {N}}^{{J}}}$
62 61 oveq2d ${⊢}{\phi }\to \frac{{\left|{C}\right|}^{{J}}}{{2\cdot {N}}^{-{J}}}=\frac{{\left|{C}\right|}^{{J}}}{\frac{1}{{2\cdot {N}}^{{J}}}}$
63 1cnd ${⊢}{\phi }\to 1\in ℂ$
64 59 7 expcld ${⊢}{\phi }\to {2\cdot {N}}^{{J}}\in ℂ$
65 27 29 gtned ${⊢}{\phi }\to 1\ne 0$
66 59 60 45 expne0d ${⊢}{\phi }\to {2\cdot {N}}^{{J}}\ne 0$
67 54 63 64 65 66 divdiv2d ${⊢}{\phi }\to \frac{{\left|{C}\right|}^{{J}}}{\frac{1}{{2\cdot {N}}^{{J}}}}=\frac{{\left|{C}\right|}^{{J}}{2\cdot {N}}^{{J}}}{1}$
68 54 64 mulcld ${⊢}{\phi }\to {\left|{C}\right|}^{{J}}{2\cdot {N}}^{{J}}\in ℂ$
69 68 div1d ${⊢}{\phi }\to \frac{{\left|{C}\right|}^{{J}}{2\cdot {N}}^{{J}}}{1}={\left|{C}\right|}^{{J}}{2\cdot {N}}^{{J}}$
70 54 64 mulcomd ${⊢}{\phi }\to {\left|{C}\right|}^{{J}}{2\cdot {N}}^{{J}}={2\cdot {N}}^{{J}}{\left|{C}\right|}^{{J}}$
71 59 60 jca ${⊢}{\phi }\to \left(2\cdot {N}\in ℂ\wedge 2\cdot {N}\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 {N}\in ℂ\wedge 2\cdot {N}\ne 0\right)\wedge \left(\left|{C}\right|\in ℂ\wedge \left|{C}\right|\ne 0\right)\wedge {J}\in ℤ\right)$
77 mulexpz ${⊢}\left(\left(2\cdot {N}\in ℂ\wedge 2\cdot {N}\ne 0\right)\wedge \left(\left|{C}\right|\in ℂ\wedge \left|{C}\right|\ne 0\right)\wedge {J}\in ℤ\right)\to {2\cdot {N}\left|{C}\right|}^{{J}}={2\cdot {N}}^{{J}}{\left|{C}\right|}^{{J}}$
78 76 77 syl ${⊢}{\phi }\to {2\cdot {N}\left|{C}\right|}^{{J}}={2\cdot {N}}^{{J}}{\left|{C}\right|}^{{J}}$
79 78 eqcomd ${⊢}{\phi }\to {2\cdot {N}}^{{J}}{\left|{C}\right|}^{{J}}={2\cdot {N}\left|{C}\right|}^{{J}}$
80 69 70 79 3eqtrd ${⊢}{\phi }\to \frac{{\left|{C}\right|}^{{J}}{2\cdot {N}}^{{J}}}{1}={2\cdot {N}\left|{C}\right|}^{{J}}$
81 62 67 80 3eqtrd ${⊢}{\phi }\to \frac{{\left|{C}\right|}^{{J}}}{{2\cdot {N}}^{-{J}}}={2\cdot {N}\left|{C}\right|}^{{J}}$
82 58 81 eqtrd ${⊢}{\phi }\to \frac{\frac{{\left|{C}\right|}^{{J}}}{2}}{\frac{{2\cdot {N}}^{-{J}}}{2}}={2\cdot {N}\left|{C}\right|}^{{J}}$
83 82 oveq1d ${⊢}{\phi }\to \left(\frac{\frac{{\left|{C}\right|}^{{J}}}{2}}{\frac{{2\cdot {N}}^{-{J}}}{2}}\right)\left(1-\left(\frac{1}{2\cdot {N}\left|{C}\right|-1}\right)\right)={2\cdot {N}\left|{C}\right|}^{{J}}\left(1-\left(\frac{1}{2\cdot {N}\left|{C}\right|-1}\right)\right)$
84 53 83 eqtrd ${⊢}{\phi }\to \left(1-\left(\frac{1}{2\cdot {N}\left|{C}\right|-1}\right)\right)\left(\frac{\frac{{\left|{C}\right|}^{{J}}}{2}}{\frac{{2\cdot {N}}^{-{J}}}{2}}\right)={2\cdot {N}\left|{C}\right|}^{{J}}\left(1-\left(\frac{1}{2\cdot {N}\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 {N}\left|{C}\right|-1}\right)\right)}{\frac{{2\cdot {N}}^{-{J}}}{2}}={2\cdot {N}\left|{C}\right|}^{{J}}\left(1-\left(\frac{1}{2\cdot {N}\left|{C}\right|-1}\right)\right)$
86 85 eqcomd ${⊢}{\phi }\to {2\cdot {N}\left|{C}\right|}^{{J}}\left(1-\left(\frac{1}{2\cdot {N}\left|{C}\right|-1}\right)\right)=\frac{\left(\frac{{\left|{C}\right|}^{{J}}}{2}\right)\left(1-\left(\frac{1}{2\cdot {N}\left|{C}\right|-1}\right)\right)}{\frac{{2\cdot {N}}^{-{J}}}{2}}$
87 20 37 remulcld ${⊢}{\phi }\to \left(\frac{{\left|{C}\right|}^{{J}}}{2}\right)\left(1-\left(\frac{1}{2\cdot {N}\left|{C}\right|-1}\right)\right)\in ℝ$
88 5 a1i ${⊢}{\phi }\to {B}=\left(\frac{{2\cdot {N}}^{-{J}}}{2}\right)\left({M}+1\right)$
89 8 peano2zd ${⊢}{\phi }\to {M}+1\in ℤ$
90 9 45 89 knoppndvlem1 ${⊢}{\phi }\to \left(\frac{{2\cdot {N}}^{-{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 {N}}^{-{J}}}{2}\right)\cdot {M}$
95 9 45 8 knoppndvlem1 ${⊢}{\phi }\to \left(\frac{{2\cdot {N}}^{-{J}}}{2}\right)\cdot {M}\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 {N}\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 {N}\left|{C}\right|-1}\right)\right)}{\frac{{2\cdot {N}}^{-{J}}}{2}}\le \frac{\left|{W}\left({B}\right)-{W}\left({A}\right)\right|}{\frac{{2\cdot {N}}^{-{J}}}{2}}$
102 86 101 eqbrtrd ${⊢}{\phi }\to {2\cdot {N}\left|{C}\right|}^{{J}}\left(1-\left(\frac{1}{2\cdot {N}\left|{C}\right|-1}\right)\right)\le \frac{\left|{W}\left({B}\right)-{W}\left({A}\right)\right|}{\frac{{2\cdot {N}}^{-{J}}}{2}}$
103 4 5 7 8 9 knoppndvlem16 ${⊢}{\phi }\to {B}-{A}=\frac{{2\cdot {N}}^{-{J}}}{2}$
104 103 eqcomd ${⊢}{\phi }\to \frac{{2\cdot {N}}^{-{J}}}{2}={B}-{A}$
105 104 oveq2d ${⊢}{\phi }\to \frac{\left|{W}\left({B}\right)-{W}\left({A}\right)\right|}{\frac{{2\cdot {N}}^{-{J}}}{2}}=\frac{\left|{W}\left({B}\right)-{W}\left({A}\right)\right|}{{B}-{A}}$
106 102 105 breqtrd ${⊢}{\phi }\to {2\cdot {N}\left|{C}\right|}^{{J}}\left(1-\left(\frac{1}{2\cdot {N}\left|{C}\right|-1}\right)\right)\le \frac{\left|{W}\left({B}\right)-{W}\left({A}\right)\right|}{{B}-{A}}$