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 25782

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 11720	. . 3 ⊢ 3 ∈ ℝ
2	1	a1i 11	. 2 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → 3 ∈ ℝ)
3		simpl 485	. 2 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → 𝑁 ∈ ℝ)
4		ppicl 25710	. . . . . . . 8 ⊢ (𝑁 ∈ ℝ → (π‘𝑁) ∈ ℕ₀)
5	4	nn0red 11959	. . . . . . 7 ⊢ (𝑁 ∈ ℝ → (π‘𝑁) ∈ ℝ)
6	5	adantr 483	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘𝑁) ∈ ℝ)
7		2re 11714	. . . . . 6 ⊢ 2 ∈ ℝ
8		resubcl 10952	. . . . . 6 ⊢ (((π‘𝑁) ∈ ℝ ∧ 2 ∈ ℝ) → ((π‘𝑁) − 2) ∈ ℝ)
9	6, 7, 8	sylancl 588	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ∈ ℝ)
10		fzfi 13343	. . . . . . . . 9 ⊢ (4...(⌊‘𝑁)) ∈ Fin
11		ssrab2 4058	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ⊆ (4...(⌊‘𝑁))
12		ssfi 8740	. . . . . . . . 9 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ⊆ (4...(⌊‘𝑁))) → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ∈ Fin)
13	10, 11, 12	mp2an 690	. . . . . . . 8 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ∈ Fin
14		hashcl 13720	. . . . . . . 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 11911	. . . . . 6 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℝ
17	16	a1i 11	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℝ)
18		3nn 11719	. . . . . . 7 ⊢ 3 ∈ ℕ
19		nndivre 11681	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℕ) → (𝑁 / 3) ∈ ℝ)
20	18, 19	mpan2 689	. . . . . 6 ⊢ (𝑁 ∈ ℝ → (𝑁 / 3) ∈ ℝ)
21	20	adantr 483	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 / 3) ∈ ℝ)
22		ppifl 25739	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ → (π‘(⌊‘𝑁)) = (π‘𝑁))
23	22	adantr 483	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘(⌊‘𝑁)) = (π‘𝑁))
24		ppi3 25750	. . . . . . . . 9 ⊢ (π‘3) = 2
25	24	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘3) = 2)
26	23, 25	oveq12d 7176	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = ((π‘𝑁) − 2))
27		3z 12018	. . . . . . . . . . 11 ⊢ 3 ∈ ℤ
28	27	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 3 ∈ ℤ)
29		flcl 13168	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (⌊‘𝑁) ∈ ℤ)
30	29	adantr 483	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ ℤ)
31		flge 13178	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℤ) → (3 ≤ 𝑁 ↔ 3 ≤ (⌊‘𝑁)))
32	27, 31	mpan2 689	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (3 ≤ 𝑁 ↔ 3 ≤ (⌊‘𝑁)))
33	32	biimpa 479	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 3 ≤ (⌊‘𝑁))
34		eluz2 12252	. . . . . . . . . 10 ⊢ ((⌊‘𝑁) ∈ (ℤ_≥‘3) ↔ (3 ∈ ℤ ∧ (⌊‘𝑁) ∈ ℤ ∧ 3 ≤ (⌊‘𝑁)))
35	28, 30, 33, 34	syl3anbrc 1339	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ (ℤ_≥‘3))
36		ppidif 25742	. . . . . . . . 9 ⊢ ((⌊‘𝑁) ∈ (ℤ_≥‘3) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ)))
37	35, 36	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ)))
38		df-4 11705	. . . . . . . . . . 11 ⊢ 4 = (3 + 1)
39	38	oveq1i 7168	. . . . . . . . . 10 ⊢ (4...(⌊‘𝑁)) = ((3 + 1)...(⌊‘𝑁))
40	39	ineq1i 4187	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) = (((3 + 1)...(⌊‘𝑁)) ∩ ℙ)
41	40	fveq2i 6675	. . . . . . . 8 ⊢ (♯‘((4...(⌊‘𝑁)) ∩ ℙ)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ))
42	37, 41	syl6eqr 2876	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘((4...(⌊‘𝑁)) ∩ ℙ)))
43	26, 42	eqtr3d 2860	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) = (♯‘((4...(⌊‘𝑁)) ∩ ℙ)))
44		dfin5 3946	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 𝑘 ∈ ℙ}
45		elfzle1 12913	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 4 ≤ 𝑘)
46		ppiublem2 25781	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℙ ∧ 4 ≤ 𝑘) → (𝑘 mod 6) ∈ {1, 5})
47	46	expcom 416	. . . . . . . . . . 11 ⊢ (4 ≤ 𝑘 → (𝑘 ∈ ℙ → (𝑘 mod 6) ∈ {1, 5}))
48	45, 47	syl 17	. . . . . . . . . 10 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → (𝑘 ∈ ℙ → (𝑘 mod 6) ∈ {1, 5}))
49	48	ss2rabi 4055	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 𝑘 ∈ ℙ} ⊆ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}
50	44, 49	eqsstri 4003	. . . . . . . 8 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}
51		ssdomg 8557	. . . . . . . 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 4207	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ (4...(⌊‘𝑁))
54		ssfi 8740	. . . . . . . . 9 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ (4...(⌊‘𝑁))) → ((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin)
55	10, 53, 54	mp2an 690	. . . . . . . 8 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin
56		hashdom 13743	. . . . . . . 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 690	. . . . . . 7 ⊢ ((♯‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ↔ ((4...(⌊‘𝑁)) ∩ ℙ) ≼ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}})
58	52, 57	mpbir 233	. . . . . 6 ⊢ (♯‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}})
59	43, 58	eqbrtrdi 5107	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ≤ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}))
60		reflcl 13169	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (⌊‘𝑁) ∈ ℝ)
61	60	adantr 483	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ ℝ)
62		peano2rem 10955	. . . . . . . . . 10 ⊢ ((⌊‘𝑁) ∈ ℝ → ((⌊‘𝑁) − 1) ∈ ℝ)
63	61, 62	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ∈ ℝ)
64		6nn 11729	. . . . . . . . 9 ⊢ 6 ∈ ℕ
65		nndivre 11681	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 1) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 1) / 6) ∈ ℝ)
66	63, 64, 65	sylancl 588	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) / 6) ∈ ℝ)
67		reflcl 13169	. . . . . . . 8 ⊢ ((((⌊‘𝑁) − 1) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℝ)
68	66, 67	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℝ)
69		5re 11727	. . . . . . . . . . 11 ⊢ 5 ∈ ℝ
70		resubcl 10952	. . . . . . . . . . 11 ⊢ (((⌊‘𝑁) ∈ ℝ ∧ 5 ∈ ℝ) → ((⌊‘𝑁) − 5) ∈ ℝ)
71	61, 69, 70	sylancl 588	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ∈ ℝ)
72		nndivre 11681	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 5) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 5) / 6) ∈ ℝ)
73	71, 64, 72	sylancl 588	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) / 6) ∈ ℝ)
74		reflcl 13169	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 5) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ)
75	73, 74	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ)
76		peano2re 10815	. . . . . . . 8 ⊢ ((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈ ℝ)
77	75, 76	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈ ℝ)
78		peano2rem 10955	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
79	78	adantr 483	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℝ)
80		nndivre 11681	. . . . . . . 8 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝑁 − 1) / 6) ∈ ℝ)
81	79, 64, 80	sylancl 588	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 1) / 6) ∈ ℝ)
82		simpl 485	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℝ)
83		resubcl 10952	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 5 ∈ ℝ) → (𝑁 − 5) ∈ ℝ)
84	82, 69, 83	sylancl 588	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 5) ∈ ℝ)
85		nndivre 11681	. . . . . . . . 9 ⊢ (((𝑁 − 5) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝑁 − 5) / 6) ∈ ℝ)
86	84, 64, 85	sylancl 588	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 5) / 6) ∈ ℝ)
87		peano2re 10815	. . . . . . . 8 ⊢ (((𝑁 − 5) / 6) ∈ ℝ → (((𝑁 − 5) / 6) + 1) ∈ ℝ)
88	86, 87	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 − 5) / 6) + 1) ∈ ℝ)
89		flle 13172	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 1) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ (((⌊‘𝑁) − 1) / 6))
90	66, 89	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ (((⌊‘𝑁) − 1) / 6))
91		1re 10643	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
92	91	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 1 ∈ ℝ)
93		flle 13172	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (⌊‘𝑁) ≤ 𝑁)
94	93	adantr 483	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ≤ 𝑁)
95	61, 82, 92, 94	lesub1dd 11258	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ≤ (𝑁 − 1))
96		6re 11730	. . . . . . . . . . 11 ⊢ 6 ∈ ℝ
97	96	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 6 ∈ ℝ)
98		6pos 11750	. . . . . . . . . . 11 ⊢ 0 < 6
99	98	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 0 < 6)
100		lediv1 11507	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 1) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6)) → (((⌊‘𝑁) − 1) ≤ (𝑁 − 1) ↔ (((⌊‘𝑁) − 1) / 6) ≤ ((𝑁 − 1) / 6)))
101	63, 79, 97, 99, 100	syl112anc 1370	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) ≤ (𝑁 − 1) ↔ (((⌊‘𝑁) − 1) / 6) ≤ ((𝑁 − 1) / 6)))
102	95, 101	mpbid 234	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) / 6) ≤ ((𝑁 − 1) / 6))
103	68, 66, 81, 90, 102	letrd 10799	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ ((𝑁 − 1) / 6))
104		flle 13172	. . . . . . . . . 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 11258	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ≤ (𝑁 − 5))
108		lediv1 11507	. . . . . . . . . . 11 ⊢ ((((⌊‘𝑁) − 5) ∈ ℝ ∧ (𝑁 − 5) ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6)) → (((⌊‘𝑁) − 5) ≤ (𝑁 − 5) ↔ (((⌊‘𝑁) − 5) / 6) ≤ ((𝑁 − 5) / 6)))
109	71, 84, 97, 99, 108	syl112anc 1370	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) ≤ (𝑁 − 5) ↔ (((⌊‘𝑁) − 5) / 6) ≤ ((𝑁 − 5) / 6)))
110	107, 109	mpbid 234	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) / 6) ≤ ((𝑁 − 5) / 6))
111	75, 73, 86, 105, 110	letrd 10799	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ≤ ((𝑁 − 5) / 6))
112	75, 86, 92, 111	leadd1dd 11256	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ≤ (((𝑁 − 5) / 6) + 1))
113	68, 77, 81, 88, 103, 112	le2addd 11261	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) ≤ (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
114		ovex 7191	. . . . . . . . . . . 12 ⊢ (𝑘 mod 6) ∈ V
115	114	elpr 4592	. . . . . . . . . . 11 ⊢ ((𝑘 mod 6) ∈ {1, 5} ↔ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5))
116	115	rabbii 3475	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)}
117		unrab 4276	. . . . . . . . . 10 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)}
118	116, 117	eqtr4i 2849	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} = ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})
119	118	fveq2i 6675	. . . . . . . 8 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = (♯‘({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}))
120		ssrab2 4058	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ⊆ (4...(⌊‘𝑁))
121		ssfi 8740	. . . . . . . . . 10 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ⊆ (4...(⌊‘𝑁))) → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∈ Fin)
122	10, 120, 121	mp2an 690	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∈ Fin
123		ssrab2 4058	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ⊆ (4...(⌊‘𝑁))
124		ssfi 8740	. . . . . . . . . 10 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ⊆ (4...(⌊‘𝑁))) → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ∈ Fin)
125	10, 123, 124	mp2an 690	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ∈ Fin
126		inrab 4277	. . . . . . . . . 10 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∩ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)}
127		rabeq0 4340	. . . . . . . . . . 11 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)} = ∅ ↔ ∀𝑘 ∈ (4...(⌊‘𝑁)) ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5))
128		1lt5 11820	. . . . . . . . . . . . . 14 ⊢ 1 < 5
129	91, 128	ltneii 10755	. . . . . . . . . . . . 13 ⊢ 1 ≠ 5
130		eqtr2 2844	. . . . . . . . . . . . . 14 ⊢ (((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5) → 1 = 5)
131	130	necon3ai 3043	. . . . . . . . . . . . 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 3155	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)} = ∅
135	126, 134	eqtri 2846	. . . . . . . . 9 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∩ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ∅
136		hashun 13746	. . . . . . . . 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 1457	. . . . . . . 8 ⊢ (♯‘({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})) = ((♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}))
138	119, 137	eqtri 2846	. . . . . . 7 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = ((♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}))
139		elfzelz 12911	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 𝑘 ∈ ℤ)
140		nnrp 12403	. . . . . . . . . . . . . . . . 17 ⊢ (6 ∈ ℕ → 6 ∈ ℝ⁺)
141	64, 140	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ ℝ⁺
142		0le1 11165	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 1
143		1lt6 11825	. . . . . . . . . . . . . . . 16 ⊢ 1 < 6
144		modid 13267	. . . . . . . . . . . . . . . 16 ⊢ (((1 ∈ ℝ ∧ 6 ∈ ℝ⁺) ∧ (0 ≤ 1 ∧ 1 < 6)) → (1 mod 6) = 1)
145	91, 141, 142, 143, 144	mp4an 691	. . . . . . . . . . . . . . 15 ⊢ (1 mod 6) = 1
146	145	eqeq2i 2836	. . . . . . . . . . . . . 14 ⊢ ((𝑘 mod 6) = (1 mod 6) ↔ (𝑘 mod 6) = 1)
147		1z 12015	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
148		moddvds 15620	. . . . . . . . . . . . . . 15 ⊢ ((6 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑘 mod 6) = (1 mod 6) ↔ 6 ∥ (𝑘 − 1)))
149	64, 147, 148	mp3an13 1448	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = (1 mod 6) ↔ 6 ∥ (𝑘 − 1)))
150	146, 149	syl5bbr 287	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = 1 ↔ 6 ∥ (𝑘 − 1)))
151	139, 150	syl 17	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → ((𝑘 mod 6) = 1 ↔ 6 ∥ (𝑘 − 1)))
152	151	rabbiia 3474	. . . . . . . . . . 11 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)}
153	152	fveq2i 6675	. . . . . . . . . 10 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)})
154	64	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 6 ∈ ℕ)
155		4z 12019	. . . . . . . . . . . 12 ⊢ 4 ∈ ℤ
156	155	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 4 ∈ ℤ)
157		4m1e3 11769	. . . . . . . . . . . . 13 ⊢ (4 − 1) = 3
158	157	fveq2i 6675	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘(4 − 1)) = (ℤ_≥‘3)
159	35, 158	eleqtrrdi 2926	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ (ℤ_≥‘(4 − 1)))
160	147	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 1 ∈ ℤ)
161	154, 156, 159, 160	hashdvds 16114	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))))
162	153, 161	syl5eq 2870	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))))
163		2cn 11715	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
164		ax-1cn 10597	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
165		df-3 11704	. . . . . . . . . . . . . . . 16 ⊢ 3 = (2 + 1)
166	157, 165	eqtri 2846	. . . . . . . . . . . . . . 15 ⊢ (4 − 1) = (2 + 1)
167	163, 164, 166	mvrraddi 10905	. . . . . . . . . . . . . 14 ⊢ ((4 − 1) − 1) = 2
168	167	oveq1i 7168	. . . . . . . . . . . . 13 ⊢ (((4 − 1) − 1) / 6) = (2 / 6)
169	168	fveq2i 6675	. . . . . . . . . . . 12 ⊢ (⌊‘(((4 − 1) − 1) / 6)) = (⌊‘(2 / 6))
170		0re 10645	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
171	64	nnne0i 11680	. . . . . . . . . . . . . . 15 ⊢ 6 ≠ 0
172	7, 96, 171	redivcli 11409	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ∈ ℝ
173		2pos 11743	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
174	7, 96, 173, 98	divgt0ii 11559	. . . . . . . . . . . . . 14 ⊢ 0 < (2 / 6)
175	170, 172, 174	ltleii 10765	. . . . . . . . . . . . 13 ⊢ 0 ≤ (2 / 6)
176		2lt6 11824	. . . . . . . . . . . . . . . 16 ⊢ 2 < 6
177		6cn 11731	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℂ
178	177	mulid1i 10647	. . . . . . . . . . . . . . . 16 ⊢ (6 · 1) = 6
179	176, 178	breqtrri 5095	. . . . . . . . . . . . . . 15 ⊢ 2 < (6 · 1)
180	96, 98	pm3.2i 473	. . . . . . . . . . . . . . . 16 ⊢ (6 ∈ ℝ ∧ 0 < 6)
181		ltdivmul 11517	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ ∧ 1 ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6)) → ((2 / 6) < 1 ↔ 2 < (6 · 1)))
182	7, 91, 180, 181	mp3an 1457	. . . . . . . . . . . . . . 15 ⊢ ((2 / 6) < 1 ↔ 2 < (6 · 1))
183	179, 182	mpbir 233	. . . . . . . . . . . . . 14 ⊢ (2 / 6) < 1
184		1e0p1 12143	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
185	183, 184	breqtri 5093	. . . . . . . . . . . . 13 ⊢ (2 / 6) < (0 + 1)
186		0z 11995	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℤ
187		flbi 13189	. . . . . . . . . . . . . 14 ⊢ (((2 / 6) ∈ ℝ ∧ 0 ∈ ℤ) → ((⌊‘(2 / 6)) = 0 ↔ (0 ≤ (2 / 6) ∧ (2 / 6) < (0 + 1))))
188	172, 186, 187	mp2an 690	. . . . . . . . . . . . 13 ⊢ ((⌊‘(2 / 6)) = 0 ↔ (0 ≤ (2 / 6) ∧ (2 / 6) < (0 + 1)))
189	175, 185, 188	mpbir2an 709	. . . . . . . . . . . 12 ⊢ (⌊‘(2 / 6)) = 0
190	169, 189	eqtri 2846	. . . . . . . . . . 11 ⊢ (⌊‘(((4 − 1) − 1) / 6)) = 0
191	190	oveq2i 7169	. . . . . . . . . 10 ⊢ ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − 0)
192	66	flcld 13171	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℤ)
193	192	zcnd 12091	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℂ)
194	193	subid1d 10988	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) − 0) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
195	191, 194	syl5eq 2870	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
196	162, 195	eqtrd 2858	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
197		5pos 11749	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 5
198	170, 69, 197	ltleii 10765	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 5
199		5lt6 11821	. . . . . . . . . . . . . . . 16 ⊢ 5 < 6
200		modid 13267	. . . . . . . . . . . . . . . 16 ⊢ (((5 ∈ ℝ ∧ 6 ∈ ℝ⁺) ∧ (0 ≤ 5 ∧ 5 < 6)) → (5 mod 6) = 5)
201	69, 141, 198, 199, 200	mp4an 691	. . . . . . . . . . . . . . 15 ⊢ (5 mod 6) = 5
202	201	eqeq2i 2836	. . . . . . . . . . . . . 14 ⊢ ((𝑘 mod 6) = (5 mod 6) ↔ (𝑘 mod 6) = 5)
203		5nn 11726	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ ℕ
204	203	nnzi 12009	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℤ
205		moddvds 15620	. . . . . . . . . . . . . . 15 ⊢ ((6 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 5 ∈ ℤ) → ((𝑘 mod 6) = (5 mod 6) ↔ 6 ∥ (𝑘 − 5)))
206	64, 204, 205	mp3an13 1448	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = (5 mod 6) ↔ 6 ∥ (𝑘 − 5)))
207	202, 206	syl5bbr 287	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = 5 ↔ 6 ∥ (𝑘 − 5)))
208	139, 207	syl 17	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → ((𝑘 mod 6) = 5 ↔ 6 ∥ (𝑘 − 5)))
209	208	rabbiia 3474	. . . . . . . . . . 11 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)}
210	209	fveq2i 6675	. . . . . . . . . 10 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)})
211	204	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 5 ∈ ℤ)
212	154, 156, 159, 211	hashdvds 16114	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))))
213	210, 212	syl5eq 2870	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))))
214	157	oveq1i 7168	. . . . . . . . . . . . . . . 16 ⊢ ((4 − 1) − 5) = (3 − 5)
215		5cn 11728	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℂ
216		3cn 11721	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℂ
217	215, 216	negsubdi2i 10974	. . . . . . . . . . . . . . . 16 ⊢ -(5 − 3) = (3 − 5)
218		3p2e5 11791	. . . . . . . . . . . . . . . . . . 19 ⊢ (3 + 2) = 5
219	218	oveq1i 7168	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 + 2) − 3) = (5 − 3)
220		pncan2 10895	. . . . . . . . . . . . . . . . . . 19 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
221	216, 163, 220	mp2an 690	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 + 2) − 3) = 2
222	219, 221	eqtr3i 2848	. . . . . . . . . . . . . . . . 17 ⊢ (5 − 3) = 2
223	222	negeqi 10881	. . . . . . . . . . . . . . . 16 ⊢ -(5 − 3) = -2
224	214, 217, 223	3eqtr2i 2852	. . . . . . . . . . . . . . 15 ⊢ ((4 − 1) − 5) = -2
225	224	oveq1i 7168	. . . . . . . . . . . . . 14 ⊢ (((4 − 1) − 5) / 6) = (-2 / 6)
226		divneg 11334	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 6 ∈ ℂ ∧ 6 ≠ 0) → -(2 / 6) = (-2 / 6))
227	163, 177, 171, 226	mp3an 1457	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) = (-2 / 6)
228	225, 227	eqtr4i 2849	. . . . . . . . . . . . 13 ⊢ (((4 − 1) − 5) / 6) = -(2 / 6)
229	228	fveq2i 6675	. . . . . . . . . . . 12 ⊢ (⌊‘(((4 − 1) − 5) / 6)) = (⌊‘-(2 / 6))
230	172, 91, 183	ltleii 10765	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ≤ 1
231	172, 91	lenegi 11187	. . . . . . . . . . . . . 14 ⊢ ((2 / 6) ≤ 1 ↔ -1 ≤ -(2 / 6))
232	230, 231	mpbi 232	. . . . . . . . . . . . 13 ⊢ -1 ≤ -(2 / 6)
233	170, 172	ltnegi 11186	. . . . . . . . . . . . . . 15 ⊢ (0 < (2 / 6) ↔ -(2 / 6) < -0)
234	174, 233	mpbi 232	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) < -0
235		neg0 10934	. . . . . . . . . . . . . . . 16 ⊢ -0 = 0
236		1pneg1e0 11759	. . . . . . . . . . . . . . . 16 ⊢ (1 + -1) = 0
237	235, 236	eqtr4i 2849	. . . . . . . . . . . . . . 15 ⊢ -0 = (1 + -1)
238		neg1cn 11754	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℂ
239	238, 164	addcomi 10833	. . . . . . . . . . . . . . 15 ⊢ (-1 + 1) = (1 + -1)
240	237, 239	eqtr4i 2849	. . . . . . . . . . . . . 14 ⊢ -0 = (-1 + 1)
241	234, 240	breqtri 5093	. . . . . . . . . . . . 13 ⊢ -(2 / 6) < (-1 + 1)
242	172	renegcli 10949	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) ∈ ℝ
243		neg1z 12021	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℤ
244		flbi 13189	. . . . . . . . . . . . . 14 ⊢ ((-(2 / 6) ∈ ℝ ∧ -1 ∈ ℤ) → ((⌊‘-(2 / 6)) = -1 ↔ (-1 ≤ -(2 / 6) ∧ -(2 / 6) < (-1 + 1))))
245	242, 243, 244	mp2an 690	. . . . . . . . . . . . 13 ⊢ ((⌊‘-(2 / 6)) = -1 ↔ (-1 ≤ -(2 / 6) ∧ -(2 / 6) < (-1 + 1)))
246	232, 241, 245	mpbir2an 709	. . . . . . . . . . . 12 ⊢ (⌊‘-(2 / 6)) = -1
247	229, 246	eqtri 2846	. . . . . . . . . . 11 ⊢ (⌊‘(((4 − 1) − 5) / 6)) = -1
248	247	oveq2i 7169	. . . . . . . . . 10 ⊢ ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1)
249	73	flcld 13171	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℤ)
250	249	zcnd 12091	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℂ)
251		subneg 10937	. . . . . . . . . . 11 ⊢ (((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℂ ∧ 1 ∈ ℂ) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
252	250, 164, 251	sylancl 588	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
253	248, 252	syl5eq 2870	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
254	213, 253	eqtrd 2858	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
255	196, 254	oveq12d 7176	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)))
256	138, 255	syl5eq 2870	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)))
257	82	recnd 10671	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℂ)
258	257	2timesd 11883	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (2 · 𝑁) = (𝑁 + 𝑁))
259		df-6 11707	. . . . . . . . . . . . . 14 ⊢ 6 = (5 + 1)
260	215, 164	addcomi 10833	. . . . . . . . . . . . . 14 ⊢ (5 + 1) = (1 + 5)
261	259, 260	eqtri 2846	. . . . . . . . . . . . 13 ⊢ 6 = (1 + 5)
262	261	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 6 = (1 + 5))
263	258, 262	oveq12d 7176	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) − 6) = ((𝑁 + 𝑁) − (1 + 5)))
264		addsub4 10931	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ (1 ∈ ℂ ∧ 5 ∈ ℂ)) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
265	164, 215, 264	mpanr12 703	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
266	257, 257, 265	syl2anc 586	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
267	263, 266	eqtrd 2858	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) − 6) = ((𝑁 − 1) + (𝑁 − 5)))
268	267	oveq1d 7173	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = (((𝑁 − 1) + (𝑁 − 5)) / 6))
269		mulcl 10623	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) ∈ ℂ)
270	163, 257, 269	sylancr 589	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (2 · 𝑁) ∈ ℂ)
271	177, 171	pm3.2i 473	. . . . . . . . . . . 12 ⊢ (6 ∈ ℂ ∧ 6 ≠ 0)
272		divsubdir 11336	. . . . . . . . . . . 12 ⊢ (((2 · 𝑁) ∈ ℂ ∧ 6 ∈ ℂ ∧ (6 ∈ ℂ ∧ 6 ≠ 0)) → (((2 · 𝑁) − 6) / 6) = (((2 · 𝑁) / 6) − (6 / 6)))
273	177, 271, 272	mp3an23 1449	. . . . . . . . . . 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 11806	. . . . . . . . . . . . . 14 ⊢ (3 · 2) = 6
276	216, 163	mulcomi 10651	. . . . . . . . . . . . . 14 ⊢ (3 · 2) = (2 · 3)
277	275, 276	eqtr3i 2848	. . . . . . . . . . . . 13 ⊢ 6 = (2 · 3)
278	277	oveq2i 7169	. . . . . . . . . . . 12 ⊢ ((2 · 𝑁) / 6) = ((2 · 𝑁) / (2 · 3))
279		3ne0 11746	. . . . . . . . . . . . . . 15 ⊢ 3 ≠ 0
280	216, 279	pm3.2i 473	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℂ ∧ 3 ≠ 0)
281		2cnne0 11850	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
282		divcan5 11344	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 𝑁) / (2 · 3)) = (𝑁 / 3))
283	280, 281, 282	mp3an23 1449	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℂ → ((2 · 𝑁) / (2 · 3)) = (𝑁 / 3))
284	257, 283	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) / (2 · 3)) = (𝑁 / 3))
285	278, 284	syl5eq 2870	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) / 6) = (𝑁 / 3))
286	177, 171	dividi 11375	. . . . . . . . . . . 12 ⊢ (6 / 6) = 1
287	286	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (6 / 6) = 1)
288	285, 287	oveq12d 7176	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) / 6) − (6 / 6)) = ((𝑁 / 3) − 1))
289	274, 288	eqtrd 2858	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = ((𝑁 / 3) − 1))
290	79	recnd 10671	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℂ)
291	84	recnd 10671	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 5) ∈ ℂ)
292		divdir 11325	. . . . . . . . . . 11 ⊢ (((𝑁 − 1) ∈ ℂ ∧ (𝑁 − 5) ∈ ℂ ∧ (6 ∈ ℂ ∧ 6 ≠ 0)) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
293	271, 292	mp3an3 1446	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℂ ∧ (𝑁 − 5) ∈ ℂ) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
294	290, 291, 293	syl2anc 586	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
295	268, 289, 294	3eqtr3d 2866	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 / 3) − 1) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
296	295	oveq1d 7173	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 / 3) − 1) + 1) = ((((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)) + 1))
297	21	recnd 10671	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 / 3) ∈ ℂ)
298		npcan 10897	. . . . . . . 8 ⊢ (((𝑁 / 3) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3))
299	297, 164, 298	sylancl 588	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3))
300	81	recnd 10671	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 1) / 6) ∈ ℂ)
301	86	recnd 10671	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 5) / 6) ∈ ℂ)
302	164	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 1 ∈ ℂ)
303	300, 301, 302	addassd 10665	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)) + 1) = (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
304	296, 299, 303	3eqtr3d 2866	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 / 3) = (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
305	113, 256, 304	3brtr4d 5100	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ≤ (𝑁 / 3))
306	9, 17, 21, 59, 305	letrd 10799	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ≤ (𝑁 / 3))
307	7	a1i 11	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 2 ∈ ℝ)
308	6, 307, 21	lesubaddd 11239	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((π‘𝑁) − 2) ≤ (𝑁 / 3) ↔ (π‘𝑁) ≤ ((𝑁 / 3) + 2)))
309	306, 308	mpbid 234	. . 3 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
310	309	adantlr 713	. 2 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 3 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
311	5	ad2antrr 724	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ∈ ℝ)
312	7	a1i 11	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → 2 ∈ ℝ)
313	20	ad2antrr 724	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (𝑁 / 3) ∈ ℝ)
314		readdcl 10622	. . . 4 ⊢ (((𝑁 / 3) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑁 / 3) + 2) ∈ ℝ)
315	313, 7, 314	sylancl 588	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → ((𝑁 / 3) + 2) ∈ ℝ)
316		ppiwordi 25741	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
317	1, 316	mp3an2 1445	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
318	317	adantlr 713	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
319	318, 24	breqtrdi 5109	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ 2)
320		3pos 11745	. . . . . 6 ⊢ 0 < 3
321		divge0 11511	. . . . . 6 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ (3 ∈ ℝ ∧ 0 < 3)) → 0 ≤ (𝑁 / 3))
322	1, 320, 321	mpanr12 703	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → 0 ≤ (𝑁 / 3))
323	322	adantr 483	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → 0 ≤ (𝑁 / 3))
324		addge02 11153	. . . . 5 ⊢ ((2 ∈ ℝ ∧ (𝑁 / 3) ∈ ℝ) → (0 ≤ (𝑁 / 3) ↔ 2 ≤ ((𝑁 / 3) + 2)))
325	7, 313, 324	sylancr 589	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (0 ≤ (𝑁 / 3) ↔ 2 ≤ ((𝑁 / 3) + 2)))
326	323, 325	mpbid 234	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → 2 ≤ ((𝑁 / 3) + 2))
327	311, 312, 315, 319, 326	letrd 10799	. 2 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
328	2, 3, 310, 327	lecasei 10748	1 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 = wceq 1537 ∈ wcel 2114 ≠ wne 3018 {crab 3144 ∪ cun 3936 ∩ cin 3937 ⊆ wss 3938 ∅c0 4293 {cpr 4571 class class class wbr 5068 ‘cfv 6357 (class class class)co 7158 ≼ cdom 8509 Fincfn 8511 ℂcc 10537 ℝcr 10538 0cc0 10539 1c1 10540 + caddc 10542 · cmul 10544 < clt 10677 ≤ cle 10678 − cmin 10872 -cneg 10873 / cdiv 11299 ℕcn 11640 2c2 11695 3c3 11696 4c4 11697 5c5 11698 6c6 11699 ℕ₀cn0 11900 ℤcz 11984 ℤ_≥cuz 12246 ℝ⁺crp 12392 ...cfz 12895 ⌊cfl 13163 mod cmo 13240 ♯chash 13693 ∥ cdvds 15609 ℙcprime 16017 πcppi 25673

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616 ax-pre-sup 10617

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-om 7583 df-1st 7691 df-2nd 7692 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-1o 8104 df-2o 8105 df-oadd 8108 df-er 8291 df-en 8512 df-dom 8513 df-sdom 8514 df-fin 8515 df-sup 8908 df-inf 8909 df-dju 9332 df-card 9370 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-div 11300 df-nn 11641 df-2 11703 df-3 11704 df-4 11705 df-5 11706 df-6 11707 df-n0 11901 df-xnn0 11971 df-z 11985 df-uz 12247 df-rp 12393 df-icc 12748 df-fz 12896 df-fl 13165 df-mod 13241 df-seq 13373 df-exp 13433 df-hash 13694 df-cj 14460 df-re 14461 df-im 14462 df-sqrt 14596 df-abs 14597 df-dvds 15610 df-prm 16018 df-ppi 25679

This theorem is referenced by: bposlem5 25866

W3C validator