Metamath Proof Explorer

Theorem knoppndvlem21

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

Ref Expression
Hypotheses knoppndvlem21.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
knoppndvlem21.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
knoppndvlem21.w ⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
knoppndvlem21.g ⊢ 𝐺 = ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )
knoppndvlem21.c ⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
knoppndvlem21.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
knoppndvlem21.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
knoppndvlem21.h ⊢ ( 𝜑 → 𝐻 ∈ ℝ )
knoppndvlem21.j ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
knoppndvlem21.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
knoppndvlem21.1 ⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
knoppndvlem21.2 ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) < 𝐷 )
knoppndvlem21.3 ⊢ ( 𝜑 → 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · 𝐺 ) )
Assertion knoppndvlem21 ( 𝜑 → ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ( ( 𝑎 ≤ 𝐻 ∧ 𝐻 ≤ 𝑏 ) ∧ ( ( 𝑏 − 𝑎 ) < 𝐷 ∧ 𝑎 ≠ 𝑏 ) ∧ 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ 𝑎 ) ) ) / ( 𝑏 − 𝑎 ) ) ) )

Proof

Step Hyp Ref Expression
1 knoppndvlem21.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 knoppndvlem21.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3 knoppndvlem21.w ⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
4 knoppndvlem21.g ⊢ 𝐺 = ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )
5 knoppndvlem21.c ⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
6 knoppndvlem21.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
7 knoppndvlem21.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
8 knoppndvlem21.h ⊢ ( 𝜑 → 𝐻 ∈ ℝ )
9 knoppndvlem21.j ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
10 knoppndvlem21.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
11 knoppndvlem21.1 ⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
12 knoppndvlem21.2 ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) < 𝐷 )
13 knoppndvlem21.3 ⊢ ( 𝜑 → 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · 𝐺 ) )
14 eqid ⊢ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 )
15 eqid ⊢ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) )
16 14 15 9 8 10 knoppndvlem19 ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℤ ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) )
17 2re ⊢ 2 ∈ ℝ
18 17 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
19 10 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
20 18 19 remulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
21 2pos ⊢ 0 < 2
22 21 a1i ⊢ ( 𝜑 → 0 < 2 )
23 10 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
24 18 19 22 23 mulgt0d ⊢ ( 𝜑 → 0 < ( 2 · 𝑁 ) )
25 24 gt0ne0d ⊢ ( 𝜑 → ( 2 · 𝑁 ) ≠ 0 )
26 9 nn0zd ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
27 26 znegcld ⊢ ( 𝜑 → - 𝐽 ∈ ℤ )
28 20 25 27 reexpclzd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ∈ ℝ )
29 28 rehalfcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ∈ ℝ )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ∈ ℝ )
31 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℤ )
32 31 zred ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℝ )
33 30 32 remulcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ∈ ℝ )
34 33 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ) ) → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ∈ ℝ )
35 peano2re ⊢ ( 𝑚 ∈ ℝ → ( 𝑚 + 1 ) ∈ ℝ )
36 32 35 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( 𝑚 + 1 ) ∈ ℝ )
37 30 36 jca ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ∈ ℝ ∧ ( 𝑚 + 1 ) ∈ ℝ ) )
38 remulcl ⊢ ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ∈ ℝ ∧ ( 𝑚 + 1 ) ∈ ℝ ) → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ∈ ℝ )
39 37 38 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ∈ ℝ )
40 39 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ) ) → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ∈ ℝ )
41 simprr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ) ) → ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) )
42 9 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 𝐽 ∈ ℕ0 )
43 10 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 𝑁 ∈ ℕ )
44 14 15 42 31 43 knoppndvlem16 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )
45 12 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) < 𝐷 )
46 44 45 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) < 𝐷 )
47 20 27 24 3jca ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ∈ ℝ ∧ - 𝐽 ∈ ℤ ∧ 0 < ( 2 · 𝑁 ) ) )
48 expgt0 ⊢ ( ( ( 2 · 𝑁 ) ∈ ℝ ∧ - 𝐽 ∈ ℤ ∧ 0 < ( 2 · 𝑁 ) ) → 0 < ( ( 2 · 𝑁 ) ↑ - 𝐽 ) )
49 47 48 syl ⊢ ( 𝜑 → 0 < ( ( 2 · 𝑁 ) ↑ - 𝐽 ) )
50 28 18 49 22 divgt0d ⊢ ( 𝜑 → 0 < ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 0 < ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )
52 44 eqcomd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) = ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) )
53 51 52 breqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 0 < ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) )
54 33 39 posdifd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) < ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ↔ 0 < ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) )
55 53 54 mpbird ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) < ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) )
56 33 55 ltned ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≠ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) )
57 46 56 jca ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) < 𝐷 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≠ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) )
58 57 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ) ) → ( ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) < 𝐷 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≠ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) )
59 7 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
60 59 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 𝐸 ∈ ℝ )
61 5 knoppndvlem3 ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( abs ‘ 𝐶 ) < 1 ) )
62 61 simpld ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
63 62 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
64 63 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℝ )
65 20 64 remulcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ∈ ℝ )
66 65 9 reexpcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) ∈ ℝ )
67 4 a1i ⊢ ( 𝜑 → 𝐺 = ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) )
68 5 10 11 knoppndvlem20 ⊢ ( 𝜑 → ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ+ )
69 68 rpred ⊢ ( 𝜑 → ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ )
70 67 69 eqeltrd ⊢ ( 𝜑 → 𝐺 ∈ ℝ )
71 66 70 remulcld ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · 𝐺 ) ∈ ℝ )
72 71 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · 𝐺 ) ∈ ℝ )
73 62 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 𝐶 ∈ ℝ )
74 61 simprd ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) < 1 )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( abs ‘ 𝐶 ) < 1 )
76 1 2 3 39 43 73 75 knoppcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ∈ ℂ )
77 1 2 3 33 43 73 75 knoppcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ∈ ℂ )
78 76 77 subcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ∈ ℂ )
79 78 abscld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( abs ‘ ( ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) ∈ ℝ )
80 44 30 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ∈ ℝ )
81 53 gt0ne0d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ≠ 0 )
82 79 80 81 redivcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( abs ‘ ( ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ∈ ℝ )
83 13 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · 𝐺 ) )
84 4 oveq2i ⊢ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · 𝐺 ) = ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) )
85 84 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · 𝐺 ) = ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
86 5 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 𝐶 ∈ ( - 1 (,) 1 ) )
87 11 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
88 1 2 3 14 15 86 42 31 43 87 knoppndvlem17 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ≤ ( ( abs ‘ ( ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) )
89 85 88 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝐽 ) · 𝐺 ) ≤ ( ( abs ‘ ( ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) )
90 60 72 82 83 89 letrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) )
91 90 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ) ) → 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) )
92 41 58 91 3jca ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ) ) → ( ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ∧ ( ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) < 𝐷 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≠ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ∧ 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) )
93 34 40 92 3jca ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ) ) → ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ∈ ℝ ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ∈ ℝ ∧ ( ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ∧ ( ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) < 𝐷 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≠ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ∧ 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) ) )
94 breq1 ⊢ ( 𝑎 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) → ( 𝑎 ≤ 𝐻 ↔ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ) )
95 94 anbi1d ⊢ ( 𝑎 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) → ( ( 𝑎 ≤ 𝐻 ∧ 𝐻 ≤ 𝑏 ) ↔ ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ 𝑏 ) ) )
96 oveq2 ⊢ ( 𝑎 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) → ( 𝑏 − 𝑎 ) = ( 𝑏 − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) )
97 96 breq1d ⊢ ( 𝑎 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) → ( ( 𝑏 − 𝑎 ) < 𝐷 ↔ ( 𝑏 − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) < 𝐷 ) )
98 neeq1 ⊢ ( 𝑎 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) → ( 𝑎 ≠ 𝑏 ↔ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≠ 𝑏 ) )
99 97 98 anbi12d ⊢ ( 𝑎 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) → ( ( ( 𝑏 − 𝑎 ) < 𝐷 ∧ 𝑎 ≠ 𝑏 ) ↔ ( ( 𝑏 − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) < 𝐷 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≠ 𝑏 ) ) )
100 fveq2 ⊢ ( 𝑎 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) → ( 𝑊 ‘ 𝑎 ) = ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) )
101 100 oveq2d ⊢ ( 𝑎 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) → ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ 𝑎 ) ) = ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) )
102 101 fveq2d ⊢ ( 𝑎 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) → ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ 𝑎 ) ) ) = ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) )
103 102 96 oveq12d ⊢ ( 𝑎 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) → ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ 𝑎 ) ) ) / ( 𝑏 − 𝑎 ) ) = ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( 𝑏 − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) )
104 103 breq2d ⊢ ( 𝑎 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) → ( 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ 𝑎 ) ) ) / ( 𝑏 − 𝑎 ) ) ↔ 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( 𝑏 − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) )
105 95 99 104 3anbi123d ⊢ ( 𝑎 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) → ( ( ( 𝑎 ≤ 𝐻 ∧ 𝐻 ≤ 𝑏 ) ∧ ( ( 𝑏 − 𝑎 ) < 𝐷 ∧ 𝑎 ≠ 𝑏 ) ∧ 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ 𝑎 ) ) ) / ( 𝑏 − 𝑎 ) ) ) ↔ ( ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ 𝑏 ) ∧ ( ( 𝑏 − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) < 𝐷 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≠ 𝑏 ) ∧ 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( 𝑏 − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) ) )
106 breq2 ⊢ ( 𝑏 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) → ( 𝐻 ≤ 𝑏 ↔ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) )
107 106 anbi2d ⊢ ( 𝑏 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) → ( ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ 𝑏 ) ↔ ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ) )
108 oveq1 ⊢ ( 𝑏 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) → ( 𝑏 − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) = ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) )
109 108 breq1d ⊢ ( 𝑏 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) → ( ( 𝑏 − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) < 𝐷 ↔ ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) < 𝐷 ) )
110 neeq2 ⊢ ( 𝑏 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) → ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≠ 𝑏 ↔ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≠ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) )
111 109 110 anbi12d ⊢ ( 𝑏 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) → ( ( ( 𝑏 − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) < 𝐷 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≠ 𝑏 ) ↔ ( ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) < 𝐷 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≠ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ) )
112 fveq2 ⊢ ( 𝑏 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) → ( 𝑊 ‘ 𝑏 ) = ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) )
113 112 fvoveq1d ⊢ ( 𝑏 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) → ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) = ( abs ‘ ( ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) )
114 113 108 oveq12d ⊢ ( 𝑏 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) → ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( 𝑏 − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) = ( ( abs ‘ ( ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) )
115 114 breq2d ⊢ ( 𝑏 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) → ( 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( 𝑏 − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ↔ 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) )
116 107 111 115 3anbi123d ⊢ ( 𝑏 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) → ( ( ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ 𝑏 ) ∧ ( ( 𝑏 − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) < 𝐷 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≠ 𝑏 ) ∧ 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( 𝑏 − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) ↔ ( ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ∧ ( ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) < 𝐷 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≠ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ∧ 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) ) )
117 105 116 rspc2ev ⊢ ( ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ∈ ℝ ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ∈ ℝ ∧ ( ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ∧ ( ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) < 𝐷 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≠ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ∧ 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) − ( 𝑊 ‘ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) / ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ) ) ) ) → ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ( ( 𝑎 ≤ 𝐻 ∧ 𝐻 ≤ 𝑏 ) ∧ ( ( 𝑏 − 𝑎 ) < 𝐷 ∧ 𝑎 ≠ 𝑏 ) ∧ 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ 𝑎 ) ) ) / ( 𝑏 − 𝑎 ) ) ) )
118 93 117 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) ) ) ) → ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ( ( 𝑎 ≤ 𝐻 ∧ 𝐻 ≤ 𝑏 ) ∧ ( ( 𝑏 − 𝑎 ) < 𝐷 ∧ 𝑎 ≠ 𝑏 ) ∧ 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ 𝑎 ) ) ) / ( 𝑏 − 𝑎 ) ) ) )
119 16 118 rexlimddv ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ( ( 𝑎 ≤ 𝐻 ∧ 𝐻 ≤ 𝑏 ) ∧ ( ( 𝑏 − 𝑎 ) < 𝐷 ∧ 𝑎 ≠ 𝑏 ) ∧ 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ 𝑎 ) ) ) / ( 𝑏 − 𝑎 ) ) ) )