Step | Hyp | Ref
| Expression |
1 | | 3re 11286 |
. . 3
⊢ 3 ∈
ℝ |
2 | 1 | a1i 11 |
. 2
⊢ ((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) → 3 ∈
ℝ) |
3 | | simpl 474 |
. 2
⊢ ((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) → 𝑁 ∈ ℝ) |
4 | | ppicl 25056 |
. . . . . . . 8
⊢ (𝑁 ∈ ℝ →
(π‘𝑁)
∈ ℕ0) |
5 | 4 | nn0red 11544 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ →
(π‘𝑁)
∈ ℝ) |
6 | 5 | adantr 472 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(π‘𝑁)
∈ ℝ) |
7 | | 2re 11282 |
. . . . . 6
⊢ 2 ∈
ℝ |
8 | | resubcl 10537 |
. . . . . 6
⊢
(((π‘𝑁) ∈ ℝ ∧ 2 ∈ ℝ)
→ ((π‘𝑁) − 2) ∈
ℝ) |
9 | 6, 7, 8 | sylancl 697 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((π‘𝑁)
− 2) ∈ ℝ) |
10 | | fzfi 12965 |
. . . . . . . . 9
⊢
(4...(⌊‘𝑁)) ∈ Fin |
11 | | ssrab2 3828 |
. . . . . . . . 9
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} ⊆ (4...(⌊‘𝑁)) |
12 | | ssfi 8345 |
. . . . . . . . 9
⊢
(((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ⊆
(4...(⌊‘𝑁)))
→ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} ∈ Fin) |
13 | 10, 11, 12 | mp2an 710 |
. . . . . . . 8
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} ∈ Fin |
14 | | hashcl 13339 |
. . . . . . . 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 11495 |
. . . . . 6
⊢
(♯‘{𝑘
∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈
ℝ |
17 | 16 | a1i 11 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) ∈ ℝ) |
18 | | 3nn 11378 |
. . . . . . 7
⊢ 3 ∈
ℕ |
19 | | nndivre 11248 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ∈
ℕ) → (𝑁 / 3)
∈ ℝ) |
20 | 18, 19 | mpan2 709 |
. . . . . 6
⊢ (𝑁 ∈ ℝ → (𝑁 / 3) ∈
ℝ) |
21 | 20 | adantr 472 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (𝑁 / 3) ∈
ℝ) |
22 | | ppifl 25085 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℝ →
(π‘(⌊‘𝑁)) = (π‘𝑁)) |
23 | 22 | adantr 472 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(π‘(⌊‘𝑁)) = (π‘𝑁)) |
24 | | ppi3 25096 |
. . . . . . . . 9
⊢
(π‘3) = 2 |
25 | 24 | a1i 11 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(π‘3) = 2) |
26 | 23, 25 | oveq12d 6831 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((π‘(⌊‘𝑁)) − (π‘3)) =
((π‘𝑁)
− 2)) |
27 | | 3z 11602 |
. . . . . . . . . . 11
⊢ 3 ∈
ℤ |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 3 ∈
ℤ) |
29 | | flcl 12790 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ →
(⌊‘𝑁) ∈
ℤ) |
30 | 29 | adantr 472 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘𝑁) ∈
ℤ) |
31 | | flge 12800 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 3 ∈
ℤ) → (3 ≤ 𝑁
↔ 3 ≤ (⌊‘𝑁))) |
32 | 27, 31 | mpan2 709 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ → (3 ≤
𝑁 ↔ 3 ≤
(⌊‘𝑁))) |
33 | 32 | biimpa 502 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 3 ≤
(⌊‘𝑁)) |
34 | | eluz2 11885 |
. . . . . . . . . 10
⊢
((⌊‘𝑁)
∈ (ℤ≥‘3) ↔ (3 ∈ ℤ ∧
(⌊‘𝑁) ∈
ℤ ∧ 3 ≤ (⌊‘𝑁))) |
35 | 28, 30, 33, 34 | syl3anbrc 1429 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘𝑁) ∈
(ℤ≥‘3)) |
36 | | ppidif 25088 |
. . . . . . . . 9
⊢
((⌊‘𝑁)
∈ (ℤ≥‘3) →
((π‘(⌊‘𝑁)) − (π‘3)) =
(♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ))) |
37 | 35, 36 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((π‘(⌊‘𝑁)) − (π‘3)) =
(♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ))) |
38 | | df-4 11273 |
. . . . . . . . . . 11
⊢ 4 = (3 +
1) |
39 | 38 | oveq1i 6823 |
. . . . . . . . . 10
⊢
(4...(⌊‘𝑁)) = ((3 + 1)...(⌊‘𝑁)) |
40 | 39 | ineq1i 3953 |
. . . . . . . . 9
⊢
((4...(⌊‘𝑁)) ∩ ℙ) = (((3 +
1)...(⌊‘𝑁))
∩ ℙ) |
41 | 40 | fveq2i 6355 |
. . . . . . . 8
⊢
(♯‘((4...(⌊‘𝑁)) ∩ ℙ)) = (♯‘(((3 +
1)...(⌊‘𝑁))
∩ ℙ)) |
42 | 37, 41 | syl6eqr 2812 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((π‘(⌊‘𝑁)) − (π‘3)) =
(♯‘((4...(⌊‘𝑁)) ∩ ℙ))) |
43 | 26, 42 | eqtr3d 2796 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((π‘𝑁)
− 2) = (♯‘((4...(⌊‘𝑁)) ∩ ℙ))) |
44 | | dfin5 3723 |
. . . . . . . . 9
⊢
((4...(⌊‘𝑁)) ∩ ℙ) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 𝑘 ∈ ℙ} |
45 | | elfzle1 12537 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(4...(⌊‘𝑁))
→ 4 ≤ 𝑘) |
46 | | ppiublem2 25127 |
. . . . . . . . . . . 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 3825 |
. . . . . . . . 9
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ 𝑘 ∈ ℙ}
⊆ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} |
50 | 44, 49 | eqsstri 3776 |
. . . . . . . 8
⊢
((4...(⌊‘𝑁)) ∩ ℙ) ⊆ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} |
51 | | ssdomg 8167 |
. . . . . . . 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 3976 |
. . . . . . . . 9
⊢
((4...(⌊‘𝑁)) ∩ ℙ) ⊆
(4...(⌊‘𝑁)) |
54 | | ssfi 8345 |
. . . . . . . . 9
⊢
(((4...(⌊‘𝑁)) ∈ Fin ∧
((4...(⌊‘𝑁))
∩ ℙ) ⊆ (4...(⌊‘𝑁))) → ((4...(⌊‘𝑁)) ∩ ℙ) ∈
Fin) |
55 | 10, 53, 54 | mp2an 710 |
. . . . . . . 8
⊢
((4...(⌊‘𝑁)) ∩ ℙ) ∈
Fin |
56 | | hashdom 13360 |
. . . . . . . 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 710 |
. . . . . . 7
⊢
((♯‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤
(♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) ↔ ((4...(⌊‘𝑁)) ∩ ℙ) ≼ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) |
58 | 52, 57 | mpbir 221 |
. . . . . 6
⊢
(♯‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤
(♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) |
59 | 43, 58 | syl6eqbr 4843 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((π‘𝑁)
− 2) ≤ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}})) |
60 | | reflcl 12791 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ →
(⌊‘𝑁) ∈
ℝ) |
61 | 60 | adantr 472 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘𝑁) ∈
ℝ) |
62 | | peano2rem 10540 |
. . . . . . . . . 10
⊢
((⌊‘𝑁)
∈ ℝ → ((⌊‘𝑁) − 1) ∈
ℝ) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘𝑁) −
1) ∈ ℝ) |
64 | | 6nn 11381 |
. . . . . . . . 9
⊢ 6 ∈
ℕ |
65 | | nndivre 11248 |
. . . . . . . . 9
⊢
((((⌊‘𝑁)
− 1) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 1) / 6) ∈
ℝ) |
66 | 63, 64, 65 | sylancl 697 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(((⌊‘𝑁) −
1) / 6) ∈ ℝ) |
67 | | reflcl 12791 |
. . . . . . . 8
⊢
((((⌊‘𝑁)
− 1) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈
ℝ) |
68 | 66, 67 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 1) / 6)) ∈
ℝ) |
69 | | 5re 11291 |
. . . . . . . . . . 11
⊢ 5 ∈
ℝ |
70 | | resubcl 10537 |
. . . . . . . . . . 11
⊢
(((⌊‘𝑁)
∈ ℝ ∧ 5 ∈ ℝ) → ((⌊‘𝑁) − 5) ∈
ℝ) |
71 | 61, 69, 70 | sylancl 697 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘𝑁) −
5) ∈ ℝ) |
72 | | nndivre 11248 |
. . . . . . . . . 10
⊢
((((⌊‘𝑁)
− 5) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 5) / 6) ∈
ℝ) |
73 | 71, 64, 72 | sylancl 697 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(((⌊‘𝑁) −
5) / 6) ∈ ℝ) |
74 | | reflcl 12791 |
. . . . . . . . 9
⊢
((((⌊‘𝑁)
− 5) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈
ℝ) |
75 | 73, 74 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 5) / 6)) ∈
ℝ) |
76 | | peano2re 10401 |
. . . . . . . 8
⊢
((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ →
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈
ℝ) |
77 | 75, 76 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈
ℝ) |
78 | | peano2rem 10540 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
79 | 78 | adantr 472 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (𝑁 − 1) ∈
ℝ) |
80 | | nndivre 11248 |
. . . . . . . 8
⊢ (((𝑁 − 1) ∈ ℝ ∧
6 ∈ ℕ) → ((𝑁 − 1) / 6) ∈
ℝ) |
81 | 79, 64, 80 | sylancl 697 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((𝑁 − 1) / 6) ∈
ℝ) |
82 | | simpl 474 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 𝑁 ∈ ℝ) |
83 | | resubcl 10537 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 5 ∈
ℝ) → (𝑁 −
5) ∈ ℝ) |
84 | 82, 69, 83 | sylancl 697 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (𝑁 − 5) ∈
ℝ) |
85 | | nndivre 11248 |
. . . . . . . . 9
⊢ (((𝑁 − 5) ∈ ℝ ∧
6 ∈ ℕ) → ((𝑁 − 5) / 6) ∈
ℝ) |
86 | 84, 64, 85 | sylancl 697 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((𝑁 − 5) / 6) ∈
ℝ) |
87 | | peano2re 10401 |
. . . . . . . 8
⊢ (((𝑁 − 5) / 6) ∈ ℝ
→ (((𝑁 − 5) / 6)
+ 1) ∈ ℝ) |
88 | 86, 87 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (((𝑁 − 5) / 6) + 1) ∈
ℝ) |
89 | | flle 12794 |
. . . . . . . . 9
⊢
((((⌊‘𝑁)
− 1) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤
(((⌊‘𝑁) −
1) / 6)) |
90 | 66, 89 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 1) / 6)) ≤
(((⌊‘𝑁) −
1) / 6)) |
91 | | 1re 10231 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
92 | 91 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 1 ∈
ℝ) |
93 | | flle 12794 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ →
(⌊‘𝑁) ≤
𝑁) |
94 | 93 | adantr 472 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘𝑁) ≤
𝑁) |
95 | 61, 82, 92, 94 | lesub1dd 10835 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘𝑁) −
1) ≤ (𝑁 −
1)) |
96 | | 6re 11293 |
. . . . . . . . . . 11
⊢ 6 ∈
ℝ |
97 | 96 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 6 ∈
ℝ) |
98 | | 6pos 11311 |
. . . . . . . . . . 11
⊢ 0 <
6 |
99 | 98 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 0 <
6) |
100 | | lediv1 11080 |
. . . . . . . . . 10
⊢
((((⌊‘𝑁)
− 1) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ (6 ∈
ℝ ∧ 0 < 6)) → (((⌊‘𝑁) − 1) ≤ (𝑁 − 1) ↔ (((⌊‘𝑁) − 1) / 6) ≤ ((𝑁 − 1) /
6))) |
101 | 63, 79, 97, 99, 100 | syl112anc 1481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(((⌊‘𝑁) −
1) ≤ (𝑁 − 1)
↔ (((⌊‘𝑁)
− 1) / 6) ≤ ((𝑁
− 1) / 6))) |
102 | 95, 101 | mpbid 222 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(((⌊‘𝑁) −
1) / 6) ≤ ((𝑁 − 1)
/ 6)) |
103 | 68, 66, 81, 90, 102 | letrd 10386 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ ((𝑁 − 1) / 6)) |
104 | | flle 12794 |
. . . . . . . . . 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 10835 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘𝑁) −
5) ≤ (𝑁 −
5)) |
108 | | lediv1 11080 |
. . . . . . . . . . 11
⊢
((((⌊‘𝑁)
− 5) ∈ ℝ ∧ (𝑁 − 5) ∈ ℝ ∧ (6 ∈
ℝ ∧ 0 < 6)) → (((⌊‘𝑁) − 5) ≤ (𝑁 − 5) ↔ (((⌊‘𝑁) − 5) / 6) ≤ ((𝑁 − 5) /
6))) |
109 | 71, 84, 97, 99, 108 | syl112anc 1481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(((⌊‘𝑁) −
5) ≤ (𝑁 − 5)
↔ (((⌊‘𝑁)
− 5) / 6) ≤ ((𝑁
− 5) / 6))) |
110 | 107, 109 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(((⌊‘𝑁) −
5) / 6) ≤ ((𝑁 − 5)
/ 6)) |
111 | 75, 73, 86, 105, 110 | letrd 10386 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 5) / 6)) ≤ ((𝑁 − 5) / 6)) |
112 | 75, 86, 92, 111 | leadd1dd 10833 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ≤ (((𝑁 − 5) / 6) +
1)) |
113 | 68, 77, 81, 88, 103, 112 | le2addd 10838 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘(((⌊‘𝑁) − 1) / 6)) +
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) ≤ (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) +
1))) |
114 | | ovex 6841 |
. . . . . . . . . . . 12
⊢ (𝑘 mod 6) ∈
V |
115 | 114 | elpr 4343 |
. . . . . . . . . . 11
⊢ ((𝑘 mod 6) ∈ {1, 5} ↔
((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)) |
116 | 115 | rabbii 3325 |
. . . . . . . . . 10
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} = {𝑘 ∈
(4...(⌊‘𝑁))
∣ ((𝑘 mod 6) = 1 ∨
(𝑘 mod 6) =
5)} |
117 | | unrab 4041 |
. . . . . . . . . 10
⊢ ({𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
∪ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}) =
{𝑘 ∈
(4...(⌊‘𝑁))
∣ ((𝑘 mod 6) = 1 ∨
(𝑘 mod 6) =
5)} |
118 | 116, 117 | eqtr4i 2785 |
. . . . . . . . 9
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}} = ({𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
∪ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) =
5}) |
119 | 118 | fveq2i 6355 |
. . . . . . . 8
⊢
(♯‘{𝑘
∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) =
(♯‘({𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
∪ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) =
5})) |
120 | | ssrab2 3828 |
. . . . . . . . . 10
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
⊆ (4...(⌊‘𝑁)) |
121 | | ssfi 8345 |
. . . . . . . . . 10
⊢
(((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ⊆
(4...(⌊‘𝑁)))
→ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
∈ Fin) |
122 | 10, 120, 121 | mp2an 710 |
. . . . . . . . 9
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
∈ Fin |
123 | | ssrab2 3828 |
. . . . . . . . . 10
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}
⊆ (4...(⌊‘𝑁)) |
124 | | ssfi 8345 |
. . . . . . . . . 10
⊢
(((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ⊆
(4...(⌊‘𝑁)))
→ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}
∈ Fin) |
125 | 10, 123, 124 | mp2an 710 |
. . . . . . . . 9
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}
∈ Fin |
126 | | inrab 4042 |
. . . . . . . . . 10
⊢ ({𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
∩ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}) =
{𝑘 ∈
(4...(⌊‘𝑁))
∣ ((𝑘 mod 6) = 1
∧ (𝑘 mod 6) =
5)} |
127 | | rabeq0 4100 |
. . . . . . . . . . 11
⊢ ({𝑘 ∈
(4...(⌊‘𝑁))
∣ ((𝑘 mod 6) = 1
∧ (𝑘 mod 6) = 5)} =
∅ ↔ ∀𝑘
∈ (4...(⌊‘𝑁)) ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)) |
128 | | 1lt5 11395 |
. . . . . . . . . . . . . 14
⊢ 1 <
5 |
129 | 91, 128 | ltneii 10342 |
. . . . . . . . . . . . 13
⊢ 1 ≠
5 |
130 | | eqtr2 2780 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5) → 1 =
5) |
131 | 130 | necon3ai 2957 |
. . . . . . . . . . . . 13
⊢ (1 ≠ 5
→ ¬ ((𝑘 mod 6) = 1
∧ (𝑘 mod 6) =
5)) |
132 | 129, 131 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ¬
((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5) |
133 | 132 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(4...(⌊‘𝑁))
→ ¬ ((𝑘 mod 6) = 1
∧ (𝑘 mod 6) =
5)) |
134 | 127, 133 | mprgbir 3065 |
. . . . . . . . . 10
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ ((𝑘 mod 6) = 1
∧ (𝑘 mod 6) = 5)} =
∅ |
135 | 126, 134 | eqtri 2782 |
. . . . . . . . 9
⊢ ({𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}
∩ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}) =
∅ |
136 | | hashun 13363 |
. . . . . . . . 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}))) |
137 | 122, 125,
135, 136 | mp3an 1573 |
. . . . . . . 8
⊢
(♯‘({𝑘
∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})) = ((♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}) +
(♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) =
5})) |
138 | 119, 137 | eqtri 2782 |
. . . . . . 7
⊢
(♯‘{𝑘
∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) =
((♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}) +
(♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) =
5})) |
139 | | elfzelz 12535 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(4...(⌊‘𝑁))
→ 𝑘 ∈
ℤ) |
140 | | nnrp 12035 |
. . . . . . . . . . . . . . . . 17
⊢ (6 ∈
ℕ → 6 ∈ ℝ+) |
141 | 64, 140 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ 6 ∈
ℝ+ |
142 | | 0le1 10743 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≤
1 |
143 | | 1lt6 11400 |
. . . . . . . . . . . . . . . 16
⊢ 1 <
6 |
144 | | modid 12889 |
. . . . . . . . . . . . . . . 16
⊢ (((1
∈ ℝ ∧ 6 ∈ ℝ+) ∧ (0 ≤ 1 ∧ 1 <
6)) → (1 mod 6) = 1) |
145 | 91, 141, 142, 143, 144 | mp4an 711 |
. . . . . . . . . . . . . . 15
⊢ (1 mod 6)
= 1 |
146 | 145 | eqeq2i 2772 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 mod 6) = (1 mod 6) ↔
(𝑘 mod 6) =
1) |
147 | | 1z 11599 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℤ |
148 | | moddvds 15193 |
. . . . . . . . . . . . . . 15
⊢ ((6
∈ ℕ ∧ 𝑘
∈ ℤ ∧ 1 ∈ ℤ) → ((𝑘 mod 6) = (1 mod 6) ↔ 6 ∥ (𝑘 − 1))) |
149 | 64, 147, 148 | mp3an13 1564 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = (1 mod 6) ↔ 6
∥ (𝑘 −
1))) |
150 | 146, 149 | syl5bbr 274 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = 1 ↔ 6 ∥
(𝑘 −
1))) |
151 | 139, 150 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(4...(⌊‘𝑁))
→ ((𝑘 mod 6) = 1
↔ 6 ∥ (𝑘 −
1))) |
152 | 151 | rabbiia 3324 |
. . . . . . . . . . 11
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1} =
{𝑘 ∈
(4...(⌊‘𝑁))
∣ 6 ∥ (𝑘
− 1)} |
153 | 152 | fveq2i 6355 |
. . . . . . . . . 10
⊢
(♯‘{𝑘
∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = (♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ 6 ∥ (𝑘
− 1)}) |
154 | 64 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 6 ∈
ℕ) |
155 | | 4z 11603 |
. . . . . . . . . . . 12
⊢ 4 ∈
ℤ |
156 | 155 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 4 ∈
ℤ) |
157 | 38 | oveq1i 6823 |
. . . . . . . . . . . . . 14
⊢ (4
− 1) = ((3 + 1) − 1) |
158 | | 3cn 11287 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℂ |
159 | | ax-1cn 10186 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
160 | 158, 159 | pncan3oi 10489 |
. . . . . . . . . . . . . 14
⊢ ((3 + 1)
− 1) = 3 |
161 | 157, 160 | eqtri 2782 |
. . . . . . . . . . . . 13
⊢ (4
− 1) = 3 |
162 | 161 | fveq2i 6355 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘(4 − 1)) =
(ℤ≥‘3) |
163 | 35, 162 | syl6eleqr 2850 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘𝑁) ∈
(ℤ≥‘(4 − 1))) |
164 | 147 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 1 ∈
ℤ) |
165 | 154, 156,
163, 164 | hashdvds 15682 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ 6 ∥ (𝑘
− 1)}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) −
(⌊‘(((4 − 1) − 1) / 6)))) |
166 | 153, 165 | syl5eq 2806 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}) =
((⌊‘(((⌊‘𝑁) − 1) / 6)) −
(⌊‘(((4 − 1) − 1) / 6)))) |
167 | | df-3 11272 |
. . . . . . . . . . . . . . . . 17
⊢ 3 = (2 +
1) |
168 | 161, 167 | eqtri 2782 |
. . . . . . . . . . . . . . . 16
⊢ (4
− 1) = (2 + 1) |
169 | 168 | oveq1i 6823 |
. . . . . . . . . . . . . . 15
⊢ ((4
− 1) − 1) = ((2 + 1) − 1) |
170 | | 2cn 11283 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℂ |
171 | 170, 159 | pncan3oi 10489 |
. . . . . . . . . . . . . . 15
⊢ ((2 + 1)
− 1) = 2 |
172 | 169, 171 | eqtri 2782 |
. . . . . . . . . . . . . 14
⊢ ((4
− 1) − 1) = 2 |
173 | 172 | oveq1i 6823 |
. . . . . . . . . . . . 13
⊢ (((4
− 1) − 1) / 6) = (2 / 6) |
174 | 173 | fveq2i 6355 |
. . . . . . . . . . . 12
⊢
(⌊‘(((4 − 1) − 1) / 6)) = (⌊‘(2 /
6)) |
175 | | 0re 10232 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
176 | 64 | nnne0i 11247 |
. . . . . . . . . . . . . . 15
⊢ 6 ≠
0 |
177 | 7, 96, 176 | redivcli 10984 |
. . . . . . . . . . . . . 14
⊢ (2 / 6)
∈ ℝ |
178 | | 2pos 11304 |
. . . . . . . . . . . . . . 15
⊢ 0 <
2 |
179 | 7, 96, 178, 98 | divgt0ii 11133 |
. . . . . . . . . . . . . 14
⊢ 0 < (2
/ 6) |
180 | 175, 177,
179 | ltleii 10352 |
. . . . . . . . . . . . 13
⊢ 0 ≤ (2
/ 6) |
181 | | 2lt6 11399 |
. . . . . . . . . . . . . . . 16
⊢ 2 <
6 |
182 | | 6cn 11294 |
. . . . . . . . . . . . . . . . 17
⊢ 6 ∈
ℂ |
183 | 182 | mulid1i 10234 |
. . . . . . . . . . . . . . . 16
⊢ (6
· 1) = 6 |
184 | 181, 183 | breqtrri 4831 |
. . . . . . . . . . . . . . 15
⊢ 2 < (6
· 1) |
185 | 96, 98 | pm3.2i 470 |
. . . . . . . . . . . . . . . 16
⊢ (6 ∈
ℝ ∧ 0 < 6) |
186 | | ltdivmul 11090 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℝ ∧ 1 ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6))
→ ((2 / 6) < 1 ↔ 2 < (6 · 1))) |
187 | 7, 91, 185, 186 | mp3an 1573 |
. . . . . . . . . . . . . . 15
⊢ ((2 / 6)
< 1 ↔ 2 < (6 · 1)) |
188 | 184, 187 | mpbir 221 |
. . . . . . . . . . . . . 14
⊢ (2 / 6)
< 1 |
189 | | 1e0p1 11744 |
. . . . . . . . . . . . . 14
⊢ 1 = (0 +
1) |
190 | 188, 189 | breqtri 4829 |
. . . . . . . . . . . . 13
⊢ (2 / 6)
< (0 + 1) |
191 | | 0z 11580 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℤ |
192 | | flbi 12811 |
. . . . . . . . . . . . . 14
⊢ (((2 / 6)
∈ ℝ ∧ 0 ∈ ℤ) → ((⌊‘(2 / 6)) = 0
↔ (0 ≤ (2 / 6) ∧ (2 / 6) < (0 + 1)))) |
193 | 177, 191,
192 | mp2an 710 |
. . . . . . . . . . . . 13
⊢
((⌊‘(2 / 6)) = 0 ↔ (0 ≤ (2 / 6) ∧ (2 / 6) <
(0 + 1))) |
194 | 180, 190,
193 | mpbir2an 993 |
. . . . . . . . . . . 12
⊢
(⌊‘(2 / 6)) = 0 |
195 | 174, 194 | eqtri 2782 |
. . . . . . . . . . 11
⊢
(⌊‘(((4 − 1) − 1) / 6)) = 0 |
196 | 195 | oveq2i 6824 |
. . . . . . . . . 10
⊢
((⌊‘(((⌊‘𝑁) − 1) / 6)) −
(⌊‘(((4 − 1) − 1) / 6))) =
((⌊‘(((⌊‘𝑁) − 1) / 6)) −
0) |
197 | 66 | flcld 12793 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 1) / 6)) ∈
ℤ) |
198 | 197 | zcnd 11675 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 1) / 6)) ∈
ℂ) |
199 | 198 | subid1d 10573 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘(((⌊‘𝑁) − 1) / 6)) − 0) =
(⌊‘(((⌊‘𝑁) − 1) / 6))) |
200 | 196, 199 | syl5eq 2806 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘(((⌊‘𝑁) − 1) / 6)) −
(⌊‘(((4 − 1) − 1) / 6))) =
(⌊‘(((⌊‘𝑁) − 1) / 6))) |
201 | 166, 200 | eqtrd 2794 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}) =
(⌊‘(((⌊‘𝑁) − 1) / 6))) |
202 | | 5pos 11310 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
5 |
203 | 175, 69, 202 | ltleii 10352 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≤
5 |
204 | | 5lt6 11396 |
. . . . . . . . . . . . . . . 16
⊢ 5 <
6 |
205 | | modid 12889 |
. . . . . . . . . . . . . . . 16
⊢ (((5
∈ ℝ ∧ 6 ∈ ℝ+) ∧ (0 ≤ 5 ∧ 5 <
6)) → (5 mod 6) = 5) |
206 | 69, 141, 203, 204, 205 | mp4an 711 |
. . . . . . . . . . . . . . 15
⊢ (5 mod 6)
= 5 |
207 | 206 | eqeq2i 2772 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 mod 6) = (5 mod 6) ↔
(𝑘 mod 6) =
5) |
208 | | 5nn 11380 |
. . . . . . . . . . . . . . . 16
⊢ 5 ∈
ℕ |
209 | 208 | nnzi 11593 |
. . . . . . . . . . . . . . 15
⊢ 5 ∈
ℤ |
210 | | moddvds 15193 |
. . . . . . . . . . . . . . 15
⊢ ((6
∈ ℕ ∧ 𝑘
∈ ℤ ∧ 5 ∈ ℤ) → ((𝑘 mod 6) = (5 mod 6) ↔ 6 ∥ (𝑘 − 5))) |
211 | 64, 209, 210 | mp3an13 1564 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = (5 mod 6) ↔ 6
∥ (𝑘 −
5))) |
212 | 207, 211 | syl5bbr 274 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = 5 ↔ 6 ∥
(𝑘 −
5))) |
213 | 139, 212 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(4...(⌊‘𝑁))
→ ((𝑘 mod 6) = 5
↔ 6 ∥ (𝑘 −
5))) |
214 | 213 | rabbiia 3324 |
. . . . . . . . . . 11
⊢ {𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5} =
{𝑘 ∈
(4...(⌊‘𝑁))
∣ 6 ∥ (𝑘
− 5)} |
215 | 214 | fveq2i 6355 |
. . . . . . . . . 10
⊢
(♯‘{𝑘
∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = (♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ 6 ∥ (𝑘
− 5)}) |
216 | 209 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 5 ∈
ℤ) |
217 | 154, 156,
163, 216 | hashdvds 15682 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ 6 ∥ (𝑘
− 5)}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) −
(⌊‘(((4 − 1) − 5) / 6)))) |
218 | 215, 217 | syl5eq 2806 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}) =
((⌊‘(((⌊‘𝑁) − 5) / 6)) −
(⌊‘(((4 − 1) − 5) / 6)))) |
219 | 161 | oveq1i 6823 |
. . . . . . . . . . . . . . . 16
⊢ ((4
− 1) − 5) = (3 − 5) |
220 | | 5cn 11292 |
. . . . . . . . . . . . . . . . 17
⊢ 5 ∈
ℂ |
221 | 220, 158 | negsubdi2i 10559 |
. . . . . . . . . . . . . . . 16
⊢ -(5
− 3) = (3 − 5) |
222 | | 3p2e5 11352 |
. . . . . . . . . . . . . . . . . . 19
⊢ (3 + 2) =
5 |
223 | 222 | oveq1i 6823 |
. . . . . . . . . . . . . . . . . 18
⊢ ((3 + 2)
− 3) = (5 − 3) |
224 | | pncan2 10480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((3
∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) =
2) |
225 | 158, 170,
224 | mp2an 710 |
. . . . . . . . . . . . . . . . . 18
⊢ ((3 + 2)
− 3) = 2 |
226 | 223, 225 | eqtr3i 2784 |
. . . . . . . . . . . . . . . . 17
⊢ (5
− 3) = 2 |
227 | 226 | negeqi 10466 |
. . . . . . . . . . . . . . . 16
⊢ -(5
− 3) = -2 |
228 | 219, 221,
227 | 3eqtr2i 2788 |
. . . . . . . . . . . . . . 15
⊢ ((4
− 1) − 5) = -2 |
229 | 228 | oveq1i 6823 |
. . . . . . . . . . . . . 14
⊢ (((4
− 1) − 5) / 6) = (-2 / 6) |
230 | | divneg 10911 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 6 ∈ ℂ ∧ 6 ≠ 0) → -(2 / 6) = (-2 /
6)) |
231 | 170, 182,
176, 230 | mp3an 1573 |
. . . . . . . . . . . . . 14
⊢ -(2 / 6)
= (-2 / 6) |
232 | 229, 231 | eqtr4i 2785 |
. . . . . . . . . . . . 13
⊢ (((4
− 1) − 5) / 6) = -(2 / 6) |
233 | 232 | fveq2i 6355 |
. . . . . . . . . . . 12
⊢
(⌊‘(((4 − 1) − 5) / 6)) = (⌊‘-(2 /
6)) |
234 | 177, 91, 188 | ltleii 10352 |
. . . . . . . . . . . . . 14
⊢ (2 / 6)
≤ 1 |
235 | 177, 91 | lenegi 10765 |
. . . . . . . . . . . . . 14
⊢ ((2 / 6)
≤ 1 ↔ -1 ≤ -(2 / 6)) |
236 | 234, 235 | mpbi 220 |
. . . . . . . . . . . . 13
⊢ -1 ≤
-(2 / 6) |
237 | 175, 177 | ltnegi 10764 |
. . . . . . . . . . . . . . 15
⊢ (0 <
(2 / 6) ↔ -(2 / 6) < -0) |
238 | 179, 237 | mpbi 220 |
. . . . . . . . . . . . . 14
⊢ -(2 / 6)
< -0 |
239 | | neg0 10519 |
. . . . . . . . . . . . . . . 16
⊢ -0 =
0 |
240 | | 1pneg1e0 11321 |
. . . . . . . . . . . . . . . 16
⊢ (1 + -1)
= 0 |
241 | 239, 240 | eqtr4i 2785 |
. . . . . . . . . . . . . . 15
⊢ -0 = (1 +
-1) |
242 | | neg1cn 11316 |
. . . . . . . . . . . . . . . 16
⊢ -1 ∈
ℂ |
243 | 242, 159 | addcomi 10419 |
. . . . . . . . . . . . . . 15
⊢ (-1 + 1)
= (1 + -1) |
244 | 241, 243 | eqtr4i 2785 |
. . . . . . . . . . . . . 14
⊢ -0 = (-1
+ 1) |
245 | 238, 244 | breqtri 4829 |
. . . . . . . . . . . . 13
⊢ -(2 / 6)
< (-1 + 1) |
246 | 177 | renegcli 10534 |
. . . . . . . . . . . . . 14
⊢ -(2 / 6)
∈ ℝ |
247 | | neg1z 11605 |
. . . . . . . . . . . . . 14
⊢ -1 ∈
ℤ |
248 | | flbi 12811 |
. . . . . . . . . . . . . 14
⊢ ((-(2 /
6) ∈ ℝ ∧ -1 ∈ ℤ) → ((⌊‘-(2 / 6)) =
-1 ↔ (-1 ≤ -(2 / 6) ∧ -(2 / 6) < (-1 + 1)))) |
249 | 246, 247,
248 | mp2an 710 |
. . . . . . . . . . . . 13
⊢
((⌊‘-(2 / 6)) = -1 ↔ (-1 ≤ -(2 / 6) ∧ -(2 / 6)
< (-1 + 1))) |
250 | 236, 245,
249 | mpbir2an 993 |
. . . . . . . . . . . 12
⊢
(⌊‘-(2 / 6)) = -1 |
251 | 233, 250 | eqtri 2782 |
. . . . . . . . . . 11
⊢
(⌊‘(((4 − 1) − 5) / 6)) = -1 |
252 | 251 | oveq2i 6824 |
. . . . . . . . . 10
⊢
((⌊‘(((⌊‘𝑁) − 5) / 6)) −
(⌊‘(((4 − 1) − 5) / 6))) =
((⌊‘(((⌊‘𝑁) − 5) / 6)) −
-1) |
253 | 73 | flcld 12793 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 5) / 6)) ∈
ℤ) |
254 | 253 | zcnd 11675 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(⌊‘(((⌊‘𝑁) − 5) / 6)) ∈
ℂ) |
255 | | subneg 10522 |
. . . . . . . . . . 11
⊢
(((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℂ ∧ 1
∈ ℂ) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1) =
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) |
256 | 254, 159,
255 | sylancl 697 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1) =
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) |
257 | 252, 256 | syl5eq 2806 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((⌊‘(((⌊‘𝑁) − 5) / 6)) −
(⌊‘(((4 − 1) − 5) / 6))) =
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) |
258 | 218, 257 | eqtrd 2794 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5}) =
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) |
259 | 201, 258 | oveq12d 6831 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 1}) +
(♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) = 5})) =
((⌊‘(((⌊‘𝑁) − 1) / 6)) +
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))) |
260 | 138, 259 | syl5eq 2806 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) +
((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))) |
261 | 82 | recnd 10260 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 𝑁 ∈ ℂ) |
262 | 261 | 2timesd 11467 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (2 · 𝑁) = (𝑁 + 𝑁)) |
263 | | df-6 11275 |
. . . . . . . . . . . . . 14
⊢ 6 = (5 +
1) |
264 | 220, 159 | addcomi 10419 |
. . . . . . . . . . . . . 14
⊢ (5 + 1) =
(1 + 5) |
265 | 263, 264 | eqtri 2782 |
. . . . . . . . . . . . 13
⊢ 6 = (1 +
5) |
266 | 265 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 6 = (1 +
5)) |
267 | 262, 266 | oveq12d 6831 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((2 ·
𝑁) − 6) = ((𝑁 + 𝑁) − (1 + 5))) |
268 | | addsub4 10516 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ (1 ∈
ℂ ∧ 5 ∈ ℂ)) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5))) |
269 | 159, 220,
268 | mpanr12 723 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5))) |
270 | 261, 261,
269 | syl2anc 696 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5))) |
271 | 267, 270 | eqtrd 2794 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((2 ·
𝑁) − 6) = ((𝑁 − 1) + (𝑁 − 5))) |
272 | 271 | oveq1d 6828 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (((2 ·
𝑁) − 6) / 6) =
(((𝑁 − 1) + (𝑁 − 5)) /
6)) |
273 | | mulcl 10212 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 𝑁
∈ ℂ) → (2 · 𝑁) ∈ ℂ) |
274 | 170, 261,
273 | sylancr 698 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (2 · 𝑁) ∈
ℂ) |
275 | 182, 176 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (6 ∈
ℂ ∧ 6 ≠ 0) |
276 | | divsubdir 10913 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑁) ∈ ℂ
∧ 6 ∈ ℂ ∧ (6 ∈ ℂ ∧ 6 ≠ 0)) → (((2
· 𝑁) − 6) / 6)
= (((2 · 𝑁) / 6)
− (6 / 6))) |
277 | 182, 275,
276 | mp3an23 1565 |
. . . . . . . . . . 11
⊢ ((2
· 𝑁) ∈ ℂ
→ (((2 · 𝑁)
− 6) / 6) = (((2 · 𝑁) / 6) − (6 / 6))) |
278 | 274, 277 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (((2 ·
𝑁) − 6) / 6) = (((2
· 𝑁) / 6) − (6
/ 6))) |
279 | | 3t2e6 11371 |
. . . . . . . . . . . . . 14
⊢ (3
· 2) = 6 |
280 | 158, 170 | mulcomi 10238 |
. . . . . . . . . . . . . 14
⊢ (3
· 2) = (2 · 3) |
281 | 279, 280 | eqtr3i 2784 |
. . . . . . . . . . . . 13
⊢ 6 = (2
· 3) |
282 | 281 | oveq2i 6824 |
. . . . . . . . . . . 12
⊢ ((2
· 𝑁) / 6) = ((2
· 𝑁) / (2 ·
3)) |
283 | | 3ne0 11307 |
. . . . . . . . . . . . . . 15
⊢ 3 ≠
0 |
284 | 158, 283 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) |
285 | | 2cnne0 11434 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
286 | | divcan5 10919 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℂ ∧ (3 ∈
ℂ ∧ 3 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2
· 𝑁) / (2 ·
3)) = (𝑁 /
3)) |
287 | 284, 285,
286 | mp3an23 1565 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℂ → ((2
· 𝑁) / (2 ·
3)) = (𝑁 /
3)) |
288 | 261, 287 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((2 ·
𝑁) / (2 · 3)) =
(𝑁 / 3)) |
289 | 282, 288 | syl5eq 2806 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((2 ·
𝑁) / 6) = (𝑁 / 3)) |
290 | 182, 176 | dividi 10950 |
. . . . . . . . . . . 12
⊢ (6 / 6) =
1 |
291 | 290 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (6 / 6) =
1) |
292 | 289, 291 | oveq12d 6831 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (((2 ·
𝑁) / 6) − (6 / 6)) =
((𝑁 / 3) −
1)) |
293 | 278, 292 | eqtrd 2794 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (((2 ·
𝑁) − 6) / 6) =
((𝑁 / 3) −
1)) |
294 | 79 | recnd 10260 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (𝑁 − 1) ∈
ℂ) |
295 | 84 | recnd 10260 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (𝑁 − 5) ∈
ℂ) |
296 | | divdir 10902 |
. . . . . . . . . . 11
⊢ (((𝑁 − 1) ∈ ℂ ∧
(𝑁 − 5) ∈
ℂ ∧ (6 ∈ ℂ ∧ 6 ≠ 0)) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6))) |
297 | 275, 296 | mp3an3 1562 |
. . . . . . . . . 10
⊢ (((𝑁 − 1) ∈ ℂ ∧
(𝑁 − 5) ∈
ℂ) → (((𝑁
− 1) + (𝑁 − 5))
/ 6) = (((𝑁 − 1) / 6)
+ ((𝑁 − 5) /
6))) |
298 | 294, 295,
297 | syl2anc 696 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6))) |
299 | 272, 293,
298 | 3eqtr3d 2802 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((𝑁 / 3) − 1) = (((𝑁 − 1) / 6) + ((𝑁 − 5) /
6))) |
300 | 299 | oveq1d 6828 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (((𝑁 / 3) − 1) + 1) =
((((𝑁 − 1) / 6) +
((𝑁 − 5) / 6)) +
1)) |
301 | 21 | recnd 10260 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (𝑁 / 3) ∈
ℂ) |
302 | | npcan 10482 |
. . . . . . . 8
⊢ (((𝑁 / 3) ∈ ℂ ∧ 1
∈ ℂ) → (((𝑁
/ 3) − 1) + 1) = (𝑁 /
3)) |
303 | 301, 159,
302 | sylancl 697 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3)) |
304 | 81 | recnd 10260 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((𝑁 − 1) / 6) ∈
ℂ) |
305 | 86 | recnd 10260 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((𝑁 − 5) / 6) ∈
ℂ) |
306 | 159 | a1i 11 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 1 ∈
ℂ) |
307 | 304, 305,
306 | addassd 10254 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → ((((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)) + 1) =
(((𝑁 − 1) / 6) +
(((𝑁 − 5) / 6) +
1))) |
308 | 300, 303,
307 | 3eqtr3d 2802 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → (𝑁 / 3) = (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1))) |
309 | 113, 260,
308 | 3brtr4d 4836 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(♯‘{𝑘 ∈
(4...(⌊‘𝑁))
∣ (𝑘 mod 6) ∈
{1, 5}}) ≤ (𝑁 /
3)) |
310 | 9, 17, 21, 59, 309 | letrd 10386 |
. . . 4
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
((π‘𝑁)
− 2) ≤ (𝑁 /
3)) |
311 | 7 | a1i 11 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) → 2 ∈
ℝ) |
312 | 6, 311, 21 | lesubaddd 10816 |
. . . 4
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(((π‘𝑁)
− 2) ≤ (𝑁 / 3)
↔ (π‘𝑁) ≤ ((𝑁 / 3) + 2))) |
313 | 310, 312 | mpbid 222 |
. . 3
⊢ ((𝑁 ∈ ℝ ∧ 3 ≤
𝑁) →
(π‘𝑁) ≤
((𝑁 / 3) +
2)) |
314 | 313 | adantlr 753 |
. 2
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 3 ≤ 𝑁) →
(π‘𝑁) ≤
((𝑁 / 3) +
2)) |
315 | 5 | ad2antrr 764 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ∈
ℝ) |
316 | 7 | a1i 11 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → 2 ∈
ℝ) |
317 | 20 | ad2antrr 764 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → (𝑁 / 3) ∈ ℝ) |
318 | | readdcl 10211 |
. . . 4
⊢ (((𝑁 / 3) ∈ ℝ ∧ 2
∈ ℝ) → ((𝑁
/ 3) + 2) ∈ ℝ) |
319 | 317, 7, 318 | sylancl 697 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → ((𝑁 / 3) + 2) ∈ ℝ) |
320 | | ppiwordi 25087 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 3 ∈
ℝ ∧ 𝑁 ≤ 3)
→ (π‘𝑁) ≤
(π‘3)) |
321 | 1, 320 | mp3an2 1561 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 𝑁 ≤ 3) →
(π‘𝑁) ≤
(π‘3)) |
322 | 321 | adantlr 753 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤
(π‘3)) |
323 | 322, 24 | syl6breq 4845 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ 2) |
324 | | 3pos 11306 |
. . . . . 6
⊢ 0 <
3 |
325 | | divge0 11084 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ (3 ∈ ℝ
∧ 0 < 3)) → 0 ≤ (𝑁 / 3)) |
326 | 1, 324, 325 | mpanr12 723 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) → 0 ≤ (𝑁 / 3)) |
327 | 326 | adantr 472 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → 0 ≤ (𝑁 / 3)) |
328 | | addge02 10731 |
. . . . 5
⊢ ((2
∈ ℝ ∧ (𝑁 /
3) ∈ ℝ) → (0 ≤ (𝑁 / 3) ↔ 2 ≤ ((𝑁 / 3) + 2))) |
329 | 7, 317, 328 | sylancr 698 |
. . . 4
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → (0 ≤ (𝑁 / 3) ↔ 2 ≤ ((𝑁 / 3) + 2))) |
330 | 327, 329 | mpbid 222 |
. . 3
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → 2 ≤ ((𝑁 / 3) + 2)) |
331 | 315, 316,
319, 323, 330 | letrd 10386 |
. 2
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ ((𝑁 / 3) + 2)) |
332 | 2, 3, 314, 331 | lecasei 10335 |
1
⊢ ((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) →
(π‘𝑁) ≤
((𝑁 / 3) +
2)) |