Metamath Proof Explorer

Theorem knoppndvlem21

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

Ref Expression
Hypotheses knoppndvlem21.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
knoppndvlem21.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
knoppndvlem21.w ⊢ W = w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i
knoppndvlem21.g ⊢ G = 1 − 1 2 ⋅ N ⁢ C − 1
knoppndvlem21.c ⊢ φ → C ∈ − 1 1
knoppndvlem21.d ⊢ φ → D ∈ ℝ +
knoppndvlem21.e ⊢ φ → E ∈ ℝ +
knoppndvlem21.h ⊢ φ → H ∈ ℝ
knoppndvlem21.j ⊢ φ → J ∈ ℕ 0
knoppndvlem21.n ⊢ φ → N ∈ ℕ
knoppndvlem21.1 ⊢ φ → 1 < N ⁢ C
knoppndvlem21.2 ⊢ φ → 2 ⋅ N − J 2 < D
knoppndvlem21.3 ⊢ φ → E ≤ 2 ⋅ N ⁢ C J ⁢ G
Assertion knoppndvlem21 ⊢ φ → ∃ a ∈ ℝ ∃ b ∈ ℝ a ≤ H ∧ H ≤ b ∧ b − a < D ∧ a ≠ b ∧ E ≤ W ⁡ b − W ⁡ a b − a

Proof

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