ppiqub - Intuitionistic Logic Explorer

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

Theorem ppiqub 16194

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 16163	. . . . . . . 8 ⊢ (𝑁 ∈ ℚ → (π‘𝑁) ∈ ℕ₀)
2	1	nn0red 9625	. . . . . . 7 ⊢ (𝑁 ∈ ℚ → (π‘𝑁) ∈ ℝ)
3	2	adantr 276	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (π‘𝑁) ∈ ℝ)
4		2re 9376	. . . . . 6 ⊢ 2 ∈ ℝ
5		resubcl 8591	. . . . . 6 ⊢ (((π‘𝑁) ∈ ℝ ∧ 2 ∈ ℝ) → ((π‘𝑁) − 2) ∈ ℝ)
6	3, 4, 5	sylancl 417	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ∈ ℝ)
7		4z 9678	. . . . . . . . . . 11 ⊢ 4 ∈ ℤ
8	7	a1i 9	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℚ → 4 ∈ ℤ)
9		flqcl 10718	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℚ → (⌊‘𝑁) ∈ ℤ)
10	8, 9	fzfigd 10881	. . . . . . . . 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 10438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (4...(⌊‘𝑁)) → 𝑥 ∈ ℤ)
17	16	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → 𝑥 ∈ ℤ)
18		6nn 9474	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℕ
19		zmodcl 10794	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ 6 ∈ ℕ) → (𝑥 mod 6) ∈ ℕ₀)
20	17, 18, 19	sylancl 417	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → (𝑥 mod 6) ∈ ℕ₀)
21	20	nn0zd 9770	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → (𝑥 mod 6) ∈ ℤ)
22		1z 9674	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
23		zdceq 9724	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 mod 6) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑥 mod 6) = 1)
24	21, 22, 23	sylancl 417	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℚ ∧ 𝑥 ∈ (4...(⌊‘𝑁))) → DECID (𝑥 mod 6) = 1)
25		5nn 9473	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ ℕ
26	25	nnzi 9669	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℤ
27		zdceq 9724	. . . . . . . . . . . . . . 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 11234	. . . . . . . 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 9625	. . . . . 6 ⊢ (𝑁 ∈ ℚ → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℝ)
47	46	adantr 276	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℝ)
48		qre 10034	. . . . . . 7 ⊢ (𝑁 ∈ ℚ → 𝑁 ∈ ℝ)
49		3nn 9471	. . . . . . 7 ⊢ 3 ∈ ℕ
50		nndivre 9342	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℕ) → (𝑁 / 3) ∈ ℝ)
51	48, 49, 50	sylancl 417	. . . . . 6 ⊢ (𝑁 ∈ ℚ → (𝑁 / 3) ∈ ℝ)
52	51	adantr 276	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 / 3) ∈ ℝ)
53		ppiqfl 16172	. . . . . . . . 9 ⊢ (𝑁 ∈ ℚ → (π‘(⌊‘𝑁)) = (π‘𝑁))
54	53	adantr 276	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (π‘(⌊‘𝑁)) = (π‘𝑁))
55		ppi3 16180	. . . . . . . . 9 ⊢ (π‘3) = 2
56	55	a1i 9	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (π‘3) = 2)
57	54, 56	oveq12d 6103	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = ((π‘𝑁) − 2))
58		3z 9677	. . . . . . . . . . 11 ⊢ 3 ∈ ℤ
59	58	a1i 9	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 3 ∈ ℤ)
60	9	adantr 276	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ ℤ)
61		flqge 10729	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℚ ∧ 3 ∈ ℤ) → (3 ≤ 𝑁 ↔ 3 ≤ (⌊‘𝑁)))
62	58, 61	mpan2 429	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℚ → (3 ≤ 𝑁 ↔ 3 ≤ (⌊‘𝑁)))
63	62	biimpa 296	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 3 ≤ (⌊‘𝑁))
64		eluz2 9936	. . . . . . . . . 10 ⊢ ((⌊‘𝑁) ∈ (ℤ_≥‘3) ↔ (3 ∈ ℤ ∧ (⌊‘𝑁) ∈ ℤ ∧ 3 ≤ (⌊‘𝑁)))
65	59, 60, 63, 64	syl3anbrc 1212	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ (ℤ_≥‘3))
66		ppidif 16175	. . . . . . . . 9 ⊢ ((⌊‘𝑁) ∈ (ℤ_≥‘3) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ)))
67	65, 66	syl 14	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ)))
68		df-4 9367	. . . . . . . . . . 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 10441	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 4 ≤ 𝑘)
76		ppiublem2 16193	. . . . . . . . . . . . 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 12925	. . . . . . . . . . . . . 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 11257	. . . . . . . . 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 9686	. . . . . . . . . . 11 ⊢ ((⌊‘𝑁) ∈ ℤ → ((⌊‘𝑁) − 1) ∈ ℤ)
100	60, 99	syl 14	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ∈ ℤ)
101		znq 10033	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 1) ∈ ℤ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 1) / 6) ∈ ℚ)
102	100, 18, 101	sylancl 417	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) / 6) ∈ ℚ)
103	102	flqcld 10724	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℤ)
104	103	zred 9772	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℝ)
105	26	a1i 9	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 5 ∈ ℤ)
106	60, 105	zsubcld 9777	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ∈ ℤ)
107		znq 10033	. . . . . . . . . . 11 ⊢ ((((⌊‘𝑁) − 5) ∈ ℤ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 5) / 6) ∈ ℚ)
108	106, 18, 107	sylancl 417	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) / 6) ∈ ℚ)
109	108	flqcld 10724	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℤ)
110	109	zred 9772	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ)
111		peano2re 8463	. . . . . . . 8 ⊢ ((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈ ℝ)
112	110, 111	syl 14	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈ ℝ)
113		peano2rem 8594	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
114	48, 113	syl 14	. . . . . . . . 9 ⊢ (𝑁 ∈ ℚ → (𝑁 − 1) ∈ ℝ)
115	114	adantr 276	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℝ)
116		nndivre 9342	. . . . . . . 8 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝑁 − 1) / 6) ∈ ℝ)
117	115, 18, 116	sylancl 417	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((𝑁 − 1) / 6) ∈ ℝ)
118	48	adantr 276	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℝ)
119		5re 9385	. . . . . . . . . 10 ⊢ 5 ∈ ℝ
120		resubcl 8591	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 5 ∈ ℝ) → (𝑁 − 5) ∈ ℝ)
121	118, 119, 120	sylancl 417	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 − 5) ∈ ℝ)
122		nndivre 9342	. . . . . . . . 9 ⊢ (((𝑁 − 5) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝑁 − 5) / 6) ∈ ℝ)
123	121, 18, 122	sylancl 417	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((𝑁 − 5) / 6) ∈ ℝ)
124		peano2re 8463	. . . . . . . 8 ⊢ (((𝑁 − 5) / 6) ∈ ℝ → (((𝑁 − 5) / 6) + 1) ∈ ℝ)
125	123, 124	syl 14	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((𝑁 − 5) / 6) + 1) ∈ ℝ)
126		qre 10034	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 1) / 6) ∈ ℚ → (((⌊‘𝑁) − 1) / 6) ∈ ℝ)
127	102, 126	syl 14	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) / 6) ∈ ℝ)
128		flqle 10725	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 1) / 6) ∈ ℚ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ (((⌊‘𝑁) − 1) / 6))
129	102, 128	syl 14	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ (((⌊‘𝑁) − 1) / 6))
130	60	zred 9772	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ ℝ)
131		1red 8341	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 1 ∈ ℝ)
132		flqle 10725	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℚ → (⌊‘𝑁) ≤ 𝑁)
133	132	adantr 276	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ≤ 𝑁)
134	130, 118, 131, 133	lesub1dd 8890	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ≤ (𝑁 − 1))
135	100	zred 9772	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ∈ ℝ)
136		6re 9387	. . . . . . . . . . 11 ⊢ 6 ∈ ℝ
137	136	a1i 9	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 6 ∈ ℝ)
138		6pos 9407	. . . . . . . . . . 11 ⊢ 0 < 6
139	138	a1i 9	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 0 < 6)
140		lediv1 9201	. . . . . . . . . 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 8451	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ ((𝑁 − 1) / 6))
144		resubcl 8591	. . . . . . . . . . 11 ⊢ (((⌊‘𝑁) ∈ ℝ ∧ 5 ∈ ℝ) → ((⌊‘𝑁) − 5) ∈ ℝ)
145	130, 119, 144	sylancl 417	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ∈ ℝ)
146		nndivre 9342	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 5) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 5) / 6) ∈ ℝ)
147	145, 18, 146	sylancl 417	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) / 6) ∈ ℝ)
148		flqle 10725	. . . . . . . . . 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 8890	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ≤ (𝑁 − 5))
152		lediv1 9201	. . . . . . . . . . 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 8451	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ≤ ((𝑁 − 5) / 6))
156	110, 123, 131, 155	leadd1dd 8888	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ≤ (((𝑁 − 5) / 6) + 1))
157	104, 112, 117, 125, 143, 156	le2addd 8893	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) ≤ (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
158		elfzelz 10438	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 𝑘 ∈ ℤ)
159	18	a1i 9	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 6 ∈ ℕ)
160	158, 159	zmodcld 10795	. . . . . . . . . . . . 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 8325	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℝ
190		1lt5 9487	. . . . . . . . . . . . . . . 16 ⊢ 1 < 5
191	189, 190	ltneii 8423	. . . . . . . . . . . . . . 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 11259	. . . . . . . . . 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 10035	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
204	22, 203	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℚ
205		nnq 10042	. . . . . . . . . . . . . . . . 17 ⊢ (6 ∈ ℕ → 6 ∈ ℚ)
206	18, 205	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ ℚ
207		0le1 8810	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 1
208		1lt6 9492	. . . . . . . . . . . . . . . 16 ⊢ 1 < 6
209		modqid 10799	. . . . . . . . . . . . . . . 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 12582	. . . . . . . . . . . . . . 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 9427	. . . . . . . . . . . . 13 ⊢ (4 − 1) = 3
221	220	fveq2i 5698	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘(4 − 1)) = (ℤ_≥‘3)
222	65, 221	eleqtrrdi 2332	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ (ℤ_≥‘(4 − 1)))
223		1zzd 9675	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 1 ∈ ℤ)
224	218, 219, 222, 223	hashdvds 13019	. . . . . . . . . 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 9377	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
227		ax-1cn 8272	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
228		df-3 9366	. . . . . . . . . . . . . . . 16 ⊢ 3 = (2 + 1)
229	220, 228	eqtri 2259	. . . . . . . . . . . . . . 15 ⊢ (4 − 1) = (2 + 1)
230	226, 227, 229	mvrraddi 8544	. . . . . . . . . . . . . 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 8326	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
234	136, 138	gt0ap0ii 8958	. . . . . . . . . . . . . . 15 ⊢ 6 # 0
235	4, 136, 234	redivclapi 9111	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ∈ ℝ
236		2pos 9397	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
237	4, 136, 236, 138	divgt0ii 9251	. . . . . . . . . . . . . 14 ⊢ 0 < (2 / 6)
238	233, 235, 237	ltleii 8429	. . . . . . . . . . . . 13 ⊢ 0 ≤ (2 / 6)
239		2lt6 9491	. . . . . . . . . . . . . . . 16 ⊢ 2 < 6
240		6cn 9388	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℂ
241	240	mulridi 8328	. . . . . . . . . . . . . . . 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 9208	. . . . . . . . . . . . . . . 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 9827	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
248	246, 247	breqtri 4155	. . . . . . . . . . . . 13 ⊢ (2 / 6) < (0 + 1)
249		2z 9676	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
250		znq 10033	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℤ ∧ 6 ∈ ℕ) → (2 / 6) ∈ ℚ)
251	249, 18, 250	mp2an 430	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ∈ ℚ
252		0z 9659	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℤ
253		flqbi 10738	. . . . . . . . . . . . . 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 9773	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℂ)
259	258	subid1d 8627	. . . . . . . . . 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 10042	. . . . . . . . . . . . . . . . 17 ⊢ (5 ∈ ℕ → 5 ∈ ℚ)
263	25, 262	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ ℚ
264		5pos 9406	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 5
265	233, 119, 264	ltleii 8429	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 5
266		5lt6 9488	. . . . . . . . . . . . . . . 16 ⊢ 5 < 6
267		modqid 10799	. . . . . . . . . . . . . . . 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 12582	. . . . . . . . . . . . . . 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 13019	. . . . . . . . . 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 9386	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℂ
280		3cn 9381	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℂ
281	279, 280	negsubdi2i 8613	. . . . . . . . . . . . . . . 16 ⊢ -(5 − 3) = (3 − 5)
282		3p2e5 9448	. . . . . . . . . . . . . . . . . . 19 ⊢ (3 + 2) = 5
283	282	oveq1i 6095	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 + 2) − 3) = (5 − 3)
284		pncan2 8534	. . . . . . . . . . . . . . . . . . 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 8521	. . . . . . . . . . . . . . . 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 9038	. . . . . . . . . . . . . . 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 8429	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ≤ 1
295	235, 189	lenegi 8823	. . . . . . . . . . . . . 14 ⊢ ((2 / 6) ≤ 1 ↔ -1 ≤ -(2 / 6))
296	294, 295	mpbi 145	. . . . . . . . . . . . 13 ⊢ -1 ≤ -(2 / 6)
297	233, 235	ltnegi 8822	. . . . . . . . . . . . . . 15 ⊢ (0 < (2 / 6) ↔ -(2 / 6) < -0)
298	237, 297	mpbi 145	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) < -0
299		neg0 8573	. . . . . . . . . . . . . . . 16 ⊢ -0 = 0
300		1pneg1e0 9417	. . . . . . . . . . . . . . . 16 ⊢ (1 + -1) = 0
301	299, 300	eqtr4i 2262	. . . . . . . . . . . . . . 15 ⊢ -0 = (1 + -1)
302		neg1cn 9411	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℂ
303	302, 227	addcomi 8471	. . . . . . . . . . . . . . 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 10045	. . . . . . . . . . . . . . 15 ⊢ ((2 / 6) ∈ ℚ → -(2 / 6) ∈ ℚ)
307	251, 306	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) ∈ ℚ
308		neg1z 9680	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℤ
309		flqbi 10738	. . . . . . . . . . . . . 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 9773	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℂ)
315		subneg 8576	. . . . . . . . . . 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 8354	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℂ)
322	321	2timesd 9552	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (2 · 𝑁) = (𝑁 + 𝑁))
323		df-6 9369	. . . . . . . . . . . . . 14 ⊢ 6 = (5 + 1)
324	279, 227	addcomi 8471	. . . . . . . . . . . . . 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 8570	. . . . . . . . . . . . 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 8306	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) ∈ ℂ)
334	226, 321, 333	sylancr 418	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (2 · 𝑁) ∈ ℂ)
335	240, 234	pm3.2i 272	. . . . . . . . . . . 12 ⊢ (6 ∈ ℂ ∧ 6 # 0)
336		divsubdirap 9040	. . . . . . . . . . . 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 9464	. . . . . . . . . . . . 13 ⊢ (2 · 3) = 6
340	339	oveq2i 6096	. . . . . . . . . . . 12 ⊢ ((2 · 𝑁) / (2 · 3)) = ((2 · 𝑁) / 6)
341		3ap0 9402	. . . . . . . . . . . . . . 15 ⊢ 3 # 0
342	280, 341	pm3.2i 272	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℂ ∧ 3 # 0)
343		2ap0 9399	. . . . . . . . . . . . . . 15 ⊢ 2 # 0
344	226, 343	pm3.2i 272	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℂ ∧ 2 # 0)
345		divcanap5 9046	. . . . . . . . . . . . . 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 9077	. . . . . . . . . . . 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 8354	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℂ)
354	121	recnd 8354	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 − 5) ∈ ℂ)
355		divdirap 9029	. . . . . . . . . . 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 8354	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (𝑁 / 3) ∈ ℂ)
361		npcan 8536	. . . . . . . 8 ⊢ (((𝑁 / 3) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3))
362	360, 227, 361	sylancl 417	. . . . . . 7 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3))
363	117	recnd 8354	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((𝑁 − 1) / 6) ∈ ℂ)
364	123	recnd 8354	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((𝑁 − 5) / 6) ∈ ℂ)
365	227	a1i 9	. . . . . . . 8 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 1 ∈ ℂ)
366	363, 364, 365	addassd 8348	. . . . . . 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 8451	. . . 4 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ≤ (𝑁 / 3))
370	4	a1i 9	. . . . 5 ⊢ ((𝑁 ∈ ℚ ∧ 3 ≤ 𝑁) → 2 ∈ ℝ)
371	3, 370, 52	lesubaddd 8871	. . . 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 8305	. . . 4 ⊢ (((𝑁 / 3) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑁 / 3) + 2) ∈ ℝ)
378	376, 4, 377	sylancl 417	. . 3 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → ((𝑁 / 3) + 2) ∈ ℝ)
379		zq 10035	. . . . . . 7 ⊢ (3 ∈ ℤ → 3 ∈ ℚ)
380	58, 379	ax-mp 5	. . . . . 6 ⊢ 3 ∈ ℚ
381		ppiqwordi 16174	. . . . . 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 9380	. . . . . . 7 ⊢ 3 ∈ ℝ
388	387	a1i 9	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → 3 ∈ ℝ)
389		3pos 9400	. . . . . . 7 ⊢ 0 < 3
390	389	a1i 9	. . . . . 6 ⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → 0 < 3)
391		divge0 9205	. . . . . 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 8802	. . . . 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 8451	. 2 ⊢ (((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
398		simpl 109	. . 3 ⊢ ((𝑁 ∈ ℚ ∧ 0 ≤ 𝑁) → 𝑁 ∈ ℚ)
399		qletric 10686	. . 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 8177 ℝcr 8178 0cc0 8179 1c1 8180 + caddc 8182 · cmul 8184 < clt 8360 ≤ cle 8361 − cmin 8498 -cneg 8499 # cap 8911 / cdiv 9004 ℕcn 9306 2c2 9357 3c3 9358 4c4 9359 5c5 9360 6c6 9361 ℕ₀cn0 9567 ℤcz 9648 ℤ_≥cuz 9930 ℚcq 10028 ...cfz 10421 ⌊cfl 10713 mod cmo 10772 ♯chash 11228 ∥ cdvds 12570 ℙcprime 12901 πcppi 16152

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 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-mulrcl 8278 ax-addcom 8279 ax-mulcom 8280 ax-addass 8281 ax-mulass 8282 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-1rid 8286 ax-0id 8287 ax-rnegex 8288 ax-precex 8289 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295 ax-pre-mulgt0 8296 ax-pre-mulext 8297 ax-arch 8298 ax-caucvg 8299

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 7324 df-inf 7325 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8500 df-neg 8501 df-reap 8905 df-ap 8912 df-div 9005 df-inn 9307 df-2 9365 df-3 9366 df-4 9367 df-5 9368 df-6 9369 df-n0 9568 df-z 9649 df-uz 9931 df-q 10029 df-rp 10065 df-icc 10307 df-fz 10422 df-fl 10715 df-mod 10773 df-seqfrec 10898 df-exp 10989 df-ihash 11229 df-cj 11621 df-re 11622 df-im 11623 df-rsqrt 11778 df-abs 11779 df-dvds 12571 df-prm 12902 df-ppi 16154

This theorem is used by: bposlem5 16213

W3C validator