ppiub - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ppiub		Structured version Visualization version GIF version

Theorem ppiub 24863

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
ppiub	⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))

Proof of Theorem ppiub Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		3re 11054	. . 3 ⊢ 3 ∈ ℝ
2	1	a1i 11	. 2 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → 3 ∈ ℝ)
3		simpl 473	. 2 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → 𝑁 ∈ ℝ)
4		ppicl 24791	. . . . . . . 8 ⊢ (𝑁 ∈ ℝ → (π‘𝑁) ∈ ℕ₀)
5	4	nn0red 11312	. . . . . . 7 ⊢ (𝑁 ∈ ℝ → (π‘𝑁) ∈ ℝ)
6	5	adantr 481	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘𝑁) ∈ ℝ)
7		2re 11050	. . . . . 6 ⊢ 2 ∈ ℝ
8		resubcl 10305	. . . . . 6 ⊢ (((π‘𝑁) ∈ ℝ ∧ 2 ∈ ℝ) → ((π‘𝑁) − 2) ∈ ℝ)
9	6, 7, 8	sylancl 693	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ∈ ℝ)
10		fzfi 12727	. . . . . . . . 9 ⊢ (4...(⌊‘𝑁)) ∈ Fin
11		ssrab2 3672	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ⊆ (4...(⌊‘𝑁))
12		ssfi 8140	. . . . . . . . 9 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ⊆ (4...(⌊‘𝑁))) → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ∈ Fin)
13	10, 11, 12	mp2an 707	. . . . . . . 8 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ∈ Fin
14		hashcl 13103	. . . . . . . 8 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ∈ Fin → (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℕ₀)
15	13, 14	ax-mp 5	. . . . . . 7 ⊢ (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℕ₀
16	15	nn0rei 11263	. . . . . 6 ⊢ (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℝ
17	16	a1i 11	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℝ)
18		3nn 11146	. . . . . . 7 ⊢ 3 ∈ ℕ
19		nndivre 11016	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℕ) → (𝑁 / 3) ∈ ℝ)
20	18, 19	mpan2 706	. . . . . 6 ⊢ (𝑁 ∈ ℝ → (𝑁 / 3) ∈ ℝ)
21	20	adantr 481	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 / 3) ∈ ℝ)
22		ppifl 24820	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ → (π‘(⌊‘𝑁)) = (π‘𝑁))
23	22	adantr 481	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘(⌊‘𝑁)) = (π‘𝑁))
24		ppi3 24831	. . . . . . . . 9 ⊢ (π‘3) = 2
25	24	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘3) = 2)
26	23, 25	oveq12d 6633	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = ((π‘𝑁) − 2))
27		3z 11370	. . . . . . . . . . 11 ⊢ 3 ∈ ℤ
28	27	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 3 ∈ ℤ)
29		flcl 12552	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (⌊‘𝑁) ∈ ℤ)
30	29	adantr 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ ℤ)
31		flge 12562	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℤ) → (3 ≤ 𝑁 ↔ 3 ≤ (⌊‘𝑁)))
32	27, 31	mpan2 706	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (3 ≤ 𝑁 ↔ 3 ≤ (⌊‘𝑁)))
33	32	biimpa 501	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 3 ≤ (⌊‘𝑁))
34		eluz2 11653	. . . . . . . . . 10 ⊢ ((⌊‘𝑁) ∈ (ℤ_≥‘3) ↔ (3 ∈ ℤ ∧ (⌊‘𝑁) ∈ ℤ ∧ 3 ≤ (⌊‘𝑁)))
35	28, 30, 33, 34	syl3anbrc 1244	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ (ℤ_≥‘3))
36		ppidif 24823	. . . . . . . . 9 ⊢ ((⌊‘𝑁) ∈ (ℤ_≥‘3) → ((π‘(⌊‘𝑁)) − (π‘3)) = (#‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ)))
37	35, 36	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = (#‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ)))
38		df-4 11041	. . . . . . . . . . 11 ⊢ 4 = (3 + 1)
39	38	oveq1i 6625	. . . . . . . . . 10 ⊢ (4...(⌊‘𝑁)) = ((3 + 1)...(⌊‘𝑁))
40	39	ineq1i 3794	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) = (((3 + 1)...(⌊‘𝑁)) ∩ ℙ)
41	40	fveq2i 6161	. . . . . . . 8 ⊢ (#‘((4...(⌊‘𝑁)) ∩ ℙ)) = (#‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ))
42	37, 41	syl6eqr 2673	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = (#‘((4...(⌊‘𝑁)) ∩ ℙ)))
43	26, 42	eqtr3d 2657	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) = (#‘((4...(⌊‘𝑁)) ∩ ℙ)))
44		dfin5 3568	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 𝑘 ∈ ℙ}
45		elfzle1 12302	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 4 ≤ 𝑘)
46		ppiublem2 24862	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℙ ∧ 4 ≤ 𝑘) → (𝑘 mod 6) ∈ {1, 5})
47	46	expcom 451	. . . . . . . . . . 11 ⊢ (4 ≤ 𝑘 → (𝑘 ∈ ℙ → (𝑘 mod 6) ∈ {1, 5}))
48	45, 47	syl 17	. . . . . . . . . 10 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → (𝑘 ∈ ℙ → (𝑘 mod 6) ∈ {1, 5}))
49	48	ss2rabi 3669	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 𝑘 ∈ ℙ} ⊆ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}
50	44, 49	eqsstri 3620	. . . . . . . 8 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}
51		ssdomg 7961	. . . . . . . 8 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ∈ Fin → (((4...(⌊‘𝑁)) ∩ ℙ) ⊆ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} → ((4...(⌊‘𝑁)) ∩ ℙ) ≼ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}))
52	13, 50, 51	mp2 9	. . . . . . 7 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ≼ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}
53		inss1 3817	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ (4...(⌊‘𝑁))
54		ssfi 8140	. . . . . . . . 9 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ (4...(⌊‘𝑁))) → ((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin)
55	10, 53, 54	mp2an 707	. . . . . . . 8 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin
56		hashdom 13124	. . . . . . . 8 ⊢ ((((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ∈ Fin) → ((#‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤ (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ↔ ((4...(⌊‘𝑁)) ∩ ℙ) ≼ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}))
57	55, 13, 56	mp2an 707	. . . . . . 7 ⊢ ((#‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤ (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ↔ ((4...(⌊‘𝑁)) ∩ ℙ) ≼ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}})
58	52, 57	mpbir 221	. . . . . 6 ⊢ (#‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤ (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}})
59	43, 58	syl6eqbr 4662	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ≤ (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}))
60		reflcl 12553	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (⌊‘𝑁) ∈ ℝ)
61	60	adantr 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ ℝ)
62		peano2rem 10308	. . . . . . . . . 10 ⊢ ((⌊‘𝑁) ∈ ℝ → ((⌊‘𝑁) − 1) ∈ ℝ)
63	61, 62	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ∈ ℝ)
64		6nn 11149	. . . . . . . . 9 ⊢ 6 ∈ ℕ
65		nndivre 11016	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 1) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 1) / 6) ∈ ℝ)
66	63, 64, 65	sylancl 693	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) / 6) ∈ ℝ)
67		reflcl 12553	. . . . . . . 8 ⊢ ((((⌊‘𝑁) − 1) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℝ)
68	66, 67	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℝ)
69		5re 11059	. . . . . . . . . . 11 ⊢ 5 ∈ ℝ
70		resubcl 10305	. . . . . . . . . . 11 ⊢ (((⌊‘𝑁) ∈ ℝ ∧ 5 ∈ ℝ) → ((⌊‘𝑁) − 5) ∈ ℝ)
71	61, 69, 70	sylancl 693	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ∈ ℝ)
72		nndivre 11016	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 5) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 5) / 6) ∈ ℝ)
73	71, 64, 72	sylancl 693	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) / 6) ∈ ℝ)
74		reflcl 12553	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 5) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ)
75	73, 74	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ)
76		peano2re 10169	. . . . . . . 8 ⊢ ((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈ ℝ)
77	75, 76	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈ ℝ)
78		peano2rem 10308	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
79	78	adantr 481	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℝ)
80		nndivre 11016	. . . . . . . 8 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝑁 − 1) / 6) ∈ ℝ)
81	79, 64, 80	sylancl 693	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 1) / 6) ∈ ℝ)
82		simpl 473	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℝ)
83		resubcl 10305	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 5 ∈ ℝ) → (𝑁 − 5) ∈ ℝ)
84	82, 69, 83	sylancl 693	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 5) ∈ ℝ)
85		nndivre 11016	. . . . . . . . 9 ⊢ (((𝑁 − 5) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝑁 − 5) / 6) ∈ ℝ)
86	84, 64, 85	sylancl 693	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 5) / 6) ∈ ℝ)
87		peano2re 10169	. . . . . . . 8 ⊢ (((𝑁 − 5) / 6) ∈ ℝ → (((𝑁 − 5) / 6) + 1) ∈ ℝ)
88	86, 87	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 − 5) / 6) + 1) ∈ ℝ)
89		flle 12556	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 1) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ (((⌊‘𝑁) − 1) / 6))
90	66, 89	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ (((⌊‘𝑁) − 1) / 6))
91		1re 9999	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
92	91	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 1 ∈ ℝ)
93		flle 12556	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (⌊‘𝑁) ≤ 𝑁)
94	93	adantr 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ≤ 𝑁)
95	61, 82, 92, 94	lesub1dd 10603	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ≤ (𝑁 − 1))
96		6re 11061	. . . . . . . . . . 11 ⊢ 6 ∈ ℝ
97	96	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 6 ∈ ℝ)
98		6pos 11079	. . . . . . . . . . 11 ⊢ 0 < 6
99	98	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 0 < 6)
100		lediv1 10848	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 1) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6)) → (((⌊‘𝑁) − 1) ≤ (𝑁 − 1) ↔ (((⌊‘𝑁) − 1) / 6) ≤ ((𝑁 − 1) / 6)))
101	63, 79, 97, 99, 100	syl112anc 1327	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) ≤ (𝑁 − 1) ↔ (((⌊‘𝑁) − 1) / 6) ≤ ((𝑁 − 1) / 6)))
102	95, 101	mpbid 222	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) / 6) ≤ ((𝑁 − 1) / 6))
103	68, 66, 81, 90, 102	letrd 10154	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ ((𝑁 − 1) / 6))
104		flle 12556	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 5) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 5) / 6)) ≤ (((⌊‘𝑁) − 5) / 6))
105	73, 104	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ≤ (((⌊‘𝑁) − 5) / 6))
106	69	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 5 ∈ ℝ)
107	61, 82, 106, 94	lesub1dd 10603	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ≤ (𝑁 − 5))
108		lediv1 10848	. . . . . . . . . . 11 ⊢ ((((⌊‘𝑁) − 5) ∈ ℝ ∧ (𝑁 − 5) ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6)) → (((⌊‘𝑁) − 5) ≤ (𝑁 − 5) ↔ (((⌊‘𝑁) − 5) / 6) ≤ ((𝑁 − 5) / 6)))
109	71, 84, 97, 99, 108	syl112anc 1327	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) ≤ (𝑁 − 5) ↔ (((⌊‘𝑁) − 5) / 6) ≤ ((𝑁 − 5) / 6)))
110	107, 109	mpbid 222	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) / 6) ≤ ((𝑁 − 5) / 6))
111	75, 73, 86, 105, 110	letrd 10154	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ≤ ((𝑁 − 5) / 6))
112	75, 86, 92, 111	leadd1dd 10601	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ≤ (((𝑁 − 5) / 6) + 1))
113	68, 77, 81, 88, 103, 112	le2addd 10606	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) ≤ (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
114		ovex 6643	. . . . . . . . . . . . 13 ⊢ (𝑘 mod 6) ∈ V
115	114	elpr 4176	. . . . . . . . . . . 12 ⊢ ((𝑘 mod 6) ∈ {1, 5} ↔ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5))
116	115	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → ((𝑘 mod 6) ∈ {1, 5} ↔ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)))
117	116	rabbiia 3177	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)}
118		unrab 3880	. . . . . . . . . 10 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)}
119	117, 118	eqtr4i 2646	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} = ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})
120	119	fveq2i 6161	. . . . . . . 8 ⊢ (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = (#‘({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}))
121		ssrab2 3672	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ⊆ (4...(⌊‘𝑁))
122		ssfi 8140	. . . . . . . . . 10 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ⊆ (4...(⌊‘𝑁))) → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∈ Fin)
123	10, 121, 122	mp2an 707	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∈ Fin
124		ssrab2 3672	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ⊆ (4...(⌊‘𝑁))
125		ssfi 8140	. . . . . . . . . 10 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ⊆ (4...(⌊‘𝑁))) → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ∈ Fin)
126	10, 124, 125	mp2an 707	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ∈ Fin
127		inrab 3881	. . . . . . . . . 10 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∩ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)}
128		rabeq0 3937	. . . . . . . . . . 11 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)} = ∅ ↔ ∀𝑘 ∈ (4...(⌊‘𝑁)) ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5))
129		1lt5 11163	. . . . . . . . . . . . . 14 ⊢ 1 < 5
130	91, 129	ltneii 10110	. . . . . . . . . . . . 13 ⊢ 1 ≠ 5
131		eqtr2 2641	. . . . . . . . . . . . . 14 ⊢ (((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5) → 1 = 5)
132	131	necon3ai 2815	. . . . . . . . . . . . 13 ⊢ (1 ≠ 5 → ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5))
133	130, 132	ax-mp 5	. . . . . . . . . . . 12 ⊢ ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)
134	133	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5))
135	128, 134	mprgbir 2923	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)} = ∅
136	127, 135	eqtri 2643	. . . . . . . . 9 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∩ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ∅
137		hashun 13127	. . . . . . . . 9 ⊢ (({𝑘 ∈ (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})))
138	123, 126, 136, 137	mp3an 1421	. . . . . . . 8 ⊢ (#‘({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})) = ((#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}))
139	120, 138	eqtri 2643	. . . . . . 7 ⊢ (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = ((#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}))
140		elfzelz 12300	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 𝑘 ∈ ℤ)
141		nnrp 11802	. . . . . . . . . . . . . . . . 17 ⊢ (6 ∈ ℕ → 6 ∈ ℝ⁺)
142	64, 141	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ ℝ⁺
143		0le1 10511	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 1
144		1lt6 11168	. . . . . . . . . . . . . . . 16 ⊢ 1 < 6
145		modid 12651	. . . . . . . . . . . . . . . 16 ⊢ (((1 ∈ ℝ ∧ 6 ∈ ℝ⁺) ∧ (0 ≤ 1 ∧ 1 < 6)) → (1 mod 6) = 1)
146	91, 142, 143, 144, 145	mp4an 708	. . . . . . . . . . . . . . 15 ⊢ (1 mod 6) = 1
147	146	eqeq2i 2633	. . . . . . . . . . . . . 14 ⊢ ((𝑘 mod 6) = (1 mod 6) ↔ (𝑘 mod 6) = 1)
148		1z 11367	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
149		moddvds 14934	. . . . . . . . . . . . . . 15 ⊢ ((6 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑘 mod 6) = (1 mod 6) ↔ 6 ∥ (𝑘 − 1)))
150	64, 148, 149	mp3an13 1412	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = (1 mod 6) ↔ 6 ∥ (𝑘 − 1)))
151	147, 150	syl5bbr 274	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = 1 ↔ 6 ∥ (𝑘 − 1)))
152	140, 151	syl 17	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → ((𝑘 mod 6) = 1 ↔ 6 ∥ (𝑘 − 1)))
153	152	rabbiia 3177	. . . . . . . . . . 11 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)}
154	153	fveq2i 6161	. . . . . . . . . 10 ⊢ (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)})
155	64	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 6 ∈ ℕ)
156		4z 11371	. . . . . . . . . . . 12 ⊢ 4 ∈ ℤ
157	156	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 4 ∈ ℤ)
158	38	oveq1i 6625	. . . . . . . . . . . . . 14 ⊢ (4 − 1) = ((3 + 1) − 1)
159		3cn 11055	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℂ
160		ax-1cn 9954	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
161	159, 160	pncan3oi 10257	. . . . . . . . . . . . . 14 ⊢ ((3 + 1) − 1) = 3
162	158, 161	eqtri 2643	. . . . . . . . . . . . 13 ⊢ (4 − 1) = 3
163	162	fveq2i 6161	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘(4 − 1)) = (ℤ_≥‘3)
164	35, 163	syl6eleqr 2709	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ (ℤ_≥‘(4 − 1)))
165	148	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 1 ∈ ℤ)
166	155, 157, 164, 165	hashdvds 15423	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))))
167	154, 166	syl5eq 2667	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))))
168		df-3 11040	. . . . . . . . . . . . . . . . 17 ⊢ 3 = (2 + 1)
169	162, 168	eqtri 2643	. . . . . . . . . . . . . . . 16 ⊢ (4 − 1) = (2 + 1)
170	169	oveq1i 6625	. . . . . . . . . . . . . . 15 ⊢ ((4 − 1) − 1) = ((2 + 1) − 1)
171		2cn 11051	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
172	171, 160	pncan3oi 10257	. . . . . . . . . . . . . . 15 ⊢ ((2 + 1) − 1) = 2
173	170, 172	eqtri 2643	. . . . . . . . . . . . . 14 ⊢ ((4 − 1) − 1) = 2
174	173	oveq1i 6625	. . . . . . . . . . . . 13 ⊢ (((4 − 1) − 1) / 6) = (2 / 6)
175	174	fveq2i 6161	. . . . . . . . . . . 12 ⊢ (⌊‘(((4 − 1) − 1) / 6)) = (⌊‘(2 / 6))
176		0re 10000	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
177	64	nnne0i 11015	. . . . . . . . . . . . . . 15 ⊢ 6 ≠ 0
178	7, 96, 177	redivcli 10752	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ∈ ℝ
179		2pos 11072	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
180	7, 96, 179, 98	divgt0ii 10901	. . . . . . . . . . . . . 14 ⊢ 0 < (2 / 6)
181	176, 178, 180	ltleii 10120	. . . . . . . . . . . . 13 ⊢ 0 ≤ (2 / 6)
182		2lt6 11167	. . . . . . . . . . . . . . . 16 ⊢ 2 < 6
183		6cn 11062	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℂ
184	183	mulid1i 10002	. . . . . . . . . . . . . . . 16 ⊢ (6 · 1) = 6
185	182, 184	breqtrri 4650	. . . . . . . . . . . . . . 15 ⊢ 2 < (6 · 1)
186	96, 98	pm3.2i 471	. . . . . . . . . . . . . . . 16 ⊢ (6 ∈ ℝ ∧ 0 < 6)
187		ltdivmul 10858	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ ∧ 1 ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6)) → ((2 / 6) < 1 ↔ 2 < (6 · 1)))
188	7, 91, 186, 187	mp3an 1421	. . . . . . . . . . . . . . 15 ⊢ ((2 / 6) < 1 ↔ 2 < (6 · 1))
189	185, 188	mpbir 221	. . . . . . . . . . . . . 14 ⊢ (2 / 6) < 1
190		1e0p1 11512	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
191	189, 190	breqtri 4648	. . . . . . . . . . . . 13 ⊢ (2 / 6) < (0 + 1)
192		0z 11348	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℤ
193		flbi 12573	. . . . . . . . . . . . . 14 ⊢ (((2 / 6) ∈ ℝ ∧ 0 ∈ ℤ) → ((⌊‘(2 / 6)) = 0 ↔ (0 ≤ (2 / 6) ∧ (2 / 6) < (0 + 1))))
194	178, 192, 193	mp2an 707	. . . . . . . . . . . . 13 ⊢ ((⌊‘(2 / 6)) = 0 ↔ (0 ≤ (2 / 6) ∧ (2 / 6) < (0 + 1)))
195	181, 191, 194	mpbir2an 954	. . . . . . . . . . . 12 ⊢ (⌊‘(2 / 6)) = 0
196	175, 195	eqtri 2643	. . . . . . . . . . 11 ⊢ (⌊‘(((4 − 1) − 1) / 6)) = 0
197	196	oveq2i 6626	. . . . . . . . . 10 ⊢ ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − 0)
198	66	flcld 12555	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℤ)
199	198	zcnd 11443	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℂ)
200	199	subid1d 10341	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) − 0) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
201	197, 200	syl5eq 2667	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
202	167, 201	eqtrd 2655	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
203		5pos 11078	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 5
204	176, 69, 203	ltleii 10120	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 5
205		5lt6 11164	. . . . . . . . . . . . . . . 16 ⊢ 5 < 6
206		modid 12651	. . . . . . . . . . . . . . . 16 ⊢ (((5 ∈ ℝ ∧ 6 ∈ ℝ⁺) ∧ (0 ≤ 5 ∧ 5 < 6)) → (5 mod 6) = 5)
207	69, 142, 204, 205, 206	mp4an 708	. . . . . . . . . . . . . . 15 ⊢ (5 mod 6) = 5
208	207	eqeq2i 2633	. . . . . . . . . . . . . 14 ⊢ ((𝑘 mod 6) = (5 mod 6) ↔ (𝑘 mod 6) = 5)
209		5nn 11148	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ ℕ
210	209	nnzi 11361	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℤ
211		moddvds 14934	. . . . . . . . . . . . . . 15 ⊢ ((6 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 5 ∈ ℤ) → ((𝑘 mod 6) = (5 mod 6) ↔ 6 ∥ (𝑘 − 5)))
212	64, 210, 211	mp3an13 1412	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = (5 mod 6) ↔ 6 ∥ (𝑘 − 5)))
213	208, 212	syl5bbr 274	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = 5 ↔ 6 ∥ (𝑘 − 5)))
214	140, 213	syl 17	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → ((𝑘 mod 6) = 5 ↔ 6 ∥ (𝑘 − 5)))
215	214	rabbiia 3177	. . . . . . . . . . 11 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)}
216	215	fveq2i 6161	. . . . . . . . . 10 ⊢ (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)})
217	210	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 5 ∈ ℤ)
218	155, 157, 164, 217	hashdvds 15423	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))))
219	216, 218	syl5eq 2667	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))))
220	162	oveq1i 6625	. . . . . . . . . . . . . . . 16 ⊢ ((4 − 1) − 5) = (3 − 5)
221		5cn 11060	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℂ
222	221, 159	negsubdi2i 10327	. . . . . . . . . . . . . . . 16 ⊢ -(5 − 3) = (3 − 5)
223		3p2e5 11120	. . . . . . . . . . . . . . . . . . 19 ⊢ (3 + 2) = 5
224	223	oveq1i 6625	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 + 2) − 3) = (5 − 3)
225		pncan2 10248	. . . . . . . . . . . . . . . . . . 19 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
226	159, 171, 225	mp2an 707	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 + 2) − 3) = 2
227	224, 226	eqtr3i 2645	. . . . . . . . . . . . . . . . 17 ⊢ (5 − 3) = 2
228	227	negeqi 10234	. . . . . . . . . . . . . . . 16 ⊢ -(5 − 3) = -2
229	220, 222, 228	3eqtr2i 2649	. . . . . . . . . . . . . . 15 ⊢ ((4 − 1) − 5) = -2
230	229	oveq1i 6625	. . . . . . . . . . . . . 14 ⊢ (((4 − 1) − 5) / 6) = (-2 / 6)
231		divneg 10679	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 6 ∈ ℂ ∧ 6 ≠ 0) → -(2 / 6) = (-2 / 6))
232	171, 183, 177, 231	mp3an 1421	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) = (-2 / 6)
233	230, 232	eqtr4i 2646	. . . . . . . . . . . . 13 ⊢ (((4 − 1) − 5) / 6) = -(2 / 6)
234	233	fveq2i 6161	. . . . . . . . . . . 12 ⊢ (⌊‘(((4 − 1) − 5) / 6)) = (⌊‘-(2 / 6))
235	178, 91, 189	ltleii 10120	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ≤ 1
236	178, 91	lenegi 10533	. . . . . . . . . . . . . 14 ⊢ ((2 / 6) ≤ 1 ↔ -1 ≤ -(2 / 6))
237	235, 236	mpbi 220	. . . . . . . . . . . . 13 ⊢ -1 ≤ -(2 / 6)
238	176, 178	ltnegi 10532	. . . . . . . . . . . . . . 15 ⊢ (0 < (2 / 6) ↔ -(2 / 6) < -0)
239	180, 238	mpbi 220	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) < -0
240		neg0 10287	. . . . . . . . . . . . . . . 16 ⊢ -0 = 0
241		1pneg1e0 11089	. . . . . . . . . . . . . . . 16 ⊢ (1 + -1) = 0
242	240, 241	eqtr4i 2646	. . . . . . . . . . . . . . 15 ⊢ -0 = (1 + -1)
243		neg1cn 11084	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℂ
244	243, 160	addcomi 10187	. . . . . . . . . . . . . . 15 ⊢ (-1 + 1) = (1 + -1)
245	242, 244	eqtr4i 2646	. . . . . . . . . . . . . 14 ⊢ -0 = (-1 + 1)
246	239, 245	breqtri 4648	. . . . . . . . . . . . 13 ⊢ -(2 / 6) < (-1 + 1)
247	178	renegcli 10302	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) ∈ ℝ
248		neg1z 11373	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℤ
249		flbi 12573	. . . . . . . . . . . . . 14 ⊢ ((-(2 / 6) ∈ ℝ ∧ -1 ∈ ℤ) → ((⌊‘-(2 / 6)) = -1 ↔ (-1 ≤ -(2 / 6) ∧ -(2 / 6) < (-1 + 1))))
250	247, 248, 249	mp2an 707	. . . . . . . . . . . . 13 ⊢ ((⌊‘-(2 / 6)) = -1 ↔ (-1 ≤ -(2 / 6) ∧ -(2 / 6) < (-1 + 1)))
251	237, 246, 250	mpbir2an 954	. . . . . . . . . . . 12 ⊢ (⌊‘-(2 / 6)) = -1
252	234, 251	eqtri 2643	. . . . . . . . . . 11 ⊢ (⌊‘(((4 − 1) − 5) / 6)) = -1
253	252	oveq2i 6626	. . . . . . . . . 10 ⊢ ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1)
254	73	flcld 12555	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℤ)
255	254	zcnd 11443	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℂ)
256		subneg 10290	. . . . . . . . . . 11 ⊢ (((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℂ ∧ 1 ∈ ℂ) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
257	255, 160, 256	sylancl 693	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
258	253, 257	syl5eq 2667	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
259	219, 258	eqtrd 2655	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
260	202, 259	oveq12d 6633	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)))
261	139, 260	syl5eq 2667	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)))
262	82	recnd 10028	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℂ)
263	262	2timesd 11235	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (2 · 𝑁) = (𝑁 + 𝑁))
264		df-6 11043	. . . . . . . . . . . . . 14 ⊢ 6 = (5 + 1)
265	221, 160	addcomi 10187	. . . . . . . . . . . . . 14 ⊢ (5 + 1) = (1 + 5)
266	264, 265	eqtri 2643	. . . . . . . . . . . . 13 ⊢ 6 = (1 + 5)
267	266	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 6 = (1 + 5))
268	263, 267	oveq12d 6633	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) − 6) = ((𝑁 + 𝑁) − (1 + 5)))
269		addsub4 10284	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ (1 ∈ ℂ ∧ 5 ∈ ℂ)) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
270	160, 221, 269	mpanr12 720	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
271	262, 262, 270	syl2anc 692	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
272	268, 271	eqtrd 2655	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) − 6) = ((𝑁 − 1) + (𝑁 − 5)))
273	272	oveq1d 6630	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = (((𝑁 − 1) + (𝑁 − 5)) / 6))
274		mulcl 9980	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) ∈ ℂ)
275	171, 262, 274	sylancr 694	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (2 · 𝑁) ∈ ℂ)
276	183, 177	pm3.2i 471	. . . . . . . . . . . 12 ⊢ (6 ∈ ℂ ∧ 6 ≠ 0)
277		divsubdir 10681	. . . . . . . . . . . 12 ⊢ (((2 · 𝑁) ∈ ℂ ∧ 6 ∈ ℂ ∧ (6 ∈ ℂ ∧ 6 ≠ 0)) → (((2 · 𝑁) − 6) / 6) = (((2 · 𝑁) / 6) − (6 / 6)))
278	183, 276, 277	mp3an23 1413	. . . . . . . . . . 11 ⊢ ((2 · 𝑁) ∈ ℂ → (((2 · 𝑁) − 6) / 6) = (((2 · 𝑁) / 6) − (6 / 6)))
279	275, 278	syl 17	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = (((2 · 𝑁) / 6) − (6 / 6)))
280		3t2e6 11139	. . . . . . . . . . . . . 14 ⊢ (3 · 2) = 6
281	159, 171	mulcomi 10006	. . . . . . . . . . . . . 14 ⊢ (3 · 2) = (2 · 3)
282	280, 281	eqtr3i 2645	. . . . . . . . . . . . 13 ⊢ 6 = (2 · 3)
283	282	oveq2i 6626	. . . . . . . . . . . 12 ⊢ ((2 · 𝑁) / 6) = ((2 · 𝑁) / (2 · 3))
284		3ne0 11075	. . . . . . . . . . . . . . 15 ⊢ 3 ≠ 0
285	159, 284	pm3.2i 471	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℂ ∧ 3 ≠ 0)
286		2cnne0 11202	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
287		divcan5 10687	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 𝑁) / (2 · 3)) = (𝑁 / 3))
288	285, 286, 287	mp3an23 1413	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℂ → ((2 · 𝑁) / (2 · 3)) = (𝑁 / 3))
289	262, 288	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) / (2 · 3)) = (𝑁 / 3))
290	283, 289	syl5eq 2667	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) / 6) = (𝑁 / 3))
291	183, 177	dividi 10718	. . . . . . . . . . . 12 ⊢ (6 / 6) = 1
292	291	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (6 / 6) = 1)
293	290, 292	oveq12d 6633	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) / 6) − (6 / 6)) = ((𝑁 / 3) − 1))
294	279, 293	eqtrd 2655	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = ((𝑁 / 3) − 1))
295	79	recnd 10028	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℂ)
296	84	recnd 10028	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 5) ∈ ℂ)
297		divdir 10670	. . . . . . . . . . 11 ⊢ (((𝑁 − 1) ∈ ℂ ∧ (𝑁 − 5) ∈ ℂ ∧ (6 ∈ ℂ ∧ 6 ≠ 0)) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
298	276, 297	mp3an3 1410	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℂ ∧ (𝑁 − 5) ∈ ℂ) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
299	295, 296, 298	syl2anc 692	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
300	273, 294, 299	3eqtr3d 2663	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 / 3) − 1) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
301	300	oveq1d 6630	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 / 3) − 1) + 1) = ((((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)) + 1))
302	21	recnd 10028	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 / 3) ∈ ℂ)
303		npcan 10250	. . . . . . . 8 ⊢ (((𝑁 / 3) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3))
304	302, 160, 303	sylancl 693	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3))
305	81	recnd 10028	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 1) / 6) ∈ ℂ)
306	86	recnd 10028	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 5) / 6) ∈ ℂ)
307	160	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 1 ∈ ℂ)
308	305, 306, 307	addassd 10022	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)) + 1) = (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
309	301, 304, 308	3eqtr3d 2663	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 / 3) = (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
310	113, 261, 309	3brtr4d 4655	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (#‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ≤ (𝑁 / 3))
311	9, 17, 21, 59, 310	letrd 10154	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ≤ (𝑁 / 3))
312	7	a1i 11	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 2 ∈ ℝ)
313	6, 312, 21	lesubaddd 10584	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((π‘𝑁) − 2) ≤ (𝑁 / 3) ↔ (π‘𝑁) ≤ ((𝑁 / 3) + 2)))
314	311, 313	mpbid 222	. . 3 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
315	314	adantlr 750	. 2 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 3 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
316	5	ad2antrr 761	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ∈ ℝ)
317	7	a1i 11	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → 2 ∈ ℝ)
318	20	ad2antrr 761	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (𝑁 / 3) ∈ ℝ)
319		readdcl 9979	. . . 4 ⊢ (((𝑁 / 3) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑁 / 3) + 2) ∈ ℝ)
320	318, 7, 319	sylancl 693	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → ((𝑁 / 3) + 2) ∈ ℝ)
321		ppiwordi 24822	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
322	1, 321	mp3an2 1409	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
323	322	adantlr 750	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
324	323, 24	syl6breq 4664	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ 2)
325		3pos 11074	. . . . . 6 ⊢ 0 < 3
326		divge0 10852	. . . . . 6 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ (3 ∈ ℝ ∧ 0 < 3)) → 0 ≤ (𝑁 / 3))
327	1, 325, 326	mpanr12 720	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → 0 ≤ (𝑁 / 3))
328	327	adantr 481	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → 0 ≤ (𝑁 / 3))
329		addge02 10499	. . . . 5 ⊢ ((2 ∈ ℝ ∧ (𝑁 / 3) ∈ ℝ) → (0 ≤ (𝑁 / 3) ↔ 2 ≤ ((𝑁 / 3) + 2)))
330	7, 318, 329	sylancr 694	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (0 ≤ (𝑁 / 3) ↔ 2 ≤ ((𝑁 / 3) + 2)))
331	328, 330	mpbid 222	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → 2 ≤ ((𝑁 / 3) + 2))
332	316, 317, 320, 324, 331	letrd 10154	. 2 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
333	2, 3, 315, 332	lecasei 10103	1 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 = wceq 1480 ∈ wcel 1987 ≠ wne 2790 {crab 2912 ∪ cun 3558 ∩ cin 3559 ⊆ wss 3560 ∅c0 3897 {cpr 4157 class class class wbr 4623 ‘cfv 5857 (class class class)co 6615 ≼ cdom 7913 Fincfn 7915 ℂcc 9894 ℝcr 9895 0cc0 9896 1c1 9897 + caddc 9899 · cmul 9901 < clt 10034 ≤ cle 10035 − cmin 10226 -cneg 10227 / cdiv 10644 ℕcn 10980 2c2 11030 3c3 11031 4c4 11032 5c5 11033 6c6 11034 ℕ₀cn0 11252 ℤcz 11337 ℤ_≥cuz 11647 ℝ⁺crp 11792 ...cfz 12284 ⌊cfl 12547 mod cmo 12624 #chash 13073 ∥ cdvds 14926 ℙcprime 15328 πcppi 24754

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-8 1989 ax-9 1996 ax-10 2016 ax-11 2031 ax-12 2044 ax-13 2245 ax-ext 2601 ax-rep 4741 ax-sep 4751 ax-nul 4759 ax-pow 4813 ax-pr 4877 ax-un 6914 ax-cnex 9952 ax-resscn 9953 ax-1cn 9954 ax-icn 9955 ax-addcl 9956 ax-addrcl 9957 ax-mulcl 9958 ax-mulrcl 9959 ax-mulcom 9960 ax-addass 9961 ax-mulass 9962 ax-distr 9963 ax-i2m1 9964 ax-1ne0 9965 ax-1rid 9966 ax-rnegex 9967 ax-rrecex 9968 ax-cnre 9969 ax-pre-lttri 9970 ax-pre-lttrn 9971 ax-pre-ltadd 9972 ax-pre-mulgt0 9973 ax-pre-sup 9974

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1483 df-ex 1702 df-nf 1707 df-sb 1878 df-eu 2473 df-mo 2474 df-clab 2608 df-cleq 2614 df-clel 2617 df-nfc 2750 df-ne 2791 df-nel 2894 df-ral 2913 df-rex 2914 df-reu 2915 df-rmo 2916 df-rab 2917 df-v 3192 df-sbc 3423 df-csb 3520 df-dif 3563 df-un 3565 df-in 3567 df-ss 3574 df-pss 3576 df-nul 3898 df-if 4065 df-pw 4138 df-sn 4156 df-pr 4158 df-tp 4160 df-op 4162 df-uni 4410 df-int 4448 df-iun 4494 df-br 4624 df-opab 4684 df-mpt 4685 df-tr 4723 df-eprel 4995 df-id 4999 df-po 5005 df-so 5006 df-fr 5043 df-we 5045 df-xp 5090 df-rel 5091 df-cnv 5092 df-co 5093 df-dm 5094 df-rn 5095 df-res 5096 df-ima 5097 df-pred 5649 df-ord 5695 df-on 5696 df-lim 5697 df-suc 5698 df-iota 5820 df-fun 5859 df-fn 5860 df-f 5861 df-f1 5862 df-fo 5863 df-f1o 5864 df-fv 5865 df-riota 6576 df-ov 6618 df-oprab 6619 df-mpt2 6620 df-om 7028 df-1st 7128 df-2nd 7129 df-wrecs 7367 df-recs 7428 df-rdg 7466 df-1o 7520 df-2o 7521 df-oadd 7524 df-er 7702 df-en 7916 df-dom 7917 df-sdom 7918 df-fin 7919 df-sup 8308 df-inf 8309 df-card 8725 df-cda 8950 df-pnf 10036 df-mnf 10037 df-xr 10038 df-ltxr 10039 df-le 10040 df-sub 10228 df-neg 10229 df-div 10645 df-nn 10981 df-2 11039 df-3 11040 df-4 11041 df-5 11042 df-6 11043 df-n0 11253 df-xnn0 11324 df-z 11338 df-uz 11648 df-rp 11793 df-icc 12140 df-fz 12285 df-fl 12549 df-mod 12625 df-seq 12758 df-exp 12817 df-hash 13074 df-cj 13789 df-re 13790 df-im 13791 df-sqrt 13925 df-abs 13926 df-dvds 14927 df-prm 15329 df-ppi 24760

This theorem is referenced by: bposlem5 24947

W3C validator