Proof of Theorem bposlem4
Step | Hyp | Ref
| Expression |
1 | | 2nn 12046 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
2 | | 5nn 12059 |
. . . . . . . . 9
⊢ 5 ∈
ℕ |
3 | | bpos.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘5)) |
4 | | eluznn 12658 |
. . . . . . . . 9
⊢ ((5
∈ ℕ ∧ 𝑁
∈ (ℤ≥‘5)) → 𝑁 ∈ ℕ) |
5 | 2, 3, 4 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
6 | | nnmulcl 11997 |
. . . . . . . 8
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ) → (2 · 𝑁) ∈ ℕ) |
7 | 1, 5, 6 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝑁) ∈
ℕ) |
8 | 7 | nnred 11988 |
. . . . . 6
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) |
9 | 7 | nnrpd 12770 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ+) |
10 | 9 | rpge0d 12776 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (2 · 𝑁)) |
11 | 8, 10 | resqrtcld 15129 |
. . . . 5
⊢ (𝜑 → (√‘(2 ·
𝑁)) ∈
ℝ) |
12 | 11 | flcld 13518 |
. . . 4
⊢ (𝜑 →
(⌊‘(√‘(2 · 𝑁))) ∈ ℤ) |
13 | | sqrt9 14985 |
. . . . . 6
⊢
(√‘9) = 3 |
14 | | 9re 12072 |
. . . . . . . . 9
⊢ 9 ∈
ℝ |
15 | 14 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 9 ∈
ℝ) |
16 | | 10re 12456 |
. . . . . . . . 9
⊢ ;10 ∈ ℝ |
17 | 16 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ;10 ∈ ℝ) |
18 | | lep1 11816 |
. . . . . . . . . . 11
⊢ (9 ∈
ℝ → 9 ≤ (9 + 1)) |
19 | 14, 18 | ax-mp 5 |
. . . . . . . . . 10
⊢ 9 ≤ (9
+ 1) |
20 | | 9p1e10 12439 |
. . . . . . . . . 10
⊢ (9 + 1) =
;10 |
21 | 19, 20 | breqtri 5099 |
. . . . . . . . 9
⊢ 9 ≤
;10 |
22 | 21 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 9 ≤ ;10) |
23 | | 5cn 12061 |
. . . . . . . . . 10
⊢ 5 ∈
ℂ |
24 | | 2cn 12048 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
25 | | 5t2e10 12537 |
. . . . . . . . . 10
⊢ (5
· 2) = ;10 |
26 | 23, 24, 25 | mulcomli 10984 |
. . . . . . . . 9
⊢ (2
· 5) = ;10 |
27 | | eluzle 12595 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘5) → 5 ≤ 𝑁) |
28 | 3, 27 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 5 ≤ 𝑁) |
29 | 5 | nnred 11988 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℝ) |
30 | | 5re 12060 |
. . . . . . . . . . . 12
⊢ 5 ∈
ℝ |
31 | | 2re 12047 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
32 | | 2pos 12076 |
. . . . . . . . . . . . 13
⊢ 0 <
2 |
33 | 31, 32 | pm3.2i 471 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℝ ∧ 0 < 2) |
34 | | lemul2 11828 |
. . . . . . . . . . . 12
⊢ ((5
∈ ℝ ∧ 𝑁
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (5 ≤ 𝑁 ↔ (2 · 5) ≤ (2
· 𝑁))) |
35 | 30, 33, 34 | mp3an13 1451 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ → (5 ≤
𝑁 ↔ (2 · 5)
≤ (2 · 𝑁))) |
36 | 29, 35 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (5 ≤ 𝑁 ↔ (2 · 5) ≤ (2 ·
𝑁))) |
37 | 28, 36 | mpbid 231 |
. . . . . . . . 9
⊢ (𝜑 → (2 · 5) ≤ (2
· 𝑁)) |
38 | 26, 37 | eqbrtrrid 5110 |
. . . . . . . 8
⊢ (𝜑 → ;10 ≤ (2 · 𝑁)) |
39 | 15, 17, 8, 22, 38 | letrd 11132 |
. . . . . . 7
⊢ (𝜑 → 9 ≤ (2 · 𝑁)) |
40 | | 0re 10977 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
41 | | 9pos 12086 |
. . . . . . . . . 10
⊢ 0 <
9 |
42 | 40, 14, 41 | ltleii 11098 |
. . . . . . . . 9
⊢ 0 ≤
9 |
43 | 14, 42 | pm3.2i 471 |
. . . . . . . 8
⊢ (9 ∈
ℝ ∧ 0 ≤ 9) |
44 | 9 | rprege0d 12779 |
. . . . . . . 8
⊢ (𝜑 → ((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2
· 𝑁))) |
45 | | sqrtle 14972 |
. . . . . . . 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 231 |
. . . . . 6
⊢ (𝜑 → (√‘9) ≤
(√‘(2 · 𝑁))) |
48 | 13, 47 | eqbrtrrid 5110 |
. . . . 5
⊢ (𝜑 → 3 ≤ (√‘(2
· 𝑁))) |
49 | | 3z 12353 |
. . . . . 6
⊢ 3 ∈
ℤ |
50 | | flge 13525 |
. . . . . 6
⊢
(((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℤ)
→ (3 ≤ (√‘(2 · 𝑁)) ↔ 3 ≤
(⌊‘(√‘(2 · 𝑁))))) |
51 | 11, 49, 50 | sylancl 586 |
. . . . 5
⊢ (𝜑 → (3 ≤ (√‘(2
· 𝑁)) ↔ 3 ≤
(⌊‘(√‘(2 · 𝑁))))) |
52 | 48, 51 | mpbid 231 |
. . . 4
⊢ (𝜑 → 3 ≤
(⌊‘(√‘(2 · 𝑁)))) |
53 | 49 | eluz1i 12590 |
. . . 4
⊢
((⌊‘(√‘(2 · 𝑁))) ∈ (ℤ≥‘3)
↔ ((⌊‘(√‘(2 · 𝑁))) ∈ ℤ ∧ 3 ≤
(⌊‘(√‘(2 · 𝑁))))) |
54 | 12, 52, 53 | sylanbrc 583 |
. . 3
⊢ (𝜑 →
(⌊‘(√‘(2 · 𝑁))) ∈
(ℤ≥‘3)) |
55 | | 3nn 12052 |
. . . . 5
⊢ 3 ∈
ℕ |
56 | | nndivre 12014 |
. . . . 5
⊢ (((2
· 𝑁) ∈ ℝ
∧ 3 ∈ ℕ) → ((2 · 𝑁) / 3) ∈ ℝ) |
57 | 8, 55, 56 | sylancl 586 |
. . . 4
⊢ (𝜑 → ((2 · 𝑁) / 3) ∈
ℝ) |
58 | | 3re 12053 |
. . . . . . . . 9
⊢ 3 ∈
ℝ |
59 | 58 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 3 ∈
ℝ) |
60 | 9 | sqrtgt0d 15124 |
. . . . . . . 8
⊢ (𝜑 → 0 < (√‘(2
· 𝑁))) |
61 | | lemul2 11828 |
. . . . . . . 8
⊢ ((3
∈ ℝ ∧ (√‘(2 · 𝑁)) ∈ ℝ ∧ ((√‘(2
· 𝑁)) ∈ ℝ
∧ 0 < (√‘(2 · 𝑁)))) → (3 ≤ (√‘(2
· 𝑁)) ↔
((√‘(2 · 𝑁)) · 3) ≤ ((√‘(2
· 𝑁)) ·
(√‘(2 · 𝑁))))) |
62 | 59, 11, 11, 60, 61 | syl112anc 1373 |
. . . . . . 7
⊢ (𝜑 → (3 ≤ (√‘(2
· 𝑁)) ↔
((√‘(2 · 𝑁)) · 3) ≤ ((√‘(2
· 𝑁)) ·
(√‘(2 · 𝑁))))) |
63 | 48, 62 | mpbid 231 |
. . . . . 6
⊢ (𝜑 → ((√‘(2
· 𝑁)) · 3)
≤ ((√‘(2 · 𝑁)) · (√‘(2 · 𝑁)))) |
64 | | remsqsqrt 14968 |
. . . . . . 7
⊢ (((2
· 𝑁) ∈ ℝ
∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁)) · (√‘(2
· 𝑁))) = (2 ·
𝑁)) |
65 | 8, 10, 64 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((√‘(2
· 𝑁)) ·
(√‘(2 · 𝑁))) = (2 · 𝑁)) |
66 | 63, 65 | breqtrd 5100 |
. . . . 5
⊢ (𝜑 → ((√‘(2
· 𝑁)) · 3)
≤ (2 · 𝑁)) |
67 | | 3pos 12078 |
. . . . . . . 8
⊢ 0 <
3 |
68 | 58, 67 | pm3.2i 471 |
. . . . . . 7
⊢ (3 ∈
ℝ ∧ 0 < 3) |
69 | 68 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (3 ∈ ℝ ∧ 0
< 3)) |
70 | | lemuldiv 11855 |
. . . . . 6
⊢
(((√‘(2 · 𝑁)) ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ (3 ∈
ℝ ∧ 0 < 3)) → (((√‘(2 · 𝑁)) · 3) ≤ (2 · 𝑁) ↔ (√‘(2
· 𝑁)) ≤ ((2
· 𝑁) /
3))) |
71 | 11, 8, 69, 70 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → (((√‘(2
· 𝑁)) · 3)
≤ (2 · 𝑁) ↔
(√‘(2 · 𝑁)) ≤ ((2 · 𝑁) / 3))) |
72 | 66, 71 | mpbid 231 |
. . . 4
⊢ (𝜑 → (√‘(2 ·
𝑁)) ≤ ((2 · 𝑁) / 3)) |
73 | | flword2 13533 |
. . . 4
⊢
(((√‘(2 · 𝑁)) ∈ ℝ ∧ ((2 · 𝑁) / 3) ∈ ℝ ∧
(√‘(2 · 𝑁)) ≤ ((2 · 𝑁) / 3)) → (⌊‘((2 ·
𝑁) / 3)) ∈
(ℤ≥‘(⌊‘(√‘(2 · 𝑁))))) |
74 | 11, 57, 72, 73 | syl3anc 1370 |
. . 3
⊢ (𝜑 → (⌊‘((2
· 𝑁) / 3)) ∈
(ℤ≥‘(⌊‘(√‘(2 · 𝑁))))) |
75 | | elfzuzb 13250 |
. . 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 7286 |
. 2
⊢
(3...𝐾) =
(3...(⌊‘((2 · 𝑁) / 3))) |
80 | 76, 77, 79 | 3eltr4g 2856 |
1
⊢ (𝜑 → 𝑀 ∈ (3...𝐾)) |