Metamath Proof Explorer

Theorem ppiub

Description: An upper bound on the prime-counting function ppi , which counts the number of primes less than N . (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Assertion ppiub ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) → ( π ‘ 𝑁 ) ≤ ( ( 𝑁 / 3 ) + 2 ) )

Proof

Step Hyp Ref Expression
1 3re ⊢ 3 ∈ ℝ
2 1 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) → 3 ∈ ℝ )
3 simpl ⊢ ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
4 ppicl ⊢ ( 𝑁 ∈ ℝ → ( π ‘ 𝑁 ) ∈ ℕ0 )
5 4 nn0red ⊢ ( 𝑁 ∈ ℝ → ( π ‘ 𝑁 ) ∈ ℝ )
6 5 adantr ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( π ‘ 𝑁 ) ∈ ℝ )
7 2re ⊢ 2 ∈ ℝ
8 resubcl ⊢ ( ( ( π ‘ 𝑁 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( π ‘ 𝑁 ) − 2 ) ∈ ℝ )
9 6 7 8 sylancl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( π ‘ 𝑁 ) − 2 ) ∈ ℝ )
10 fzfi ⊢ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∈ Fin
11 ssrab2 ⊢ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ⊆ ( 4 ... ( ⌊ ‘ 𝑁 ) )
12 ssfi ⊢ ( ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∈ Fin ∧ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ⊆ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ) → { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ∈ Fin )
13 10 11 12 mp2an ⊢ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ∈ Fin
14 hashcl ⊢ ( { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ∈ Fin → ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ) ∈ ℕ0 )
15 13 14 ax-mp ⊢ ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ) ∈ ℕ0
16 15 nn0rei ⊢ ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ) ∈ ℝ
17 16 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ) ∈ ℝ )
18 3nn ⊢ 3 ∈ ℕ
19 nndivre ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ∈ ℕ ) → ( 𝑁 / 3 ) ∈ ℝ )
20 18 19 mpan2 ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 / 3 ) ∈ ℝ )
21 20 adantr ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( 𝑁 / 3 ) ∈ ℝ )
22 ppifl ⊢ ( 𝑁 ∈ ℝ → ( π ‘ ( ⌊ ‘ 𝑁 ) ) = ( π ‘ 𝑁 ) )
23 22 adantr ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( π ‘ ( ⌊ ‘ 𝑁 ) ) = ( π ‘ 𝑁 ) )
24 ppi3 ⊢ ( π ‘ 3 ) = 2
25 24 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( π ‘ 3 ) = 2 )
26 23 25 oveq12d ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( π ‘ ( ⌊ ‘ 𝑁 ) ) − ( π ‘ 3 ) ) = ( ( π ‘ 𝑁 ) − 2 ) )
27 3z ⊢ 3 ∈ ℤ
28 27 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → 3 ∈ ℤ )
29 flcl ⊢ ( 𝑁 ∈ ℝ → ( ⌊ ‘ 𝑁 ) ∈ ℤ )
30 29 adantr ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ⌊ ‘ 𝑁 ) ∈ ℤ )
31 flge ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ∈ ℤ ) → ( 3 ≤ 𝑁 ↔ 3 ≤ ( ⌊ ‘ 𝑁 ) ) )
32 27 31 mpan2 ⊢ ( 𝑁 ∈ ℝ → ( 3 ≤ 𝑁 ↔ 3 ≤ ( ⌊ ‘ 𝑁 ) ) )
33 32 biimpa ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → 3 ≤ ( ⌊ ‘ 𝑁 ) )
34 eluz2 ⊢ ( ( ⌊ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ ( ⌊ ‘ 𝑁 ) ∈ ℤ ∧ 3 ≤ ( ⌊ ‘ 𝑁 ) ) )
35 28 30 33 34 syl3anbrc ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ⌊ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 3 ) )
36 ppidif ⊢ ( ( ⌊ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 3 ) → ( ( π ‘ ( ⌊ ‘ 𝑁 ) ) − ( π ‘ 3 ) ) = ( ♯ ‘ ( ( ( 3 + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) )
37 35 36 syl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( π ‘ ( ⌊ ‘ 𝑁 ) ) − ( π ‘ 3 ) ) = ( ♯ ‘ ( ( ( 3 + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) )
38 df-4 ⊢ 4 = ( 3 + 1 )
39 38 oveq1i ⊢ ( 4 ... ( ⌊ ‘ 𝑁 ) ) = ( ( 3 + 1 ) ... ( ⌊ ‘ 𝑁 ) )
40 39 ineq1i ⊢ ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) = ( ( ( 3 + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ )
41 40 fveq2i ⊢ ( ♯ ‘ ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) = ( ♯ ‘ ( ( ( 3 + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) )
42 37 41 eqtr4di ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( π ‘ ( ⌊ ‘ 𝑁 ) ) − ( π ‘ 3 ) ) = ( ♯ ‘ ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) )
43 26 42 eqtr3d ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( π ‘ 𝑁 ) − 2 ) = ( ♯ ‘ ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) )
44 dfin5 ⊢ ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) = { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ 𝑘 ∈ ℙ }
45 elfzle1 ⊢ ( 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) → 4 ≤ 𝑘 )
46 ppiublem2 ⊢ ( ( 𝑘 ∈ ℙ ∧ 4 ≤ 𝑘 ) → ( 𝑘 mod 6 ) ∈ { 1 , 5 } )
47 46 expcom ⊢ ( 4 ≤ 𝑘 → ( 𝑘 ∈ ℙ → ( 𝑘 mod 6 ) ∈ { 1 , 5 } ) )
48 45 47 syl ⊢ ( 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) → ( 𝑘 ∈ ℙ → ( 𝑘 mod 6 ) ∈ { 1 , 5 } ) )
49 48 ss2rabi ⊢ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ 𝑘 ∈ ℙ } ⊆ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } }
50 44 49 eqsstri ⊢ ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ⊆ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } }
51 ssdomg ⊢ ( { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ∈ Fin → ( ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ⊆ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } → ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ≼ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ) )
52 13 50 51 mp2 ⊢ ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ≼ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } }
53 inss1 ⊢ ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ⊆ ( 4 ... ( ⌊ ‘ 𝑁 ) )
54 ssfi ⊢ ( ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∈ Fin ∧ ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ⊆ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ) → ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ∈ Fin )
55 10 53 54 mp2an ⊢ ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ∈ Fin
56 hashdom ⊢ ( ( ( ( 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 ⊢ ( ( ♯ ‘ ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) ≤ ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ) ↔ ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ≼ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } )
58 52 57 mpbir ⊢ ( ♯ ‘ ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) ≤ ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } )
59 43 58 eqbrtrdi ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( π ‘ 𝑁 ) − 2 ) ≤ ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ) )
60 reflcl ⊢ ( 𝑁 ∈ ℝ → ( ⌊ ‘ 𝑁 ) ∈ ℝ )
61 60 adantr ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ⌊ ‘ 𝑁 ) ∈ ℝ )
62 peano2rem ⊢ ( ( ⌊ ‘ 𝑁 ) ∈ ℝ → ( ( ⌊ ‘ 𝑁 ) − 1 ) ∈ ℝ )
63 61 62 syl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ⌊ ‘ 𝑁 ) − 1 ) ∈ ℝ )
64 6nn ⊢ 6 ∈ ℕ
65 nndivre ⊢ ( ( ( ( ⌊ ‘ 𝑁 ) − 1 ) ∈ ℝ ∧ 6 ∈ ℕ ) → ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ∈ ℝ )
66 63 64 65 sylancl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ∈ ℝ )
67 reflcl ⊢ ( ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ∈ ℝ → ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) ∈ ℝ )
68 66 67 syl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) ∈ ℝ )
69 5re ⊢ 5 ∈ ℝ
70 resubcl ⊢ ( ( ( ⌊ ‘ 𝑁 ) ∈ ℝ ∧ 5 ∈ ℝ ) → ( ( ⌊ ‘ 𝑁 ) − 5 ) ∈ ℝ )
71 61 69 70 sylancl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ⌊ ‘ 𝑁 ) − 5 ) ∈ ℝ )
72 nndivre ⊢ ( ( ( ( ⌊ ‘ 𝑁 ) − 5 ) ∈ ℝ ∧ 6 ∈ ℕ ) → ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ∈ ℝ )
73 71 64 72 sylancl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ∈ ℝ )
74 reflcl ⊢ ( ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ∈ ℝ → ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) ∈ ℝ )
75 73 74 syl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) ∈ ℝ )
76 peano2re ⊢ ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) ∈ ℝ → ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) + 1 ) ∈ ℝ )
77 75 76 syl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) + 1 ) ∈ ℝ )
78 peano2rem ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ )
79 78 adantr ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℝ )
80 nndivre ⊢ ( ( ( 𝑁 − 1 ) ∈ ℝ ∧ 6 ∈ ℕ ) → ( ( 𝑁 − 1 ) / 6 ) ∈ ℝ )
81 79 64 80 sylancl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( 𝑁 − 1 ) / 6 ) ∈ ℝ )
82 simpl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
83 resubcl ⊢ ( ( 𝑁 ∈ ℝ ∧ 5 ∈ ℝ ) → ( 𝑁 − 5 ) ∈ ℝ )
84 82 69 83 sylancl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( 𝑁 − 5 ) ∈ ℝ )
85 nndivre ⊢ ( ( ( 𝑁 − 5 ) ∈ ℝ ∧ 6 ∈ ℕ ) → ( ( 𝑁 − 5 ) / 6 ) ∈ ℝ )
86 84 64 85 sylancl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( 𝑁 − 5 ) / 6 ) ∈ ℝ )
87 peano2re ⊢ ( ( ( 𝑁 − 5 ) / 6 ) ∈ ℝ → ( ( ( 𝑁 − 5 ) / 6 ) + 1 ) ∈ ℝ )
88 86 87 syl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ( 𝑁 − 5 ) / 6 ) + 1 ) ∈ ℝ )
89 flle ⊢ ( ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ∈ ℝ → ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) ≤ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) )
90 66 89 syl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) ≤ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) )
91 1re ⊢ 1 ∈ ℝ
92 91 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → 1 ∈ ℝ )
93 flle ⊢ ( 𝑁 ∈ ℝ → ( ⌊ ‘ 𝑁 ) ≤ 𝑁 )
94 93 adantr ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ⌊ ‘ 𝑁 ) ≤ 𝑁 )
95 61 82 92 94 lesub1dd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ⌊ ‘ 𝑁 ) − 1 ) ≤ ( 𝑁 − 1 ) )
96 6re ⊢ 6 ∈ ℝ
97 96 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → 6 ∈ ℝ )
98 6pos ⊢ 0 < 6
99 98 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → 0 < 6 )
100 lediv1 ⊢ ( ( ( ( ⌊ ‘ 𝑁 ) − 1 ) ∈ ℝ ∧ ( 𝑁 − 1 ) ∈ ℝ ∧ ( 6 ∈ ℝ ∧ 0 < 6 ) ) → ( ( ( ⌊ ‘ 𝑁 ) − 1 ) ≤ ( 𝑁 − 1 ) ↔ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ≤ ( ( 𝑁 − 1 ) / 6 ) ) )
101 63 79 97 99 100 syl112anc ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ( ⌊ ‘ 𝑁 ) − 1 ) ≤ ( 𝑁 − 1 ) ↔ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ≤ ( ( 𝑁 − 1 ) / 6 ) ) )
102 95 101 mpbid ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ≤ ( ( 𝑁 − 1 ) / 6 ) )
103 68 66 81 90 102 letrd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) ≤ ( ( 𝑁 − 1 ) / 6 ) )
104 flle ⊢ ( ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ∈ ℝ → ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) ≤ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) )
105 73 104 syl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) ≤ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) )
106 69 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → 5 ∈ ℝ )
107 61 82 106 94 lesub1dd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ⌊ ‘ 𝑁 ) − 5 ) ≤ ( 𝑁 − 5 ) )
108 lediv1 ⊢ ( ( ( ( ⌊ ‘ 𝑁 ) − 5 ) ∈ ℝ ∧ ( 𝑁 − 5 ) ∈ ℝ ∧ ( 6 ∈ ℝ ∧ 0 < 6 ) ) → ( ( ( ⌊ ‘ 𝑁 ) − 5 ) ≤ ( 𝑁 − 5 ) ↔ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ≤ ( ( 𝑁 − 5 ) / 6 ) ) )
109 71 84 97 99 108 syl112anc ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ( ⌊ ‘ 𝑁 ) − 5 ) ≤ ( 𝑁 − 5 ) ↔ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ≤ ( ( 𝑁 − 5 ) / 6 ) ) )
110 107 109 mpbid ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ≤ ( ( 𝑁 − 5 ) / 6 ) )
111 75 73 86 105 110 letrd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) ≤ ( ( 𝑁 − 5 ) / 6 ) )
112 75 86 92 111 leadd1dd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) + 1 ) ≤ ( ( ( 𝑁 − 5 ) / 6 ) + 1 ) )
113 68 77 81 88 103 112 le2addd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) + ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) + 1 ) ) ≤ ( ( ( 𝑁 − 1 ) / 6 ) + ( ( ( 𝑁 − 5 ) / 6 ) + 1 ) ) )
114 ovex ⊢ ( 𝑘 mod 6 ) ∈ V
115 114 elpr ⊢ ( ( 𝑘 mod 6 ) ∈ { 1 , 5 } ↔ ( ( 𝑘 mod 6 ) = 1 ∨ ( 𝑘 mod 6 ) = 5 ) )
116 115 rabbii ⊢ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } = { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( ( 𝑘 mod 6 ) = 1 ∨ ( 𝑘 mod 6 ) = 5 ) }
117 unrab ⊢ ( { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } ∪ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } ) = { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( ( 𝑘 mod 6 ) = 1 ∨ ( 𝑘 mod 6 ) = 5 ) }
118 116 117 eqtr4i ⊢ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } = ( { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } ∪ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } )
119 118 fveq2i ⊢ ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ) = ( ♯ ‘ ( { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } ∪ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } ) )
120 ssrab2 ⊢ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } ⊆ ( 4 ... ( ⌊ ‘ 𝑁 ) )
121 ssfi ⊢ ( ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∈ Fin ∧ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } ⊆ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ) → { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } ∈ Fin )
122 10 120 121 mp2an ⊢ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } ∈ Fin
123 ssrab2 ⊢ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } ⊆ ( 4 ... ( ⌊ ‘ 𝑁 ) )
124 ssfi ⊢ ( ( ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∈ Fin ∧ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } ⊆ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ) → { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } ∈ Fin )
125 10 123 124 mp2an ⊢ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } ∈ Fin
126 inrab ⊢ ( { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } ∩ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } ) = { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( ( 𝑘 mod 6 ) = 1 ∧ ( 𝑘 mod 6 ) = 5 ) }
127 rabeq0 ⊢ ( { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( ( 𝑘 mod 6 ) = 1 ∧ ( 𝑘 mod 6 ) = 5 ) } = ∅ ↔ ∀ 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ¬ ( ( 𝑘 mod 6 ) = 1 ∧ ( 𝑘 mod 6 ) = 5 ) )
128 1lt5 ⊢ 1 < 5
129 91 128 ltneii ⊢ 1 ≠ 5
130 eqtr2 ⊢ ( ( ( 𝑘 mod 6 ) = 1 ∧ ( 𝑘 mod 6 ) = 5 ) → 1 = 5 )
131 130 necon3ai ⊢ ( 1 ≠ 5 → ¬ ( ( 𝑘 mod 6 ) = 1 ∧ ( 𝑘 mod 6 ) = 5 ) )
132 129 131 ax-mp ⊢ ¬ ( ( 𝑘 mod 6 ) = 1 ∧ ( 𝑘 mod 6 ) = 5 )
133 132 a1i ⊢ ( 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) → ¬ ( ( 𝑘 mod 6 ) = 1 ∧ ( 𝑘 mod 6 ) = 5 ) )
134 127 133 mprgbir ⊢ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( ( 𝑘 mod 6 ) = 1 ∧ ( 𝑘 mod 6 ) = 5 ) } = ∅
135 126 134 eqtri ⊢ ( { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } ∩ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } ) = ∅
136 hashun ⊢ ( ( { 𝑘 ∈ ( 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 ⊢ ( ♯ ‘ ( { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } ∪ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } ) ) = ( ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } ) + ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } ) )
138 119 137 eqtri ⊢ ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ) = ( ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } ) + ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } ) )
139 elfzelz ⊢ ( 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) → 𝑘 ∈ ℤ )
140 nnrp ⊢ ( 6 ∈ ℕ → 6 ∈ ℝ+ )
141 64 140 ax-mp ⊢ 6 ∈ ℝ+
142 0le1 ⊢ 0 ≤ 1
143 1lt6 ⊢ 1 < 6
144 modid ⊢ ( ( ( 1 ∈ ℝ ∧ 6 ∈ ℝ+ ) ∧ ( 0 ≤ 1 ∧ 1 < 6 ) ) → ( 1 mod 6 ) = 1 )
145 91 141 142 143 144 mp4an ⊢ ( 1 mod 6 ) = 1
146 145 eqeq2i ⊢ ( ( 𝑘 mod 6 ) = ( 1 mod 6 ) ↔ ( 𝑘 mod 6 ) = 1 )
147 1z ⊢ 1 ∈ ℤ
148 moddvds ⊢ ( ( 6 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( 𝑘 mod 6 ) = ( 1 mod 6 ) ↔ 6 ∥ ( 𝑘 − 1 ) ) )
149 64 147 148 mp3an13 ⊢ ( 𝑘 ∈ ℤ → ( ( 𝑘 mod 6 ) = ( 1 mod 6 ) ↔ 6 ∥ ( 𝑘 − 1 ) ) )
150 146 149 bitr3id ⊢ ( 𝑘 ∈ ℤ → ( ( 𝑘 mod 6 ) = 1 ↔ 6 ∥ ( 𝑘 − 1 ) ) )
151 139 150 syl ⊢ ( 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) → ( ( 𝑘 mod 6 ) = 1 ↔ 6 ∥ ( 𝑘 − 1 ) ) )
152 151 rabbiia ⊢ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } = { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ 6 ∥ ( 𝑘 − 1 ) }
153 152 fveq2i ⊢ ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } ) = ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ 6 ∥ ( 𝑘 − 1 ) } )
154 64 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → 6 ∈ ℕ )
155 4z ⊢ 4 ∈ ℤ
156 155 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → 4 ∈ ℤ )
157 4m1e3 ⊢ ( 4 − 1 ) = 3
158 157 fveq2i ⊢ ( ℤ≥ ‘ ( 4 − 1 ) ) = ( ℤ≥ ‘ 3 )
159 35 158 eleqtrrdi ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ⌊ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ ( 4 − 1 ) ) )
160 147 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → 1 ∈ ℤ )
161 154 156 159 160 hashdvds ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ 6 ∥ ( 𝑘 − 1 ) } ) = ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) − ( ⌊ ‘ ( ( ( 4 − 1 ) − 1 ) / 6 ) ) ) )
162 153 161 eqtrid ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } ) = ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) − ( ⌊ ‘ ( ( ( 4 − 1 ) − 1 ) / 6 ) ) ) )
163 2cn ⊢ 2 ∈ ℂ
164 ax-1cn ⊢ 1 ∈ ℂ
165 df-3 ⊢ 3 = ( 2 + 1 )
166 157 165 eqtri ⊢ ( 4 − 1 ) = ( 2 + 1 )
167 163 164 166 mvrraddi ⊢ ( ( 4 − 1 ) − 1 ) = 2
168 167 oveq1i ⊢ ( ( ( 4 − 1 ) − 1 ) / 6 ) = ( 2 / 6 )
169 168 fveq2i ⊢ ( ⌊ ‘ ( ( ( 4 − 1 ) − 1 ) / 6 ) ) = ( ⌊ ‘ ( 2 / 6 ) )
170 0re ⊢ 0 ∈ ℝ
171 64 nnne0i ⊢ 6 ≠ 0
172 7 96 171 redivcli ⊢ ( 2 / 6 ) ∈ ℝ
173 2pos ⊢ 0 < 2
174 7 96 173 98 divgt0ii ⊢ 0 < ( 2 / 6 )
175 170 172 174 ltleii ⊢ 0 ≤ ( 2 / 6 )
176 2lt6 ⊢ 2 < 6
177 6cn ⊢ 6 ∈ ℂ
178 177 mulridi ⊢ ( 6 · 1 ) = 6
179 176 178 breqtrri ⊢ 2 < ( 6 · 1 )
180 96 98 pm3.2i ⊢ ( 6 ∈ ℝ ∧ 0 < 6 )
181 ltdivmul ⊢ ( ( 2 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 6 ∈ ℝ ∧ 0 < 6 ) ) → ( ( 2 / 6 ) < 1 ↔ 2 < ( 6 · 1 ) ) )
182 7 91 180 181 mp3an ⊢ ( ( 2 / 6 ) < 1 ↔ 2 < ( 6 · 1 ) )
183 179 182 mpbir ⊢ ( 2 / 6 ) < 1
184 1e0p1 ⊢ 1 = ( 0 + 1 )
185 183 184 breqtri ⊢ ( 2 / 6 ) < ( 0 + 1 )
186 0z ⊢ 0 ∈ ℤ
187 flbi ⊢ ( ( ( 2 / 6 ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( ( ⌊ ‘ ( 2 / 6 ) ) = 0 ↔ ( 0 ≤ ( 2 / 6 ) ∧ ( 2 / 6 ) < ( 0 + 1 ) ) ) )
188 172 186 187 mp2an ⊢ ( ( ⌊ ‘ ( 2 / 6 ) ) = 0 ↔ ( 0 ≤ ( 2 / 6 ) ∧ ( 2 / 6 ) < ( 0 + 1 ) ) )
189 175 185 188 mpbir2an ⊢ ( ⌊ ‘ ( 2 / 6 ) ) = 0
190 169 189 eqtri ⊢ ( ⌊ ‘ ( ( ( 4 − 1 ) − 1 ) / 6 ) ) = 0
191 190 oveq2i ⊢ ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) − ( ⌊ ‘ ( ( ( 4 − 1 ) − 1 ) / 6 ) ) ) = ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) − 0 )
192 66 flcld ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) ∈ ℤ )
193 192 zcnd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) ∈ ℂ )
194 193 subid1d ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) − 0 ) = ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) )
195 191 194 eqtrid ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) − ( ⌊ ‘ ( ( ( 4 − 1 ) − 1 ) / 6 ) ) ) = ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) )
196 162 195 eqtrd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } ) = ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) )
197 5pos ⊢ 0 < 5
198 170 69 197 ltleii ⊢ 0 ≤ 5
199 5lt6 ⊢ 5 < 6
200 modid ⊢ ( ( ( 5 ∈ ℝ ∧ 6 ∈ ℝ+ ) ∧ ( 0 ≤ 5 ∧ 5 < 6 ) ) → ( 5 mod 6 ) = 5 )
201 69 141 198 199 200 mp4an ⊢ ( 5 mod 6 ) = 5
202 201 eqeq2i ⊢ ( ( 𝑘 mod 6 ) = ( 5 mod 6 ) ↔ ( 𝑘 mod 6 ) = 5 )
203 5nn ⊢ 5 ∈ ℕ
204 203 nnzi ⊢ 5 ∈ ℤ
205 moddvds ⊢ ( ( 6 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 5 ∈ ℤ ) → ( ( 𝑘 mod 6 ) = ( 5 mod 6 ) ↔ 6 ∥ ( 𝑘 − 5 ) ) )
206 64 204 205 mp3an13 ⊢ ( 𝑘 ∈ ℤ → ( ( 𝑘 mod 6 ) = ( 5 mod 6 ) ↔ 6 ∥ ( 𝑘 − 5 ) ) )
207 202 206 bitr3id ⊢ ( 𝑘 ∈ ℤ → ( ( 𝑘 mod 6 ) = 5 ↔ 6 ∥ ( 𝑘 − 5 ) ) )
208 139 207 syl ⊢ ( 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) → ( ( 𝑘 mod 6 ) = 5 ↔ 6 ∥ ( 𝑘 − 5 ) ) )
209 208 rabbiia ⊢ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } = { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ 6 ∥ ( 𝑘 − 5 ) }
210 209 fveq2i ⊢ ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } ) = ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ 6 ∥ ( 𝑘 − 5 ) } )
211 204 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → 5 ∈ ℤ )
212 154 156 159 211 hashdvds ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ 6 ∥ ( 𝑘 − 5 ) } ) = ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) − ( ⌊ ‘ ( ( ( 4 − 1 ) − 5 ) / 6 ) ) ) )
213 210 212 eqtrid ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } ) = ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) − ( ⌊ ‘ ( ( ( 4 − 1 ) − 5 ) / 6 ) ) ) )
214 157 oveq1i ⊢ ( ( 4 − 1 ) − 5 ) = ( 3 − 5 )
215 5cn ⊢ 5 ∈ ℂ
216 3cn ⊢ 3 ∈ ℂ
217 215 216 negsubdi2i ⊢ - ( 5 − 3 ) = ( 3 − 5 )
218 3p2e5 ⊢ ( 3 + 2 ) = 5
219 218 oveq1i ⊢ ( ( 3 + 2 ) − 3 ) = ( 5 − 3 )
220 pncan2 ⊢ ( ( 3 ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 3 + 2 ) − 3 ) = 2 )
221 216 163 220 mp2an ⊢ ( ( 3 + 2 ) − 3 ) = 2
222 219 221 eqtr3i ⊢ ( 5 − 3 ) = 2
223 222 negeqi ⊢ - ( 5 − 3 ) = - 2
224 214 217 223 3eqtr2i ⊢ ( ( 4 − 1 ) − 5 ) = - 2
225 224 oveq1i ⊢ ( ( ( 4 − 1 ) − 5 ) / 6 ) = ( - 2 / 6 )
226 divneg ⊢ ( ( 2 ∈ ℂ ∧ 6 ∈ ℂ ∧ 6 ≠ 0 ) → - ( 2 / 6 ) = ( - 2 / 6 ) )
227 163 177 171 226 mp3an ⊢ - ( 2 / 6 ) = ( - 2 / 6 )
228 225 227 eqtr4i ⊢ ( ( ( 4 − 1 ) − 5 ) / 6 ) = - ( 2 / 6 )
229 228 fveq2i ⊢ ( ⌊ ‘ ( ( ( 4 − 1 ) − 5 ) / 6 ) ) = ( ⌊ ‘ - ( 2 / 6 ) )
230 172 91 183 ltleii ⊢ ( 2 / 6 ) ≤ 1
231 172 91 lenegi ⊢ ( ( 2 / 6 ) ≤ 1 ↔ - 1 ≤ - ( 2 / 6 ) )
232 230 231 mpbi ⊢ - 1 ≤ - ( 2 / 6 )
233 170 172 ltnegi ⊢ ( 0 < ( 2 / 6 ) ↔ - ( 2 / 6 ) < - 0 )
234 174 233 mpbi ⊢ - ( 2 / 6 ) < - 0
235 neg0 ⊢ - 0 = 0
236 1pneg1e0 ⊢ ( 1 + - 1 ) = 0
237 235 236 eqtr4i ⊢ - 0 = ( 1 + - 1 )
238 neg1cn ⊢ - 1 ∈ ℂ
239 238 164 addcomi ⊢ ( - 1 + 1 ) = ( 1 + - 1 )
240 237 239 eqtr4i ⊢ - 0 = ( - 1 + 1 )
241 234 240 breqtri ⊢ - ( 2 / 6 ) < ( - 1 + 1 )
242 172 renegcli ⊢ - ( 2 / 6 ) ∈ ℝ
243 neg1z ⊢ - 1 ∈ ℤ
244 flbi ⊢ ( ( - ( 2 / 6 ) ∈ ℝ ∧ - 1 ∈ ℤ ) → ( ( ⌊ ‘ - ( 2 / 6 ) ) = - 1 ↔ ( - 1 ≤ - ( 2 / 6 ) ∧ - ( 2 / 6 ) < ( - 1 + 1 ) ) ) )
245 242 243 244 mp2an ⊢ ( ( ⌊ ‘ - ( 2 / 6 ) ) = - 1 ↔ ( - 1 ≤ - ( 2 / 6 ) ∧ - ( 2 / 6 ) < ( - 1 + 1 ) ) )
246 232 241 245 mpbir2an ⊢ ( ⌊ ‘ - ( 2 / 6 ) ) = - 1
247 229 246 eqtri ⊢ ( ⌊ ‘ ( ( ( 4 − 1 ) − 5 ) / 6 ) ) = - 1
248 247 oveq2i ⊢ ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) − ( ⌊ ‘ ( ( ( 4 − 1 ) − 5 ) / 6 ) ) ) = ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) − - 1 )
249 73 flcld ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) ∈ ℤ )
250 249 zcnd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) ∈ ℂ )
251 subneg ⊢ ( ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) − - 1 ) = ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) + 1 ) )
252 250 164 251 sylancl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) − - 1 ) = ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) + 1 ) )
253 248 252 eqtrid ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) − ( ⌊ ‘ ( ( ( 4 − 1 ) − 5 ) / 6 ) ) ) = ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) + 1 ) )
254 213 253 eqtrd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } ) = ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) + 1 ) )
255 196 254 oveq12d ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 1 } ) + ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) = 5 } ) ) = ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) + ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) + 1 ) ) )
256 138 255 eqtrid ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ) = ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 1 ) / 6 ) ) + ( ( ⌊ ‘ ( ( ( ⌊ ‘ 𝑁 ) − 5 ) / 6 ) ) + 1 ) ) )
257 82 recnd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → 𝑁 ∈ ℂ )
258 257 2timesd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
259 df-6 ⊢ 6 = ( 5 + 1 )
260 215 164 addcomi ⊢ ( 5 + 1 ) = ( 1 + 5 )
261 259 260 eqtri ⊢ 6 = ( 1 + 5 )
262 261 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → 6 = ( 1 + 5 ) )
263 258 262 oveq12d ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( 2 · 𝑁 ) − 6 ) = ( ( 𝑁 + 𝑁 ) − ( 1 + 5 ) ) )
264 addsub4 ⊢ ( ( ( 𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ∧ ( 1 ∈ ℂ ∧ 5 ∈ ℂ ) ) → ( ( 𝑁 + 𝑁 ) − ( 1 + 5 ) ) = ( ( 𝑁 − 1 ) + ( 𝑁 − 5 ) ) )
265 164 215 264 mpanr12 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑁 + 𝑁 ) − ( 1 + 5 ) ) = ( ( 𝑁 − 1 ) + ( 𝑁 − 5 ) ) )
266 257 257 265 syl2anc ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( 𝑁 + 𝑁 ) − ( 1 + 5 ) ) = ( ( 𝑁 − 1 ) + ( 𝑁 − 5 ) ) )
267 263 266 eqtrd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( 2 · 𝑁 ) − 6 ) = ( ( 𝑁 − 1 ) + ( 𝑁 − 5 ) ) )
268 267 oveq1d ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ( 2 · 𝑁 ) − 6 ) / 6 ) = ( ( ( 𝑁 − 1 ) + ( 𝑁 − 5 ) ) / 6 ) )
269 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 2 · 𝑁 ) ∈ ℂ )
270 163 257 269 sylancr ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( 2 · 𝑁 ) ∈ ℂ )
271 177 171 pm3.2i ⊢ ( 6 ∈ ℂ ∧ 6 ≠ 0 )
272 divsubdir ⊢ ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ 6 ∈ ℂ ∧ ( 6 ∈ ℂ ∧ 6 ≠ 0 ) ) → ( ( ( 2 · 𝑁 ) − 6 ) / 6 ) = ( ( ( 2 · 𝑁 ) / 6 ) − ( 6 / 6 ) ) )
273 177 271 272 mp3an23 ⊢ ( ( 2 · 𝑁 ) ∈ ℂ → ( ( ( 2 · 𝑁 ) − 6 ) / 6 ) = ( ( ( 2 · 𝑁 ) / 6 ) − ( 6 / 6 ) ) )
274 270 273 syl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ( 2 · 𝑁 ) − 6 ) / 6 ) = ( ( ( 2 · 𝑁 ) / 6 ) − ( 6 / 6 ) ) )
275 3t2e6 ⊢ ( 3 · 2 ) = 6
276 216 163 mulcomi ⊢ ( 3 · 2 ) = ( 2 · 3 )
277 275 276 eqtr3i ⊢ 6 = ( 2 · 3 )
278 277 oveq2i ⊢ ( ( 2 · 𝑁 ) / 6 ) = ( ( 2 · 𝑁 ) / ( 2 · 3 ) )
279 3ne0 ⊢ 3 ≠ 0
280 216 279 pm3.2i ⊢ ( 3 ∈ ℂ ∧ 3 ≠ 0 )
281 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
282 divcan5 ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 2 · 𝑁 ) / ( 2 · 3 ) ) = ( 𝑁 / 3 ) )
283 280 281 282 mp3an23 ⊢ ( 𝑁 ∈ ℂ → ( ( 2 · 𝑁 ) / ( 2 · 3 ) ) = ( 𝑁 / 3 ) )
284 257 283 syl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( 2 · 𝑁 ) / ( 2 · 3 ) ) = ( 𝑁 / 3 ) )
285 278 284 eqtrid ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( 2 · 𝑁 ) / 6 ) = ( 𝑁 / 3 ) )
286 177 171 dividi ⊢ ( 6 / 6 ) = 1
287 286 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( 6 / 6 ) = 1 )
288 285 287 oveq12d ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ( 2 · 𝑁 ) / 6 ) − ( 6 / 6 ) ) = ( ( 𝑁 / 3 ) − 1 ) )
289 274 288 eqtrd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ( 2 · 𝑁 ) − 6 ) / 6 ) = ( ( 𝑁 / 3 ) − 1 ) )
290 79 recnd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℂ )
291 84 recnd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( 𝑁 − 5 ) ∈ ℂ )
292 divdir ⊢ ( ( ( 𝑁 − 1 ) ∈ ℂ ∧ ( 𝑁 − 5 ) ∈ ℂ ∧ ( 6 ∈ ℂ ∧ 6 ≠ 0 ) ) → ( ( ( 𝑁 − 1 ) + ( 𝑁 − 5 ) ) / 6 ) = ( ( ( 𝑁 − 1 ) / 6 ) + ( ( 𝑁 − 5 ) / 6 ) ) )
293 271 292 mp3an3 ⊢ ( ( ( 𝑁 − 1 ) ∈ ℂ ∧ ( 𝑁 − 5 ) ∈ ℂ ) → ( ( ( 𝑁 − 1 ) + ( 𝑁 − 5 ) ) / 6 ) = ( ( ( 𝑁 − 1 ) / 6 ) + ( ( 𝑁 − 5 ) / 6 ) ) )
294 290 291 293 syl2anc ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ( 𝑁 − 1 ) + ( 𝑁 − 5 ) ) / 6 ) = ( ( ( 𝑁 − 1 ) / 6 ) + ( ( 𝑁 − 5 ) / 6 ) ) )
295 268 289 294 3eqtr3d ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( 𝑁 / 3 ) − 1 ) = ( ( ( 𝑁 − 1 ) / 6 ) + ( ( 𝑁 − 5 ) / 6 ) ) )
296 295 oveq1d ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ( 𝑁 / 3 ) − 1 ) + 1 ) = ( ( ( ( 𝑁 − 1 ) / 6 ) + ( ( 𝑁 − 5 ) / 6 ) ) + 1 ) )
297 21 recnd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( 𝑁 / 3 ) ∈ ℂ )
298 npcan ⊢ ( ( ( 𝑁 / 3 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝑁 / 3 ) − 1 ) + 1 ) = ( 𝑁 / 3 ) )
299 297 164 298 sylancl ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ( 𝑁 / 3 ) − 1 ) + 1 ) = ( 𝑁 / 3 ) )
300 81 recnd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( 𝑁 − 1 ) / 6 ) ∈ ℂ )
301 86 recnd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( 𝑁 − 5 ) / 6 ) ∈ ℂ )
302 164 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → 1 ∈ ℂ )
303 300 301 302 addassd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ( ( 𝑁 − 1 ) / 6 ) + ( ( 𝑁 − 5 ) / 6 ) ) + 1 ) = ( ( ( 𝑁 − 1 ) / 6 ) + ( ( ( 𝑁 − 5 ) / 6 ) + 1 ) ) )
304 296 299 303 3eqtr3d ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( 𝑁 / 3 ) = ( ( ( 𝑁 − 1 ) / 6 ) + ( ( ( 𝑁 − 5 ) / 6 ) + 1 ) ) )
305 113 256 304 3brtr4d ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ♯ ‘ { 𝑘 ∈ ( 4 ... ( ⌊ ‘ 𝑁 ) ) ∣ ( 𝑘 mod 6 ) ∈ { 1 , 5 } } ) ≤ ( 𝑁 / 3 ) )
306 9 17 21 59 305 letrd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( π ‘ 𝑁 ) − 2 ) ≤ ( 𝑁 / 3 ) )
307 7 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → 2 ∈ ℝ )
308 6 307 21 lesubaddd ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( ( ( π ‘ 𝑁 ) − 2 ) ≤ ( 𝑁 / 3 ) ↔ ( π ‘ 𝑁 ) ≤ ( ( 𝑁 / 3 ) + 2 ) ) )
309 306 308 mpbid ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ≤ 𝑁 ) → ( π ‘ 𝑁 ) ≤ ( ( 𝑁 / 3 ) + 2 ) )
310 309 adantlr ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) ∧ 3 ≤ 𝑁 ) → ( π ‘ 𝑁 ) ≤ ( ( 𝑁 / 3 ) + 2 ) )
311 5 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) ∧ 𝑁 ≤ 3 ) → ( π ‘ 𝑁 ) ∈ ℝ )
312 7 a1i ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) ∧ 𝑁 ≤ 3 ) → 2 ∈ ℝ )
313 20 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) ∧ 𝑁 ≤ 3 ) → ( 𝑁 / 3 ) ∈ ℝ )
314 readdcl ⊢ ( ( ( 𝑁 / 3 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( 𝑁 / 3 ) + 2 ) ∈ ℝ )
315 313 7 314 sylancl ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) ∧ 𝑁 ≤ 3 ) → ( ( 𝑁 / 3 ) + 2 ) ∈ ℝ )
316 ppiwordi ⊢ ( ( 𝑁 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ≤ 3 ) → ( π ‘ 𝑁 ) ≤ ( π ‘ 3 ) )
317 1 316 mp3an2 ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑁 ≤ 3 ) → ( π ‘ 𝑁 ) ≤ ( π ‘ 3 ) )
318 317 adantlr ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) ∧ 𝑁 ≤ 3 ) → ( π ‘ 𝑁 ) ≤ ( π ‘ 3 ) )
319 318 24 breqtrdi ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) ∧ 𝑁 ≤ 3 ) → ( π ‘ 𝑁 ) ≤ 2 )
320 3pos ⊢ 0 < 3
321 divge0 ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ) → 0 ≤ ( 𝑁 / 3 ) )
322 1 320 321 mpanr12 ⊢ ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) → 0 ≤ ( 𝑁 / 3 ) )
323 322 adantr ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) ∧ 𝑁 ≤ 3 ) → 0 ≤ ( 𝑁 / 3 ) )
324 addge02 ⊢ ( ( 2 ∈ ℝ ∧ ( 𝑁 / 3 ) ∈ ℝ ) → ( 0 ≤ ( 𝑁 / 3 ) ↔ 2 ≤ ( ( 𝑁 / 3 ) + 2 ) ) )
325 7 313 324 sylancr ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) ∧ 𝑁 ≤ 3 ) → ( 0 ≤ ( 𝑁 / 3 ) ↔ 2 ≤ ( ( 𝑁 / 3 ) + 2 ) ) )
326 323 325 mpbid ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) ∧ 𝑁 ≤ 3 ) → 2 ≤ ( ( 𝑁 / 3 ) + 2 ) )
327 311 312 315 319 326 letrd ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) ∧ 𝑁 ≤ 3 ) → ( π ‘ 𝑁 ) ≤ ( ( 𝑁 / 3 ) + 2 ) )
328 2 3 310 327 lecasei ⊢ ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) → ( π ‘ 𝑁 ) ≤ ( ( 𝑁 / 3 ) + 2 ) )