Metamath Proof Explorer

Theorem knoppndvlem15

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

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

Proof

Step Hyp Ref Expression
1 knoppndvlem15.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 knoppndvlem15.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3 knoppndvlem15.w ⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
4 knoppndvlem15.a ⊢ 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 )
5 knoppndvlem15.b ⊢ 𝐵 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) )
6 knoppndvlem15.c ⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
7 knoppndvlem15.j ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
8 knoppndvlem15.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
9 knoppndvlem15.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
10 knoppndvlem15.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 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
22 9 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
23 17 22 remulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
24 23 14 remulcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ∈ ℝ )
25 24 21 resubcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ∈ ℝ )
26 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
27 0lt1 ⊢ 0 < 1
28 27 a1i ⊢ ( 𝜑 → 0 < 1 )
29 6 9 10 knoppndvlem12 ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ≠ 1 ∧ 1 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )
30 29 simprd ⊢ ( 𝜑 → 1 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) )
31 26 21 25 28 30 lttrd ⊢ ( 𝜑 → 0 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) )
32 25 31 jca ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ∈ ℝ ∧ 0 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )
33 gt0ne0 ⊢ ( ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ∈ ℝ ∧ 0 < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ≠ 0 )
34 32 33 syl ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ≠ 0 )
35 21 25 34 redivcld ⊢ ( 𝜑 → ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ∈ ℝ )
36 21 35 resubcld ⊢ ( 𝜑 → ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ )
37 20 36 remulcld ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ∈ ℝ )
38 4 a1i ⊢ ( 𝜑 → 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) )
39 7 nn0zd ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
40 9 39 8 knoppndvlem1 ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ∈ ℝ )
41 38 40 eqeltrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
42 1 2 9 12 41 7 knoppcnlem3 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ∈ ℝ )
43 42 recnd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ∈ ℂ )
44 5 a1i ⊢ ( 𝜑 → 𝐵 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) )
45 8 peano2zd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℤ )
46 9 39 45 knoppndvlem1 ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) ∈ ℝ )
47 44 46 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
48 1 2 9 12 47 7 knoppcnlem3 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ∈ ℝ )
49 48 recnd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ∈ ℂ )
50 43 49 subcld ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ∈ ℂ )
51 50 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) ∈ ℝ )
52 1 2 47 12 9 knoppndvlem5 ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) ∈ ℝ )
53 52 recnd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) ∈ ℂ )
54 1 2 41 12 9 knoppndvlem5 ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℝ )
55 54 recnd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℂ )
56 53 55 subcld ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ∈ ℂ )
57 56 abscld ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ∈ ℝ )
58 51 57 resubcld ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) − ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ) ∈ ℝ )
59 50 56 subcld ⊢ ( 𝜑 → ( ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) − ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ∈ ℂ )
60 59 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) − ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ) ∈ ℝ )
61 20 35 jca ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ∈ ℝ ∧ ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ∈ ℝ ) )
62 remulcl ⊢ ( ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ∈ ℝ ∧ ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ∈ ℝ ) → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ )
63 61 62 syl ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ )
64 20 63 jca ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ∈ ℝ ∧ ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ ) )
65 resubcl ⊢ ( ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ∈ ℝ ∧ ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ ) → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ∈ ℝ )
66 64 65 syl ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ∈ ℝ )
67 20 recnd ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ∈ ℂ )
68 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
69 35 recnd ⊢ ( 𝜑 → ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ∈ ℂ )
70 67 68 69 subdid ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) = ( ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · 1 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
71 67 mulid1d ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · 1 ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) )
72 71 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · 1 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) = ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
73 66 leidd ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
74 72 73 eqbrtrd ⊢ ( 𝜑 → ( ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · 1 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
75 70 74 eqbrtrd ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
76 20 35 remulcld ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ )
77 20 leidd ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ≤ ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) )
78 43 49 abssubd ⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ) ) )
79 1 2 4 5 6 7 8 9 knoppndvlem10 ⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ) ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) )
80 78 79 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) )
81 80 eqcomd ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) )
82 77 81 breqtrd ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) ≤ ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) )
83 1 2 4 5 6 7 8 9 10 knoppndvlem14 ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ≤ ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) )
84 20 57 51 76 82 83 le2subd ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) − ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) − ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ) )
85 37 66 58 75 84 letrd ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) − ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ) )
86 50 56 abs2difd ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) − ( abs ‘ ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ) ≤ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) − ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ) )
87 37 58 60 85 86 letrd ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( abs ‘ ( ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) − ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ) )
88 50 56 abssubd ⊢ ( 𝜑 → ( abs ‘ ( ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) − ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) ) ) = ( abs ‘ ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) − ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) ) )
89 87 88 breqtrd ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( abs ‘ ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) − ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) ) )
90 1 2 3 5 6 7 45 9 knoppndvlem6 ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐵 ) = Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) )
91 elnn0uz ⊢ ( 𝐽 ∈ ℕ0 ↔ 𝐽 ∈ ( ℤ≥ ‘ 0 ) )
92 7 91 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( ℤ≥ ‘ 0 ) )
93 9 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → 𝑁 ∈ ℕ )
94 12 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → 𝐶 ∈ ℝ )
95 47 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → 𝐵 ∈ ℝ )
96 elfznn0 ⊢ ( 𝑖 ∈ ( 0 ... 𝐽 ) → 𝑖 ∈ ℕ0 )
97 96 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → 𝑖 ∈ ℕ0 )
98 1 2 93 94 95 97 knoppcnlem3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) ∈ ℝ )
99 98 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) ∈ ℂ )
100 fveq2 ⊢ ( 𝑖 = 𝐽 → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) )
101 92 99 100 fsumm1 ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) = ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) )
102 90 101 eqtrd ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐵 ) = ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) )
103 1 2 3 4 6 7 8 9 knoppndvlem6 ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐴 ) = Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) )
104 41 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → 𝐴 ∈ ℝ )
105 1 2 93 94 104 97 knoppcnlem3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℝ )
106 105 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℂ )
107 fveq2 ⊢ ( 𝑖 = 𝐽 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) )
108 92 106 107 fsumm1 ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) = ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ) )
109 103 108 eqtrd ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐴 ) = ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ) )
110 102 109 oveq12d ⊢ ( 𝜑 → ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) = ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) − ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ) ) )
111 53 55 43 49 subadd4d ⊢ ( 𝜑 → ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) − ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) = ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) − ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ) ) )
112 111 eqcomd ⊢ ( 𝜑 → ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) − ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) ) ) = ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) − ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) )
113 110 112 eqtrd ⊢ ( 𝜑 → ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) = ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) − ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) )
114 113 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) ) = ( abs ‘ ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) − ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) ) )
115 114 eqcomd ⊢ ( 𝜑 → ( abs ‘ ( ( Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑖 ) − Σ 𝑖 ∈ ( 0 ... ( 𝐽 − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) − ( ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) − ( ( 𝐹 ‘ 𝐵 ) ‘ 𝐽 ) ) ) ) = ( abs ‘ ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) ) )
116 89 115 breqtrd ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐶 ) ↑ 𝐽 ) / 2 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( abs ‘ ( ( 𝑊 ‘ 𝐵 ) − ( 𝑊 ‘ 𝐴 ) ) ) )