Metamath Proof Explorer

Theorem knoppndvlem14

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 1-Jul-2021) (Revised by Asger C. Ipsen, 7-Jul-2021)

Ref Expression
Hypotheses knoppndvlem14.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
knoppndvlem14.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
knoppndvlem14.a ⊢ 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 )
knoppndvlem14.b ⊢ 𝐵 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) )
knoppndvlem14.c ⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
knoppndvlem14.j ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
knoppndvlem14.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
knoppndvlem14.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
knoppndvlem14.1 ⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
Assertion knoppndvlem14 ( 𝜑 → ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ≤ ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 knoppndvlem14.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 knoppndvlem14.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3 knoppndvlem14.a ⊢ 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 )
4 knoppndvlem14.b ⊢ 𝐵 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) )
5 knoppndvlem14.c ⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
6 knoppndvlem14.j ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
7 knoppndvlem14.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
8 knoppndvlem14.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9 knoppndvlem14.1 ⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
10 4 a1i ⊢ ( 𝜑 → 𝐵 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) )
11 6 nn0zd ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
12 7 peano2zd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℤ )
13 8 11 12 knoppndvlem1 ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) ∈ ℝ )
14 10 13 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
15 5 knoppndvlem3 ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( abs ‘ 𝐶 ) < 1 ) )
16 15 simpld ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
17 1 2 14 16 8 knoppndvlem5 ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) ∈ ℝ )
18 3 a1i ⊢ ( 𝜑 → 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) )
19 8 11 7 knoppndvlem1 ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ∈ ℝ )
20 18 19 eqeltrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
21 1 2 20 16 8 knoppndvlem5 ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℝ )
22 17 21 resubcld ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ∈ ℝ )
23 22 recnd ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ∈ ℂ )
24 23 abscld ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ∈ ℝ )
25 14 20 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
26 25 recnd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℂ )
27 26 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐴 ) ) ∈ ℝ )
28 fzfid ⊢ ( 𝜑 → ( 0 ... ( 𝐽 − 1 ) ) ∈ Fin )
29 2re ⊢ 2 ∈ ℝ
30 29 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
31 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
32 8 31 syl ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
33 30 32 remulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
34 16 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
35 34 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℝ )
36 33 35 remulcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ∈ ℝ )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ∈ ℝ )
38 elfznn0 ⊢ ( 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) → 𝑖 ∈ ℕ0 )
39 38 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → 𝑖 ∈ ℕ0 )
40 37 39 reexpcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ) → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ∈ ℝ )
41 28 40 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ∈ ℝ )
42 27 41 remulcld ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) ∈ ℝ )
43 35 6 reexpcld ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ∈ ℝ )
44 2ne0 ⊢ 2 ≠ 0
45 44 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
46 43 30 45 redivcld ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ∈ ℝ )
47 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
48 36 47 resubcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ∈ ℝ )
49 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
50 0lt1 ⊢ 0 < 1
51 50 a1i ⊢ ( 𝜑 → 0 < 1 )
52 5 8 9 knoppndvlem12 ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ≠ 1 ∧ 1 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )
53 52 simprd ⊢ ( 𝜑 → 1 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) )
54 49 47 48 51 53 lttrd ⊢ ( 𝜑 → 0 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) )
55 49 54 jca ⊢ ( 𝜑 → ( 0 ∈ ℝ ∧ 0 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )
56 ltne ⊢ ( ( 0 ∈ ℝ ∧ 0 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ≠ 0 )
57 55 56 syl ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ≠ 0 )
58 47 48 57 redivcld ⊢ ( 𝜑 → ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ∈ ℝ )
59 46 58 remulcld ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ )
60 1 2 20 14 5 6 8 knoppndvlem11 ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ≤ ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) )
61 10 18 oveq12d ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) )
62 30 recnd ⊢ ( 𝜑 → 2 ∈ ℂ )
63 32 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
64 nnge1 ⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
65 8 64 syl ⊢ ( 𝜑 → 1 ≤ 𝑁 )
66 49 47 32 51 65 ltletrd ⊢ ( 𝜑 → 0 < 𝑁 )
67 49 66 jca ⊢ ( 𝜑 → ( 0 ∈ ℝ ∧ 0 < 𝑁 ) )
68 ltne ⊢ ( ( 0 ∈ ℝ ∧ 0 < 𝑁 ) → 𝑁 ≠ 0 )
69 67 68 syl ⊢ ( 𝜑 → 𝑁 ≠ 0 )
70 62 63 45 69 mulne0d ⊢ ( 𝜑 → ( 2 · 𝑁 ) ≠ 0 )
71 11 znegcld ⊢ ( 𝜑 → - 𝐽 ∈ ℤ )
72 33 70 71 reexpclzd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ∈ ℝ )
73 72 30 45 redivcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ∈ ℝ )
74 73 recnd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ∈ ℂ )
75 12 zcnd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℂ )
76 7 zcnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
77 74 75 76 subdid ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( 𝑀 + 1 ) − 𝑀 ) ) = ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) )
78 77 eqcomd ⊢ ( 𝜑 → ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( 𝑀 + 1 ) − 𝑀 ) ) )
79 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
80 76 79 pncan2d ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) − 𝑀 ) = 1 )
81 80 oveq2d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( 𝑀 + 1 ) − 𝑀 ) ) = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 1 ) )
82 74 mulid1d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 1 ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )
83 78 81 82 3eqtrd ⊢ ( 𝜑 → ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )
84 61 83 eqtrd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )
85 84 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐴 ) ) = ( abs ‘ ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) )
86 72 recnd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ∈ ℂ )
87 86 62 45 absdivd ⊢ ( 𝜑 → ( abs ‘ ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) = ( ( abs ‘ ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) / ( abs ‘ 2 ) ) )
88 62 63 mulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
89 88 70 71 3jca ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( 2 · 𝑁 ) ≠ 0 ∧ - 𝐽 ∈ ℤ ) )
90 absexpz ⊢ ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( 2 · 𝑁 ) ≠ 0 ∧ - 𝐽 ∈ ℤ ) → ( abs ‘ ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) = ( ( abs ‘ ( 2 · 𝑁 ) ) ↑ - 𝐽 ) )
91 89 90 syl ⊢ ( 𝜑 → ( abs ‘ ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) = ( ( abs ‘ ( 2 · 𝑁 ) ) ↑ - 𝐽 ) )
92 62 63 absmuld ⊢ ( 𝜑 → ( abs ‘ ( 2 · 𝑁 ) ) = ( ( abs ‘ 2 ) · ( abs ‘ 𝑁 ) ) )
93 0le2 ⊢ 0 ≤ 2
94 29 93 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 ≤ 2 )
95 absid ⊢ ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) → ( abs ‘ 2 ) = 2 )
96 94 95 ax-mp ⊢ ( abs ‘ 2 ) = 2
97 96 a1i ⊢ ( 𝜑 → ( abs ‘ 2 ) = 2 )
98 49 32 66 ltled ⊢ ( 𝜑 → 0 ≤ 𝑁 )
99 32 98 absidd ⊢ ( 𝜑 → ( abs ‘ 𝑁 ) = 𝑁 )
100 97 99 oveq12d ⊢ ( 𝜑 → ( ( abs ‘ 2 ) · ( abs ‘ 𝑁 ) ) = ( 2 · 𝑁 ) )
101 92 100 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( 2 · 𝑁 ) ) = ( 2 · 𝑁 ) )
102 101 oveq1d ⊢ ( 𝜑 → ( ( abs ‘ ( 2 · 𝑁 ) ) ↑ - 𝐽 ) = ( ( 2 · 𝑁 ) ↑ - 𝐽 ) )
103 91 102 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) = ( ( 2 · 𝑁 ) ↑ - 𝐽 ) )
104 103 97 oveq12d ⊢ ( 𝜑 → ( ( abs ‘ ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) / ( abs ‘ 2 ) ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )
105 87 104 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )
106 85 105 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐴 ) ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )
107 36 recnd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ∈ ℂ )
108 52 simpld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ≠ 1 )
109 107 108 6 geoser ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) = ( ( 1 − ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) ) / ( 1 − ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ) ) )
110 107 6 expcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) ∈ ℂ )
111 108 necomd ⊢ ( 𝜑 → 1 ≠ ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) )
112 79 110 79 107 111 div2subd ⊢ ( 𝜑 → ( ( 1 − ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) ) / ( 1 − ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ) ) = ( ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) − 1 ) / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )
113 109 112 eqtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) = ( ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) − 1 ) / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )
114 106 113 oveq12d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) − 1 ) / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) )
115 113 41 eqeltrrd ⊢ ( 𝜑 → ( ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) − 1 ) / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ∈ ℝ )
116 36 6 reexpcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) ∈ ℝ )
117 116 48 57 redivcld ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ∈ ℝ )
118 2rp ⊢ 2 ∈ ℝ+
119 118 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
120 119 rpgt0d ⊢ ( 𝜑 → 0 < 2 )
121 30 32 120 66 mulgt0d ⊢ ( 𝜑 → 0 < ( 2 · 𝑁 ) )
122 33 71 121 3jca ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ∈ ℝ ∧ - 𝐽 ∈ ℤ ∧ 0 < ( 2 · 𝑁 ) ) )
123 expgt0 ⊢ ( ( ( 2 · 𝑁 ) ∈ ℝ ∧ - 𝐽 ∈ ℤ ∧ 0 < ( 2 · 𝑁 ) ) → 0 < ( ( 2 · 𝑁 ) ↑ - 𝐽 ) )
124 122 123 syl ⊢ ( 𝜑 → 0 < ( ( 2 · 𝑁 ) ↑ - 𝐽 ) )
125 49 72 124 ltled ⊢ ( 𝜑 → 0 ≤ ( ( 2 · 𝑁 ) ↑ - 𝐽 ) )
126 72 119 125 divge0d ⊢ ( 𝜑 → 0 ≤ ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )
127 116 47 resubcld ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) − 1 ) ∈ ℝ )
128 48 54 elrpd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ∈ ℝ+ )
129 116 lem1d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) − 1 ) ≤ ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) )
130 127 116 128 129 lediv1dd ⊢ ( 𝜑 → ( ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) − 1 ) / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )
131 115 117 73 126 130 lemul2ad ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) − 1 ) / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) )
132 48 recnd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ∈ ℂ )
133 110 132 57 divrecd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) = ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) )
134 133 oveq2d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
135 58 recnd ⊢ ( 𝜑 → ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ∈ ℂ )
136 74 110 135 mulassd ⊢ ( 𝜑 → ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
137 136 eqcomd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) = ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) )
138 86 110 62 45 div23d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) ) / 2 ) = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) ) )
139 138 eqcomd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) ) = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) ) / 2 ) )
140 88 70 jca ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( 2 · 𝑁 ) ≠ 0 ) )
141 35 recnd ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℂ )
142 5 8 9 knoppndvlem13 ⊢ ( 𝜑 → 𝐶 ≠ 0 )
143 34 142 absne0d ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ≠ 0 )
144 141 143 jca ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) ∈ ℂ ∧ ( abs ‘ 𝐶 ) ≠ 0 ) )
145 140 144 11 3jca ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( 2 · 𝑁 ) ≠ 0 ) ∧ ( ( abs ‘ 𝐶 ) ∈ ℂ ∧ ( abs ‘ 𝐶 ) ≠ 0 ) ∧ 𝐽 ∈ ℤ ) )
146 mulexpz ⊢ ( ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( 2 · 𝑁 ) ≠ 0 ) ∧ ( ( abs ‘ 𝐶 ) ∈ ℂ ∧ ( abs ‘ 𝐶 ) ≠ 0 ) ∧ 𝐽 ∈ ℤ ) → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) = ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ) )
147 145 146 syl ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) = ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ) )
148 147 oveq2d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) · ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ) ) )
149 88 6 expcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 𝐽 ) ∈ ℂ )
150 43 recnd ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ∈ ℂ )
151 86 149 150 mulassd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) · ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) · ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) · ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ) ) )
152 151 eqcomd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) · ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ) ) = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) · ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) · ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ) )
153 140 71 11 jca32 ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( 2 · 𝑁 ) ≠ 0 ) ∧ ( - 𝐽 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ) )
154 expaddz ⊢ ( ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( 2 · 𝑁 ) ≠ 0 ) ∧ ( - 𝐽 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ) → ( ( 2 · 𝑁 ) ↑ ( - 𝐽 + 𝐽 ) ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) · ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) )
155 153 154 syl ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ ( - 𝐽 + 𝐽 ) ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) · ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) )
156 155 eqcomd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) · ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) = ( ( 2 · 𝑁 ) ↑ ( - 𝐽 + 𝐽 ) ) )
157 71 zcnd ⊢ ( 𝜑 → - 𝐽 ∈ ℂ )
158 6 nn0cnd ⊢ ( 𝜑 → 𝐽 ∈ ℂ )
159 157 158 addcomd ⊢ ( 𝜑 → ( - 𝐽 + 𝐽 ) = ( 𝐽 + - 𝐽 ) )
160 158 negidd ⊢ ( 𝜑 → ( 𝐽 + - 𝐽 ) = 0 )
161 159 160 eqtrd ⊢ ( 𝜑 → ( - 𝐽 + 𝐽 ) = 0 )
162 161 oveq2d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ ( - 𝐽 + 𝐽 ) ) = ( ( 2 · 𝑁 ) ↑ 0 ) )
163 88 exp0d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 0 ) = 1 )
164 156 162 163 3eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) · ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) = 1 )
165 164 oveq1d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) · ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) · ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ) = ( 1 · ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ) )
166 150 mulid2d ⊢ ( 𝜑 → ( 1 · ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ) = ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) )
167 165 166 eqtrd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) · ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) · ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ) = ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) )
168 148 152 167 3eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) ) = ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) )
169 168 oveq1d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) ) / 2 ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) )
170 139 169 eqtrd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) )
171 170 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) = ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) )
172 134 137 171 3eqtrd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) = ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) )
173 131 172 breqtrd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) − 1 ) / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ≤ ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) )
174 114 173 eqbrtrd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) · Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑖 ) ) ≤ ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) )
175 24 42 59 60 174 letrd ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ≤ ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) )