ppiqub - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > ppiqub		GIF version

Theorem ppiqub 16293

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

**Assertion**
Ref	Expression
ppiqub	⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))

Proof of Theorem ppiqub Dummy variables 𝑥 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ppiqcl 16251	. . . . . . . 8 ⊢ (𝑁 ∈ ℚ → (π‘𝑁) ∈ ℕ₀)
2	1	nn0red 9632	. . . . . . 7 ⊢ (𝑁 ∈ ℚ → (π‘𝑁) ∈ ℝ)
3	2	adantr 276	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (π‘𝑁) ∈ ℝ)
4		2re 9383	. . . . . 6 ⊢ 2 ∈ ℝ
5		resubcl 8597	. . . . . 6 ⊢ (((π‘𝑁) ∈ ℝ ∧ 2 ∈ ℝ) → ((π‘𝑁) − 2) ∈ ℝ)
6	3, 4, 5	sylancl 417	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ∈ ℝ)
7		4z 9685	. . . . . . . . . . 11 ⊢ 4 ∈ ℤ
8	7	a1i 9	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℚ → 4 ∈ ℤ)
9		flqcl 10725	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℚ → (⌊‘𝑁) ∈ ℤ)
10	8, 9	fzfigd 10889	. . . . . . . . 9 ⊢ (𝑁 ∈ ℚ → (4...(⌊‘𝑁)) ∈ Fin)
11		ssrab2 3333	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ⊆ (4...(⌊‘𝑁))
12	11	a1i 9	. . . . . . . . 9 ⊢ (𝑁 ∈ ℚ → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ⊆ (4...(⌊‘𝑁)))
13		animorrl 838	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → (𝑥 ∈ (4...(⌊‘𝑁)) ∨ ¬ 𝑥 ∈ (4...(⌊‘𝑁))))
14		df-dc 847	. . . . . . . . . . . . 13 ⊢ (DECID 𝑥 ∈ (4...(⌊‘𝑁)) ↔ (𝑥 ∈ (4...(⌊‘𝑁)) ∨ ¬ 𝑥 ∈ (4...(⌊‘𝑁))))
15	13, 14	sylibr 134	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → DECID 𝑥 ∈ (4...(⌊‘𝑁)))
16		elfzelz 10445	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (4...(⌊‘𝑁)) → 𝑥 ∈ ℤ)
17	16	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → 𝑥 ∈ ℤ)
18		6nn 9481	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℕ
19		zmodcl 10802	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ 6 ∈ ℕ) → (𝑥 mod 6) ∈ ℕ₀)
20	17, 18, 19	sylancl 417	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → (𝑥 mod 6) ∈ ℕ₀)
21	20	nn0zd 9777	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → (𝑥 mod 6) ∈ ℤ)
22		1z 9681	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
23		zdceq 9731	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 mod 6) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑥 mod 6) = 1)
24	21, 22, 23	sylancl 417	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → DECID (𝑥 mod 6) = 1)
25		5nn 9480	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ ℕ
26	25	nnzi 9676	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℤ
27		zdceq 9731	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 mod 6) ∈ ℤ ∧ 5 ∈ ℤ) → DECID (𝑥 mod 6) = 5)
28	21, 26, 27	sylancl 417	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → DECID (𝑥 mod 6) = 5)
29		dcor 948	. . . . . . . . . . . . . 14 ⊢ (DECID (𝑥 mod 6) = 1 → (DECID (𝑥 mod 6) = 5 → DECID ((𝑥 mod 6) = 1 ∨ (𝑥 mod 6) = 5)))
30	24, 28, 29	sylc 62	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → DECID ((𝑥 mod 6) = 1 ∨ (𝑥 mod 6) = 5))
31		elprg 3729	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 mod 6) ∈ ℕ₀ → ((𝑥 mod 6) ∈ {1, 5} ↔ ((𝑥 mod 6) = 1 ∨ (𝑥 mod 6) = 5)))
32	20, 31	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → ((𝑥 mod 6) ∈ {1, 5} ↔ ((𝑥 mod 6) = 1 ∨ (𝑥 mod 6) = 5)))
33	32	dcbid 850	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → (DECID (𝑥 mod 6) ∈ {1, 5} ↔ DECID ((𝑥 mod 6) = 1 ∨ (𝑥 mod 6) = 5)))
34	30, 33	mpbird 167	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → DECID (𝑥 mod 6) ∈ {1, 5})
35	15, 34	dcand 945	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → DECID (𝑥 ∈ (4...(⌊‘𝑁)) ∧ (𝑥 mod 6) ∈ {1, 5}))
36		oveq1 6095	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑘 mod 6) = (𝑥 mod 6))
37	36	eleq1d 2307	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → ((𝑘 mod 6) ∈ {1, 5} ↔ (𝑥 mod 6) ∈ {1, 5}))
38	37	elrab 2982	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ↔ (𝑥 ∈ (4...(⌊‘𝑁)) ∧ (𝑥 mod 6) ∈ {1, 5}))
39	38	dcbii 852	. . . . . . . . . . 11 ⊢ (DECID 𝑥 ∈ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ↔ DECID (𝑥 ∈ (4...(⌊‘𝑁)) ∧ (𝑥 mod 6) ∈ {1, 5}))
40	35, 39	sylibr 134	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → DECID 𝑥 ∈ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}})
41	40	ralrimiva 2623	. . . . . . . . 9 ⊢ (𝑁 ∈ ℚ → ∀𝑥 ∈ (4...(⌊‘𝑁))DECID 𝑥 ∈ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}})
42		ssfidc 7249	. . . . . . . . 9 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ⊆ (4...(⌊‘𝑁)) ∧ ∀𝑥 ∈ (4...(⌊‘𝑁))DECID 𝑥 ∈ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ∈ Fin)
43	10, 12, 41, 42	syl3anc 1278	. . . . . . . 8 ⊢ (𝑁 ∈ ℚ → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ∈ Fin)
44		hashcl 11242	. . . . . . . 8 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ∈ Fin → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℕ₀)
45	43, 44	syl 14	. . . . . . 7 ⊢ (𝑁 ∈ ℚ → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℕ₀)
46	45	nn0red 9632	. . . . . 6 ⊢ (𝑁 ∈ ℚ → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℝ)
47	46	adantr 276	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℝ)
48		qre 10041	. . . . . . 7 ⊢ (𝑁 ∈ ℚ → 𝑁 ∈ ℝ)
49		3nn 9478	. . . . . . 7 ⊢ 3 ∈ ℕ
50		nndivre 9349	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℕ) → (𝑁 / 3) ∈ ℝ)
51	48, 49, 50	sylancl 417	. . . . . 6 ⊢ (𝑁 ∈ ℚ → (𝑁 / 3) ∈ ℝ)
52	51	adantr 276	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 / 3) ∈ ℝ)
53		ppiqfl 16266	. . . . . . . . 9 ⊢ (𝑁 ∈ ℚ → (π‘(⌊‘𝑁)) = (π‘𝑁))
54	53	adantr 276	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (π‘(⌊‘𝑁)) = (π‘𝑁))
55		ppi3 16275	. . . . . . . . 9 ⊢ (π‘3) = 2
56	55	a1i 9	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (π‘3) = 2)
57	54, 56	oveq12d 6106	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = ((π‘𝑁) − 2))
58		3z 9684	. . . . . . . . . . 11 ⊢ 3 ∈ ℤ
59	58	a1i 9	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 3 ∈ ℤ)
60	9	adantr 276	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ ℤ)
61		flqge 10736	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℚ ∧ 3 ∈ ℤ) → (3 ≤ 𝑁 ↔ 3 ≤ (⌊‘𝑁)))
62	58, 61	mpan2 429	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℚ → (3 ≤ 𝑁 ↔ 3 ≤ (⌊‘𝑁)))
63	62	biimpa 296	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 3 ≤ (⌊‘𝑁))
64		eluz2 9943	. . . . . . . . . 10 ⊢ ((⌊‘𝑁) ∈ (ℤ_≥‘3) ↔ (3 ∈ ℤ ∧ (⌊‘𝑁) ∈ ℤ ∧ 3 ≤ (⌊‘𝑁)))
65	59, 60, 63, 64	syl3anbrc 1212	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ (ℤ_≥‘3))
66		ppidif 16269	. . . . . . . . 9 ⊢ ((⌊‘𝑁) ∈ (ℤ_≥‘3) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ)))
67	65, 66	syl 14	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ)))
68		df-4 9374	. . . . . . . . . . 11 ⊢ 4 = (3 + 1)
69	68	oveq1i 6098	. . . . . . . . . 10 ⊢ (4...(⌊‘𝑁)) = ((3 + 1)...(⌊‘𝑁))
70	69	ineq1i 3428	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) = (((3 + 1)...(⌊‘𝑁)) ∩ ℙ)
71	70	fveq2i 5701	. . . . . . . 8 ⊢ (♯‘((4...(⌊‘𝑁)) ∩ ℙ)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ))
72	67, 71	eqtr4di 2289	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘((4...(⌊‘𝑁)) ∩ ℙ)))
73	57, 72	eqtr3d 2273	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) = (♯‘((4...(⌊‘𝑁)) ∩ ℙ)))
74		dfin5 3227	. . . . . . . . . 10 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 𝑘 ∈ ℙ}
75		elfzle1 10448	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 4 ≤ 𝑘)
76		ppiublem2 16292	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℙ ∧ 4 ≤ 𝑘) → (𝑘 mod 6) ∈ {1, 5})
77	76	expcom 116	. . . . . . . . . . . 12 ⊢ (4 ≤ 𝑘 → (𝑘 ∈ ℙ → (𝑘 mod 6) ∈ {1, 5}))
78	75, 77	syl 14	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → (𝑘 ∈ ℙ → (𝑘 mod 6) ∈ {1, 5}))
79	78	ss2rabi 3330	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 𝑘 ∈ ℙ} ⊆ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}
80	74, 79	eqsstri 3280	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}
81		ssdomg 7069	. . . . . . . . 9 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ∈ Fin → (((4...(⌊‘𝑁)) ∩ ℙ) ⊆ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} → ((4...(⌊‘𝑁)) ∩ ℙ) ≼ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}))
82	43, 80, 81	mpisyl 1496	. . . . . . . 8 ⊢ (𝑁 ∈ ℚ → ((4...(⌊‘𝑁)) ∩ ℙ) ≼ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}})
83		inss1 3451	. . . . . . . . . . 11 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ (4...(⌊‘𝑁))
84	83	a1i 9	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℚ → ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ (4...(⌊‘𝑁)))
85		prmdcz 12934	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℤ → DECID 𝑥 ∈ ℙ)
86	17, 85	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → DECID 𝑥 ∈ ℙ)
87	15, 86	dcand 945	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → DECID (𝑥 ∈ (4...(⌊‘𝑁)) ∧ 𝑥 ∈ ℙ))
88		elin 3412	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ((4...(⌊‘𝑁)) ∩ ℙ) ↔ (𝑥 ∈ (4...(⌊‘𝑁)) ∧ 𝑥 ∈ ℙ))
89	88	dcbii 852	. . . . . . . . . . . 12 ⊢ (DECID 𝑥 ∈ ((4...(⌊‘𝑁)) ∩ ℙ) ↔ DECID (𝑥 ∈ (4...(⌊‘𝑁)) ∧ 𝑥 ∈ ℙ))
90	87, 89	sylibr 134	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → DECID 𝑥 ∈ ((4...(⌊‘𝑁)) ∩ ℙ))
91	90	ralrimiva 2623	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℚ → ∀𝑥 ∈ (4...(⌊‘𝑁))DECID 𝑥 ∈ ((4...(⌊‘𝑁)) ∩ ℙ))
92		ssfidc 7249	. . . . . . . . . 10 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ (4...(⌊‘𝑁)) ∧ ∀𝑥 ∈ (4...(⌊‘𝑁))DECID 𝑥 ∈ ((4...(⌊‘𝑁)) ∩ ℙ)) → ((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin)
93	10, 84, 91, 92	syl3anc 1278	. . . . . . . . 9 ⊢ (𝑁 ∈ ℚ → ((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin)
94		fihashdom 11265	. . . . . . . . 9 ⊢ ((((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ∈ Fin) → ((♯‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ↔ ((4...(⌊‘𝑁)) ∩ ℙ) ≼ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}))
95	93, 43, 94	syl2anc 415	. . . . . . . 8 ⊢ (𝑁 ∈ ℚ → ((♯‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ↔ ((4...(⌊‘𝑁)) ∩ ℙ) ≼ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}))
96	82, 95	mpbird 167	. . . . . . 7 ⊢ (𝑁 ∈ ℚ → (♯‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}))
97	96	adantr 276	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (♯‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}))
98	73, 97	eqbrtrd 4153	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ≤ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}))
99		peano2zm 9693	. . . . . . . . . . 11 ⊢ ((⌊‘𝑁) ∈ ℤ → ((⌊‘𝑁) − 1) ∈ ℤ)
100	60, 99	syl 14	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ∈ ℤ)
101		znq 10040	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 1) ∈ ℤ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 1) / 6) ∈ ℚ)
102	100, 18, 101	sylancl 417	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) / 6) ∈ ℚ)
103	102	flqcld 10731	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℤ)
104	103	zred 9779	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℝ)
105	26	a1i 9	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 5 ∈ ℤ)
106	60, 105	zsubcld 9784	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ∈ ℤ)
107		znq 10040	. . . . . . . . . . 11 ⊢ ((((⌊‘𝑁) − 5) ∈ ℤ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 5) / 6) ∈ ℚ)
108	106, 18, 107	sylancl 417	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) / 6) ∈ ℚ)
109	108	flqcld 10731	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℤ)
110	109	zred 9779	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ)
111		peano2re 8469	. . . . . . . 8 ⊢ ((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈ ℝ)
112	110, 111	syl 14	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈ ℝ)
113		peano2rem 8600	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
114	48, 113	syl 14	. . . . . . . . 9 ⊢ (𝑁 ∈ ℚ → (𝑁 − 1) ∈ ℝ)
115	114	adantr 276	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℝ)
116		nndivre 9349	. . . . . . . 8 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝑁 − 1) / 6) ∈ ℝ)
117	115, 18, 116	sylancl 417	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((𝑁 − 1) / 6) ∈ ℝ)
118	48	adantr 276	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℝ)
119		5re 9392	. . . . . . . . . 10 ⊢ 5 ∈ ℝ
120		resubcl 8597	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 5 ∈ ℝ) → (𝑁 − 5) ∈ ℝ)
121	118, 119, 120	sylancl 417	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 − 5) ∈ ℝ)
122		nndivre 9349	. . . . . . . . 9 ⊢ (((𝑁 − 5) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝑁 − 5) / 6) ∈ ℝ)
123	121, 18, 122	sylancl 417	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((𝑁 − 5) / 6) ∈ ℝ)
124		peano2re 8469	. . . . . . . 8 ⊢ (((𝑁 − 5) / 6) ∈ ℝ → (((𝑁 − 5) / 6) + 1) ∈ ℝ)
125	123, 124	syl 14	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((𝑁 − 5) / 6) + 1) ∈ ℝ)
126		qre 10041	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 1) / 6) ∈ ℚ → (((⌊‘𝑁) − 1) / 6) ∈ ℝ)
127	102, 126	syl 14	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) / 6) ∈ ℝ)
128		flqle 10732	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 1) / 6) ∈ ℚ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ (((⌊‘𝑁) − 1) / 6))
129	102, 128	syl 14	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ (((⌊‘𝑁) − 1) / 6))
130	60	zred 9779	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ ℝ)
131		1red 8347	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 1 ∈ ℝ)
132		flqle 10732	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℚ → (⌊‘𝑁) ≤ 𝑁)
133	132	adantr 276	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ≤ 𝑁)
134	130, 118, 131, 133	lesub1dd 8896	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ≤ (𝑁 − 1))
135	100	zred 9779	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ∈ ℝ)
136		6re 9394	. . . . . . . . . . 11 ⊢ 6 ∈ ℝ
137	136	a1i 9	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 6 ∈ ℝ)
138		6pos 9414	. . . . . . . . . . 11 ⊢ 0 < 6
139	138	a1i 9	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 0 < 6)
140		lediv1 9207	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 1) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6)) → (((⌊‘𝑁) − 1) ≤ (𝑁 − 1) ↔ (((⌊‘𝑁) − 1) / 6) ≤ ((𝑁 − 1) / 6)))
141	135, 115, 137, 139, 140	syl112anc 1282	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) ≤ (𝑁 − 1) ↔ (((⌊‘𝑁) − 1) / 6) ≤ ((𝑁 − 1) / 6)))
142	134, 141	mpbid 147	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) / 6) ≤ ((𝑁 − 1) / 6))
143	104, 127, 117, 129, 142	letrd 8457	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ ((𝑁 − 1) / 6))
144		resubcl 8597	. . . . . . . . . . 11 ⊢ (((⌊‘𝑁) ∈ ℝ ∧ 5 ∈ ℝ) → ((⌊‘𝑁) − 5) ∈ ℝ)
145	130, 119, 144	sylancl 417	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ∈ ℝ)
146		nndivre 9349	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 5) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 5) / 6) ∈ ℝ)
147	145, 18, 146	sylancl 417	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) / 6) ∈ ℝ)
148		flqle 10732	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 5) / 6) ∈ ℚ → (⌊‘(((⌊‘𝑁) − 5) / 6)) ≤ (((⌊‘𝑁) − 5) / 6))
149	108, 148	syl 14	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ≤ (((⌊‘𝑁) − 5) / 6))
150	119	a1i 9	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 5 ∈ ℝ)
151	130, 118, 150, 133	lesub1dd 8896	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ≤ (𝑁 − 5))
152		lediv1 9207	. . . . . . . . . . 11 ⊢ ((((⌊‘𝑁) − 5) ∈ ℝ ∧ (𝑁 − 5) ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6)) → (((⌊‘𝑁) − 5) ≤ (𝑁 − 5) ↔ (((⌊‘𝑁) − 5) / 6) ≤ ((𝑁 − 5) / 6)))
153	145, 121, 137, 139, 152	syl112anc 1282	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) ≤ (𝑁 − 5) ↔ (((⌊‘𝑁) − 5) / 6) ≤ ((𝑁 − 5) / 6)))
154	151, 153	mpbid 147	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) / 6) ≤ ((𝑁 − 5) / 6))
155	110, 147, 123, 149, 154	letrd 8457	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ≤ ((𝑁 − 5) / 6))
156	110, 123, 131, 155	leadd1dd 8894	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ≤ (((𝑁 − 5) / 6) + 1))
157	104, 112, 117, 125, 143, 156	le2addd 8899	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) ≤ (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
158		elfzelz 10445	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 𝑘 ∈ ℤ)
159	18	a1i 9	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 6 ∈ ℕ)
160	158, 159	zmodcld 10803	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → (𝑘 mod 6) ∈ ℕ₀)
161		elprg 3729	. . . . . . . . . . . . 13 ⊢ ((𝑘 mod 6) ∈ ℕ₀ → ((𝑘 mod 6) ∈ {1, 5} ↔ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)))
162	160, 161	syl 14	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → ((𝑘 mod 6) ∈ {1, 5} ↔ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)))
163	162	rabbiia 2807	. . . . . . . . . . 11 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)}
164		unrab 3504	. . . . . . . . . . 11 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)}
165	163, 164	eqtr4i 2262	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} = ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})
166	165	fveq2i 5701	. . . . . . . . 9 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = (♯‘({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}))
167		ssrab2 3333	. . . . . . . . . . . 12 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ⊆ (4...(⌊‘𝑁))
168	167	a1i 9	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℚ → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ⊆ (4...(⌊‘𝑁)))
169	15, 24	dcand 945	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → DECID (𝑥 ∈ (4...(⌊‘𝑁)) ∧ (𝑥 mod 6) = 1))
170	36	eqeq1d 2247	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → ((𝑘 mod 6) = 1 ↔ (𝑥 mod 6) = 1))
171	170	elrab 2982	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ↔ (𝑥 ∈ (4...(⌊‘𝑁)) ∧ (𝑥 mod 6) = 1))
172	171	dcbii 852	. . . . . . . . . . . . 13 ⊢ (DECID 𝑥 ∈ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ↔ DECID (𝑥 ∈ (4...(⌊‘𝑁)) ∧ (𝑥 mod 6) = 1))
173	169, 172	sylibr 134	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → DECID 𝑥 ∈ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1})
174	173	ralrimiva 2623	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℚ → ∀𝑥 ∈ (4...(⌊‘𝑁))DECID 𝑥 ∈ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1})
175		ssfidc 7249	. . . . . . . . . . 11 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ⊆ (4...(⌊‘𝑁)) ∧ ∀𝑥 ∈ (4...(⌊‘𝑁))DECID 𝑥 ∈ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∈ Fin)
176	10, 168, 174, 175	syl3anc 1278	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℚ → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∈ Fin)
177		ssrab2 3333	. . . . . . . . . . . 12 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ⊆ (4...(⌊‘𝑁))
178	177	a1i 9	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℚ → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ⊆ (4...(⌊‘𝑁)))
179	15, 28	dcand 945	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → DECID (𝑥 ∈ (4...(⌊‘𝑁)) ∧ (𝑥 mod 6) = 5))
180	36	eqeq1d 2247	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → ((𝑘 mod 6) = 5 ↔ (𝑥 mod 6) = 5))
181	180	elrab 2982	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ↔ (𝑥 ∈ (4...(⌊‘𝑁)) ∧ (𝑥 mod 6) = 5))
182	181	dcbii 852	. . . . . . . . . . . . 13 ⊢ (DECID 𝑥 ∈ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ↔ DECID (𝑥 ∈ (4...(⌊‘𝑁)) ∧ (𝑥 mod 6) = 5))
183	179, 182	sylibr 134	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → DECID 𝑥 ∈ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})
184	183	ralrimiva 2623	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℚ → ∀𝑥 ∈ (4...(⌊‘𝑁))DECID 𝑥 ∈ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})
185		ssfidc 7249	. . . . . . . . . . 11 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ⊆ (4...(⌊‘𝑁)) ∧ ∀𝑥 ∈ (4...(⌊‘𝑁))DECID 𝑥 ∈ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ∈ Fin)
186	10, 178, 184, 185	syl3anc 1278	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℚ → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ∈ Fin)
187		inrab 3505	. . . . . . . . . . . 12 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∩ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)}
188		rabeq0 3552	. . . . . . . . . . . . 13 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)} = ∅ ↔ ∀𝑘 ∈ (4...(⌊‘𝑁)) ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5))
189		1re 8331	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℝ
190		1lt5 9494	. . . . . . . . . . . . . . . 16 ⊢ 1 < 5
191	189, 190	ltneii 8429	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 5
192		eqtr2 2257	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5) → 1 = 5)
193	192	necon3ai 2469	. . . . . . . . . . . . . . 15 ⊢ (1 ≠ 5 → ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5))
194	191, 193	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)
195	194	a1i 9	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5))
196	188, 195	mprgbir 2608	. . . . . . . . . . . 12 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)} = ∅
197	187, 196	eqtri 2259	. . . . . . . . . . 11 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∩ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ∅
198	197	a1i 9	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℚ → ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∩ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ∅)
199		hashun 11267	. . . . . . . . . 10 ⊢ (({𝑘 ∈ (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})))
200	176, 186, 198, 199	syl3anc 1278	. . . . . . . . 9 ⊢ (𝑁 ∈ ℚ → (♯‘({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})) = ((♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})))
201	166, 200	eqtrid 2283	. . . . . . . 8 ⊢ (𝑁 ∈ ℚ → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = ((♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})))
202	201	adantr 276	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = ((♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})))
203		zq 10042	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
204	22, 203	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℚ
205		nnq 10049	. . . . . . . . . . . . . . . . 17 ⊢ (6 ∈ ℕ → 6 ∈ ℚ)
206	18, 205	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ ℚ
207		0le1 8816	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 1
208		1lt6 9499	. . . . . . . . . . . . . . . 16 ⊢ 1 < 6
209		modqid 10807	. . . . . . . . . . . . . . . 16 ⊢ (((1 ∈ ℚ ∧ 6 ∈ ℚ) ∧ (0 ≤ 1 ∧ 1 < 6)) → (1 mod 6) = 1)
210	204, 206, 207, 208, 209	mp4an 431	. . . . . . . . . . . . . . 15 ⊢ (1 mod 6) = 1
211	210	eqeq2i 2249	. . . . . . . . . . . . . 14 ⊢ ((𝑘 mod 6) = (1 mod 6) ↔ (𝑘 mod 6) = 1)
212		moddvds 12591	. . . . . . . . . . . . . . 15 ⊢ ((6 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑘 mod 6) = (1 mod 6) ↔ 6 ∥ (𝑘 − 1)))
213	18, 22, 212	mp3an13 1369	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = (1 mod 6) ↔ 6 ∥ (𝑘 − 1)))
214	211, 213	bitr3id 194	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = 1 ↔ 6 ∥ (𝑘 − 1)))
215	158, 214	syl 14	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → ((𝑘 mod 6) = 1 ↔ 6 ∥ (𝑘 − 1)))
216	215	rabbiia 2807	. . . . . . . . . . 11 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)}
217	216	fveq2i 5701	. . . . . . . . . 10 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)})
218	18	a1i 9	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 6 ∈ ℕ)
219	7	a1i 9	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 4 ∈ ℤ)
220		4m1e3 9434	. . . . . . . . . . . . 13 ⊢ (4 − 1) = 3
221	220	fveq2i 5701	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘(4 − 1)) = (ℤ_≥‘3)
222	65, 221	eleqtrrdi 2332	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ (ℤ_≥‘(4 − 1)))
223		1zzd 9682	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 1 ∈ ℤ)
224	218, 219, 222, 223	hashdvds 13028	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))))
225	217, 224	eqtrid 2283	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))))
226		2cn 9384	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
227		ax-1cn 8278	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
228		df-3 9373	. . . . . . . . . . . . . . . 16 ⊢ 3 = (2 + 1)
229	220, 228	eqtri 2259	. . . . . . . . . . . . . . 15 ⊢ (4 − 1) = (2 + 1)
230	226, 227, 229	mvrraddi 8550	. . . . . . . . . . . . . 14 ⊢ ((4 − 1) − 1) = 2
231	230	oveq1i 6098	. . . . . . . . . . . . 13 ⊢ (((4 − 1) − 1) / 6) = (2 / 6)
232	231	fveq2i 5701	. . . . . . . . . . . 12 ⊢ (⌊‘(((4 − 1) − 1) / 6)) = (⌊‘(2 / 6))
233		0re 8332	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
234	136, 138	gt0ap0ii 8964	. . . . . . . . . . . . . . 15 ⊢ 6 # 0
235	4, 136, 234	redivclapi 9117	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ∈ ℝ
236		2pos 9404	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
237	4, 136, 236, 138	divgt0ii 9257	. . . . . . . . . . . . . 14 ⊢ 0 < (2 / 6)
238	233, 235, 237	ltleii 8435	. . . . . . . . . . . . 13 ⊢ 0 ≤ (2 / 6)
239		2lt6 9498	. . . . . . . . . . . . . . . 16 ⊢ 2 < 6
240		6cn 9395	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℂ
241	240	mulridi 8334	. . . . . . . . . . . . . . . 16 ⊢ (6 · 1) = 6
242	239, 241	breqtrri 4158	. . . . . . . . . . . . . . 15 ⊢ 2 < (6 · 1)
243	136, 138	pm3.2i 272	. . . . . . . . . . . . . . . 16 ⊢ (6 ∈ ℝ ∧ 0 < 6)
244		ltdivmul 9214	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ ∧ 1 ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6)) → ((2 / 6) < 1 ↔ 2 < (6 · 1)))
245	4, 189, 243, 244	mp3an 1378	. . . . . . . . . . . . . . 15 ⊢ ((2 / 6) < 1 ↔ 2 < (6 · 1))
246	242, 245	mpbir 146	. . . . . . . . . . . . . 14 ⊢ (2 / 6) < 1
247		1e0p1 9834	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
248	246, 247	breqtri 4156	. . . . . . . . . . . . 13 ⊢ (2 / 6) < (0 + 1)
249		2z 9683	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
250		znq 10040	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℤ ∧ 6 ∈ ℕ) → (2 / 6) ∈ ℚ)
251	249, 18, 250	mp2an 430	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ∈ ℚ
252		0z 9666	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℤ
253		flqbi 10746	. . . . . . . . . . . . . 14 ⊢ (((2 / 6) ∈ ℚ ∧ 0 ∈ ℤ) → ((⌊‘(2 / 6)) = 0 ↔ (0 ≤ (2 / 6) ∧ (2 / 6) < (0 + 1))))
254	251, 252, 253	mp2an 430	. . . . . . . . . . . . 13 ⊢ ((⌊‘(2 / 6)) = 0 ↔ (0 ≤ (2 / 6) ∧ (2 / 6) < (0 + 1)))
255	238, 248, 254	mpbir2an 955	. . . . . . . . . . . 12 ⊢ (⌊‘(2 / 6)) = 0
256	232, 255	eqtri 2259	. . . . . . . . . . 11 ⊢ (⌊‘(((4 − 1) − 1) / 6)) = 0
257	256	oveq2i 6099	. . . . . . . . . 10 ⊢ ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − 0)
258	103	zcnd 9780	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℂ)
259	258	subid1d 8633	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) − 0) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
260	257, 259	eqtrid 2283	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
261	225, 260	eqtrd 2271	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
262		nnq 10049	. . . . . . . . . . . . . . . . 17 ⊢ (5 ∈ ℕ → 5 ∈ ℚ)
263	25, 262	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ ℚ
264		5pos 9413	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 5
265	233, 119, 264	ltleii 8435	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 5
266		5lt6 9495	. . . . . . . . . . . . . . . 16 ⊢ 5 < 6
267		modqid 10807	. . . . . . . . . . . . . . . 16 ⊢ (((5 ∈ ℚ ∧ 6 ∈ ℚ) ∧ (0 ≤ 5 ∧ 5 < 6)) → (5 mod 6) = 5)
268	263, 206, 265, 266, 267	mp4an 431	. . . . . . . . . . . . . . 15 ⊢ (5 mod 6) = 5
269	268	eqeq2i 2249	. . . . . . . . . . . . . 14 ⊢ ((𝑘 mod 6) = (5 mod 6) ↔ (𝑘 mod 6) = 5)
270		moddvds 12591	. . . . . . . . . . . . . . 15 ⊢ ((6 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 5 ∈ ℤ) → ((𝑘 mod 6) = (5 mod 6) ↔ 6 ∥ (𝑘 − 5)))
271	18, 26, 270	mp3an13 1369	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = (5 mod 6) ↔ 6 ∥ (𝑘 − 5)))
272	269, 271	bitr3id 194	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = 5 ↔ 6 ∥ (𝑘 − 5)))
273	158, 272	syl 14	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → ((𝑘 mod 6) = 5 ↔ 6 ∥ (𝑘 − 5)))
274	273	rabbiia 2807	. . . . . . . . . . 11 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)}
275	274	fveq2i 5701	. . . . . . . . . 10 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)})
276	218, 219, 222, 105	hashdvds 13028	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))))
277	275, 276	eqtrid 2283	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))))
278	220	oveq1i 6098	. . . . . . . . . . . . . . . 16 ⊢ ((4 − 1) − 5) = (3 − 5)
279		5cn 9393	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℂ
280		3cn 9388	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℂ
281	279, 280	negsubdi2i 8619	. . . . . . . . . . . . . . . 16 ⊢ -(5 − 3) = (3 − 5)
282		3p2e5 9455	. . . . . . . . . . . . . . . . . . 19 ⊢ (3 + 2) = 5
283	282	oveq1i 6098	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 + 2) − 3) = (5 − 3)
284		pncan2 8540	. . . . . . . . . . . . . . . . . . 19 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
285	280, 226, 284	mp2an 430	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 + 2) − 3) = 2
286	283, 285	eqtr3i 2261	. . . . . . . . . . . . . . . . 17 ⊢ (5 − 3) = 2
287	286	negeqi 8527	. . . . . . . . . . . . . . . 16 ⊢ -(5 − 3) = -2
288	278, 281, 287	3eqtr2i 2265	. . . . . . . . . . . . . . 15 ⊢ ((4 − 1) − 5) = -2
289	288	oveq1i 6098	. . . . . . . . . . . . . 14 ⊢ (((4 − 1) − 5) / 6) = ( -2 / 6)
290		divnegap 9044	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 6 ∈ ℂ ∧ 6 # 0) → -(2 / 6) = ( -2 / 6))
291	226, 240, 234, 290	mp3an 1378	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) = ( -2 / 6)
292	289, 291	eqtr4i 2262	. . . . . . . . . . . . 13 ⊢ (((4 − 1) − 5) / 6) = -(2 / 6)
293	292	fveq2i 5701	. . . . . . . . . . . 12 ⊢ (⌊‘(((4 − 1) − 5) / 6)) = (⌊‘ -(2 / 6))
294	235, 189, 246	ltleii 8435	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ≤ 1
295	235, 189	lenegi 8829	. . . . . . . . . . . . . 14 ⊢ ((2 / 6) ≤ 1 ↔ -1 ≤ -(2 / 6))
296	294, 295	mpbi 145	. . . . . . . . . . . . 13 ⊢ -1 ≤ -(2 / 6)
297	233, 235	ltnegi 8828	. . . . . . . . . . . . . . 15 ⊢ (0 < (2 / 6) ↔ -(2 / 6) < -0)
298	237, 297	mpbi 145	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) < -0
299		neg0 8579	. . . . . . . . . . . . . . . 16 ⊢ -0 = 0
300		1pneg1e0 9424	. . . . . . . . . . . . . . . 16 ⊢ (1 + -1) = 0
301	299, 300	eqtr4i 2262	. . . . . . . . . . . . . . 15 ⊢ -0 = (1 + -1)
302		neg1cn 9418	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℂ
303	302, 227	addcomi 8477	. . . . . . . . . . . . . . 15 ⊢ ( -1 + 1) = (1 + -1)
304	301, 303	eqtr4i 2262	. . . . . . . . . . . . . 14 ⊢ -0 = ( -1 + 1)
305	298, 304	breqtri 4156	. . . . . . . . . . . . 13 ⊢ -(2 / 6) < ( -1 + 1)
306		qnegcl 10052	. . . . . . . . . . . . . . 15 ⊢ ((2 / 6) ∈ ℚ → -(2 / 6) ∈ ℚ)
307	251, 306	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) ∈ ℚ
308		neg1z 9687	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℤ
309		flqbi 10746	. . . . . . . . . . . . . 14 ⊢ (( -(2 / 6) ∈ ℚ ∧ -1 ∈ ℤ) → ((⌊‘ -(2 / 6)) = -1 ↔ ( -1 ≤ -(2 / 6) ∧ -(2 / 6) < ( -1 + 1))))
310	307, 308, 309	mp2an 430	. . . . . . . . . . . . 13 ⊢ ((⌊‘ -(2 / 6)) = -1 ↔ ( -1 ≤ -(2 / 6) ∧ -(2 / 6) < ( -1 + 1)))
311	296, 305, 310	mpbir2an 955	. . . . . . . . . . . 12 ⊢ (⌊‘ -(2 / 6)) = -1
312	293, 311	eqtri 2259	. . . . . . . . . . 11 ⊢ (⌊‘(((4 − 1) − 5) / 6)) = -1
313	312	oveq2i 6099	. . . . . . . . . 10 ⊢ ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1)
314	109	zcnd 9780	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℂ)
315		subneg 8582	. . . . . . . . . . 11 ⊢ (((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℂ ∧ 1 ∈ ℂ) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
316	314, 227, 315	sylancl 417	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
317	313, 316	eqtrid 2283	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
318	277, 317	eqtrd 2271	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
319	261, 318	oveq12d 6106	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)))
320	202, 319	eqtrd 2271	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)))
321	118	recnd 8360	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℂ)
322	321	2timesd 9559	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (2 · 𝑁) = (𝑁 + 𝑁))
323		df-6 9376	. . . . . . . . . . . . . 14 ⊢ 6 = (5 + 1)
324	279, 227	addcomi 8477	. . . . . . . . . . . . . 14 ⊢ (5 + 1) = (1 + 5)
325	323, 324	eqtri 2259	. . . . . . . . . . . . 13 ⊢ 6 = (1 + 5)
326	325	a1i 9	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 6 = (1 + 5))
327	322, 326	oveq12d 6106	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) − 6) = ((𝑁 + 𝑁) − (1 + 5)))
328		addsub4 8576	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ (1 ∈ ℂ ∧ 5 ∈ ℂ)) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
329	227, 279, 328	mpanr12 443	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
330	321, 321, 329	syl2anc 415	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
331	327, 330	eqtrd 2271	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) − 6) = ((𝑁 − 1) + (𝑁 − 5)))
332	331	oveq1d 6103	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = (((𝑁 − 1) + (𝑁 − 5)) / 6))
333		mulcl 8312	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) ∈ ℂ)
334	226, 321, 333	sylancr 418	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (2 · 𝑁) ∈ ℂ)
335	240, 234	pm3.2i 272	. . . . . . . . . . . 12 ⊢ (6 ∈ ℂ ∧ 6 # 0)
336		divsubdirap 9046	. . . . . . . . . . . 12 ⊢ (((2 · 𝑁) ∈ ℂ ∧ 6 ∈ ℂ ∧ (6 ∈ ℂ ∧ 6 # 0)) → (((2 · 𝑁) − 6) / 6) = (((2 · 𝑁) / 6) − (6 / 6)))
337	240, 335, 336	mp3an23 1370	. . . . . . . . . . 11 ⊢ ((2 · 𝑁) ∈ ℂ → (((2 · 𝑁) − 6) / 6) = (((2 · 𝑁) / 6) − (6 / 6)))
338	334, 337	syl 14	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = (((2 · 𝑁) / 6) − (6 / 6)))
339		2t3e6 9471	. . . . . . . . . . . . 13 ⊢ (2 · 3) = 6
340	339	oveq2i 6099	. . . . . . . . . . . 12 ⊢ ((2 · 𝑁) / (2 · 3)) = ((2 · 𝑁) / 6)
341		3ap0 9409	. . . . . . . . . . . . . . 15 ⊢ 3 # 0
342	280, 341	pm3.2i 272	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℂ ∧ 3 # 0)
343		2ap0 9406	. . . . . . . . . . . . . . 15 ⊢ 2 # 0
344	226, 343	pm3.2i 272	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℂ ∧ 2 # 0)
345		divcanap5 9052	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 # 0) ∧ (2 ∈ ℂ ∧ 2 # 0)) → ((2 · 𝑁) / (2 · 3)) = (𝑁 / 3))
346	342, 344, 345	mp3an23 1370	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℂ → ((2 · 𝑁) / (2 · 3)) = (𝑁 / 3))
347	321, 346	syl 14	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) / (2 · 3)) = (𝑁 / 3))
348	340, 347	eqtr3id 2285	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) / 6) = (𝑁 / 3))
349	240, 234	dividapi 9083	. . . . . . . . . . . 12 ⊢ (6 / 6) = 1
350	349	a1i 9	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (6 / 6) = 1)
351	348, 350	oveq12d 6106	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) / 6) − (6 / 6)) = ((𝑁 / 3) − 1))
352	338, 351	eqtrd 2271	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = ((𝑁 / 3) − 1))
353	115	recnd 8360	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℂ)
354	121	recnd 8360	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 − 5) ∈ ℂ)
355		divdirap 9035	. . . . . . . . . . 11 ⊢ (((𝑁 − 1) ∈ ℂ ∧ (𝑁 − 5) ∈ ℂ ∧ (6 ∈ ℂ ∧ 6 # 0)) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
356	335, 355	mp3an3 1367	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℂ ∧ (𝑁 − 5) ∈ ℂ) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
357	353, 354, 356	syl2anc 415	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
358	332, 352, 357	3eqtr3d 2279	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((𝑁 / 3) − 1) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
359	358	oveq1d 6103	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((𝑁 / 3) − 1) + 1) = ((((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)) + 1))
360	52	recnd 8360	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 / 3) ∈ ℂ)
361		npcan 8542	. . . . . . . 8 ⊢ (((𝑁 / 3) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3))
362	360, 227, 361	sylancl 417	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3))
363	117	recnd 8360	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((𝑁 − 1) / 6) ∈ ℂ)
364	123	recnd 8360	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((𝑁 − 5) / 6) ∈ ℂ)
365	227	a1i 9	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 1 ∈ ℂ)
366	363, 364, 365	addassd 8354	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)) + 1) = (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
367	359, 362, 366	3eqtr3d 2279	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 / 3) = (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
368	157, 320, 367	3brtr4d 4163	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ≤ (𝑁 / 3))
369	6, 47, 52, 98, 368	letrd 8457	. . . 4 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ≤ (𝑁 / 3))
370	4	a1i 9	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 2 ∈ ℝ)
371	3, 370, 52	lesubaddd 8877	. . . 4 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((π‘𝑁) − 2) ≤ (𝑁 / 3) ↔ (π‘𝑁) ≤ ((𝑁 / 3) + 2)))
372	369, 371	mpbid 147	. . 3 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
373	372	adantlr 481	. 2 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 3 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
374	2	ad2antrr 492	. . 3 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ∈ ℝ)
375	4	a1i 9	. . 3 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → 2 ∈ ℝ)
376	51	ad2antrr 492	. . . 4 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (𝑁 / 3) ∈ ℝ)
377		readdcl 8311	. . . 4 ⊢ (((𝑁 / 3) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑁 / 3) + 2) ∈ ℝ)
378	376, 4, 377	sylancl 417	. . 3 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → ((𝑁 / 3) + 2) ∈ ℝ)
379		zq 10042	. . . . . . 7 ⊢ (3 ∈ ℤ → 3 ∈ ℚ)
380	58, 379	ax-mp 5	. . . . . 6 ⊢ 3 ∈ ℚ
381		ppiqwordi 16268	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 3 ∈ ℚ ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
382	380, 381	mp3an2 1366	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
383	382	adantlr 481	. . . 4 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
384	383, 55	breqtrdi 4172	. . 3 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ 2)
385	48	adantr 276	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → 𝑁 ∈ ℝ)
386		simpr 110	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → 0 ≤ 𝑁)
387		3re 9387	. . . . . . 7 ⊢ 3 ∈ ℝ
388	387	a1i 9	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → 3 ∈ ℝ)
389		3pos 9407	. . . . . . 7 ⊢ 0 < 3
390	389	a1i 9	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → 0 < 3)
391		divge0 9211	. . . . . 6 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ (3 ∈ ℝ ∧ 0 < 3)) → 0 ≤ (𝑁 / 3))
392	385, 386, 388, 390, 391	syl22anc 1279	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → 0 ≤ (𝑁 / 3))
393	392	adantr 276	. . . 4 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → 0 ≤ (𝑁 / 3))
394		addge02 8808	. . . . 5 ⊢ ((2 ∈ ℝ ∧ (𝑁 / 3) ∈ ℝ) → (0 ≤ (𝑁 / 3) ↔ 2 ≤ ((𝑁 / 3) + 2)))
395	4, 376, 394	sylancr 418	. . . 4 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (0 ≤ (𝑁 / 3) ↔ 2 ≤ ((𝑁 / 3) + 2)))
396	393, 395	mpbid 147	. . 3 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → 2 ≤ ((𝑁 / 3) + 2))
397	374, 375, 378, 384, 396	letrd 8457	. 2 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
398		simpl 109	. . 3 ⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → 𝑁 ∈ ℚ)
399		qletric 10693	. . 3 ⊢ ((3 ∈ ℚ ∧ 𝑁 ∈ ℚ) → (3 ≤ 𝑁 ∨ 𝑁 ≤ 3))
400	380, 398, 399	sylancr 418	. 2 ⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → (3 ≤ 𝑁 ∨ 𝑁 ≤ 3))
401	373, 397, 400	mpjaodan 810	1 ⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))

Colors of variables: wff set class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 DECID wdc 846 = wceq 1402 ∈ wcel 2209 ≠ wne 2420 ∀wral 2528 {crab 2532 ∪ cun 3218 ∩ cin 3219 ⊆ wss 3220 ∅c0 3520 {cpr 3710 class class class wbr 4131 ‘cfv 5380 (class class class)co 6088 ≼ cdom 7025 Fincfn 7026 ℂcc 8183 ℝcr 8184 0cc0 8185 1c1 8186 + caddc 8188 · cmul 8190 < clt 8366 ≤ cle 8367 − cmin 8504 -cneg 8505 # cap 8917 / cdiv 9010 ℕcn 9313 2c2 9364 3c3 9365 4c4 9366 5c5 9367 6c6 9368 ℕ₀cn0 9574 ℤcz 9655 ℤ_≥cuz 9937 ℚcq 10035 ...cfz 10428 ⌊cfl 10720 mod cmo 10780 ♯chash 11236 ∥ cdvds 12579 ℙcprime 12910 πcppi 16234

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4248 ax-sep 4251 ax-nul 4261 ax-pow 4313 ax-pr 4348 ax-un 4580 ax-setind 4686 ax-iinf 4737 ax-cnex 8276 ax-resscn 8277 ax-1cn 8278 ax-1re 8279 ax-icn 8280 ax-addcl 8281 ax-addrcl 8282 ax-mulcl 8283 ax-mulrcl 8284 ax-addcom 8285 ax-mulcom 8286 ax-addass 8287 ax-mulass 8288 ax-distr 8289 ax-i2m1 8290 ax-0lt1 8291 ax-1rid 8292 ax-0id 8293 ax-rnegex 8294 ax-precex 8295 ax-cnre 8296 ax-pre-ltirr 8297 ax-pre-ltwlin 8298 ax-pre-lttrn 8299 ax-pre-apti 8300 ax-pre-ltadd 8301 ax-pre-mulgt0 8302 ax-pre-mulext 8303 ax-arch 8304 ax-caucvg 8305

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4132 df-opab 4194 df-mpt 4195 df-tr 4232 df-id 4440 df-po 4443 df-iso 4444 df-iord 4513 df-on 4515 df-ilim 4516 df-suc 4518 df-iom 4740 df-xp 4782 df-rel 4783 df-cnv 4784 df-co 4785 df-dm 4786 df-rn 4787 df-res 4788 df-ima 4789 df-iota 5340 df-fun 5382 df-fn 5383 df-f 5384 df-f1 5385 df-fo 5386 df-f1o 5387 df-fv 5388 df-isom 5389 df-riota 6041 df-ov 6091 df-oprab 6092 df-mpo 6093 df-1st 6378 df-2nd 6379 df-recs 6580 df-irdg 6645 df-frec 6666 df-1o 6691 df-2o 6692 df-oadd 6695 df-er 6811 df-en 7027 df-dom 7028 df-fin 7029 df-sup 7330 df-inf 7331 df-pnf 8368 df-mnf 8369 df-xr 8370 df-ltxr 8371 df-le 8372 df-sub 8506 df-neg 8507 df-reap 8911 df-ap 8918 df-div 9011 df-inn 9314 df-2 9372 df-3 9373 df-4 9374 df-5 9375 df-6 9376 df-n0 9575 df-z 9656 df-uz 9938 df-q 10036 df-rp 10072 df-icc 10314 df-fz 10429 df-fl 10722 df-mod 10781 df-seqfrec 10906 df-exp 10997 df-ihash 11237 df-cj 11629 df-re 11630 df-im 11631 df-rsqrt 11786 df-abs 11787 df-dvds 12580 df-prm 12911 df-ppi 16237

This theorem is used by: bposlem5 16315

W3C validator