Metamath Proof Explorer

Theorem knoppndvlem17

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

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

Proof

Step Hyp Ref Expression
1 knoppndvlem17.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 knoppndvlem17.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3 knoppndvlem17.w ⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
4 knoppndvlem17.a ⊢ 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 )
5 knoppndvlem17.b ⊢ 𝐵 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) )
6 knoppndvlem17.c ⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
7 knoppndvlem17.j ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
8 knoppndvlem17.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
9 knoppndvlem17.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
10 knoppndvlem17.1 ⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
11 6 knoppndvlem3 ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( abs ‘ 𝐶 ) < 1 ) )
12 11 simpld ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
13 12 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
14 13 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℝ )
15 14 7 reexpcld ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ∈ ℝ )
16 2re ⊢ 2 ∈ ℝ
17 16 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
18 2ne0 ⊢ 2 ≠ 0
19 18 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
20 15 17 19 redivcld ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ∈ ℝ )
21 20 recnd ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ∈ ℂ )
22 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
23 9 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
24 17 23 remulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
25 24 14 remulcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ∈ ℝ )
26 25 22 resubcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ∈ ℝ )
27 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
28 0lt1 ⊢ 0 < 1
29 28 a1i ⊢ ( 𝜑 → 0 < 1 )
30 6 9 10 knoppndvlem12 ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ≠ 1 ∧ 1 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )
31 30 simprd ⊢ ( 𝜑 → 1 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) )
32 27 22 26 29 31 lttrd ⊢ ( 𝜑 → 0 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) )
33 26 32 jca ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ∈ ℝ ∧ 0 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )
34 gt0ne0 ⊢ ( ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ∈ ℝ ∧ 0 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ≠ 0 )
35 33 34 syl ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ≠ 0 )
36 22 26 35 redivcld ⊢ ( 𝜑 → ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ∈ ℝ )
37 22 36 resubcld ⊢ ( 𝜑 → ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ )
38 37 recnd ⊢ ( 𝜑 → ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℂ )
39 21 38 mulcomd ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) = ( ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) · ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ) )
40 39 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) = ( ( ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) · ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) )
41 2rp ⊢ 2 ∈ ℝ+
42 41 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
43 9 nnrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
44 42 43 rpmulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ+ )
45 7 nn0zd ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
46 45 znegcld ⊢ ( 𝜑 → - 𝐽 ∈ ℤ )
47 44 46 rpexpcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ∈ ℝ+ )
48 47 rphalfcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ∈ ℝ+ )
49 48 rpcnd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ∈ ℂ )
50 48 rpne0d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ≠ 0 )
51 38 21 49 50 divassd ⊢ ( 𝜑 → ( ( ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) · ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) = ( ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) · ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) )
52 21 49 50 divcld ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ∈ ℂ )
53 38 52 mulcomd ⊢ ( 𝜑 → ( ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) · ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) = ( ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
54 15 recnd ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ∈ ℂ )
55 47 rpcnd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ∈ ℂ )
56 17 recnd ⊢ ( 𝜑 → 2 ∈ ℂ )
57 47 rpne0d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ≠ 0 )
58 54 55 56 57 19 divcan7d ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) )
59 24 recnd ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
60 44 rpne0d ⊢ ( 𝜑 → ( 2 · 𝑁 ) ≠ 0 )
61 59 60 45 expnegd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ - 𝐽 ) = ( 1 / ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) )
62 61 oveq2d ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / ( 1 / ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) ) )
63 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
64 59 7 expcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 𝐽 ) ∈ ℂ )
65 27 29 gtned ⊢ ( 𝜑 → 1 ≠ 0 )
66 59 60 45 expne0d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 𝐽 ) ≠ 0 )
67 54 63 64 65 66 divdiv2d ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / ( 1 / ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) ) = ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) · ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) / 1 ) )
68 54 64 mulcld ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) · ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) ∈ ℂ )
69 68 div1d ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) · ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) / 1 ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) · ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) )
70 54 64 mulcomd ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) · ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) = ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ) )
71 59 60 jca ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( 2 · 𝑁 ) ≠ 0 ) )
72 14 recnd ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℂ )
73 6 9 10 knoppndvlem13 ⊢ ( 𝜑 → 𝐶 ≠ 0 )
74 13 73 absne0d ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ≠ 0 )
75 72 74 jca ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) ∈ ℂ ∧ ( abs ‘ 𝐶 ) ≠ 0 ) )
76 71 75 45 3jca ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( 2 · 𝑁 ) ≠ 0 ) ∧ ( ( abs ‘ 𝐶 ) ∈ ℂ ∧ ( abs ‘ 𝐶 ) ≠ 0 ) ∧ 𝐽 ∈ ℤ ) )
77 mulexpz ⊢ ( ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( 2 · 𝑁 ) ≠ 0 ) ∧ ( ( abs ‘ 𝐶 ) ∈ ℂ ∧ ( abs ‘ 𝐶 ) ≠ 0 ) ∧ 𝐽 ∈ ℤ ) → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) = ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ) )
78 76 77 syl ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) = ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ) )
79 78 eqcomd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) ) = ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) )
80 69 70 79 3eqtrd ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) · ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) / 1 ) = ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) )
81 62 67 80 3eqtrd ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) = ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) )
82 58 81 eqtrd ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) = ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) )
83 82 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) = ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
84 53 83 eqtrd ⊢ ( 𝜑 → ( ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) · ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) = ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
85 40 51 84 3eqtrd ⊢ ( 𝜑 → ( ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) = ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
86 85 eqcomd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) = ( ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) )
87 20 37 remulcld ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ∈ ℝ )
88 5 a1i ⊢ ( 𝜑 → 𝐵 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) )
89 8 peano2zd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℤ )
90 9 45 89 knoppndvlem1 ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) ∈ ℝ )
91 88 90 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
92 11 simprd ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) < 1 )
93 1 2 3 91 9 12 92 knoppcld ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐵 ) ∈ ℂ )
94 4 a1i ⊢ ( 𝜑 → 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) )
95 9 45 8 knoppndvlem1 ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ∈ ℝ )
96 94 95 eqeltrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
97 1 2 3 96 9 12 92 knoppcld ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐴 ) ∈ ℂ )
98 93 97 subcld ⊢ ( 𝜑 → ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) ∈ ℂ )
99 98 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) ) ∈ ℝ )
100 1 2 3 4 5 6 7 8 9 10 knoppndvlem15 ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( abs ‘ ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) ) )
101 87 99 48 100 lediv1dd ⊢ ( 𝜑 → ( ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) )
102 86 101 eqbrtrd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) )
103 4 5 7 8 9 knoppndvlem16 ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )
104 103 eqcomd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) = ( 𝐵 − 𝐴 ) )
105 104 oveq2d ⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) ) / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) = ( ( abs ‘ ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) ) / ( 𝐵 − 𝐴 ) ) )
106 102 105 breqtrd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) ) / ( 𝐵 − 𝐴 ) ) )