Step | Hyp | Ref
| Expression |
1 | | 3re 10971 |
. . 3
⊢ 3 ∈
ℝ |
2 | 1 | a1i 11 |
. 2
⊢ ((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) → 3 ∈
ℝ) |
3 | | simpl 472 |
. 2
⊢ ((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) → 𝑁 ∈ ℝ) |
4 | | ppicl 24657 |
. . . . . . . 8
⊢ (𝑁 ∈ ℝ →
(π‘𝑁)
∈ ℕ0) |
5 | 4 | nn0red 11229 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ →
(π‘𝑁)
∈ ℝ) |
6 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(π‘𝑁)
∈ ℝ) |
7 | | 2re 10967 |
. . . . . 6
⊢ 2 ∈
ℝ |
8 | | resubcl 10224 |
. . . . . 6
⊢
(((π‘𝑁) ∈ ℝ ∧ 2 ∈ ℝ)
→ ((π‘𝑁) − 2) ∈
ℝ) |
9 | 6, 7, 8 | sylancl 693 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((π‘𝑁)
− 2) ∈ ℝ) |
10 | | fzfi 12633 |
. . . . . . . . 9
⊢
(4...(⌊‘𝑁)) ∈ Fin |
11 | | ssrab2 3650 |
. . . . . . . . 9
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} ⊆ (4...(⌊‘𝑁)) |
12 | | ssfi 8065 |
. . . . . . . . 9
⊢
(((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ⊆
(4...(⌊‘𝑁)))
→ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} ∈ Fin) |
13 | 10, 11, 12 | mp2an 704 |
. . . . . . . 8
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} ∈ Fin |
14 | | hashcl 13009 |
. . . . . . . 8
⊢ ({𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} ∈ Fin → (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈
ℕ0) |
15 | 13, 14 | ax-mp 5 |
. . . . . . 7
⊢
(#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) ∈ ℕ0 |
16 | 15 | nn0rei 11180 |
. . . . . 6
⊢
(#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) ∈ ℝ |
17 | 16 | a1i 11 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) ∈ ℝ) |
18 | | 3nn 11063 |
. . . . . . 7
⊢ 3 ∈
ℕ |
19 | | nndivre 10933 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ∈
ℕ) → (𝑁 / 3)
∈ ℝ) |
20 | 18, 19 | mpan2 703 |
. . . . . 6
⊢ (𝑁 ∈ ℝ → (𝑁 / 3) ∈
ℝ) |
21 | 20 | adantr 480 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (𝑁 / 3) ∈
ℝ) |
22 | | ppifl 24686 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℝ →
(π‘(⌊‘𝑁)) = (π‘𝑁)) |
23 | 22 | adantr 480 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(π‘(⌊‘𝑁)) = (π‘𝑁)) |
24 | | ppi3 24697 |
. . . . . . . . 9
⊢
(π‘3) = 2 |
25 | 24 | a1i 11 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(π‘3) = 2) |
26 | 23, 25 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((π‘(⌊‘𝑁)) − (π‘3)) =
((π‘𝑁)
− 2)) |
27 | | 3z 11287 |
. . . . . . . . . . 11
⊢ 3 ∈
ℤ |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 3 ∈
ℤ) |
29 | | flcl 12458 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ →
(⌊‘𝑁) ∈
ℤ) |
30 | 29 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘𝑁) ∈
ℤ) |
31 | | flge 12468 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 3 ∈
ℤ) → (3 ≤ 𝑁
↔ 3 ≤ (⌊‘𝑁))) |
32 | 27, 31 | mpan2 703 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ → (3 ≤
𝑁 ↔ 3 ≤
(⌊‘𝑁))) |
33 | 32 | biimpa 500 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 3 ≤
(⌊‘𝑁)) |
34 | | eluz2 11569 |
. . . . . . . . . 10
⊢
((⌊‘𝑁)
∈ (ℤ≥‘3) ↔ (3 ∈ ℤ ∧
(⌊‘𝑁) ∈
ℤ ∧ 3 ≤ (⌊‘𝑁))) |
35 | 28, 30, 33, 34 | syl3anbrc 1239 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘𝑁) ∈
(ℤ≥‘3)) |
36 | | ppidif 24689 |
. . . . . . . . 9
⊢
((⌊‘𝑁)
∈ (ℤ≥‘3) →
((π‘(⌊‘𝑁)) − (π‘3)) =
(#‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ))) |
37 | 35, 36 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((π‘(⌊‘𝑁)) − (π‘3)) =
(#‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ))) |
38 | | df-4 10958 |
. . . . . . . . . . 11
⊢ 4 = (3 +
1) |
39 | 38 | oveq1i 6559 |
. . . . . . . . . 10
⊢
(4...(⌊‘𝑁)) = ((3 + 1)...(⌊‘𝑁)) |
40 | 39 | ineq1i 3772 |
. . . . . . . . 9
⊢
((4...(⌊‘𝑁)) ∩ ℙ) = (((3 +
1)...(⌊‘𝑁))
∩ ℙ) |
41 | 40 | fveq2i 6106 |
. . . . . . . 8
⊢
(#‘((4...(⌊‘𝑁)) ∩ ℙ)) = (#‘(((3 +
1)...(⌊‘𝑁))
∩ ℙ)) |
42 | 37, 41 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((π‘(⌊‘𝑁)) − (π‘3)) =
(#‘((4...(⌊‘𝑁)) ∩ ℙ))) |
43 | 26, 42 | eqtr3d 2646 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((π‘𝑁)
− 2) = (#‘((4...(⌊‘𝑁)) ∩ ℙ))) |
44 | | dfin5 3548 |
. . . . . . . . 9
⊢
((4...(⌊‘𝑁)) ∩ ℙ) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 𝑘 ∈ ℙ} |
45 | | elfzle1 12215 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(4...(⌊‘𝑁))
→ 4 ≤ 𝑘) |
46 | | ppiublem2 24728 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℙ ∧ 4 ≤
𝑘) → (𝑘 mod 6) ∈ {1,
5}) |
47 | 46 | expcom 450 |
. . . . . . . . . . 11
⊢ (4 ≤
𝑘 → (𝑘 ∈ ℙ → (𝑘 mod 6) ∈ {1,
5})) |
48 | 45, 47 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(4...(⌊‘𝑁))
→ (𝑘 ∈ ℙ
→ (𝑘 mod 6) ∈ {1,
5})) |
49 | 48 | ss2rabi 3647 |
. . . . . . . . 9
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ 𝑘 ∈ ℙ}
⊆ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} |
50 | 44, 49 | eqsstri 3598 |
. . . . . . . 8
⊢
((4...(⌊‘𝑁)) ∩ ℙ) ⊆ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} |
51 | | ssdomg 7887 |
. . . . . . . 8
⊢ ({𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} ∈ Fin → (((4...(⌊‘𝑁)) ∩ ℙ) ⊆ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} → ((4...(⌊‘𝑁)) ∩ ℙ) ≼ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}})) |
52 | 13, 50, 51 | mp2 9 |
. . . . . . 7
⊢
((4...(⌊‘𝑁)) ∩ ℙ) ≼ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} |
53 | | inss1 3795 |
. . . . . . . . 9
⊢
((4...(⌊‘𝑁)) ∩ ℙ) ⊆
(4...(⌊‘𝑁)) |
54 | | ssfi 8065 |
. . . . . . . . 9
⊢
(((4...(⌊‘𝑁)) ∈ Fin ∧
((4...(⌊‘𝑁))
∩ ℙ) ⊆ (4...(⌊‘𝑁))) → ((4...(⌊‘𝑁)) ∩ ℙ) ∈
Fin) |
55 | 10, 53, 54 | mp2an 704 |
. . . . . . . 8
⊢
((4...(⌊‘𝑁)) ∩ ℙ) ∈
Fin |
56 | | hashdom 13029 |
. . . . . . . 8
⊢
((((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin ∧ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} ∈ Fin) → ((#‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤ (#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) ↔ ((4...(⌊‘𝑁)) ∩ ℙ) ≼ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}})) |
57 | 55, 13, 56 | mp2an 704 |
. . . . . . 7
⊢
((#‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤ (#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) ↔ ((4...(⌊‘𝑁)) ∩ ℙ) ≼ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) |
58 | 52, 57 | mpbir 220 |
. . . . . 6
⊢
(#‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤ (#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) |
59 | 43, 58 | syl6eqbr 4622 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((π‘𝑁)
− 2) ≤ (#‘{𝑘
∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}})) |
60 | | reflcl 12459 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ →
(⌊‘𝑁) ∈
ℝ) |
61 | 60 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘𝑁) ∈
ℝ) |
62 | | peano2rem 10227 |
. . . . . . . . . 10
⊢
((⌊‘𝑁)
∈ ℝ → ((⌊‘𝑁) − 1) ∈
ℝ) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘𝑁) −
1) ∈ ℝ) |
64 | | 6nn 11066 |
. . . . . . . . 9
⊢ 6 ∈
ℕ |
65 | | nndivre 10933 |
. . . . . . . . 9
⊢
((((⌊‘𝑁)
− 1) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 1) / 6) ∈
ℝ) |
66 | 63, 64, 65 | sylancl 693 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(((⌊‘𝑁) −
1) / 6) ∈ ℝ) |
67 | | reflcl 12459 |
. . . . . . . 8
⊢
((((⌊‘𝑁)
− 1) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈
ℝ) |
68 | 66, 67 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 1) / 6)) ∈
ℝ) |
69 | | 5re 10976 |
. . . . . . . . . . 11
⊢ 5 ∈
ℝ |
70 | | resubcl 10224 |
. . . . . . . . . . 11
⊢
(((⌊‘𝑁)
∈ ℝ ∧ 5 ∈ ℝ) → ((⌊‘𝑁) − 5) ∈
ℝ) |
71 | 61, 69, 70 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘𝑁) −
5) ∈ ℝ) |
72 | | nndivre 10933 |
. . . . . . . . . 10
⊢
((((⌊‘𝑁)
− 5) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 5) / 6) ∈
ℝ) |
73 | 71, 64, 72 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(((⌊‘𝑁) −
5) / 6) ∈ ℝ) |
74 | | reflcl 12459 |
. . . . . . . . 9
⊢
((((⌊‘𝑁)
− 5) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈
ℝ) |
75 | 73, 74 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 5) / 6)) ∈
ℝ) |
76 | | peano2re 10088 |
. . . . . . . 8
⊢
((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ →
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈
ℝ) |
77 | 75, 76 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈
ℝ) |
78 | | peano2rem 10227 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
79 | 78 | adantr 480 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (𝑁 − 1) ∈
ℝ) |
80 | | nndivre 10933 |
. . . . . . . 8
⊢ (((𝑁 − 1) ∈ ℝ ∧
6 ∈ ℕ) → ((𝑁 − 1) / 6) ∈
ℝ) |
81 | 79, 64, 80 | sylancl 693 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((𝑁 − 1) / 6) ∈
ℝ) |
82 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 𝑁 ∈ ℝ) |
83 | | resubcl 10224 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 5 ∈
ℝ) → (𝑁 −
5) ∈ ℝ) |
84 | 82, 69, 83 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (𝑁 − 5) ∈
ℝ) |
85 | | nndivre 10933 |
. . . . . . . . 9
⊢ (((𝑁 − 5) ∈ ℝ ∧
6 ∈ ℕ) → ((𝑁 − 5) / 6) ∈
ℝ) |
86 | 84, 64, 85 | sylancl 693 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((𝑁 − 5) / 6) ∈
ℝ) |
87 | | peano2re 10088 |
. . . . . . . 8
⊢ (((𝑁 − 5) / 6) ∈ ℝ
→ (((𝑁 − 5) / 6)
+ 1) ∈ ℝ) |
88 | 86, 87 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (((𝑁 − 5) / 6) + 1) ∈
ℝ) |
89 | | flle 12462 |
. . . . . . . . 9
⊢
((((⌊‘𝑁)
− 1) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤
(((⌊‘𝑁) −
1) / 6)) |
90 | 66, 89 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 1) / 6)) ≤
(((⌊‘𝑁) −
1) / 6)) |
91 | | 1re 9918 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
92 | 91 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 1 ∈
ℝ) |
93 | | flle 12462 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ →
(⌊‘𝑁) ≤
𝑁) |
94 | 93 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘𝑁) ≤
𝑁) |
95 | 61, 82, 92, 94 | lesub1dd 10522 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘𝑁) −
1) ≤ (𝑁 −
1)) |
96 | | 6re 10978 |
. . . . . . . . . . 11
⊢ 6 ∈
ℝ |
97 | 96 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 6 ∈
ℝ) |
98 | | 6pos 10996 |
. . . . . . . . . . 11
⊢ 0 <
6 |
99 | 98 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 0 <
6) |
100 | | lediv1 10767 |
. . . . . . . . . 10
⊢
((((⌊‘𝑁)
− 1) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ (6 ∈
ℝ ∧ 0 < 6)) → (((⌊‘𝑁) − 1) ≤ (𝑁 − 1) ↔ (((⌊‘𝑁) − 1) / 6) ≤ ((𝑁 − 1) /
6))) |
101 | 63, 79, 97, 99, 100 | syl112anc 1322 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(((⌊‘𝑁) −
1) ≤ (𝑁 − 1)
↔ (((⌊‘𝑁)
− 1) / 6) ≤ ((𝑁
− 1) / 6))) |
102 | 95, 101 | mpbid 221 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(((⌊‘𝑁) −
1) / 6) ≤ ((𝑁 − 1)
/ 6)) |
103 | 68, 66, 81, 90, 102 | letrd 10073 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ ((𝑁 − 1) / 6)) |
104 | | flle 12462 |
. . . . . . . . . 10
⊢
((((⌊‘𝑁)
− 5) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 5) / 6)) ≤
(((⌊‘𝑁) −
5) / 6)) |
105 | 73, 104 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 5) / 6)) ≤
(((⌊‘𝑁) −
5) / 6)) |
106 | 69 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 5 ∈
ℝ) |
107 | 61, 82, 106, 94 | lesub1dd 10522 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘𝑁) −
5) ≤ (𝑁 −
5)) |
108 | | lediv1 10767 |
. . . . . . . . . . 11
⊢
((((⌊‘𝑁)
− 5) ∈ ℝ ∧ (𝑁 − 5) ∈ ℝ ∧ (6 ∈
ℝ ∧ 0 < 6)) → (((⌊‘𝑁) − 5) ≤ (𝑁 − 5) ↔ (((⌊‘𝑁) − 5) / 6) ≤ ((𝑁 − 5) /
6))) |
109 | 71, 84, 97, 99, 108 | syl112anc 1322 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(((⌊‘𝑁) −
5) ≤ (𝑁 − 5)
↔ (((⌊‘𝑁)
− 5) / 6) ≤ ((𝑁
− 5) / 6))) |
110 | 107, 109 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(((⌊‘𝑁) −
5) / 6) ≤ ((𝑁 − 5)
/ 6)) |
111 | 75, 73, 86, 105, 110 | letrd 10073 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 5) / 6)) ≤ ((𝑁 − 5) / 6)) |
112 | 75, 86, 92, 111 | leadd1dd 10520 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ≤ (((𝑁 − 5) / 6) +
1)) |
113 | 68, 77, 81, 88, 103, 112 | le2addd 10525 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘(((⌊‘𝑁) − 1) / 6)) +
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) ≤ (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) +
1))) |
114 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (𝑘 mod 6) ∈
V |
115 | 114 | elpr 4146 |
. . . . . . . . . . . 12
⊢ ((𝑘 mod 6) ∈ {1, 5} ↔
((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)) |
116 | 115 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(4...(⌊‘𝑁))
→ ((𝑘 mod 6) ∈
{1, 5} ↔ ((𝑘 mod 6) =
1 ∨ (𝑘 mod 6) =
5))) |
117 | 116 | rabbiia 3161 |
. . . . . . . . . 10
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} = {𝑘 ∈
(4...(⌊‘𝑁))
∣ ((𝑘 mod 6) = 1 ∨
(𝑘 mod 6) =
5)} |
118 | | unrab 3857 |
. . . . . . . . . 10
⊢ ({𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
∪ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}) =
{𝑘 ∈
(4...(⌊‘𝑁))
∣ ((𝑘 mod 6) = 1 ∨
(𝑘 mod 6) =
5)} |
119 | 117, 118 | eqtr4i 2635 |
. . . . . . . . 9
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} = ({𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
∪ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) =
5}) |
120 | 119 | fveq2i 6106 |
. . . . . . . 8
⊢
(#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) = (#‘({𝑘
∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})) |
121 | | ssrab2 3650 |
. . . . . . . . . 10
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
⊆ (4...(⌊‘𝑁)) |
122 | | ssfi 8065 |
. . . . . . . . . 10
⊢
(((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ⊆
(4...(⌊‘𝑁)))
→ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
∈ Fin) |
123 | 10, 121, 122 | mp2an 704 |
. . . . . . . . 9
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
∈ Fin |
124 | | ssrab2 3650 |
. . . . . . . . . 10
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}
⊆ (4...(⌊‘𝑁)) |
125 | | ssfi 8065 |
. . . . . . . . . 10
⊢
(((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ⊆
(4...(⌊‘𝑁)))
→ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}
∈ Fin) |
126 | 10, 124, 125 | mp2an 704 |
. . . . . . . . 9
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}
∈ Fin |
127 | | inrab 3858 |
. . . . . . . . . 10
⊢ ({𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
∩ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}) =
{𝑘 ∈
(4...(⌊‘𝑁))
∣ ((𝑘 mod 6) = 1
∧ (𝑘 mod 6) =
5)} |
128 | | rabeq0 3911 |
. . . . . . . . . . 11
⊢ ({𝑘 ∈
(4...(⌊‘𝑁))
∣ ((𝑘 mod 6) = 1
∧ (𝑘 mod 6) = 5)} =
∅ ↔ ∀𝑘
∈ (4...(⌊‘𝑁)) ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)) |
129 | | 1lt5 11080 |
. . . . . . . . . . . . . 14
⊢ 1 <
5 |
130 | 91, 129 | ltneii 10029 |
. . . . . . . . . . . . 13
⊢ 1 ≠
5 |
131 | | eqtr2 2630 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5) → 1 =
5) |
132 | 131 | necon3ai 2807 |
. . . . . . . . . . . . 13
⊢ (1 ≠ 5
→ ¬ ((𝑘 mod 6) = 1
∧ (𝑘 mod 6) =
5)) |
133 | 130, 132 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ¬
((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5) |
134 | 133 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(4...(⌊‘𝑁))
→ ¬ ((𝑘 mod 6) = 1
∧ (𝑘 mod 6) =
5)) |
135 | 128, 134 | mprgbir 2911 |
. . . . . . . . . 10
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ ((𝑘 mod 6) = 1
∧ (𝑘 mod 6) = 5)} =
∅ |
136 | 127, 135 | eqtri 2632 |
. . . . . . . . 9
⊢ ({𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
∩ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}) =
∅ |
137 | | hashun 13032 |
. . . . . . . . 9
⊢ (({𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
∈ Fin ∧ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}
∈ Fin ∧ ({𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
∩ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}) =
∅) → (#‘({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})) = ((#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}) +
(#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) =
5}))) |
138 | 123, 126,
136, 137 | mp3an 1416 |
. . . . . . . 8
⊢
(#‘({𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
∪ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5})) =
((#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}) +
(#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) =
5})) |
139 | 120, 138 | eqtri 2632 |
. . . . . . 7
⊢
(#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) = ((#‘{𝑘
∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})) |
140 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(4...(⌊‘𝑁))
→ 𝑘 ∈
ℤ) |
141 | | nnrp 11718 |
. . . . . . . . . . . . . . . . 17
⊢ (6 ∈
ℕ → 6 ∈ ℝ+) |
142 | 64, 141 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ 6 ∈
ℝ+ |
143 | | 0le1 10430 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≤
1 |
144 | | 1lt6 11085 |
. . . . . . . . . . . . . . . 16
⊢ 1 <
6 |
145 | | modid 12557 |
. . . . . . . . . . . . . . . 16
⊢ (((1
∈ ℝ ∧ 6 ∈ ℝ+) ∧ (0 ≤ 1 ∧ 1 <
6)) → (1 mod 6) = 1) |
146 | 91, 142, 143, 144, 145 | mp4an 705 |
. . . . . . . . . . . . . . 15
⊢ (1 mod 6)
= 1 |
147 | 146 | eqeq2i 2622 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 mod 6) = (1 mod 6) ↔
(𝑘 mod 6) =
1) |
148 | | 1z 11284 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℤ |
149 | | moddvds 14829 |
. . . . . . . . . . . . . . 15
⊢ ((6
∈ ℕ ∧ 𝑘
∈ ℤ ∧ 1 ∈ ℤ) → ((𝑘 mod 6) = (1 mod 6) ↔ 6 ∥ (𝑘 − 1))) |
150 | 64, 148, 149 | mp3an13 1407 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = (1 mod 6) ↔ 6
∥ (𝑘 −
1))) |
151 | 147, 150 | syl5bbr 273 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = 1 ↔ 6 ∥
(𝑘 −
1))) |
152 | 140, 151 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(4...(⌊‘𝑁))
→ ((𝑘 mod 6) = 1
↔ 6 ∥ (𝑘 −
1))) |
153 | 152 | rabbiia 3161 |
. . . . . . . . . . 11
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1} =
{𝑘 ∈
(4...(⌊‘𝑁))
∣ 6 ∥ (𝑘
− 1)} |
154 | 153 | fveq2i 6106 |
. . . . . . . . . 10
⊢
(#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}) =
(#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ 6 ∥ (𝑘
− 1)}) |
155 | 64 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 6 ∈
ℕ) |
156 | | 4z 11288 |
. . . . . . . . . . . 12
⊢ 4 ∈
ℤ |
157 | 156 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 4 ∈
ℤ) |
158 | 38 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ (4
− 1) = ((3 + 1) − 1) |
159 | | 3cn 10972 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℂ |
160 | | ax-1cn 9873 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
161 | 159, 160 | pncan3oi 10176 |
. . . . . . . . . . . . . 14
⊢ ((3 + 1)
− 1) = 3 |
162 | 158, 161 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ (4
− 1) = 3 |
163 | 162 | fveq2i 6106 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘(4 − 1)) =
(ℤ≥‘3) |
164 | 35, 163 | syl6eleqr 2699 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘𝑁) ∈
(ℤ≥‘(4 − 1))) |
165 | 148 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 1 ∈
ℤ) |
166 | 155, 157,
164, 165 | hashdvds 15318 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ 6 ∥ (𝑘
− 1)}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) −
(⌊‘(((4 − 1) − 1) / 6)))) |
167 | 154, 166 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}) =
((⌊‘(((⌊‘𝑁) − 1) / 6)) −
(⌊‘(((4 − 1) − 1) / 6)))) |
168 | | df-3 10957 |
. . . . . . . . . . . . . . . . 17
⊢ 3 = (2 +
1) |
169 | 162, 168 | eqtri 2632 |
. . . . . . . . . . . . . . . 16
⊢ (4
− 1) = (2 + 1) |
170 | 169 | oveq1i 6559 |
. . . . . . . . . . . . . . 15
⊢ ((4
− 1) − 1) = ((2 + 1) − 1) |
171 | | 2cn 10968 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℂ |
172 | 171, 160 | pncan3oi 10176 |
. . . . . . . . . . . . . . 15
⊢ ((2 + 1)
− 1) = 2 |
173 | 170, 172 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢ ((4
− 1) − 1) = 2 |
174 | 173 | oveq1i 6559 |
. . . . . . . . . . . . 13
⊢ (((4
− 1) − 1) / 6) = (2 / 6) |
175 | 174 | fveq2i 6106 |
. . . . . . . . . . . 12
⊢
(⌊‘(((4 − 1) − 1) / 6)) = (⌊‘(2 /
6)) |
176 | | 0re 9919 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
177 | 64 | nnne0i 10932 |
. . . . . . . . . . . . . . 15
⊢ 6 ≠
0 |
178 | 7, 96, 177 | redivcli 10671 |
. . . . . . . . . . . . . 14
⊢ (2 / 6)
∈ ℝ |
179 | | 2pos 10989 |
. . . . . . . . . . . . . . 15
⊢ 0 <
2 |
180 | 7, 96, 179, 98 | divgt0ii 10820 |
. . . . . . . . . . . . . 14
⊢ 0 < (2
/ 6) |
181 | 176, 178,
180 | ltleii 10039 |
. . . . . . . . . . . . 13
⊢ 0 ≤ (2
/ 6) |
182 | | 2lt6 11084 |
. . . . . . . . . . . . . . . 16
⊢ 2 <
6 |
183 | | 6cn 10979 |
. . . . . . . . . . . . . . . . 17
⊢ 6 ∈
ℂ |
184 | 183 | mulid1i 9921 |
. . . . . . . . . . . . . . . 16
⊢ (6
· 1) = 6 |
185 | 182, 184 | breqtrri 4610 |
. . . . . . . . . . . . . . 15
⊢ 2 < (6
· 1) |
186 | 96, 98 | pm3.2i 470 |
. . . . . . . . . . . . . . . 16
⊢ (6 ∈
ℝ ∧ 0 < 6) |
187 | | ltdivmul 10777 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℝ ∧ 1 ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6))
→ ((2 / 6) < 1 ↔ 2 < (6 · 1))) |
188 | 7, 91, 186, 187 | mp3an 1416 |
. . . . . . . . . . . . . . 15
⊢ ((2 / 6)
< 1 ↔ 2 < (6 · 1)) |
189 | 185, 188 | mpbir 220 |
. . . . . . . . . . . . . 14
⊢ (2 / 6)
< 1 |
190 | | 1e0p1 11428 |
. . . . . . . . . . . . . 14
⊢ 1 = (0 +
1) |
191 | 189, 190 | breqtri 4608 |
. . . . . . . . . . . . 13
⊢ (2 / 6)
< (0 + 1) |
192 | | 0z 11265 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℤ |
193 | | flbi 12479 |
. . . . . . . . . . . . . 14
⊢ (((2 / 6)
∈ ℝ ∧ 0 ∈ ℤ) → ((⌊‘(2 / 6)) = 0
↔ (0 ≤ (2 / 6) ∧ (2 / 6) < (0 + 1)))) |
194 | 178, 192,
193 | mp2an 704 |
. . . . . . . . . . . . 13
⊢
((⌊‘(2 / 6)) = 0 ↔ (0 ≤ (2 / 6) ∧ (2 / 6) <
(0 + 1))) |
195 | 181, 191,
194 | mpbir2an 957 |
. . . . . . . . . . . 12
⊢
(⌊‘(2 / 6)) = 0 |
196 | 175, 195 | eqtri 2632 |
. . . . . . . . . . 11
⊢
(⌊‘(((4 − 1) − 1) / 6)) = 0 |
197 | 196 | oveq2i 6560 |
. . . . . . . . . 10
⊢
((⌊‘(((⌊‘𝑁) − 1) / 6)) −
(⌊‘(((4 − 1) − 1) / 6))) =
((⌊‘(((⌊‘𝑁) − 1) / 6)) −
0) |
198 | 66 | flcld 12461 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 1) / 6)) ∈
ℤ) |
199 | 198 | zcnd 11359 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 1) / 6)) ∈
ℂ) |
200 | 199 | subid1d 10260 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘(((⌊‘𝑁) − 1) / 6)) − 0) =
(⌊‘(((⌊‘𝑁) − 1) / 6))) |
201 | 197, 200 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘(((⌊‘𝑁) − 1) / 6)) −
(⌊‘(((4 − 1) − 1) / 6))) =
(⌊‘(((⌊‘𝑁) − 1) / 6))) |
202 | 167, 201 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}) =
(⌊‘(((⌊‘𝑁) − 1) / 6))) |
203 | | 5pos 10995 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
5 |
204 | 176, 69, 203 | ltleii 10039 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≤
5 |
205 | | 5lt6 11081 |
. . . . . . . . . . . . . . . 16
⊢ 5 <
6 |
206 | | modid 12557 |
. . . . . . . . . . . . . . . 16
⊢ (((5
∈ ℝ ∧ 6 ∈ ℝ+) ∧ (0 ≤ 5 ∧ 5 <
6)) → (5 mod 6) = 5) |
207 | 69, 142, 204, 205, 206 | mp4an 705 |
. . . . . . . . . . . . . . 15
⊢ (5 mod 6)
= 5 |
208 | 207 | eqeq2i 2622 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 mod 6) = (5 mod 6) ↔
(𝑘 mod 6) =
5) |
209 | | 5nn 11065 |
. . . . . . . . . . . . . . . 16
⊢ 5 ∈
ℕ |
210 | 209 | nnzi 11278 |
. . . . . . . . . . . . . . 15
⊢ 5 ∈
ℤ |
211 | | moddvds 14829 |
. . . . . . . . . . . . . . 15
⊢ ((6
∈ ℕ ∧ 𝑘
∈ ℤ ∧ 5 ∈ ℤ) → ((𝑘 mod 6) = (5 mod 6) ↔ 6 ∥ (𝑘 − 5))) |
212 | 64, 210, 211 | mp3an13 1407 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = (5 mod 6) ↔ 6
∥ (𝑘 −
5))) |
213 | 208, 212 | syl5bbr 273 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = 5 ↔ 6 ∥
(𝑘 −
5))) |
214 | 140, 213 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(4...(⌊‘𝑁))
→ ((𝑘 mod 6) = 5
↔ 6 ∥ (𝑘 −
5))) |
215 | 214 | rabbiia 3161 |
. . . . . . . . . . 11
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5} =
{𝑘 ∈
(4...(⌊‘𝑁))
∣ 6 ∥ (𝑘
− 5)} |
216 | 215 | fveq2i 6106 |
. . . . . . . . . 10
⊢
(#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}) =
(#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ 6 ∥ (𝑘
− 5)}) |
217 | 210 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 5 ∈
ℤ) |
218 | 155, 157,
164, 217 | hashdvds 15318 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ 6 ∥ (𝑘
− 5)}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) −
(⌊‘(((4 − 1) − 5) / 6)))) |
219 | 216, 218 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}) =
((⌊‘(((⌊‘𝑁) − 5) / 6)) −
(⌊‘(((4 − 1) − 5) / 6)))) |
220 | 162 | oveq1i 6559 |
. . . . . . . . . . . . . . . 16
⊢ ((4
− 1) − 5) = (3 − 5) |
221 | | 5cn 10977 |
. . . . . . . . . . . . . . . . 17
⊢ 5 ∈
ℂ |
222 | 221, 159 | negsubdi2i 10246 |
. . . . . . . . . . . . . . . 16
⊢ -(5
− 3) = (3 − 5) |
223 | | 3p2e5 11037 |
. . . . . . . . . . . . . . . . . . 19
⊢ (3 + 2) =
5 |
224 | 223 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . 18
⊢ ((3 + 2)
− 3) = (5 − 3) |
225 | | pncan2 10167 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((3
∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) =
2) |
226 | 159, 171,
225 | mp2an 704 |
. . . . . . . . . . . . . . . . . 18
⊢ ((3 + 2)
− 3) = 2 |
227 | 224, 226 | eqtr3i 2634 |
. . . . . . . . . . . . . . . . 17
⊢ (5
− 3) = 2 |
228 | 227 | negeqi 10153 |
. . . . . . . . . . . . . . . 16
⊢ -(5
− 3) = -2 |
229 | 220, 222,
228 | 3eqtr2i 2638 |
. . . . . . . . . . . . . . 15
⊢ ((4
− 1) − 5) = -2 |
230 | 229 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ (((4
− 1) − 5) / 6) = (-2 / 6) |
231 | | divneg 10598 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 6 ∈ ℂ ∧ 6 ≠ 0) → -(2 / 6) = (-2 /
6)) |
232 | 171, 183,
177, 231 | mp3an 1416 |
. . . . . . . . . . . . . 14
⊢ -(2 / 6)
= (-2 / 6) |
233 | 230, 232 | eqtr4i 2635 |
. . . . . . . . . . . . 13
⊢ (((4
− 1) − 5) / 6) = -(2 / 6) |
234 | 233 | fveq2i 6106 |
. . . . . . . . . . . 12
⊢
(⌊‘(((4 − 1) − 5) / 6)) = (⌊‘-(2 /
6)) |
235 | 178, 91, 189 | ltleii 10039 |
. . . . . . . . . . . . . 14
⊢ (2 / 6)
≤ 1 |
236 | 178, 91 | lenegi 10452 |
. . . . . . . . . . . . . 14
⊢ ((2 / 6)
≤ 1 ↔ -1 ≤ -(2 / 6)) |
237 | 235, 236 | mpbi 219 |
. . . . . . . . . . . . 13
⊢ -1 ≤
-(2 / 6) |
238 | 176, 178 | ltnegi 10451 |
. . . . . . . . . . . . . . 15
⊢ (0 <
(2 / 6) ↔ -(2 / 6) < -0) |
239 | 180, 238 | mpbi 219 |
. . . . . . . . . . . . . 14
⊢ -(2 / 6)
< -0 |
240 | | neg0 10206 |
. . . . . . . . . . . . . . . 16
⊢ -0 =
0 |
241 | | 1pneg1e0 11006 |
. . . . . . . . . . . . . . . 16
⊢ (1 + -1)
= 0 |
242 | 240, 241 | eqtr4i 2635 |
. . . . . . . . . . . . . . 15
⊢ -0 = (1 +
-1) |
243 | | neg1cn 11001 |
. . . . . . . . . . . . . . . 16
⊢ -1 ∈
ℂ |
244 | 243, 160 | addcomi 10106 |
. . . . . . . . . . . . . . 15
⊢ (-1 + 1)
= (1 + -1) |
245 | 242, 244 | eqtr4i 2635 |
. . . . . . . . . . . . . 14
⊢ -0 = (-1
+ 1) |
246 | 239, 245 | breqtri 4608 |
. . . . . . . . . . . . 13
⊢ -(2 / 6)
< (-1 + 1) |
247 | 178 | renegcli 10221 |
. . . . . . . . . . . . . 14
⊢ -(2 / 6)
∈ ℝ |
248 | | neg1z 11290 |
. . . . . . . . . . . . . 14
⊢ -1 ∈
ℤ |
249 | | flbi 12479 |
. . . . . . . . . . . . . 14
⊢ ((-(2 /
6) ∈ ℝ ∧ -1 ∈ ℤ) → ((⌊‘-(2 / 6)) =
-1 ↔ (-1 ≤ -(2 / 6) ∧ -(2 / 6) < (-1 + 1)))) |
250 | 247, 248,
249 | mp2an 704 |
. . . . . . . . . . . . 13
⊢
((⌊‘-(2 / 6)) = -1 ↔ (-1 ≤ -(2 / 6) ∧ -(2 / 6)
< (-1 + 1))) |
251 | 237, 246,
250 | mpbir2an 957 |
. . . . . . . . . . . 12
⊢
(⌊‘-(2 / 6)) = -1 |
252 | 234, 251 | eqtri 2632 |
. . . . . . . . . . 11
⊢
(⌊‘(((4 − 1) − 5) / 6)) = -1 |
253 | 252 | oveq2i 6560 |
. . . . . . . . . 10
⊢
((⌊‘(((⌊‘𝑁) − 5) / 6)) −
(⌊‘(((4 − 1) − 5) / 6))) =
((⌊‘(((⌊‘𝑁) − 5) / 6)) −
-1) |
254 | 73 | flcld 12461 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 5) / 6)) ∈
ℤ) |
255 | 254 | zcnd 11359 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 5) / 6)) ∈
ℂ) |
256 | | subneg 10209 |
. . . . . . . . . . 11
⊢
(((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℂ ∧ 1
∈ ℂ) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1) =
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) |
257 | 255, 160,
256 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1) =
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) |
258 | 253, 257 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘(((⌊‘𝑁) − 5) / 6)) −
(⌊‘(((4 − 1) − 5) / 6))) =
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) |
259 | 219, 258 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}) =
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) |
260 | 202, 259 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}) +
(#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5})) =
((⌊‘(((⌊‘𝑁) − 1) / 6)) +
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))) |
261 | 139, 260 | syl5eq 2656 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) +
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))) |
262 | 82 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 𝑁 ∈ ℂ) |
263 | 262 | 2timesd 11152 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (2 · 𝑁) = (𝑁 + 𝑁)) |
264 | | df-6 10960 |
. . . . . . . . . . . . . 14
⊢ 6 = (5 +
1) |
265 | 221, 160 | addcomi 10106 |
. . . . . . . . . . . . . 14
⊢ (5 + 1) =
(1 + 5) |
266 | 264, 265 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ 6 = (1 +
5) |
267 | 266 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 6 = (1 +
5)) |
268 | 263, 267 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((2 ·
𝑁) − 6) = ((𝑁 + 𝑁) − (1 + 5))) |
269 | | addsub4 10203 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ (1 ∈
ℂ ∧ 5 ∈ ℂ)) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5))) |
270 | 160, 221,
269 | mpanr12 717 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5))) |
271 | 262, 262,
270 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5))) |
272 | 268, 271 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((2 ·
𝑁) − 6) = ((𝑁 − 1) + (𝑁 − 5))) |
273 | 272 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (((2 ·
𝑁) − 6) / 6) =
(((𝑁 − 1) + (𝑁 − 5)) /
6)) |
274 | | mulcl 9899 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 𝑁
∈ ℂ) → (2 · 𝑁) ∈ ℂ) |
275 | 171, 262,
274 | sylancr 694 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (2 · 𝑁) ∈
ℂ) |
276 | 183, 177 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (6 ∈
ℂ ∧ 6 ≠ 0) |
277 | | divsubdir 10600 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑁) ∈ ℂ
∧ 6 ∈ ℂ ∧ (6 ∈ ℂ ∧ 6 ≠ 0)) → (((2
· 𝑁) − 6) / 6)
= (((2 · 𝑁) / 6)
− (6 / 6))) |
278 | 183, 276,
277 | mp3an23 1408 |
. . . . . . . . . . 11
⊢ ((2
· 𝑁) ∈ ℂ
→ (((2 · 𝑁)
− 6) / 6) = (((2 · 𝑁) / 6) − (6 / 6))) |
279 | 275, 278 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (((2 ·
𝑁) − 6) / 6) = (((2
· 𝑁) / 6) − (6
/ 6))) |
280 | | 3t2e6 11056 |
. . . . . . . . . . . . . 14
⊢ (3
· 2) = 6 |
281 | 159, 171 | mulcomi 9925 |
. . . . . . . . . . . . . 14
⊢ (3
· 2) = (2 · 3) |
282 | 280, 281 | eqtr3i 2634 |
. . . . . . . . . . . . 13
⊢ 6 = (2
· 3) |
283 | 282 | oveq2i 6560 |
. . . . . . . . . . . 12
⊢ ((2
· 𝑁) / 6) = ((2
· 𝑁) / (2 ·
3)) |
284 | | 3ne0 10992 |
. . . . . . . . . . . . . . 15
⊢ 3 ≠
0 |
285 | 159, 284 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) |
286 | | 2cnne0 11119 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
287 | | divcan5 10606 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℂ ∧ (3 ∈
ℂ ∧ 3 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2
· 𝑁) / (2 ·
3)) = (𝑁 /
3)) |
288 | 285, 286,
287 | mp3an23 1408 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℂ → ((2
· 𝑁) / (2 ·
3)) = (𝑁 /
3)) |
289 | 262, 288 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((2 ·
𝑁) / (2 · 3)) =
(𝑁 / 3)) |
290 | 283, 289 | syl5eq 2656 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((2 ·
𝑁) / 6) = (𝑁 / 3)) |
291 | 183, 177 | dividi 10637 |
. . . . . . . . . . . 12
⊢ (6 / 6) =
1 |
292 | 291 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (6 / 6) =
1) |
293 | 290, 292 | oveq12d 6567 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (((2 ·
𝑁) / 6) − (6 / 6)) =
((𝑁 / 3) −
1)) |
294 | 279, 293 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (((2 ·
𝑁) − 6) / 6) =
((𝑁 / 3) −
1)) |
295 | 79 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (𝑁 − 1) ∈
ℂ) |
296 | 84 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (𝑁 − 5) ∈
ℂ) |
297 | | divdir 10589 |
. . . . . . . . . . 11
⊢ (((𝑁 − 1) ∈ ℂ ∧
(𝑁 − 5) ∈
ℂ ∧ (6 ∈ ℂ ∧ 6 ≠ 0)) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6))) |
298 | 276, 297 | mp3an3 1405 |
. . . . . . . . . 10
⊢ (((𝑁 − 1) ∈ ℂ ∧
(𝑁 − 5) ∈
ℂ) → (((𝑁
− 1) + (𝑁 − 5))
/ 6) = (((𝑁 − 1) / 6)
+ ((𝑁 − 5) /
6))) |
299 | 295, 296,
298 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6))) |
300 | 273, 294,
299 | 3eqtr3d 2652 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((𝑁 / 3) − 1) = (((𝑁 − 1) / 6) + ((𝑁 − 5) /
6))) |
301 | 300 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (((𝑁 / 3) − 1) + 1) =
((((𝑁 − 1) / 6) +
((𝑁 − 5) / 6)) +
1)) |
302 | 21 | recnd 9947 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (𝑁 / 3) ∈
ℂ) |
303 | | npcan 10169 |
. . . . . . . 8
⊢ (((𝑁 / 3) ∈ ℂ ∧ 1
∈ ℂ) → (((𝑁
/ 3) − 1) + 1) = (𝑁 /
3)) |
304 | 302, 160,
303 | sylancl 693 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3)) |
305 | 81 | recnd 9947 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((𝑁 − 1) / 6) ∈
ℂ) |
306 | 86 | recnd 9947 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((𝑁 − 5) / 6) ∈
ℂ) |
307 | 160 | a1i 11 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 1 ∈
ℂ) |
308 | 305, 306,
307 | addassd 9941 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)) + 1) =
(((𝑁 − 1) / 6) +
(((𝑁 − 5) / 6) +
1))) |
309 | 301, 304,
308 | 3eqtr3d 2652 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (𝑁 / 3) = (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1))) |
310 | 113, 261,
309 | 3brtr4d 4615 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (#‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) ≤ (𝑁 /
3)) |
311 | 9, 17, 21, 59, 310 | letrd 10073 |
. . . 4
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((π‘𝑁)
− 2) ≤ (𝑁 /
3)) |
312 | 7 | a1i 11 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 2 ∈
ℝ) |
313 | 6, 312, 21 | lesubaddd 10503 |
. . . 4
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(((π‘𝑁)
− 2) ≤ (𝑁 / 3)
↔ (π‘𝑁) ≤ ((𝑁 / 3) + 2))) |
314 | 311, 313 | mpbid 221 |
. . 3
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(π‘𝑁) ≤
((𝑁 / 3) +
2)) |
315 | 314 | adantlr 747 |
. 2
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 3 ≤ 𝑁) →
(π‘𝑁) ≤
((𝑁 / 3) +
2)) |
316 | 5 | ad2antrr 758 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ∈
ℝ) |
317 | 7 | a1i 11 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → 2 ∈
ℝ) |
318 | 20 | ad2antrr 758 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → (𝑁 / 3) ∈ ℝ) |
319 | | readdcl 9898 |
. . . 4
⊢ (((𝑁 / 3) ∈ ℝ ∧ 2
∈ ℝ) → ((𝑁
/ 3) + 2) ∈ ℝ) |
320 | 318, 7, 319 | sylancl 693 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → ((𝑁 / 3) + 2) ∈ ℝ) |
321 | | ppiwordi 24688 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 3 ∈
ℝ ∧ 𝑁 ≤ 3)
→ (π‘𝑁) ≤
(π‘3)) |
322 | 1, 321 | mp3an2 1404 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 𝑁 ≤ 3) →
(π‘𝑁) ≤
(π‘3)) |
323 | 322 | adantlr 747 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤
(π‘3)) |
324 | 323, 24 | syl6breq 4624 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ 2) |
325 | | 3pos 10991 |
. . . . . 6
⊢ 0 <
3 |
326 | | divge0 10771 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ (3 ∈ ℝ
∧ 0 < 3)) → 0 ≤ (𝑁 / 3)) |
327 | 1, 325, 326 | mpanr12 717 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) → 0 ≤ (𝑁 / 3)) |
328 | 327 | adantr 480 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → 0 ≤ (𝑁 / 3)) |
329 | | addge02 10418 |
. . . . 5
⊢ ((2
∈ ℝ ∧ (𝑁 /
3) ∈ ℝ) → (0 ≤ (𝑁 / 3) ↔ 2 ≤ ((𝑁 / 3) + 2))) |
330 | 7, 318, 329 | sylancr 694 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → (0 ≤ (𝑁 / 3) ↔ 2 ≤ ((𝑁 / 3) + 2))) |
331 | 328, 330 | mpbid 221 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → 2 ≤ ((𝑁 / 3) + 2)) |
332 | 316, 317,
320, 324, 331 | letrd 10073 |
. 2
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ ((𝑁 / 3) + 2)) |
333 | 2, 3, 315, 332 | lecasei 10022 |
1
⊢ ((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) →
(π‘𝑁) ≤
((𝑁 / 3) +
2)) |