ppiqub - Intuitionistic Logic Explorer

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

Theorem ppiqub 16254

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 16212	. . . . . . . 8 ⊢ (𝑁 ∈ ℚ → (π‘𝑁) ∈ ℕ₀)
2	1	nn0red 9626	. . . . . . 7 ⊢ (𝑁 ∈ ℚ → (π‘𝑁) ∈ ℝ)
3	2	adantr 276	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (π‘𝑁) ∈ ℝ)
4		2re 9377	. . . . . 6 ⊢ 2 ∈ ℝ
5		resubcl 8592	. . . . . 6 ⊢ (((π‘𝑁) ∈ ℝ ∧ 2 ∈ ℝ) → ((π‘𝑁) − 2) ∈ ℝ)
6	3, 4, 5	sylancl 417	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ∈ ℝ)
7		4z 9679	. . . . . . . . . . 11 ⊢ 4 ∈ ℤ
8	7	a1i 9	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℚ → 4 ∈ ℤ)
9		flqcl 10719	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℚ → (⌊‘𝑁) ∈ ℤ)
10	8, 9	fzfigd 10883	. . . . . . . . 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 10439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (4...(⌊‘𝑁)) → 𝑥 ∈ ℤ)
17	16	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → 𝑥 ∈ ℤ)
18		6nn 9475	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℕ
19		zmodcl 10796	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ 6 ∈ ℕ) → (𝑥 mod 6) ∈ ℕ₀)
20	17, 18, 19	sylancl 417	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → (𝑥 mod 6) ∈ ℕ₀)
21	20	nn0zd 9771	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → (𝑥 mod 6) ∈ ℤ)
22		1z 9675	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
23		zdceq 9725	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 mod 6) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑥 mod 6) = 1)
24	21, 22, 23	sylancl 417	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → DECID (𝑥 mod 6) = 1)
25		5nn 9474	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ ℕ
26	25	nnzi 9670	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℤ
27		zdceq 9725	. . . . . . . . . . . . . . 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 6092	. . . . . . . . . . . . . 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 7245	. . . . . . . . 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 11236	. . . . . . . 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 9626	. . . . . 6 ⊢ (𝑁 ∈ ℚ → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℝ)
47	46	adantr 276	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℝ)
48		qre 10035	. . . . . . 7 ⊢ (𝑁 ∈ ℚ → 𝑁 ∈ ℝ)
49		3nn 9472	. . . . . . 7 ⊢ 3 ∈ ℕ
50		nndivre 9343	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℕ) → (𝑁 / 3) ∈ ℝ)
51	48, 49, 50	sylancl 417	. . . . . 6 ⊢ (𝑁 ∈ ℚ → (𝑁 / 3) ∈ ℝ)
52	51	adantr 276	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 / 3) ∈ ℝ)
53		ppiqfl 16227	. . . . . . . . 9 ⊢ (𝑁 ∈ ℚ → (π‘(⌊‘𝑁)) = (π‘𝑁))
54	53	adantr 276	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (π‘(⌊‘𝑁)) = (π‘𝑁))
55		ppi3 16236	. . . . . . . . 9 ⊢ (π‘3) = 2
56	55	a1i 9	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (π‘3) = 2)
57	54, 56	oveq12d 6103	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = ((π‘𝑁) − 2))
58		3z 9678	. . . . . . . . . . 11 ⊢ 3 ∈ ℤ
59	58	a1i 9	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 3 ∈ ℤ)
60	9	adantr 276	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ ℤ)
61		flqge 10730	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℚ ∧ 3 ∈ ℤ) → (3 ≤ 𝑁 ↔ 3 ≤ (⌊‘𝑁)))
62	58, 61	mpan2 429	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℚ → (3 ≤ 𝑁 ↔ 3 ≤ (⌊‘𝑁)))
63	62	biimpa 296	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 3 ≤ (⌊‘𝑁))
64		eluz2 9937	. . . . . . . . . 10 ⊢ ((⌊‘𝑁) ∈ (ℤ_≥‘3) ↔ (3 ∈ ℤ ∧ (⌊‘𝑁) ∈ ℤ ∧ 3 ≤ (⌊‘𝑁)))
65	59, 60, 63, 64	syl3anbrc 1212	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ (ℤ_≥‘3))
66		ppidif 16230	. . . . . . . . 9 ⊢ ((⌊‘𝑁) ∈ (ℤ_≥‘3) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ)))
67	65, 66	syl 14	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ)))
68		df-4 9368	. . . . . . . . . . 11 ⊢ 4 = (3 + 1)
69	68	oveq1i 6095	. . . . . . . . . 10 ⊢ (4...(⌊‘𝑁)) = ((3 + 1)...(⌊‘𝑁))
70	69	ineq1i 3428	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) = (((3 + 1)...(⌊‘𝑁)) ∩ ℙ)
71	70	fveq2i 5698	. . . . . . . 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 10442	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 4 ≤ 𝑘)
76		ppiublem2 16253	. . . . . . . . . . . . 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 7065	. . . . . . . . 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 12928	. . . . . . . . . . . . . 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 7245	. . . . . . . . . 10 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ (4...(⌊‘𝑁)) ∧ ∀𝑥 ∈ (4...(⌊‘𝑁))DECID 𝑥 ∈ ((4...(⌊‘𝑁)) ∩ ℙ)) → ((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin)
93	10, 84, 91, 92	syl3anc 1278	. . . . . . . . 9 ⊢ (𝑁 ∈ ℚ → ((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin)
94		fihashdom 11259	. . . . . . . . 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 4152	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ≤ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}))
99		peano2zm 9687	. . . . . . . . . . 11 ⊢ ((⌊‘𝑁) ∈ ℤ → ((⌊‘𝑁) − 1) ∈ ℤ)
100	60, 99	syl 14	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ∈ ℤ)
101		znq 10034	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 1) ∈ ℤ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 1) / 6) ∈ ℚ)
102	100, 18, 101	sylancl 417	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) / 6) ∈ ℚ)
103	102	flqcld 10725	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℤ)
104	103	zred 9773	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℝ)
105	26	a1i 9	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 5 ∈ ℤ)
106	60, 105	zsubcld 9778	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ∈ ℤ)
107		znq 10034	. . . . . . . . . . 11 ⊢ ((((⌊‘𝑁) − 5) ∈ ℤ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 5) / 6) ∈ ℚ)
108	106, 18, 107	sylancl 417	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) / 6) ∈ ℚ)
109	108	flqcld 10725	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℤ)
110	109	zred 9773	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ)
111		peano2re 8464	. . . . . . . 8 ⊢ ((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈ ℝ)
112	110, 111	syl 14	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈ ℝ)
113		peano2rem 8595	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
114	48, 113	syl 14	. . . . . . . . 9 ⊢ (𝑁 ∈ ℚ → (𝑁 − 1) ∈ ℝ)
115	114	adantr 276	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℝ)
116		nndivre 9343	. . . . . . . 8 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝑁 − 1) / 6) ∈ ℝ)
117	115, 18, 116	sylancl 417	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((𝑁 − 1) / 6) ∈ ℝ)
118	48	adantr 276	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℝ)
119		5re 9386	. . . . . . . . . 10 ⊢ 5 ∈ ℝ
120		resubcl 8592	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 5 ∈ ℝ) → (𝑁 − 5) ∈ ℝ)
121	118, 119, 120	sylancl 417	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 − 5) ∈ ℝ)
122		nndivre 9343	. . . . . . . . 9 ⊢ (((𝑁 − 5) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝑁 − 5) / 6) ∈ ℝ)
123	121, 18, 122	sylancl 417	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((𝑁 − 5) / 6) ∈ ℝ)
124		peano2re 8464	. . . . . . . 8 ⊢ (((𝑁 − 5) / 6) ∈ ℝ → (((𝑁 − 5) / 6) + 1) ∈ ℝ)
125	123, 124	syl 14	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((𝑁 − 5) / 6) + 1) ∈ ℝ)
126		qre 10035	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 1) / 6) ∈ ℚ → (((⌊‘𝑁) − 1) / 6) ∈ ℝ)
127	102, 126	syl 14	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) / 6) ∈ ℝ)
128		flqle 10726	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 1) / 6) ∈ ℚ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ (((⌊‘𝑁) − 1) / 6))
129	102, 128	syl 14	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ (((⌊‘𝑁) − 1) / 6))
130	60	zred 9773	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ ℝ)
131		1red 8342	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 1 ∈ ℝ)
132		flqle 10726	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℚ → (⌊‘𝑁) ≤ 𝑁)
133	132	adantr 276	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ≤ 𝑁)
134	130, 118, 131, 133	lesub1dd 8891	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ≤ (𝑁 − 1))
135	100	zred 9773	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ∈ ℝ)
136		6re 9388	. . . . . . . . . . 11 ⊢ 6 ∈ ℝ
137	136	a1i 9	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 6 ∈ ℝ)
138		6pos 9408	. . . . . . . . . . 11 ⊢ 0 < 6
139	138	a1i 9	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 0 < 6)
140		lediv1 9202	. . . . . . . . . 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 8452	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ ((𝑁 − 1) / 6))
144		resubcl 8592	. . . . . . . . . . 11 ⊢ (((⌊‘𝑁) ∈ ℝ ∧ 5 ∈ ℝ) → ((⌊‘𝑁) − 5) ∈ ℝ)
145	130, 119, 144	sylancl 417	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ∈ ℝ)
146		nndivre 9343	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 5) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 5) / 6) ∈ ℝ)
147	145, 18, 146	sylancl 417	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) / 6) ∈ ℝ)
148		flqle 10726	. . . . . . . . . 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 8891	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ≤ (𝑁 − 5))
152		lediv1 9202	. . . . . . . . . . 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 8452	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ≤ ((𝑁 − 5) / 6))
156	110, 123, 131, 155	leadd1dd 8889	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ≤ (((𝑁 − 5) / 6) + 1))
157	104, 112, 117, 125, 143, 156	le2addd 8894	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) ≤ (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
158		elfzelz 10439	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 𝑘 ∈ ℤ)
159	18	a1i 9	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 6 ∈ ℕ)
160	158, 159	zmodcld 10797	. . . . . . . . . . . . 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 5698	. . . . . . . . 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 7245	. . . . . . . . . . 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 7245	. . . . . . . . . . 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 8326	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℝ
190		1lt5 9488	. . . . . . . . . . . . . . . 16 ⊢ 1 < 5
191	189, 190	ltneii 8424	. . . . . . . . . . . . . . 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 11261	. . . . . . . . . 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 10036	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
204	22, 203	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℚ
205		nnq 10043	. . . . . . . . . . . . . . . . 17 ⊢ (6 ∈ ℕ → 6 ∈ ℚ)
206	18, 205	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ ℚ
207		0le1 8811	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 1
208		1lt6 9493	. . . . . . . . . . . . . . . 16 ⊢ 1 < 6
209		modqid 10801	. . . . . . . . . . . . . . . 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 12585	. . . . . . . . . . . . . . 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 5698	. . . . . . . . . 10 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)})
218	18	a1i 9	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 6 ∈ ℕ)
219	7	a1i 9	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 4 ∈ ℤ)
220		4m1e3 9428	. . . . . . . . . . . . 13 ⊢ (4 − 1) = 3
221	220	fveq2i 5698	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘(4 − 1)) = (ℤ_≥‘3)
222	65, 221	eleqtrrdi 2332	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ (ℤ_≥‘(4 − 1)))
223		1zzd 9676	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 1 ∈ ℤ)
224	218, 219, 222, 223	hashdvds 13022	. . . . . . . . . 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 9378	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
227		ax-1cn 8273	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
228		df-3 9367	. . . . . . . . . . . . . . . 16 ⊢ 3 = (2 + 1)
229	220, 228	eqtri 2259	. . . . . . . . . . . . . . 15 ⊢ (4 − 1) = (2 + 1)
230	226, 227, 229	mvrraddi 8545	. . . . . . . . . . . . . 14 ⊢ ((4 − 1) − 1) = 2
231	230	oveq1i 6095	. . . . . . . . . . . . 13 ⊢ (((4 − 1) − 1) / 6) = (2 / 6)
232	231	fveq2i 5698	. . . . . . . . . . . 12 ⊢ (⌊‘(((4 − 1) − 1) / 6)) = (⌊‘(2 / 6))
233		0re 8327	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
234	136, 138	gt0ap0ii 8959	. . . . . . . . . . . . . . 15 ⊢ 6 # 0
235	4, 136, 234	redivclapi 9112	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ∈ ℝ
236		2pos 9398	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
237	4, 136, 236, 138	divgt0ii 9252	. . . . . . . . . . . . . 14 ⊢ 0 < (2 / 6)
238	233, 235, 237	ltleii 8430	. . . . . . . . . . . . 13 ⊢ 0 ≤ (2 / 6)
239		2lt6 9492	. . . . . . . . . . . . . . . 16 ⊢ 2 < 6
240		6cn 9389	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℂ
241	240	mulridi 8329	. . . . . . . . . . . . . . . 16 ⊢ (6 · 1) = 6
242	239, 241	breqtrri 4157	. . . . . . . . . . . . . . 15 ⊢ 2 < (6 · 1)
243	136, 138	pm3.2i 272	. . . . . . . . . . . . . . . 16 ⊢ (6 ∈ ℝ ∧ 0 < 6)
244		ltdivmul 9209	. . . . . . . . . . . . . . . 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 9828	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
248	246, 247	breqtri 4155	. . . . . . . . . . . . 13 ⊢ (2 / 6) < (0 + 1)
249		2z 9677	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
250		znq 10034	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℤ ∧ 6 ∈ ℕ) → (2 / 6) ∈ ℚ)
251	249, 18, 250	mp2an 430	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ∈ ℚ
252		0z 9660	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℤ
253		flqbi 10740	. . . . . . . . . . . . . 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 6096	. . . . . . . . . 10 ⊢ ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − 0)
258	103	zcnd 9774	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℂ)
259	258	subid1d 8628	. . . . . . . . . 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 10043	. . . . . . . . . . . . . . . . 17 ⊢ (5 ∈ ℕ → 5 ∈ ℚ)
263	25, 262	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ ℚ
264		5pos 9407	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 5
265	233, 119, 264	ltleii 8430	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 5
266		5lt6 9489	. . . . . . . . . . . . . . . 16 ⊢ 5 < 6
267		modqid 10801	. . . . . . . . . . . . . . . 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 12585	. . . . . . . . . . . . . . 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 5698	. . . . . . . . . 10 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)})
276	218, 219, 222, 105	hashdvds 13022	. . . . . . . . . 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 6095	. . . . . . . . . . . . . . . 16 ⊢ ((4 − 1) − 5) = (3 − 5)
279		5cn 9387	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℂ
280		3cn 9382	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℂ
281	279, 280	negsubdi2i 8614	. . . . . . . . . . . . . . . 16 ⊢ -(5 − 3) = (3 − 5)
282		3p2e5 9449	. . . . . . . . . . . . . . . . . . 19 ⊢ (3 + 2) = 5
283	282	oveq1i 6095	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 + 2) − 3) = (5 − 3)
284		pncan2 8535	. . . . . . . . . . . . . . . . . . 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 8522	. . . . . . . . . . . . . . . 16 ⊢ -(5 − 3) = -2
288	278, 281, 287	3eqtr2i 2265	. . . . . . . . . . . . . . 15 ⊢ ((4 − 1) − 5) = -2
289	288	oveq1i 6095	. . . . . . . . . . . . . 14 ⊢ (((4 − 1) − 5) / 6) = (-2 / 6)
290		divnegap 9039	. . . . . . . . . . . . . . 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 5698	. . . . . . . . . . . 12 ⊢ (⌊‘(((4 − 1) − 5) / 6)) = (⌊‘-(2 / 6))
294	235, 189, 246	ltleii 8430	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ≤ 1
295	235, 189	lenegi 8824	. . . . . . . . . . . . . 14 ⊢ ((2 / 6) ≤ 1 ↔ -1 ≤ -(2 / 6))
296	294, 295	mpbi 145	. . . . . . . . . . . . 13 ⊢ -1 ≤ -(2 / 6)
297	233, 235	ltnegi 8823	. . . . . . . . . . . . . . 15 ⊢ (0 < (2 / 6) ↔ -(2 / 6) < -0)
298	237, 297	mpbi 145	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) < -0
299		neg0 8574	. . . . . . . . . . . . . . . 16 ⊢ -0 = 0
300		1pneg1e0 9418	. . . . . . . . . . . . . . . 16 ⊢ (1 + -1) = 0
301	299, 300	eqtr4i 2262	. . . . . . . . . . . . . . 15 ⊢ -0 = (1 + -1)
302		neg1cn 9412	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℂ
303	302, 227	addcomi 8472	. . . . . . . . . . . . . . 15 ⊢ (-1 + 1) = (1 + -1)
304	301, 303	eqtr4i 2262	. . . . . . . . . . . . . 14 ⊢ -0 = (-1 + 1)
305	298, 304	breqtri 4155	. . . . . . . . . . . . 13 ⊢ -(2 / 6) < (-1 + 1)
306		qnegcl 10046	. . . . . . . . . . . . . . 15 ⊢ ((2 / 6) ∈ ℚ → -(2 / 6) ∈ ℚ)
307	251, 306	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) ∈ ℚ
308		neg1z 9681	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℤ
309		flqbi 10740	. . . . . . . . . . . . . 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 6096	. . . . . . . . . 10 ⊢ ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1)
314	109	zcnd 9774	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℂ)
315		subneg 8577	. . . . . . . . . . 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 6103	. . . . . . 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 8355	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℂ)
322	321	2timesd 9553	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (2 · 𝑁) = (𝑁 + 𝑁))
323		df-6 9370	. . . . . . . . . . . . . 14 ⊢ 6 = (5 + 1)
324	279, 227	addcomi 8472	. . . . . . . . . . . . . 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 6103	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) − 6) = ((𝑁 + 𝑁) − (1 + 5)))
328		addsub4 8571	. . . . . . . . . . . . 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 6100	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = (((𝑁 − 1) + (𝑁 − 5)) / 6))
333		mulcl 8307	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) ∈ ℂ)
334	226, 321, 333	sylancr 418	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (2 · 𝑁) ∈ ℂ)
335	240, 234	pm3.2i 272	. . . . . . . . . . . 12 ⊢ (6 ∈ ℂ ∧ 6 # 0)
336		divsubdirap 9041	. . . . . . . . . . . 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 9465	. . . . . . . . . . . . 13 ⊢ (2 · 3) = 6
340	339	oveq2i 6096	. . . . . . . . . . . 12 ⊢ ((2 · 𝑁) / (2 · 3)) = ((2 · 𝑁) / 6)
341		3ap0 9403	. . . . . . . . . . . . . . 15 ⊢ 3 # 0
342	280, 341	pm3.2i 272	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℂ ∧ 3 # 0)
343		2ap0 9400	. . . . . . . . . . . . . . 15 ⊢ 2 # 0
344	226, 343	pm3.2i 272	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℂ ∧ 2 # 0)
345		divcanap5 9047	. . . . . . . . . . . . . 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 9078	. . . . . . . . . . . 12 ⊢ (6 / 6) = 1
350	349	a1i 9	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (6 / 6) = 1)
351	348, 350	oveq12d 6103	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) / 6) − (6 / 6)) = ((𝑁 / 3) − 1))
352	338, 351	eqtrd 2271	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = ((𝑁 / 3) − 1))
353	115	recnd 8355	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℂ)
354	121	recnd 8355	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 − 5) ∈ ℂ)
355		divdirap 9030	. . . . . . . . . . 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 6100	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((𝑁 / 3) − 1) + 1) = ((((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)) + 1))
360	52	recnd 8355	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 / 3) ∈ ℂ)
361		npcan 8537	. . . . . . . 8 ⊢ (((𝑁 / 3) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3))
362	360, 227, 361	sylancl 417	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3))
363	117	recnd 8355	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((𝑁 − 1) / 6) ∈ ℂ)
364	123	recnd 8355	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((𝑁 − 5) / 6) ∈ ℂ)
365	227	a1i 9	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 1 ∈ ℂ)
366	363, 364, 365	addassd 8349	. . . . . . 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 4162	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ≤ (𝑁 / 3))
369	6, 47, 52, 98, 368	letrd 8452	. . . 4 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ≤ (𝑁 / 3))
370	4	a1i 9	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 2 ∈ ℝ)
371	3, 370, 52	lesubaddd 8872	. . . 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 8306	. . . 4 ⊢ (((𝑁 / 3) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑁 / 3) + 2) ∈ ℝ)
378	376, 4, 377	sylancl 417	. . 3 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → ((𝑁 / 3) + 2) ∈ ℝ)
379		zq 10036	. . . . . . 7 ⊢ (3 ∈ ℤ → 3 ∈ ℚ)
380	58, 379	ax-mp 5	. . . . . 6 ⊢ 3 ∈ ℚ
381		ppiqwordi 16229	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 3 ∈ ℚ ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
382	380, 381	mp3an2 1366	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
383	382	adantlr 481	. . . 4 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
384	383, 55	breqtrdi 4171	. . 3 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ 2)
385	48	adantr 276	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → 𝑁 ∈ ℝ)
386		simpr 110	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → 0 ≤ 𝑁)
387		3re 9381	. . . . . . 7 ⊢ 3 ∈ ℝ
388	387	a1i 9	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → 3 ∈ ℝ)
389		3pos 9401	. . . . . . 7 ⊢ 0 < 3
390	389	a1i 9	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → 0 < 3)
391		divge0 9206	. . . . . 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 8803	. . . . 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 8452	. 2 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
398		simpl 109	. . 3 ⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → 𝑁 ∈ ℚ)
399		qletric 10687	. . 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 4130 ‘cfv 5377 (class class class)co 6085 ≼ cdom 7021 Fincfn 7022 ℂcc 8178 ℝcr 8179 0cc0 8180 1c1 8181 + caddc 8183 · cmul 8185 < clt 8361 ≤ cle 8362 − cmin 8499 -cneg 8500 # cap 8912 / cdiv 9005 ℕcn 9307 2c2 9358 3c3 9359 4c4 9360 5c5 9361 6c6 9362 ℕ₀cn0 9568 ℤcz 9649 ℤ_≥cuz 9931 ℚcq 10029 ...cfz 10422 ⌊cfl 10714 mod cmo 10774 ♯chash 11230 ∥ cdvds 12573 ℙcprime 12904 πcppi 16195

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 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8271 ax-resscn 8272 ax-1cn 8273 ax-1re 8274 ax-icn 8275 ax-addcl 8276 ax-addrcl 8277 ax-mulcl 8278 ax-mulrcl 8279 ax-addcom 8280 ax-mulcom 8281 ax-addass 8282 ax-mulass 8283 ax-distr 8284 ax-i2m1 8285 ax-0lt1 8286 ax-1rid 8287 ax-0id 8288 ax-rnegex 8289 ax-precex 8290 ax-cnre 8291 ax-pre-ltirr 8292 ax-pre-ltwlin 8293 ax-pre-lttrn 8294 ax-pre-apti 8295 ax-pre-ltadd 8296 ax-pre-mulgt0 8297 ax-pre-mulext 8298 ax-arch 8299 ax-caucvg 8300

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 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-isom 5386 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-1st 6374 df-2nd 6375 df-recs 6576 df-irdg 6641 df-frec 6662 df-1o 6687 df-2o 6688 df-oadd 6691 df-er 6807 df-en 7023 df-dom 7024 df-fin 7025 df-sup 7325 df-inf 7326 df-pnf 8363 df-mnf 8364 df-xr 8365 df-ltxr 8366 df-le 8367 df-sub 8501 df-neg 8502 df-reap 8906 df-ap 8913 df-div 9006 df-inn 9308 df-2 9366 df-3 9367 df-4 9368 df-5 9369 df-6 9370 df-n0 9569 df-z 9650 df-uz 9932 df-q 10030 df-rp 10066 df-icc 10308 df-fz 10423 df-fl 10716 df-mod 10775 df-seqfrec 10900 df-exp 10991 df-ihash 11231 df-cj 11623 df-re 11624 df-im 11625 df-rsqrt 11780 df-abs 11781 df-dvds 12574 df-prm 12905 df-ppi 16198

This theorem is used by: bposlem5 16276

W3C validator