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 ) )