Metamath Proof Explorer

Theorem knoppndvlem19

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

Ref Expression
Hypotheses knoppndvlem19.a ⊢ 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 )
knoppndvlem19.b ⊢ 𝐵 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) )
knoppndvlem19.j ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
knoppndvlem19.h ⊢ ( 𝜑 → 𝐻 ∈ ℝ )
knoppndvlem19.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion knoppndvlem19 ( 𝜑 → ∃ 𝑚 ∈ ℤ ( 𝐴 ≤ 𝐻 ∧ 𝐻 ≤ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 knoppndvlem19.a ⊢ 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 )
2 knoppndvlem19.b ⊢ 𝐵 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) )
3 knoppndvlem19.j ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
4 knoppndvlem19.h ⊢ ( 𝜑 → 𝐻 ∈ ℝ )
5 knoppndvlem19.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6 2re ⊢ 2 ∈ ℝ
7 6 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
8 5 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
9 7 8 remulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
10 2pos ⊢ 0 < 2
11 10 a1i ⊢ ( 𝜑 → 0 < 2 )
12 5 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
13 7 8 11 12 mulgt0d ⊢ ( 𝜑 → 0 < ( 2 · 𝑁 ) )
14 13 gt0ne0d ⊢ ( 𝜑 → ( 2 · 𝑁 ) ≠ 0 )
15 3 nn0zd ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
16 15 znegcld ⊢ ( 𝜑 → - 𝐽 ∈ ℤ )
17 9 14 16 reexpclzd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ∈ ℝ )
18 7 recnd ⊢ ( 𝜑 → 2 ∈ ℂ )
19 8 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
20 18 19 14 mulne0bad ⊢ ( 𝜑 → 2 ≠ 0 )
21 17 7 20 redivcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ∈ ℝ )
22 9 16 13 3jca ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ∈ ℝ ∧ - 𝐽 ∈ ℤ ∧ 0 < ( 2 · 𝑁 ) ) )
23 expgt0 ⊢ ( ( ( 2 · 𝑁 ) ∈ ℝ ∧ - 𝐽 ∈ ℤ ∧ 0 < ( 2 · 𝑁 ) ) → 0 < ( ( 2 · 𝑁 ) ↑ - 𝐽 ) )
24 22 23 syl ⊢ ( 𝜑 → 0 < ( ( 2 · 𝑁 ) ↑ - 𝐽 ) )
25 17 7 24 11 divgt0d ⊢ ( 𝜑 → 0 < ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )
26 25 gt0ne0d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ≠ 0 )
27 4 21 26 redivcld ⊢ ( 𝜑 → ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ∈ ℝ )
28 27 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) ∈ ℤ )
29 1 a1i ⊢ ( 𝑚 = ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) → 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) )
30 id ⊢ ( 𝑚 = ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) → 𝑚 = ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) )
31 30 oveq2d ⊢ ( 𝑚 = ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑚 ) = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) ) )
32 29 31 eqtrd ⊢ ( 𝑚 = ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) → 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) ) )
33 32 breq1d ⊢ ( 𝑚 = ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) → ( 𝐴 ≤ 𝐻 ↔ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) ) ≤ 𝐻 ) )
34 2 a1i ⊢ ( 𝑚 = ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) → 𝐵 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) )
35 30 oveq1d ⊢ ( 𝑚 = ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) → ( 𝑚 + 1 ) = ( ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) + 1 ) )
36 35 oveq2d ⊢ ( 𝑚 = ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑚 + 1 ) ) = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) + 1 ) ) )
37 34 36 eqtrd ⊢ ( 𝑚 = ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) → 𝐵 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) + 1 ) ) )
38 37 breq2d ⊢ ( 𝑚 = ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) → ( 𝐻 ≤ 𝐵 ↔ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) + 1 ) ) ) )
39 33 38 anbi12d ⊢ ( 𝑚 = ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) → ( ( 𝐴 ≤ 𝐻 ∧ 𝐻 ≤ 𝐵 ) ↔ ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) + 1 ) ) ) ) )
40 39 adantl ⊢ ( ( 𝜑 ∧ 𝑚 = ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) ) → ( ( 𝐴 ≤ 𝐻 ∧ 𝐻 ≤ 𝐵 ) ↔ ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) + 1 ) ) ) ) )
41 28 zred ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) ∈ ℝ )
42 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
43 42 21 25 ltled ⊢ ( 𝜑 → 0 ≤ ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )
44 flle ⊢ ( ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) ≤ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) )
45 27 44 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) ≤ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) )
46 41 27 21 43 45 lemul2ad ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) ) ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) )
47 4 recnd ⊢ ( 𝜑 → 𝐻 ∈ ℂ )
48 21 recnd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ∈ ℂ )
49 47 48 26 divcan2d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) = 𝐻 )
50 46 49 breqtrd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) ) ≤ 𝐻 )
51 49 eqcomd ⊢ ( 𝜑 → 𝐻 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) )
52 peano2re ⊢ ( ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) ∈ ℝ → ( ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) + 1 ) ∈ ℝ )
53 41 52 syl ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) + 1 ) ∈ ℝ )
54 fllep1 ⊢ ( ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ∈ ℝ → ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ≤ ( ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) + 1 ) )
55 27 54 syl ⊢ ( 𝜑 → ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ≤ ( ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) + 1 ) )
56 27 53 21 43 55 lemul2ad ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) + 1 ) ) )
57 51 56 eqbrtrd ⊢ ( 𝜑 → 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) + 1 ) ) )
58 50 57 jca ⊢ ( 𝜑 → ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) ) ≤ 𝐻 ∧ 𝐻 ≤ ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( ⌊ ‘ ( 𝐻 / ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) ) + 1 ) ) ) )
59 28 40 58 rspcedvd ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℤ ( 𝐴 ≤ 𝐻 ∧ 𝐻 ≤ 𝐵 ) )