# Metamath Proof Explorer

## Theorem knoppndvlem11

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 28-Jun-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

Ref Expression
Hypotheses knoppndvlem11.t ${⊢}{T}=\left({x}\in ℝ⟼\left|⌊{x}+\left(\frac{1}{2}\right)⌋-{x}\right|\right)$
knoppndvlem11.f ${⊢}{F}=\left({y}\in ℝ⟼\left({n}\in {ℕ}_{0}⟼{{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{y}\right)\right)\right)$
knoppndvlem11.a ${⊢}{\phi }\to {A}\in ℝ$
knoppndvlem11.b ${⊢}{\phi }\to {B}\in ℝ$
knoppndvlem11.c ${⊢}{\phi }\to {C}\in \left(-1,1\right)$
knoppndvlem11.j ${⊢}{\phi }\to {J}\in {ℕ}_{0}$
knoppndvlem11.n ${⊢}{\phi }\to {N}\in ℕ$
Assertion 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 {N}\left|{C}\right|}^{{i}}$

### Proof

Step Hyp Ref Expression
1 knoppndvlem11.t ${⊢}{T}=\left({x}\in ℝ⟼\left|⌊{x}+\left(\frac{1}{2}\right)⌋-{x}\right|\right)$
2 knoppndvlem11.f ${⊢}{F}=\left({y}\in ℝ⟼\left({n}\in {ℕ}_{0}⟼{{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{y}\right)\right)\right)$
3 knoppndvlem11.a ${⊢}{\phi }\to {A}\in ℝ$
4 knoppndvlem11.b ${⊢}{\phi }\to {B}\in ℝ$
5 knoppndvlem11.c ${⊢}{\phi }\to {C}\in \left(-1,1\right)$
6 knoppndvlem11.j ${⊢}{\phi }\to {J}\in {ℕ}_{0}$
7 knoppndvlem11.n ${⊢}{\phi }\to {N}\in ℕ$
8 fzfid ${⊢}{\phi }\to \left(0\dots {J}-1\right)\in \mathrm{Fin}$
9 7 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {N}\in ℕ$
10 5 knoppndvlem3 ${⊢}{\phi }\to \left({C}\in ℝ\wedge \left|{C}\right|<1\right)$
11 10 simpld ${⊢}{\phi }\to {C}\in ℝ$
12 11 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {C}\in ℝ$
13 4 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {B}\in ℝ$
14 elfznn0 ${⊢}{i}\in \left(0\dots {J}-1\right)\to {i}\in {ℕ}_{0}$
15 14 adantl ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {i}\in {ℕ}_{0}$
16 1 2 9 12 13 15 knoppcnlem3 ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {F}\left({B}\right)\left({i}\right)\in ℝ$
17 16 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {F}\left({B}\right)\left({i}\right)\in ℂ$
18 3 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {A}\in ℝ$
19 1 2 9 12 18 15 knoppcnlem3 ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {F}\left({A}\right)\left({i}\right)\in ℝ$
20 19 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {F}\left({A}\right)\left({i}\right)\in ℂ$
21 8 17 20 fsumsub ${⊢}{\phi }\to \sum _{{i}=0}^{{J}-1}\left({F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\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)$
22 21 eqcomd ${⊢}{\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)=\sum _{{i}=0}^{{J}-1}\left({F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)\right)$
23 22 fveq2d ${⊢}{\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|=\left|\sum _{{i}=0}^{{J}-1}\left({F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)\right)\right|$
24 17 20 subcld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)\in ℂ$
25 8 24 fsumcl ${⊢}{\phi }\to \sum _{{i}=0}^{{J}-1}\left({F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)\right)\in ℂ$
26 25 abscld ${⊢}{\phi }\to \left|\sum _{{i}=0}^{{J}-1}\left({F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)\right)\right|\in ℝ$
27 24 abscld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)\right|\in ℝ$
28 8 27 fsumrecl ${⊢}{\phi }\to \sum _{{i}=0}^{{J}-1}\left|{F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)\right|\in ℝ$
29 4 3 resubcld ${⊢}{\phi }\to {B}-{A}\in ℝ$
30 29 recnd ${⊢}{\phi }\to {B}-{A}\in ℂ$
31 30 abscld ${⊢}{\phi }\to \left|{B}-{A}\right|\in ℝ$
32 2re ${⊢}2\in ℝ$
33 32 a1i ${⊢}{\phi }\to 2\in ℝ$
34 nnre ${⊢}{N}\in ℕ\to {N}\in ℝ$
35 7 34 syl ${⊢}{\phi }\to {N}\in ℝ$
36 33 35 remulcld ${⊢}{\phi }\to 2\cdot {N}\in ℝ$
37 11 recnd ${⊢}{\phi }\to {C}\in ℂ$
38 37 abscld ${⊢}{\phi }\to \left|{C}\right|\in ℝ$
39 36 38 remulcld ${⊢}{\phi }\to 2\cdot {N}\left|{C}\right|\in ℝ$
40 39 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to 2\cdot {N}\left|{C}\right|\in ℝ$
41 40 15 reexpcld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {2\cdot {N}\left|{C}\right|}^{{i}}\in ℝ$
42 8 41 fsumrecl ${⊢}{\phi }\to \sum _{{i}=0}^{{J}-1}{2\cdot {N}\left|{C}\right|}^{{i}}\in ℝ$
43 31 42 remulcld ${⊢}{\phi }\to \left|{B}-{A}\right|\sum _{{i}=0}^{{J}-1}{2\cdot {N}\left|{C}\right|}^{{i}}\in ℝ$
44 8 24 fsumabs ${⊢}{\phi }\to \left|\sum _{{i}=0}^{{J}-1}\left({F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)\right)\right|\le \sum _{{i}=0}^{{J}-1}\left|{F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)\right|$
45 31 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{B}-{A}\right|\in ℝ$
46 45 41 remulcld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{B}-{A}\right|{2\cdot {N}\left|{C}\right|}^{{i}}\in ℝ$
47 2 13 15 knoppcnlem1 ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {F}\left({B}\right)\left({i}\right)={{C}}^{{i}}{T}\left({2\cdot {N}}^{{i}}{B}\right)$
48 2 18 15 knoppcnlem1 ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {F}\left({A}\right)\left({i}\right)={{C}}^{{i}}{T}\left({2\cdot {N}}^{{i}}{A}\right)$
49 47 48 oveq12d ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)={{C}}^{{i}}{T}\left({2\cdot {N}}^{{i}}{B}\right)-{{C}}^{{i}}{T}\left({2\cdot {N}}^{{i}}{A}\right)$
50 12 15 reexpcld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {{C}}^{{i}}\in ℝ$
51 50 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {{C}}^{{i}}\in ℂ$
52 36 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to 2\cdot {N}\in ℝ$
53 52 15 reexpcld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {2\cdot {N}}^{{i}}\in ℝ$
54 53 13 remulcld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {2\cdot {N}}^{{i}}{B}\in ℝ$
55 1 54 dnicld2 ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {T}\left({2\cdot {N}}^{{i}}{B}\right)\in ℝ$
56 55 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {T}\left({2\cdot {N}}^{{i}}{B}\right)\in ℂ$
57 53 18 remulcld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {2\cdot {N}}^{{i}}{A}\in ℝ$
58 1 57 dnicld2 ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {T}\left({2\cdot {N}}^{{i}}{A}\right)\in ℝ$
59 58 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {T}\left({2\cdot {N}}^{{i}}{A}\right)\in ℂ$
60 51 56 59 subdid ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {{C}}^{{i}}\left({T}\left({2\cdot {N}}^{{i}}{B}\right)-{T}\left({2\cdot {N}}^{{i}}{A}\right)\right)={{C}}^{{i}}{T}\left({2\cdot {N}}^{{i}}{B}\right)-{{C}}^{{i}}{T}\left({2\cdot {N}}^{{i}}{A}\right)$
61 60 eqcomd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {{C}}^{{i}}{T}\left({2\cdot {N}}^{{i}}{B}\right)-{{C}}^{{i}}{T}\left({2\cdot {N}}^{{i}}{A}\right)={{C}}^{{i}}\left({T}\left({2\cdot {N}}^{{i}}{B}\right)-{T}\left({2\cdot {N}}^{{i}}{A}\right)\right)$
62 49 61 eqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)={{C}}^{{i}}\left({T}\left({2\cdot {N}}^{{i}}{B}\right)-{T}\left({2\cdot {N}}^{{i}}{A}\right)\right)$
63 62 fveq2d ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)\right|=\left|{{C}}^{{i}}\left({T}\left({2\cdot {N}}^{{i}}{B}\right)-{T}\left({2\cdot {N}}^{{i}}{A}\right)\right)\right|$
64 56 59 subcld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {T}\left({2\cdot {N}}^{{i}}{B}\right)-{T}\left({2\cdot {N}}^{{i}}{A}\right)\in ℂ$
65 51 64 absmuld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{{C}}^{{i}}\left({T}\left({2\cdot {N}}^{{i}}{B}\right)-{T}\left({2\cdot {N}}^{{i}}{A}\right)\right)\right|=\left|{{C}}^{{i}}\right|\left|{T}\left({2\cdot {N}}^{{i}}{B}\right)-{T}\left({2\cdot {N}}^{{i}}{A}\right)\right|$
66 37 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {C}\in ℂ$
67 66 15 absexpd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{{C}}^{{i}}\right|={\left|{C}\right|}^{{i}}$
68 67 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{{C}}^{{i}}\right|\left|{T}\left({2\cdot {N}}^{{i}}{B}\right)-{T}\left({2\cdot {N}}^{{i}}{A}\right)\right|={\left|{C}\right|}^{{i}}\left|{T}\left({2\cdot {N}}^{{i}}{B}\right)-{T}\left({2\cdot {N}}^{{i}}{A}\right)\right|$
69 65 68 eqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{{C}}^{{i}}\left({T}\left({2\cdot {N}}^{{i}}{B}\right)-{T}\left({2\cdot {N}}^{{i}}{A}\right)\right)\right|={\left|{C}\right|}^{{i}}\left|{T}\left({2\cdot {N}}^{{i}}{B}\right)-{T}\left({2\cdot {N}}^{{i}}{A}\right)\right|$
70 63 69 eqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)\right|={\left|{C}\right|}^{{i}}\left|{T}\left({2\cdot {N}}^{{i}}{B}\right)-{T}\left({2\cdot {N}}^{{i}}{A}\right)\right|$
71 64 abscld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{T}\left({2\cdot {N}}^{{i}}{B}\right)-{T}\left({2\cdot {N}}^{{i}}{A}\right)\right|\in ℝ$
72 54 57 resubcld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {2\cdot {N}}^{{i}}{B}-{2\cdot {N}}^{{i}}{A}\in ℝ$
73 72 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {2\cdot {N}}^{{i}}{B}-{2\cdot {N}}^{{i}}{A}\in ℂ$
74 73 abscld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{2\cdot {N}}^{{i}}{B}-{2\cdot {N}}^{{i}}{A}\right|\in ℝ$
75 38 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{C}\right|\in ℝ$
76 75 15 reexpcld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {\left|{C}\right|}^{{i}}\in ℝ$
77 66 absge0d ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to 0\le \left|{C}\right|$
78 75 15 77 expge0d ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to 0\le {\left|{C}\right|}^{{i}}$
79 1 57 54 dnibnd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{T}\left({2\cdot {N}}^{{i}}{B}\right)-{T}\left({2\cdot {N}}^{{i}}{A}\right)\right|\le \left|{2\cdot {N}}^{{i}}{B}-{2\cdot {N}}^{{i}}{A}\right|$
80 71 74 76 78 79 lemul2ad ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {\left|{C}\right|}^{{i}}\left|{T}\left({2\cdot {N}}^{{i}}{B}\right)-{T}\left({2\cdot {N}}^{{i}}{A}\right)\right|\le {\left|{C}\right|}^{{i}}\left|{2\cdot {N}}^{{i}}{B}-{2\cdot {N}}^{{i}}{A}\right|$
81 53 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {2\cdot {N}}^{{i}}\in ℂ$
82 13 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {B}\in ℂ$
83 18 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {A}\in ℂ$
84 81 82 83 subdid ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {2\cdot {N}}^{{i}}\left({B}-{A}\right)={2\cdot {N}}^{{i}}{B}-{2\cdot {N}}^{{i}}{A}$
85 84 eqcomd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {2\cdot {N}}^{{i}}{B}-{2\cdot {N}}^{{i}}{A}={2\cdot {N}}^{{i}}\left({B}-{A}\right)$
86 85 fveq2d ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{2\cdot {N}}^{{i}}{B}-{2\cdot {N}}^{{i}}{A}\right|=\left|{2\cdot {N}}^{{i}}\left({B}-{A}\right)\right|$
87 30 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {B}-{A}\in ℂ$
88 81 87 absmuld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{2\cdot {N}}^{{i}}\left({B}-{A}\right)\right|=\left|{2\cdot {N}}^{{i}}\right|\left|{B}-{A}\right|$
89 52 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to 2\cdot {N}\in ℂ$
90 89 15 absexpd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{2\cdot {N}}^{{i}}\right|={\left|2\cdot {N}\right|}^{{i}}$
91 33 recnd ${⊢}{\phi }\to 2\in ℂ$
92 35 recnd ${⊢}{\phi }\to {N}\in ℂ$
93 91 92 absmuld ${⊢}{\phi }\to \left|2\cdot {N}\right|=\left|2\right|\left|{N}\right|$
94 0le2 ${⊢}0\le 2$
95 32 absidi ${⊢}0\le 2\to \left|2\right|=2$
96 94 95 ax-mp ${⊢}\left|2\right|=2$
97 96 a1i ${⊢}{\phi }\to \left|2\right|=2$
98 0red ${⊢}{\phi }\to 0\in ℝ$
99 1red ${⊢}{\phi }\to 1\in ℝ$
100 0le1 ${⊢}0\le 1$
101 100 a1i ${⊢}{\phi }\to 0\le 1$
102 nnge1 ${⊢}{N}\in ℕ\to 1\le {N}$
103 7 102 syl ${⊢}{\phi }\to 1\le {N}$
104 98 99 35 101 103 letrd ${⊢}{\phi }\to 0\le {N}$
105 35 104 absidd ${⊢}{\phi }\to \left|{N}\right|={N}$
106 97 105 oveq12d ${⊢}{\phi }\to \left|2\right|\left|{N}\right|=2\cdot {N}$
107 93 106 eqtrd ${⊢}{\phi }\to \left|2\cdot {N}\right|=2\cdot {N}$
108 107 oveq1d ${⊢}{\phi }\to {\left|2\cdot {N}\right|}^{{i}}={2\cdot {N}}^{{i}}$
109 108 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {\left|2\cdot {N}\right|}^{{i}}={2\cdot {N}}^{{i}}$
110 90 109 eqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{2\cdot {N}}^{{i}}\right|={2\cdot {N}}^{{i}}$
111 110 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{2\cdot {N}}^{{i}}\right|\left|{B}-{A}\right|={2\cdot {N}}^{{i}}\left|{B}-{A}\right|$
112 88 111 eqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{2\cdot {N}}^{{i}}\left({B}-{A}\right)\right|={2\cdot {N}}^{{i}}\left|{B}-{A}\right|$
113 86 112 eqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{2\cdot {N}}^{{i}}{B}-{2\cdot {N}}^{{i}}{A}\right|={2\cdot {N}}^{{i}}\left|{B}-{A}\right|$
114 113 oveq2d ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {\left|{C}\right|}^{{i}}\left|{2\cdot {N}}^{{i}}{B}-{2\cdot {N}}^{{i}}{A}\right|={\left|{C}\right|}^{{i}}{2\cdot {N}}^{{i}}\left|{B}-{A}\right|$
115 76 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {\left|{C}\right|}^{{i}}\in ℂ$
116 45 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{B}-{A}\right|\in ℂ$
117 115 81 116 mulassd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {\left|{C}\right|}^{{i}}{2\cdot {N}}^{{i}}\left|{B}-{A}\right|={\left|{C}\right|}^{{i}}{2\cdot {N}}^{{i}}\left|{B}-{A}\right|$
118 117 eqcomd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {\left|{C}\right|}^{{i}}{2\cdot {N}}^{{i}}\left|{B}-{A}\right|={\left|{C}\right|}^{{i}}{2\cdot {N}}^{{i}}\left|{B}-{A}\right|$
119 115 81 mulcld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {\left|{C}\right|}^{{i}}{2\cdot {N}}^{{i}}\in ℂ$
120 119 116 mulcomd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {\left|{C}\right|}^{{i}}{2\cdot {N}}^{{i}}\left|{B}-{A}\right|=\left|{B}-{A}\right|{\left|{C}\right|}^{{i}}{2\cdot {N}}^{{i}}$
121 115 81 mulcomd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {\left|{C}\right|}^{{i}}{2\cdot {N}}^{{i}}={2\cdot {N}}^{{i}}{\left|{C}\right|}^{{i}}$
122 75 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{C}\right|\in ℂ$
123 89 122 15 mulexpd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {2\cdot {N}\left|{C}\right|}^{{i}}={2\cdot {N}}^{{i}}{\left|{C}\right|}^{{i}}$
124 123 eqcomd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {2\cdot {N}}^{{i}}{\left|{C}\right|}^{{i}}={2\cdot {N}\left|{C}\right|}^{{i}}$
125 121 124 eqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {\left|{C}\right|}^{{i}}{2\cdot {N}}^{{i}}={2\cdot {N}\left|{C}\right|}^{{i}}$
126 125 oveq2d ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{B}-{A}\right|{\left|{C}\right|}^{{i}}{2\cdot {N}}^{{i}}=\left|{B}-{A}\right|{2\cdot {N}\left|{C}\right|}^{{i}}$
127 118 120 126 3eqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {\left|{C}\right|}^{{i}}{2\cdot {N}}^{{i}}\left|{B}-{A}\right|=\left|{B}-{A}\right|{2\cdot {N}\left|{C}\right|}^{{i}}$
128 114 127 eqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {\left|{C}\right|}^{{i}}\left|{2\cdot {N}}^{{i}}{B}-{2\cdot {N}}^{{i}}{A}\right|=\left|{B}-{A}\right|{2\cdot {N}\left|{C}\right|}^{{i}}$
129 80 128 breqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {\left|{C}\right|}^{{i}}\left|{T}\left({2\cdot {N}}^{{i}}{B}\right)-{T}\left({2\cdot {N}}^{{i}}{A}\right)\right|\le \left|{B}-{A}\right|{2\cdot {N}\left|{C}\right|}^{{i}}$
130 70 129 eqbrtrd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to \left|{F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)\right|\le \left|{B}-{A}\right|{2\cdot {N}\left|{C}\right|}^{{i}}$
131 8 27 46 130 fsumle ${⊢}{\phi }\to \sum _{{i}=0}^{{J}-1}\left|{F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)\right|\le \sum _{{i}=0}^{{J}-1}\left|{B}-{A}\right|{2\cdot {N}\left|{C}\right|}^{{i}}$
132 31 recnd ${⊢}{\phi }\to \left|{B}-{A}\right|\in ℂ$
133 125 119 eqeltrrd ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {J}-1\right)\right)\to {2\cdot {N}\left|{C}\right|}^{{i}}\in ℂ$
134 8 132 133 fsummulc2 ${⊢}{\phi }\to \left|{B}-{A}\right|\sum _{{i}=0}^{{J}-1}{2\cdot {N}\left|{C}\right|}^{{i}}=\sum _{{i}=0}^{{J}-1}\left|{B}-{A}\right|{2\cdot {N}\left|{C}\right|}^{{i}}$
135 134 eqcomd ${⊢}{\phi }\to \sum _{{i}=0}^{{J}-1}\left|{B}-{A}\right|{2\cdot {N}\left|{C}\right|}^{{i}}=\left|{B}-{A}\right|\sum _{{i}=0}^{{J}-1}{2\cdot {N}\left|{C}\right|}^{{i}}$
136 131 135 breqtrd ${⊢}{\phi }\to \sum _{{i}=0}^{{J}-1}\left|{F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)\right|\le \left|{B}-{A}\right|\sum _{{i}=0}^{{J}-1}{2\cdot {N}\left|{C}\right|}^{{i}}$
137 26 28 43 44 136 letrd ${⊢}{\phi }\to \left|\sum _{{i}=0}^{{J}-1}\left({F}\left({B}\right)\left({i}\right)-{F}\left({A}\right)\left({i}\right)\right)\right|\le \left|{B}-{A}\right|\sum _{{i}=0}^{{J}-1}{2\cdot {N}\left|{C}\right|}^{{i}}$
138 23 137 eqbrtrd ${⊢}{\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 {N}\left|{C}\right|}^{{i}}$