Proof of Theorem bposlem4
| Step | Hyp | Ref
| Expression |
| 1 | | 2nn 12339 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
| 2 | | 5nn 12352 |
. . . . . . . . 9
⊢ 5 ∈
ℕ |
| 3 | | bpos.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘5)) |
| 4 | | eluznn 12960 |
. . . . . . . . 9
⊢ ((5
∈ ℕ ∧ 𝑁
∈ (ℤ≥‘5)) → 𝑁 ∈ ℕ) |
| 5 | 2, 3, 4 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 6 | | nnmulcl 12290 |
. . . . . . . 8
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ) → (2 · 𝑁) ∈ ℕ) |
| 7 | 1, 5, 6 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝑁) ∈
ℕ) |
| 8 | 7 | nnred 12281 |
. . . . . 6
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) |
| 9 | 7 | nnrpd 13075 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ+) |
| 10 | 9 | rpge0d 13081 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (2 · 𝑁)) |
| 11 | 8, 10 | resqrtcld 15456 |
. . . . 5
⊢ (𝜑 → (√‘(2 ·
𝑁)) ∈
ℝ) |
| 12 | 11 | flcld 13838 |
. . . 4
⊢ (𝜑 →
(⌊‘(√‘(2 · 𝑁))) ∈ ℤ) |
| 13 | | sqrt9 15312 |
. . . . . 6
⊢
(√‘9) = 3 |
| 14 | | 9re 12365 |
. . . . . . . . 9
⊢ 9 ∈
ℝ |
| 15 | 14 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 9 ∈
ℝ) |
| 16 | | 10re 12752 |
. . . . . . . . 9
⊢ ;10 ∈ ℝ |
| 17 | 16 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ;10 ∈ ℝ) |
| 18 | | lep1 12108 |
. . . . . . . . . . 11
⊢ (9 ∈
ℝ → 9 ≤ (9 + 1)) |
| 19 | 14, 18 | ax-mp 5 |
. . . . . . . . . 10
⊢ 9 ≤ (9
+ 1) |
| 20 | | 9p1e10 12735 |
. . . . . . . . . 10
⊢ (9 + 1) =
;10 |
| 21 | 19, 20 | breqtri 5168 |
. . . . . . . . 9
⊢ 9 ≤
;10 |
| 22 | 21 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 9 ≤ ;10) |
| 23 | | 5cn 12354 |
. . . . . . . . . 10
⊢ 5 ∈
ℂ |
| 24 | | 2cn 12341 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
| 25 | | 5t2e10 12833 |
. . . . . . . . . 10
⊢ (5
· 2) = ;10 |
| 26 | 23, 24, 25 | mulcomli 11270 |
. . . . . . . . 9
⊢ (2
· 5) = ;10 |
| 27 | | eluzle 12891 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘5) → 5 ≤ 𝑁) |
| 28 | 3, 27 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 5 ≤ 𝑁) |
| 29 | 5 | nnred 12281 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 30 | | 5re 12353 |
. . . . . . . . . . . 12
⊢ 5 ∈
ℝ |
| 31 | | 2re 12340 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
| 32 | | 2pos 12369 |
. . . . . . . . . . . . 13
⊢ 0 <
2 |
| 33 | 31, 32 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℝ ∧ 0 < 2) |
| 34 | | lemul2 12120 |
. . . . . . . . . . . 12
⊢ ((5
∈ ℝ ∧ 𝑁
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (5 ≤ 𝑁 ↔ (2 · 5) ≤ (2
· 𝑁))) |
| 35 | 30, 33, 34 | mp3an13 1454 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ → (5 ≤
𝑁 ↔ (2 · 5)
≤ (2 · 𝑁))) |
| 36 | 29, 35 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (5 ≤ 𝑁 ↔ (2 · 5) ≤ (2 ·
𝑁))) |
| 37 | 28, 36 | mpbid 232 |
. . . . . . . . 9
⊢ (𝜑 → (2 · 5) ≤ (2
· 𝑁)) |
| 38 | 26, 37 | eqbrtrrid 5179 |
. . . . . . . 8
⊢ (𝜑 → ;10 ≤ (2 · 𝑁)) |
| 39 | 15, 17, 8, 22, 38 | letrd 11418 |
. . . . . . 7
⊢ (𝜑 → 9 ≤ (2 · 𝑁)) |
| 40 | | 0re 11263 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
| 41 | | 9pos 12379 |
. . . . . . . . . 10
⊢ 0 <
9 |
| 42 | 40, 14, 41 | ltleii 11384 |
. . . . . . . . 9
⊢ 0 ≤
9 |
| 43 | 14, 42 | pm3.2i 470 |
. . . . . . . 8
⊢ (9 ∈
ℝ ∧ 0 ≤ 9) |
| 44 | 9 | rprege0d 13084 |
. . . . . . . 8
⊢ (𝜑 → ((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2
· 𝑁))) |
| 45 | | sqrtle 15299 |
. . . . . . . 8
⊢ (((9
∈ ℝ ∧ 0 ≤ 9) ∧ ((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 ·
𝑁))) → (9 ≤ (2
· 𝑁) ↔
(√‘9) ≤ (√‘(2 · 𝑁)))) |
| 46 | 43, 44, 45 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (9 ≤ (2 · 𝑁) ↔ (√‘9) ≤
(√‘(2 · 𝑁)))) |
| 47 | 39, 46 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (√‘9) ≤
(√‘(2 · 𝑁))) |
| 48 | 13, 47 | eqbrtrrid 5179 |
. . . . 5
⊢ (𝜑 → 3 ≤ (√‘(2
· 𝑁))) |
| 49 | | 3z 12650 |
. . . . . 6
⊢ 3 ∈
ℤ |
| 50 | | flge 13845 |
. . . . . 6
⊢
(((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℤ)
→ (3 ≤ (√‘(2 · 𝑁)) ↔ 3 ≤
(⌊‘(√‘(2 · 𝑁))))) |
| 51 | 11, 49, 50 | sylancl 586 |
. . . . 5
⊢ (𝜑 → (3 ≤ (√‘(2
· 𝑁)) ↔ 3 ≤
(⌊‘(√‘(2 · 𝑁))))) |
| 52 | 48, 51 | mpbid 232 |
. . . 4
⊢ (𝜑 → 3 ≤
(⌊‘(√‘(2 · 𝑁)))) |
| 53 | 49 | eluz1i 12886 |
. . . 4
⊢
((⌊‘(√‘(2 · 𝑁))) ∈ (ℤ≥‘3)
↔ ((⌊‘(√‘(2 · 𝑁))) ∈ ℤ ∧ 3 ≤
(⌊‘(√‘(2 · 𝑁))))) |
| 54 | 12, 52, 53 | sylanbrc 583 |
. . 3
⊢ (𝜑 →
(⌊‘(√‘(2 · 𝑁))) ∈
(ℤ≥‘3)) |
| 55 | | 3nn 12345 |
. . . . 5
⊢ 3 ∈
ℕ |
| 56 | | nndivre 12307 |
. . . . 5
⊢ (((2
· 𝑁) ∈ ℝ
∧ 3 ∈ ℕ) → ((2 · 𝑁) / 3) ∈ ℝ) |
| 57 | 8, 55, 56 | sylancl 586 |
. . . 4
⊢ (𝜑 → ((2 · 𝑁) / 3) ∈
ℝ) |
| 58 | | 3re 12346 |
. . . . . . . . 9
⊢ 3 ∈
ℝ |
| 59 | 58 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 3 ∈
ℝ) |
| 60 | 9 | sqrtgt0d 15451 |
. . . . . . . 8
⊢ (𝜑 → 0 < (√‘(2
· 𝑁))) |
| 61 | | lemul2 12120 |
. . . . . . . 8
⊢ ((3
∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ ∧ ((√‘(2
· 𝑁)) ∈ ℝ
∧ 0 < (√‘(2 · 𝑁)))) → (3 ≤ (√‘(2
· 𝑁)) ↔
((√‘(2 · 𝑁)) · 3) ≤ ((√‘(2
· 𝑁)) ·
(√‘(2 · 𝑁))))) |
| 62 | 59, 11, 11, 60, 61 | syl112anc 1376 |
. . . . . . 7
⊢ (𝜑 → (3 ≤ (√‘(2
· 𝑁)) ↔
((√‘(2 · 𝑁)) · 3) ≤ ((√‘(2
· 𝑁)) ·
(√‘(2 · 𝑁))))) |
| 63 | 48, 62 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → ((√‘(2
· 𝑁)) · 3)
≤ ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁)))) |
| 64 | | remsqsqrt 15295 |
. . . . . . 7
⊢ (((2
· 𝑁) ∈ ℝ
∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁)) · (√‘(2
· 𝑁))) = (2 ·
𝑁)) |
| 65 | 8, 10, 64 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((√‘(2
· 𝑁)) ·
(√‘(2 · 𝑁))) = (2 · 𝑁)) |
| 66 | 63, 65 | breqtrd 5169 |
. . . . 5
⊢ (𝜑 → ((√‘(2
· 𝑁)) · 3)
≤ (2 · 𝑁)) |
| 67 | | 3pos 12371 |
. . . . . . . 8
⊢ 0 <
3 |
| 68 | 58, 67 | pm3.2i 470 |
. . . . . . 7
⊢ (3 ∈
ℝ ∧ 0 < 3) |
| 69 | 68 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (3 ∈ ℝ ∧ 0
< 3)) |
| 70 | | lemuldiv 12148 |
. . . . . 6
⊢
(((√‘(2 · 𝑁)) ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ (3 ∈
ℝ ∧ 0 < 3)) → (((√‘(2 · 𝑁)) · 3) ≤ (2 · 𝑁) ↔ (√‘(2
· 𝑁)) ≤ ((2
· 𝑁) /
3))) |
| 71 | 11, 8, 69, 70 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (((√‘(2
· 𝑁)) · 3)
≤ (2 · 𝑁) ↔
(√‘(2 · 𝑁)) ≤ ((2 · 𝑁) / 3))) |
| 72 | 66, 71 | mpbid 232 |
. . . 4
⊢ (𝜑 → (√‘(2 ·
𝑁)) ≤ ((2 · 𝑁) / 3)) |
| 73 | | flword2 13853 |
. . . 4
⊢
(((√‘(2 · 𝑁)) ∈ ℝ ∧ ((2 · 𝑁) / 3) ∈ ℝ ∧
(√‘(2 · 𝑁)) ≤ ((2 · 𝑁) / 3)) → (⌊‘((2 ·
𝑁) / 3)) ∈
(ℤ≥‘(⌊‘(√‘(2 · 𝑁))))) |
| 74 | 11, 57, 72, 73 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (⌊‘((2
· 𝑁) / 3)) ∈
(ℤ≥‘(⌊‘(√‘(2 · 𝑁))))) |
| 75 | | elfzuzb 13558 |
. . 3
⊢
((⌊‘(√‘(2 · 𝑁))) ∈ (3...(⌊‘((2 ·
𝑁) / 3))) ↔
((⌊‘(√‘(2 · 𝑁))) ∈ (ℤ≥‘3)
∧ (⌊‘((2 · 𝑁) / 3)) ∈
(ℤ≥‘(⌊‘(√‘(2 · 𝑁)))))) |
| 76 | 54, 74, 75 | sylanbrc 583 |
. 2
⊢ (𝜑 →
(⌊‘(√‘(2 · 𝑁))) ∈ (3...(⌊‘((2 ·
𝑁) / 3)))) |
| 77 | | bpos.5 |
. 2
⊢ 𝑀 =
(⌊‘(√‘(2 · 𝑁))) |
| 78 | | bpos.4 |
. . 3
⊢ 𝐾 = (⌊‘((2 ·
𝑁) / 3)) |
| 79 | 78 | oveq2i 7442 |
. 2
⊢
(3...𝐾) =
(3...(⌊‘((2 · 𝑁) / 3))) |
| 80 | 76, 77, 79 | 3eltr4g 2858 |
1
⊢ (𝜑 → 𝑀 ∈ (3...𝐾)) |