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=x∈ℝ⟼x+12−x
knoppndvlem11.f ⊢F=y∈ℝ⟼n∈ℕ0⟼Cn⁢T⁡2⋅ Nn⁢y
knoppndvlem11.a ⊢φ→A∈ℝ
knoppndvlem11.b ⊢φ→B∈ℝ
knoppndvlem11.c ⊢φ→C∈−11
knoppndvlem11.j ⊢φ→J∈ℕ0
knoppndvlem11.n ⊢φ→N∈ℕ
Assertion knoppndvlem11 ⊢φ→∑i=0J−1F⁡B⁡i−∑i=0J−1F⁡A⁡i≤B−A⁢∑i=0J−12⋅ N⁢Ci

Proof

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