Proof of Theorem knoppndvlem19
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | knoppndvlem19.h | . . . 4
⊢ (𝜑 → 𝐻 ∈ ℝ) | 
| 2 |  | 2re 12341 | . . . . . . . 8
⊢ 2 ∈
ℝ | 
| 3 | 2 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 2 ∈
ℝ) | 
| 4 |  | knoppndvlem19.n | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 5 | 4 | nnred 12282 | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 6 | 3, 5 | remulcld 11292 | . . . . . 6
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) | 
| 7 |  | 2pos 12370 | . . . . . . . . 9
⊢ 0 <
2 | 
| 8 | 7 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 0 < 2) | 
| 9 | 4 | nngt0d 12316 | . . . . . . . 8
⊢ (𝜑 → 0 < 𝑁) | 
| 10 | 3, 5, 8, 9 | mulgt0d 11417 | . . . . . . 7
⊢ (𝜑 → 0 < (2 · 𝑁)) | 
| 11 | 10 | gt0ne0d 11828 | . . . . . 6
⊢ (𝜑 → (2 · 𝑁) ≠ 0) | 
| 12 |  | knoppndvlem19.j | . . . . . . . 8
⊢ (𝜑 → 𝐽 ∈
ℕ0) | 
| 13 | 12 | nn0zd 12641 | . . . . . . 7
⊢ (𝜑 → 𝐽 ∈ ℤ) | 
| 14 | 13 | znegcld 12726 | . . . . . 6
⊢ (𝜑 → -𝐽 ∈ ℤ) | 
| 15 | 6, 11, 14 | reexpclzd 14289 | . . . . 5
⊢ (𝜑 → ((2 · 𝑁)↑-𝐽) ∈ ℝ) | 
| 16 | 3 | recnd 11290 | . . . . . 6
⊢ (𝜑 → 2 ∈
ℂ) | 
| 17 | 5 | recnd 11290 | . . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 18 | 16, 17, 11 | mulne0bad 11919 | . . . . 5
⊢ (𝜑 → 2 ≠ 0) | 
| 19 | 15, 3, 18 | redivcld 12096 | . . . 4
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) / 2) ∈ ℝ) | 
| 20 | 6, 14, 10 | 3jca 1128 | . . . . . . 7
⊢ (𝜑 → ((2 · 𝑁) ∈ ℝ ∧ -𝐽 ∈ ℤ ∧ 0 < (2
· 𝑁))) | 
| 21 |  | expgt0 14137 | . . . . . . 7
⊢ (((2
· 𝑁) ∈ ℝ
∧ -𝐽 ∈ ℤ
∧ 0 < (2 · 𝑁)) → 0 < ((2 · 𝑁)↑-𝐽)) | 
| 22 | 20, 21 | syl 17 | . . . . . 6
⊢ (𝜑 → 0 < ((2 · 𝑁)↑-𝐽)) | 
| 23 | 15, 3, 22, 8 | divgt0d 12204 | . . . . 5
⊢ (𝜑 → 0 < (((2 · 𝑁)↑-𝐽) / 2)) | 
| 24 | 23 | gt0ne0d 11828 | . . . 4
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) / 2) ≠ 0) | 
| 25 | 1, 19, 24 | redivcld 12096 | . . 3
⊢ (𝜑 → (𝐻 / (((2 · 𝑁)↑-𝐽) / 2)) ∈ ℝ) | 
| 26 | 25 | flcld 13839 | . 2
⊢ (𝜑 → (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) ∈ ℤ) | 
| 27 |  | knoppndvlem19.a | . . . . . . 7
⊢ 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑚) | 
| 28 | 27 | a1i 11 | . . . . . 6
⊢ (𝑚 = (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) → 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑚)) | 
| 29 |  | id 22 | . . . . . . 7
⊢ (𝑚 = (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) → 𝑚 = (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2)))) | 
| 30 | 29 | oveq2d 7448 | . . . . . 6
⊢ (𝑚 = (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) → ((((2 · 𝑁)↑-𝐽) / 2) · 𝑚) = ((((2 · 𝑁)↑-𝐽) / 2) · (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))))) | 
| 31 | 28, 30 | eqtrd 2776 | . . . . 5
⊢ (𝑚 = (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) → 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))))) | 
| 32 | 31 | breq1d 5152 | . . . 4
⊢ (𝑚 = (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) → (𝐴 ≤ 𝐻 ↔ ((((2 · 𝑁)↑-𝐽) / 2) · (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2)))) ≤ 𝐻)) | 
| 33 |  | knoppndvlem19.b | . . . . . . 7
⊢ 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝑚 + 1)) | 
| 34 | 33 | a1i 11 | . . . . . 6
⊢ (𝑚 = (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) → 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝑚 + 1))) | 
| 35 | 29 | oveq1d 7447 | . . . . . . 7
⊢ (𝑚 = (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) → (𝑚 + 1) = ((⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) + 1)) | 
| 36 | 35 | oveq2d 7448 | . . . . . 6
⊢ (𝑚 = (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) → ((((2 · 𝑁)↑-𝐽) / 2) · (𝑚 + 1)) = ((((2 · 𝑁)↑-𝐽) / 2) · ((⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) + 1))) | 
| 37 | 34, 36 | eqtrd 2776 | . . . . 5
⊢ (𝑚 = (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) → 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · ((⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) + 1))) | 
| 38 | 37 | breq2d 5154 | . . . 4
⊢ (𝑚 = (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) → (𝐻 ≤ 𝐵 ↔ 𝐻 ≤ ((((2 · 𝑁)↑-𝐽) / 2) · ((⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) + 1)))) | 
| 39 | 32, 38 | anbi12d 632 | . . 3
⊢ (𝑚 = (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) → ((𝐴 ≤ 𝐻 ∧ 𝐻 ≤ 𝐵) ↔ (((((2 · 𝑁)↑-𝐽) / 2) · (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2)))) ≤ 𝐻 ∧ 𝐻 ≤ ((((2 · 𝑁)↑-𝐽) / 2) · ((⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) + 1))))) | 
| 40 | 39 | adantl 481 | . 2
⊢ ((𝜑 ∧ 𝑚 = (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2)))) → ((𝐴 ≤ 𝐻 ∧ 𝐻 ≤ 𝐵) ↔ (((((2 · 𝑁)↑-𝐽) / 2) · (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2)))) ≤ 𝐻 ∧ 𝐻 ≤ ((((2 · 𝑁)↑-𝐽) / 2) · ((⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) + 1))))) | 
| 41 | 26 | zred 12724 | . . . . 5
⊢ (𝜑 → (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) ∈ ℝ) | 
| 42 |  | 0red 11265 | . . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) | 
| 43 | 42, 19, 23 | ltled 11410 | . . . . 5
⊢ (𝜑 → 0 ≤ (((2 · 𝑁)↑-𝐽) / 2)) | 
| 44 |  | flle 13840 | . . . . . 6
⊢ ((𝐻 / (((2 · 𝑁)↑-𝐽) / 2)) ∈ ℝ →
(⌊‘(𝐻 / (((2
· 𝑁)↑-𝐽) / 2))) ≤ (𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) | 
| 45 | 25, 44 | syl 17 | . . . . 5
⊢ (𝜑 → (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) ≤ (𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) | 
| 46 | 41, 25, 19, 43, 45 | lemul2ad 12209 | . . . 4
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2)))) ≤ ((((2 · 𝑁)↑-𝐽) / 2) · (𝐻 / (((2 · 𝑁)↑-𝐽) / 2)))) | 
| 47 | 1 | recnd 11290 | . . . . 5
⊢ (𝜑 → 𝐻 ∈ ℂ) | 
| 48 | 19 | recnd 11290 | . . . . 5
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) / 2) ∈ ℂ) | 
| 49 | 47, 48, 24 | divcan2d 12046 | . . . 4
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) = 𝐻) | 
| 50 | 46, 49 | breqtrd 5168 | . . 3
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2)))) ≤ 𝐻) | 
| 51 | 49 | eqcomd 2742 | . . . 4
⊢ (𝜑 → 𝐻 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝐻 / (((2 · 𝑁)↑-𝐽) / 2)))) | 
| 52 |  | peano2re 11435 | . . . . . 6
⊢
((⌊‘(𝐻 /
(((2 · 𝑁)↑-𝐽) / 2))) ∈ ℝ →
((⌊‘(𝐻 / (((2
· 𝑁)↑-𝐽) / 2))) + 1) ∈
ℝ) | 
| 53 | 41, 52 | syl 17 | . . . . 5
⊢ (𝜑 → ((⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) + 1) ∈
ℝ) | 
| 54 |  | fllep1 13842 | . . . . . 6
⊢ ((𝐻 / (((2 · 𝑁)↑-𝐽) / 2)) ∈ ℝ → (𝐻 / (((2 · 𝑁)↑-𝐽) / 2)) ≤ ((⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) + 1)) | 
| 55 | 25, 54 | syl 17 | . . . . 5
⊢ (𝜑 → (𝐻 / (((2 · 𝑁)↑-𝐽) / 2)) ≤ ((⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) + 1)) | 
| 56 | 25, 53, 19, 43, 55 | lemul2ad 12209 | . . . 4
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) ≤ ((((2 · 𝑁)↑-𝐽) / 2) · ((⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) + 1))) | 
| 57 | 51, 56 | eqbrtrd 5164 | . . 3
⊢ (𝜑 → 𝐻 ≤ ((((2 · 𝑁)↑-𝐽) / 2) · ((⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) + 1))) | 
| 58 | 50, 57 | jca 511 | . 2
⊢ (𝜑 → (((((2 · 𝑁)↑-𝐽) / 2) · (⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2)))) ≤ 𝐻 ∧ 𝐻 ≤ ((((2 · 𝑁)↑-𝐽) / 2) · ((⌊‘(𝐻 / (((2 · 𝑁)↑-𝐽) / 2))) + 1)))) | 
| 59 | 26, 40, 58 | rspcedvd 3623 | 1
⊢ (𝜑 → ∃𝑚 ∈ ℤ (𝐴 ≤ 𝐻 ∧ 𝐻 ≤ 𝐵)) |