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 27183

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 12237	. . 3 ⊢ 3 ∈ ℝ
2	1	a1i 11	. 2 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → 3 ∈ ℝ)
3		simpl 482	. 2 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → 𝑁 ∈ ℝ)
4		ppicl 27109	. . . . . . . 8 ⊢ (𝑁 ∈ ℝ → (π‘𝑁) ∈ ℕ₀)
5	4	nn0red 12475	. . . . . . 7 ⊢ (𝑁 ∈ ℝ → (π‘𝑁) ∈ ℝ)
6	5	adantr 480	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘𝑁) ∈ ℝ)
7		2re 12231	. . . . . 6 ⊢ 2 ∈ ℝ
8		resubcl 11457	. . . . . 6 ⊢ (((π‘𝑁) ∈ ℝ ∧ 2 ∈ ℝ) → ((π‘𝑁) − 2) ∈ ℝ)
9	6, 7, 8	sylancl 587	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ∈ ℝ)
10		fzfi 13907	. . . . . . . . 9 ⊢ (4...(⌊‘𝑁)) ∈ Fin
11		ssrab2 4034	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ⊆ (4...(⌊‘𝑁))
12		ssfi 9109	. . . . . . . . 9 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ⊆ (4...(⌊‘𝑁))) → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ∈ Fin)
13	10, 11, 12	mp2an 693	. . . . . . . 8 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ∈ Fin
14		hashcl 14291	. . . . . . . 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 12424	. . . . . 6 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℝ
17	16	a1i 11	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℝ)
18		3nn 12236	. . . . . . 7 ⊢ 3 ∈ ℕ
19		nndivre 12198	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℕ) → (𝑁 / 3) ∈ ℝ)
20	18, 19	mpan2 692	. . . . . 6 ⊢ (𝑁 ∈ ℝ → (𝑁 / 3) ∈ ℝ)
21	20	adantr 480	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 / 3) ∈ ℝ)
22		ppifl 27138	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ → (π‘(⌊‘𝑁)) = (π‘𝑁))
23	22	adantr 480	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘(⌊‘𝑁)) = (π‘𝑁))
24		ppi3 27149	. . . . . . . . 9 ⊢ (π‘3) = 2
25	24	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘3) = 2)
26	23, 25	oveq12d 7386	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = ((π‘𝑁) − 2))
27		3z 12536	. . . . . . . . . . 11 ⊢ 3 ∈ ℤ
28	27	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 3 ∈ ℤ)
29		flcl 13727	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (⌊‘𝑁) ∈ ℤ)
30	29	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ ℤ)
31		flge 13737	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℤ) → (3 ≤ 𝑁 ↔ 3 ≤ (⌊‘𝑁)))
32	27, 31	mpan2 692	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (3 ≤ 𝑁 ↔ 3 ≤ (⌊‘𝑁)))
33	32	biimpa 476	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 3 ≤ (⌊‘𝑁))
34		eluz2 12769	. . . . . . . . . 10 ⊢ ((⌊‘𝑁) ∈ (ℤ_≥‘3) ↔ (3 ∈ ℤ ∧ (⌊‘𝑁) ∈ ℤ ∧ 3 ≤ (⌊‘𝑁)))
35	28, 30, 33, 34	syl3anbrc 1345	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ (ℤ_≥‘3))
36		ppidif 27141	. . . . . . . . 9 ⊢ ((⌊‘𝑁) ∈ (ℤ_≥‘3) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ)))
37	35, 36	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ)))
38		df-4 12222	. . . . . . . . . . 11 ⊢ 4 = (3 + 1)
39	38	oveq1i 7378	. . . . . . . . . 10 ⊢ (4...(⌊‘𝑁)) = ((3 + 1)...(⌊‘𝑁))
40	39	ineq1i 4170	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) = (((3 + 1)...(⌊‘𝑁)) ∩ ℙ)
41	40	fveq2i 6845	. . . . . . . 8 ⊢ (♯‘((4...(⌊‘𝑁)) ∩ ℙ)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ))
42	37, 41	eqtr4di 2790	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘((4...(⌊‘𝑁)) ∩ ℙ)))
43	26, 42	eqtr3d 2774	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) = (♯‘((4...(⌊‘𝑁)) ∩ ℙ)))
44		dfin5 3911	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 𝑘 ∈ ℙ}
45		elfzle1 13455	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 4 ≤ 𝑘)
46		ppiublem2 27182	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℙ ∧ 4 ≤ 𝑘) → (𝑘 mod 6) ∈ {1, 5})
47	46	expcom 413	. . . . . . . . . . 11 ⊢ (4 ≤ 𝑘 → (𝑘 ∈ ℙ → (𝑘 mod 6) ∈ {1, 5}))
48	45, 47	syl 17	. . . . . . . . . 10 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → (𝑘 ∈ ℙ → (𝑘 mod 6) ∈ {1, 5}))
49	48	ss2rabi 4030	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 𝑘 ∈ ℙ} ⊆ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}
50	44, 49	eqsstri 3982	. . . . . . . 8 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}
51		ssdomg 8949	. . . . . . . 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 4191	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ (4...(⌊‘𝑁))
54		ssfi 9109	. . . . . . . . 9 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ (4...(⌊‘𝑁))) → ((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin)
55	10, 53, 54	mp2an 693	. . . . . . . 8 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin
56		hashdom 14314	. . . . . . . 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 693	. . . . . . 7 ⊢ ((♯‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ↔ ((4...(⌊‘𝑁)) ∩ ℙ) ≼ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}})
58	52, 57	mpbir 231	. . . . . 6 ⊢ (♯‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}})
59	43, 58	eqbrtrdi 5139	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ≤ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}))
60		reflcl 13728	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (⌊‘𝑁) ∈ ℝ)
61	60	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ ℝ)
62		peano2rem 11460	. . . . . . . . . 10 ⊢ ((⌊‘𝑁) ∈ ℝ → ((⌊‘𝑁) − 1) ∈ ℝ)
63	61, 62	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ∈ ℝ)
64		6nn 12246	. . . . . . . . 9 ⊢ 6 ∈ ℕ
65		nndivre 12198	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 1) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 1) / 6) ∈ ℝ)
66	63, 64, 65	sylancl 587	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) / 6) ∈ ℝ)
67		reflcl 13728	. . . . . . . 8 ⊢ ((((⌊‘𝑁) − 1) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℝ)
68	66, 67	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℝ)
69		5re 12244	. . . . . . . . . . 11 ⊢ 5 ∈ ℝ
70		resubcl 11457	. . . . . . . . . . 11 ⊢ (((⌊‘𝑁) ∈ ℝ ∧ 5 ∈ ℝ) → ((⌊‘𝑁) − 5) ∈ ℝ)
71	61, 69, 70	sylancl 587	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ∈ ℝ)
72		nndivre 12198	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 5) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 5) / 6) ∈ ℝ)
73	71, 64, 72	sylancl 587	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) / 6) ∈ ℝ)
74		reflcl 13728	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 5) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ)
75	73, 74	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ)
76		peano2re 11318	. . . . . . . 8 ⊢ ((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈ ℝ)
77	75, 76	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈ ℝ)
78		peano2rem 11460	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
79	78	adantr 480	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℝ)
80		nndivre 12198	. . . . . . . 8 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝑁 − 1) / 6) ∈ ℝ)
81	79, 64, 80	sylancl 587	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 1) / 6) ∈ ℝ)
82		simpl 482	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℝ)
83		resubcl 11457	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 5 ∈ ℝ) → (𝑁 − 5) ∈ ℝ)
84	82, 69, 83	sylancl 587	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 5) ∈ ℝ)
85		nndivre 12198	. . . . . . . . 9 ⊢ (((𝑁 − 5) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝑁 − 5) / 6) ∈ ℝ)
86	84, 64, 85	sylancl 587	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 5) / 6) ∈ ℝ)
87		peano2re 11318	. . . . . . . 8 ⊢ (((𝑁 − 5) / 6) ∈ ℝ → (((𝑁 − 5) / 6) + 1) ∈ ℝ)
88	86, 87	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 − 5) / 6) + 1) ∈ ℝ)
89		flle 13731	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 1) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ (((⌊‘𝑁) − 1) / 6))
90	66, 89	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ (((⌊‘𝑁) − 1) / 6))
91		1re 11144	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
92	91	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 1 ∈ ℝ)
93		flle 13731	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (⌊‘𝑁) ≤ 𝑁)
94	93	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ≤ 𝑁)
95	61, 82, 92, 94	lesub1dd 11765	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ≤ (𝑁 − 1))
96		6re 12247	. . . . . . . . . . 11 ⊢ 6 ∈ ℝ
97	96	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 6 ∈ ℝ)
98		6pos 12267	. . . . . . . . . . 11 ⊢ 0 < 6
99	98	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 0 < 6)
100		lediv1 12019	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 1) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6)) → (((⌊‘𝑁) − 1) ≤ (𝑁 − 1) ↔ (((⌊‘𝑁) − 1) / 6) ≤ ((𝑁 − 1) / 6)))
101	63, 79, 97, 99, 100	syl112anc 1377	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) ≤ (𝑁 − 1) ↔ (((⌊‘𝑁) − 1) / 6) ≤ ((𝑁 − 1) / 6)))
102	95, 101	mpbid 232	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) / 6) ≤ ((𝑁 − 1) / 6))
103	68, 66, 81, 90, 102	letrd 11302	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ ((𝑁 − 1) / 6))
104		flle 13731	. . . . . . . . . 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 11765	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ≤ (𝑁 − 5))
108		lediv1 12019	. . . . . . . . . . 11 ⊢ ((((⌊‘𝑁) − 5) ∈ ℝ ∧ (𝑁 − 5) ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6)) → (((⌊‘𝑁) − 5) ≤ (𝑁 − 5) ↔ (((⌊‘𝑁) − 5) / 6) ≤ ((𝑁 − 5) / 6)))
109	71, 84, 97, 99, 108	syl112anc 1377	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) ≤ (𝑁 − 5) ↔ (((⌊‘𝑁) − 5) / 6) ≤ ((𝑁 − 5) / 6)))
110	107, 109	mpbid 232	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) / 6) ≤ ((𝑁 − 5) / 6))
111	75, 73, 86, 105, 110	letrd 11302	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ≤ ((𝑁 − 5) / 6))
112	75, 86, 92, 111	leadd1dd 11763	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ≤ (((𝑁 − 5) / 6) + 1))
113	68, 77, 81, 88, 103, 112	le2addd 11768	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) ≤ (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
114		ovex 7401	. . . . . . . . . . . 12 ⊢ (𝑘 mod 6) ∈ V
115	114	elpr 4607	. . . . . . . . . . 11 ⊢ ((𝑘 mod 6) ∈ {1, 5} ↔ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5))
116	115	rabbii 3406	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)}
117		unrab 4269	. . . . . . . . . 10 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)}
118	116, 117	eqtr4i 2763	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} = ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})
119	118	fveq2i 6845	. . . . . . . 8 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = (♯‘({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}))
120		ssrab2 4034	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ⊆ (4...(⌊‘𝑁))
121		ssfi 9109	. . . . . . . . . 10 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ⊆ (4...(⌊‘𝑁))) → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∈ Fin)
122	10, 120, 121	mp2an 693	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∈ Fin
123		ssrab2 4034	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ⊆ (4...(⌊‘𝑁))
124		ssfi 9109	. . . . . . . . . 10 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ⊆ (4...(⌊‘𝑁))) → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ∈ Fin)
125	10, 123, 124	mp2an 693	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ∈ Fin
126		inrab 4270	. . . . . . . . . 10 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∩ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)}
127		rabeq0 4342	. . . . . . . . . . 11 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)} = ∅ ↔ ∀𝑘 ∈ (4...(⌊‘𝑁)) ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5))
128		1lt5 12332	. . . . . . . . . . . . . 14 ⊢ 1 < 5
129	91, 128	ltneii 11258	. . . . . . . . . . . . 13 ⊢ 1 ≠ 5
130		eqtr2 2758	. . . . . . . . . . . . . 14 ⊢ (((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5) → 1 = 5)
131	130	necon3ai 2958	. . . . . . . . . . . . 13 ⊢ (1 ≠ 5 → ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5))
132	129, 131	ax-mp 5	. . . . . . . . . . . 12 ⊢ ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)
133	132	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5))
134	127, 133	mprgbir 3059	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)} = ∅
135	126, 134	eqtri 2760	. . . . . . . . 9 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∩ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ∅
136		hashun 14317	. . . . . . . . 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})))
137	122, 125, 135, 136	mp3an 1464	. . . . . . . 8 ⊢ (♯‘({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})) = ((♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}))
138	119, 137	eqtri 2760	. . . . . . 7 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = ((♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}))
139		elfzelz 13452	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 𝑘 ∈ ℤ)
140		nnrp 12929	. . . . . . . . . . . . . . . . 17 ⊢ (6 ∈ ℕ → 6 ∈ ℝ⁺)
141	64, 140	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ ℝ⁺
142		0le1 11672	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 1
143		1lt6 12337	. . . . . . . . . . . . . . . 16 ⊢ 1 < 6
144		modid 13828	. . . . . . . . . . . . . . . 16 ⊢ (((1 ∈ ℝ ∧ 6 ∈ ℝ⁺) ∧ (0 ≤ 1 ∧ 1 < 6)) → (1 mod 6) = 1)
145	91, 141, 142, 143, 144	mp4an 694	. . . . . . . . . . . . . . 15 ⊢ (1 mod 6) = 1
146	145	eqeq2i 2750	. . . . . . . . . . . . . 14 ⊢ ((𝑘 mod 6) = (1 mod 6) ↔ (𝑘 mod 6) = 1)
147		1z 12533	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
148		moddvds 16202	. . . . . . . . . . . . . . 15 ⊢ ((6 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑘 mod 6) = (1 mod 6) ↔ 6 ∥ (𝑘 − 1)))
149	64, 147, 148	mp3an13 1455	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = (1 mod 6) ↔ 6 ∥ (𝑘 − 1)))
150	146, 149	bitr3id 285	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = 1 ↔ 6 ∥ (𝑘 − 1)))
151	139, 150	syl 17	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → ((𝑘 mod 6) = 1 ↔ 6 ∥ (𝑘 − 1)))
152	151	rabbiia 3405	. . . . . . . . . . 11 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)}
153	152	fveq2i 6845	. . . . . . . . . 10 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)})
154	64	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 6 ∈ ℕ)
155		4z 12537	. . . . . . . . . . . 12 ⊢ 4 ∈ ℤ
156	155	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 4 ∈ ℤ)
157		4m1e3 12281	. . . . . . . . . . . . 13 ⊢ (4 − 1) = 3
158	157	fveq2i 6845	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘(4 − 1)) = (ℤ_≥‘3)
159	35, 158	eleqtrrdi 2848	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ (ℤ_≥‘(4 − 1)))
160	147	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 1 ∈ ℤ)
161	154, 156, 159, 160	hashdvds 16714	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))))
162	153, 161	eqtrid 2784	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))))
163		2cn 12232	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
164		ax-1cn 11096	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
165		df-3 12221	. . . . . . . . . . . . . . . 16 ⊢ 3 = (2 + 1)
166	157, 165	eqtri 2760	. . . . . . . . . . . . . . 15 ⊢ (4 − 1) = (2 + 1)
167	163, 164, 166	mvrraddi 11409	. . . . . . . . . . . . . 14 ⊢ ((4 − 1) − 1) = 2
168	167	oveq1i 7378	. . . . . . . . . . . . 13 ⊢ (((4 − 1) − 1) / 6) = (2 / 6)
169	168	fveq2i 6845	. . . . . . . . . . . 12 ⊢ (⌊‘(((4 − 1) − 1) / 6)) = (⌊‘(2 / 6))
170		0re 11146	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
171	64	nnne0i 12197	. . . . . . . . . . . . . . 15 ⊢ 6 ≠ 0
172	7, 96, 171	redivcli 11920	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ∈ ℝ
173		2pos 12260	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
174	7, 96, 173, 98	divgt0ii 12071	. . . . . . . . . . . . . 14 ⊢ 0 < (2 / 6)
175	170, 172, 174	ltleii 11268	. . . . . . . . . . . . 13 ⊢ 0 ≤ (2 / 6)
176		2lt6 12336	. . . . . . . . . . . . . . . 16 ⊢ 2 < 6
177		6cn 12248	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℂ
178	177	mulridi 11148	. . . . . . . . . . . . . . . 16 ⊢ (6 · 1) = 6
179	176, 178	breqtrri 5127	. . . . . . . . . . . . . . 15 ⊢ 2 < (6 · 1)
180	96, 98	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ (6 ∈ ℝ ∧ 0 < 6)
181		ltdivmul 12029	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ ∧ 1 ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6)) → ((2 / 6) < 1 ↔ 2 < (6 · 1)))
182	7, 91, 180, 181	mp3an 1464	. . . . . . . . . . . . . . 15 ⊢ ((2 / 6) < 1 ↔ 2 < (6 · 1))
183	179, 182	mpbir 231	. . . . . . . . . . . . . 14 ⊢ (2 / 6) < 1
184		1e0p1 12661	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
185	183, 184	breqtri 5125	. . . . . . . . . . . . 13 ⊢ (2 / 6) < (0 + 1)
186		0z 12511	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℤ
187		flbi 13748	. . . . . . . . . . . . . 14 ⊢ (((2 / 6) ∈ ℝ ∧ 0 ∈ ℤ) → ((⌊‘(2 / 6)) = 0 ↔ (0 ≤ (2 / 6) ∧ (2 / 6) < (0 + 1))))
188	172, 186, 187	mp2an 693	. . . . . . . . . . . . 13 ⊢ ((⌊‘(2 / 6)) = 0 ↔ (0 ≤ (2 / 6) ∧ (2 / 6) < (0 + 1)))
189	175, 185, 188	mpbir2an 712	. . . . . . . . . . . 12 ⊢ (⌊‘(2 / 6)) = 0
190	169, 189	eqtri 2760	. . . . . . . . . . 11 ⊢ (⌊‘(((4 − 1) − 1) / 6)) = 0
191	190	oveq2i 7379	. . . . . . . . . 10 ⊢ ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − 0)
192	66	flcld 13730	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℤ)
193	192	zcnd 12609	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℂ)
194	193	subid1d 11493	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) − 0) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
195	191, 194	eqtrid 2784	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
196	162, 195	eqtrd 2772	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
197		5pos 12266	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 5
198	170, 69, 197	ltleii 11268	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 5
199		5lt6 12333	. . . . . . . . . . . . . . . 16 ⊢ 5 < 6
200		modid 13828	. . . . . . . . . . . . . . . 16 ⊢ (((5 ∈ ℝ ∧ 6 ∈ ℝ⁺) ∧ (0 ≤ 5 ∧ 5 < 6)) → (5 mod 6) = 5)
201	69, 141, 198, 199, 200	mp4an 694	. . . . . . . . . . . . . . 15 ⊢ (5 mod 6) = 5
202	201	eqeq2i 2750	. . . . . . . . . . . . . 14 ⊢ ((𝑘 mod 6) = (5 mod 6) ↔ (𝑘 mod 6) = 5)
203		5nn 12243	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ ℕ
204	203	nnzi 12527	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℤ
205		moddvds 16202	. . . . . . . . . . . . . . 15 ⊢ ((6 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 5 ∈ ℤ) → ((𝑘 mod 6) = (5 mod 6) ↔ 6 ∥ (𝑘 − 5)))
206	64, 204, 205	mp3an13 1455	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = (5 mod 6) ↔ 6 ∥ (𝑘 − 5)))
207	202, 206	bitr3id 285	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = 5 ↔ 6 ∥ (𝑘 − 5)))
208	139, 207	syl 17	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → ((𝑘 mod 6) = 5 ↔ 6 ∥ (𝑘 − 5)))
209	208	rabbiia 3405	. . . . . . . . . . 11 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)}
210	209	fveq2i 6845	. . . . . . . . . 10 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)})
211	204	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 5 ∈ ℤ)
212	154, 156, 159, 211	hashdvds 16714	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))))
213	210, 212	eqtrid 2784	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))))
214	157	oveq1i 7378	. . . . . . . . . . . . . . . 16 ⊢ ((4 − 1) − 5) = (3 − 5)
215		5cn 12245	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℂ
216		3cn 12238	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℂ
217	215, 216	negsubdi2i 11479	. . . . . . . . . . . . . . . 16 ⊢ -(5 − 3) = (3 − 5)
218		3p2e5 12303	. . . . . . . . . . . . . . . . . . 19 ⊢ (3 + 2) = 5
219	218	oveq1i 7378	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 + 2) − 3) = (5 − 3)
220		pncan2 11399	. . . . . . . . . . . . . . . . . . 19 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
221	216, 163, 220	mp2an 693	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 + 2) − 3) = 2
222	219, 221	eqtr3i 2762	. . . . . . . . . . . . . . . . 17 ⊢ (5 − 3) = 2
223	222	negeqi 11385	. . . . . . . . . . . . . . . 16 ⊢ -(5 − 3) = -2
224	214, 217, 223	3eqtr2i 2766	. . . . . . . . . . . . . . 15 ⊢ ((4 − 1) − 5) = -2
225	224	oveq1i 7378	. . . . . . . . . . . . . 14 ⊢ (((4 − 1) − 5) / 6) = (-2 / 6)
226		divneg 11845	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 6 ∈ ℂ ∧ 6 ≠ 0) → -(2 / 6) = (-2 / 6))
227	163, 177, 171, 226	mp3an 1464	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) = (-2 / 6)
228	225, 227	eqtr4i 2763	. . . . . . . . . . . . 13 ⊢ (((4 − 1) − 5) / 6) = -(2 / 6)
229	228	fveq2i 6845	. . . . . . . . . . . 12 ⊢ (⌊‘(((4 − 1) − 5) / 6)) = (⌊‘-(2 / 6))
230	172, 91, 183	ltleii 11268	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ≤ 1
231	172, 91	lenegi 11694	. . . . . . . . . . . . . 14 ⊢ ((2 / 6) ≤ 1 ↔ -1 ≤ -(2 / 6))
232	230, 231	mpbi 230	. . . . . . . . . . . . 13 ⊢ -1 ≤ -(2 / 6)
233	170, 172	ltnegi 11693	. . . . . . . . . . . . . . 15 ⊢ (0 < (2 / 6) ↔ -(2 / 6) < -0)
234	174, 233	mpbi 230	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) < -0
235		neg0 11439	. . . . . . . . . . . . . . . 16 ⊢ -0 = 0
236		1pneg1e0 12271	. . . . . . . . . . . . . . . 16 ⊢ (1 + -1) = 0
237	235, 236	eqtr4i 2763	. . . . . . . . . . . . . . 15 ⊢ -0 = (1 + -1)
238		neg1cn 12142	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℂ
239	238, 164	addcomi 11336	. . . . . . . . . . . . . . 15 ⊢ (-1 + 1) = (1 + -1)
240	237, 239	eqtr4i 2763	. . . . . . . . . . . . . 14 ⊢ -0 = (-1 + 1)
241	234, 240	breqtri 5125	. . . . . . . . . . . . 13 ⊢ -(2 / 6) < (-1 + 1)
242	172	renegcli 11454	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) ∈ ℝ
243		neg1z 12539	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℤ
244		flbi 13748	. . . . . . . . . . . . . 14 ⊢ ((-(2 / 6) ∈ ℝ ∧ -1 ∈ ℤ) → ((⌊‘-(2 / 6)) = -1 ↔ (-1 ≤ -(2 / 6) ∧ -(2 / 6) < (-1 + 1))))
245	242, 243, 244	mp2an 693	. . . . . . . . . . . . 13 ⊢ ((⌊‘-(2 / 6)) = -1 ↔ (-1 ≤ -(2 / 6) ∧ -(2 / 6) < (-1 + 1)))
246	232, 241, 245	mpbir2an 712	. . . . . . . . . . . 12 ⊢ (⌊‘-(2 / 6)) = -1
247	229, 246	eqtri 2760	. . . . . . . . . . 11 ⊢ (⌊‘(((4 − 1) − 5) / 6)) = -1
248	247	oveq2i 7379	. . . . . . . . . 10 ⊢ ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1)
249	73	flcld 13730	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℤ)
250	249	zcnd 12609	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℂ)
251		subneg 11442	. . . . . . . . . . 11 ⊢ (((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℂ ∧ 1 ∈ ℂ) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
252	250, 164, 251	sylancl 587	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
253	248, 252	eqtrid 2784	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
254	213, 253	eqtrd 2772	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
255	196, 254	oveq12d 7386	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)))
256	138, 255	eqtrid 2784	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)))
257	82	recnd 11172	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℂ)
258	257	2timesd 12396	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (2 · 𝑁) = (𝑁 + 𝑁))
259		df-6 12224	. . . . . . . . . . . . . 14 ⊢ 6 = (5 + 1)
260	215, 164	addcomi 11336	. . . . . . . . . . . . . 14 ⊢ (5 + 1) = (1 + 5)
261	259, 260	eqtri 2760	. . . . . . . . . . . . 13 ⊢ 6 = (1 + 5)
262	261	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 6 = (1 + 5))
263	258, 262	oveq12d 7386	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) − 6) = ((𝑁 + 𝑁) − (1 + 5)))
264		addsub4 11436	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ (1 ∈ ℂ ∧ 5 ∈ ℂ)) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
265	164, 215, 264	mpanr12 706	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
266	257, 257, 265	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
267	263, 266	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) − 6) = ((𝑁 − 1) + (𝑁 − 5)))
268	267	oveq1d 7383	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = (((𝑁 − 1) + (𝑁 − 5)) / 6))
269		mulcl 11122	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) ∈ ℂ)
270	163, 257, 269	sylancr 588	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (2 · 𝑁) ∈ ℂ)
271	177, 171	pm3.2i 470	. . . . . . . . . . . 12 ⊢ (6 ∈ ℂ ∧ 6 ≠ 0)
272		divsubdir 11847	. . . . . . . . . . . 12 ⊢ (((2 · 𝑁) ∈ ℂ ∧ 6 ∈ ℂ ∧ (6 ∈ ℂ ∧ 6 ≠ 0)) → (((2 · 𝑁) − 6) / 6) = (((2 · 𝑁) / 6) − (6 / 6)))
273	177, 271, 272	mp3an23 1456	. . . . . . . . . . 11 ⊢ ((2 · 𝑁) ∈ ℂ → (((2 · 𝑁) − 6) / 6) = (((2 · 𝑁) / 6) − (6 / 6)))
274	270, 273	syl 17	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = (((2 · 𝑁) / 6) − (6 / 6)))
275		3t2e6 12318	. . . . . . . . . . . . . 14 ⊢ (3 · 2) = 6
276	216, 163	mulcomi 11152	. . . . . . . . . . . . . 14 ⊢ (3 · 2) = (2 · 3)
277	275, 276	eqtr3i 2762	. . . . . . . . . . . . 13 ⊢ 6 = (2 · 3)
278	277	oveq2i 7379	. . . . . . . . . . . 12 ⊢ ((2 · 𝑁) / 6) = ((2 · 𝑁) / (2 · 3))
279		3ne0 12263	. . . . . . . . . . . . . . 15 ⊢ 3 ≠ 0
280	216, 279	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℂ ∧ 3 ≠ 0)
281		2cnne0 12362	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
282		divcan5 11855	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 𝑁) / (2 · 3)) = (𝑁 / 3))
283	280, 281, 282	mp3an23 1456	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℂ → ((2 · 𝑁) / (2 · 3)) = (𝑁 / 3))
284	257, 283	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) / (2 · 3)) = (𝑁 / 3))
285	278, 284	eqtrid 2784	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) / 6) = (𝑁 / 3))
286	177, 171	dividi 11886	. . . . . . . . . . . 12 ⊢ (6 / 6) = 1
287	286	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (6 / 6) = 1)
288	285, 287	oveq12d 7386	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) / 6) − (6 / 6)) = ((𝑁 / 3) − 1))
289	274, 288	eqtrd 2772	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = ((𝑁 / 3) − 1))
290	79	recnd 11172	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℂ)
291	84	recnd 11172	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 5) ∈ ℂ)
292		divdir 11833	. . . . . . . . . . 11 ⊢ (((𝑁 − 1) ∈ ℂ ∧ (𝑁 − 5) ∈ ℂ ∧ (6 ∈ ℂ ∧ 6 ≠ 0)) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
293	271, 292	mp3an3 1453	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℂ ∧ (𝑁 − 5) ∈ ℂ) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
294	290, 291, 293	syl2anc 585	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
295	268, 289, 294	3eqtr3d 2780	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 / 3) − 1) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
296	295	oveq1d 7383	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 / 3) − 1) + 1) = ((((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)) + 1))
297	21	recnd 11172	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 / 3) ∈ ℂ)
298		npcan 11401	. . . . . . . 8 ⊢ (((𝑁 / 3) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3))
299	297, 164, 298	sylancl 587	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3))
300	81	recnd 11172	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 1) / 6) ∈ ℂ)
301	86	recnd 11172	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 5) / 6) ∈ ℂ)
302	164	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 1 ∈ ℂ)
303	300, 301, 302	addassd 11166	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)) + 1) = (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
304	296, 299, 303	3eqtr3d 2780	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 / 3) = (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
305	113, 256, 304	3brtr4d 5132	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ≤ (𝑁 / 3))
306	9, 17, 21, 59, 305	letrd 11302	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ≤ (𝑁 / 3))
307	7	a1i 11	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 2 ∈ ℝ)
308	6, 307, 21	lesubaddd 11746	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((π‘𝑁) − 2) ≤ (𝑁 / 3) ↔ (π‘𝑁) ≤ ((𝑁 / 3) + 2)))
309	306, 308	mpbid 232	. . 3 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
310	309	adantlr 716	. 2 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 3 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
311	5	ad2antrr 727	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ∈ ℝ)
312	7	a1i 11	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → 2 ∈ ℝ)
313	20	ad2antrr 727	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (𝑁 / 3) ∈ ℝ)
314		readdcl 11121	. . . 4 ⊢ (((𝑁 / 3) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑁 / 3) + 2) ∈ ℝ)
315	313, 7, 314	sylancl 587	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → ((𝑁 / 3) + 2) ∈ ℝ)
316		ppiwordi 27140	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
317	1, 316	mp3an2 1452	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
318	317	adantlr 716	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
319	318, 24	breqtrdi 5141	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ 2)
320		3pos 12262	. . . . . 6 ⊢ 0 < 3
321		divge0 12023	. . . . . 6 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ (3 ∈ ℝ ∧ 0 < 3)) → 0 ≤ (𝑁 / 3))
322	1, 320, 321	mpanr12 706	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → 0 ≤ (𝑁 / 3))
323	322	adantr 480	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → 0 ≤ (𝑁 / 3))
324		addge02 11660	. . . . 5 ⊢ ((2 ∈ ℝ ∧ (𝑁 / 3) ∈ ℝ) → (0 ≤ (𝑁 / 3) ↔ 2 ≤ ((𝑁 / 3) + 2)))
325	7, 313, 324	sylancr 588	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (0 ≤ (𝑁 / 3) ↔ 2 ≤ ((𝑁 / 3) + 2)))
326	323, 325	mpbid 232	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → 2 ≤ ((𝑁 / 3) + 2))
327	311, 312, 315, 319, 326	letrd 11302	. 2 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
328	2, 3, 310, 327	lecasei 11251	1 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 {crab 3401 ∪ cun 3901 ∩ cin 3902 ⊆ wss 3903 ∅c0 4287 {cpr 4584 class class class wbr 5100 ‘cfv 6500 (class class class)co 7368 ≼ cdom 8893 Fincfn 8895 ℂcc 11036 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 < clt 11178 ≤ cle 11179 − cmin 11376 -cneg 11377 / cdiv 11806 ℕcn 12157 2c2 12212 3c3 12213 4c4 12214 5c5 12215 6c6 12216 ℕ₀cn0 12413 ℤcz 12500 ℤ_≥cuz 12763 ℝ⁺crp 12917 ...cfz 13435 ⌊cfl 13722 mod cmo 13801 ♯chash 14265 ∥ cdvds 16191 ℙcprime 16610 πcppi 27072

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-2o 8408 df-oadd 8411 df-er 8645 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9357 df-inf 9358 df-dju 9825 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-4 12222 df-5 12223 df-6 12224 df-n0 12414 df-xnn0 12487 df-z 12501 df-uz 12764 df-rp 12918 df-icc 13280 df-fz 13436 df-fl 13724 df-mod 13802 df-seq 13937 df-exp 13997 df-hash 14266 df-cj 15034 df-re 15035 df-im 15036 df-sqrt 15170 df-abs 15171 df-dvds 16192 df-prm 16611 df-ppi 27078

This theorem is referenced by: bposlem5 27267

W3C validator