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 27131

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 12226	. . 3 ⊢ 3 ∈ ℝ
2	1	a1i 11	. 2 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → 3 ∈ ℝ)
3		simpl 482	. 2 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → 𝑁 ∈ ℝ)
4		ppicl 27057	. . . . . . . 8 ⊢ (𝑁 ∈ ℝ → (π‘𝑁) ∈ ℕ₀)
5	4	nn0red 12464	. . . . . . 7 ⊢ (𝑁 ∈ ℝ → (π‘𝑁) ∈ ℝ)
6	5	adantr 480	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘𝑁) ∈ ℝ)
7		2re 12220	. . . . . 6 ⊢ 2 ∈ ℝ
8		resubcl 11446	. . . . . 6 ⊢ (((π‘𝑁) ∈ ℝ ∧ 2 ∈ ℝ) → ((π‘𝑁) − 2) ∈ ℝ)
9	6, 7, 8	sylancl 586	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ∈ ℝ)
10		fzfi 13897	. . . . . . . . 9 ⊢ (4...(⌊‘𝑁)) ∈ Fin
11		ssrab2 4033	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ⊆ (4...(⌊‘𝑁))
12		ssfi 9097	. . . . . . . . 9 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ⊆ (4...(⌊‘𝑁))) → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ∈ Fin)
13	10, 11, 12	mp2an 692	. . . . . . . 8 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ∈ Fin
14		hashcl 14281	. . . . . . . 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 12413	. . . . . 6 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℝ
17	16	a1i 11	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℝ)
18		3nn 12225	. . . . . . 7 ⊢ 3 ∈ ℕ
19		nndivre 12187	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℕ) → (𝑁 / 3) ∈ ℝ)
20	18, 19	mpan2 691	. . . . . 6 ⊢ (𝑁 ∈ ℝ → (𝑁 / 3) ∈ ℝ)
21	20	adantr 480	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 / 3) ∈ ℝ)
22		ppifl 27086	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ → (π‘(⌊‘𝑁)) = (π‘𝑁))
23	22	adantr 480	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘(⌊‘𝑁)) = (π‘𝑁))
24		ppi3 27097	. . . . . . . . 9 ⊢ (π‘3) = 2
25	24	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘3) = 2)
26	23, 25	oveq12d 7371	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = ((π‘𝑁) − 2))
27		3z 12526	. . . . . . . . . . 11 ⊢ 3 ∈ ℤ
28	27	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 3 ∈ ℤ)
29		flcl 13717	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (⌊‘𝑁) ∈ ℤ)
30	29	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ ℤ)
31		flge 13727	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℤ) → (3 ≤ 𝑁 ↔ 3 ≤ (⌊‘𝑁)))
32	27, 31	mpan2 691	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (3 ≤ 𝑁 ↔ 3 ≤ (⌊‘𝑁)))
33	32	biimpa 476	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 3 ≤ (⌊‘𝑁))
34		eluz2 12759	. . . . . . . . . 10 ⊢ ((⌊‘𝑁) ∈ (ℤ_≥‘3) ↔ (3 ∈ ℤ ∧ (⌊‘𝑁) ∈ ℤ ∧ 3 ≤ (⌊‘𝑁)))
35	28, 30, 33, 34	syl3anbrc 1344	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ (ℤ_≥‘3))
36		ppidif 27089	. . . . . . . . 9 ⊢ ((⌊‘𝑁) ∈ (ℤ_≥‘3) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ)))
37	35, 36	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ)))
38		df-4 12211	. . . . . . . . . . 11 ⊢ 4 = (3 + 1)
39	38	oveq1i 7363	. . . . . . . . . 10 ⊢ (4...(⌊‘𝑁)) = ((3 + 1)...(⌊‘𝑁))
40	39	ineq1i 4169	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) = (((3 + 1)...(⌊‘𝑁)) ∩ ℙ)
41	40	fveq2i 6829	. . . . . . . 8 ⊢ (♯‘((4...(⌊‘𝑁)) ∩ ℙ)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ))
42	37, 41	eqtr4di 2782	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘((4...(⌊‘𝑁)) ∩ ℙ)))
43	26, 42	eqtr3d 2766	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) = (♯‘((4...(⌊‘𝑁)) ∩ ℙ)))
44		dfin5 3913	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 𝑘 ∈ ℙ}
45		elfzle1 13448	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 4 ≤ 𝑘)
46		ppiublem2 27130	. . . . . . . . . . . 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 3984	. . . . . . . 8 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}
51		ssdomg 8932	. . . . . . . 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 4190	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ (4...(⌊‘𝑁))
54		ssfi 9097	. . . . . . . . 9 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ (4...(⌊‘𝑁))) → ((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin)
55	10, 53, 54	mp2an 692	. . . . . . . 8 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin
56		hashdom 14304	. . . . . . . 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 692	. . . . . . 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 5134	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ≤ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}))
60		reflcl 13718	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (⌊‘𝑁) ∈ ℝ)
61	60	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ ℝ)
62		peano2rem 11449	. . . . . . . . . 10 ⊢ ((⌊‘𝑁) ∈ ℝ → ((⌊‘𝑁) − 1) ∈ ℝ)
63	61, 62	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ∈ ℝ)
64		6nn 12235	. . . . . . . . 9 ⊢ 6 ∈ ℕ
65		nndivre 12187	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 1) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 1) / 6) ∈ ℝ)
66	63, 64, 65	sylancl 586	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) / 6) ∈ ℝ)
67		reflcl 13718	. . . . . . . 8 ⊢ ((((⌊‘𝑁) − 1) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℝ)
68	66, 67	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℝ)
69		5re 12233	. . . . . . . . . . 11 ⊢ 5 ∈ ℝ
70		resubcl 11446	. . . . . . . . . . 11 ⊢ (((⌊‘𝑁) ∈ ℝ ∧ 5 ∈ ℝ) → ((⌊‘𝑁) − 5) ∈ ℝ)
71	61, 69, 70	sylancl 586	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ∈ ℝ)
72		nndivre 12187	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 5) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 5) / 6) ∈ ℝ)
73	71, 64, 72	sylancl 586	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) / 6) ∈ ℝ)
74		reflcl 13718	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 5) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ)
75	73, 74	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ)
76		peano2re 11307	. . . . . . . 8 ⊢ ((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈ ℝ)
77	75, 76	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈ ℝ)
78		peano2rem 11449	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
79	78	adantr 480	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℝ)
80		nndivre 12187	. . . . . . . 8 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝑁 − 1) / 6) ∈ ℝ)
81	79, 64, 80	sylancl 586	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 1) / 6) ∈ ℝ)
82		simpl 482	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℝ)
83		resubcl 11446	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 5 ∈ ℝ) → (𝑁 − 5) ∈ ℝ)
84	82, 69, 83	sylancl 586	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 5) ∈ ℝ)
85		nndivre 12187	. . . . . . . . 9 ⊢ (((𝑁 − 5) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝑁 − 5) / 6) ∈ ℝ)
86	84, 64, 85	sylancl 586	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 5) / 6) ∈ ℝ)
87		peano2re 11307	. . . . . . . 8 ⊢ (((𝑁 − 5) / 6) ∈ ℝ → (((𝑁 − 5) / 6) + 1) ∈ ℝ)
88	86, 87	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 − 5) / 6) + 1) ∈ ℝ)
89		flle 13721	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 1) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ (((⌊‘𝑁) − 1) / 6))
90	66, 89	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ (((⌊‘𝑁) − 1) / 6))
91		1re 11134	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
92	91	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 1 ∈ ℝ)
93		flle 13721	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (⌊‘𝑁) ≤ 𝑁)
94	93	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ≤ 𝑁)
95	61, 82, 92, 94	lesub1dd 11754	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ≤ (𝑁 − 1))
96		6re 12236	. . . . . . . . . . 11 ⊢ 6 ∈ ℝ
97	96	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 6 ∈ ℝ)
98		6pos 12256	. . . . . . . . . . 11 ⊢ 0 < 6
99	98	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 0 < 6)
100		lediv1 12008	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 1) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6)) → (((⌊‘𝑁) − 1) ≤ (𝑁 − 1) ↔ (((⌊‘𝑁) − 1) / 6) ≤ ((𝑁 − 1) / 6)))
101	63, 79, 97, 99, 100	syl112anc 1376	. . . . . . . . 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 11291	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ ((𝑁 − 1) / 6))
104		flle 13721	. . . . . . . . . 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 11754	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ≤ (𝑁 − 5))
108		lediv1 12008	. . . . . . . . . . 11 ⊢ ((((⌊‘𝑁) − 5) ∈ ℝ ∧ (𝑁 − 5) ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6)) → (((⌊‘𝑁) − 5) ≤ (𝑁 − 5) ↔ (((⌊‘𝑁) − 5) / 6) ≤ ((𝑁 − 5) / 6)))
109	71, 84, 97, 99, 108	syl112anc 1376	. . . . . . . . . 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 11291	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ≤ ((𝑁 − 5) / 6))
112	75, 86, 92, 111	leadd1dd 11752	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ≤ (((𝑁 − 5) / 6) + 1))
113	68, 77, 81, 88, 103, 112	le2addd 11757	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) ≤ (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
114		ovex 7386	. . . . . . . . . . . 12 ⊢ (𝑘 mod 6) ∈ V
115	114	elpr 4604	. . . . . . . . . . 11 ⊢ ((𝑘 mod 6) ∈ {1, 5} ↔ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5))
116	115	rabbii 3402	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)}
117		unrab 4268	. . . . . . . . . 10 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)}
118	116, 117	eqtr4i 2755	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} = ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})
119	118	fveq2i 6829	. . . . . . . 8 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = (♯‘({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}))
120		ssrab2 4033	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ⊆ (4...(⌊‘𝑁))
121		ssfi 9097	. . . . . . . . . 10 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ⊆ (4...(⌊‘𝑁))) → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∈ Fin)
122	10, 120, 121	mp2an 692	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∈ Fin
123		ssrab2 4033	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ⊆ (4...(⌊‘𝑁))
124		ssfi 9097	. . . . . . . . . 10 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ⊆ (4...(⌊‘𝑁))) → {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ∈ Fin)
125	10, 123, 124	mp2an 692	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ∈ Fin
126		inrab 4269	. . . . . . . . . 10 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∩ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)}
127		rabeq0 4341	. . . . . . . . . . 11 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)} = ∅ ↔ ∀𝑘 ∈ (4...(⌊‘𝑁)) ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5))
128		1lt5 12321	. . . . . . . . . . . . . 14 ⊢ 1 < 5
129	91, 128	ltneii 11247	. . . . . . . . . . . . 13 ⊢ 1 ≠ 5
130		eqtr2 2750	. . . . . . . . . . . . . 14 ⊢ (((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5) → 1 = 5)
131	130	necon3ai 2950	. . . . . . . . . . . . 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 3051	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)} = ∅
135	126, 134	eqtri 2752	. . . . . . . . 9 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∩ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ∅
136		hashun 14307	. . . . . . . . 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 1463	. . . . . . . 8 ⊢ (♯‘({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})) = ((♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}))
138	119, 137	eqtri 2752	. . . . . . 7 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = ((♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}))
139		elfzelz 13445	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 𝑘 ∈ ℤ)
140		nnrp 12923	. . . . . . . . . . . . . . . . 17 ⊢ (6 ∈ ℕ → 6 ∈ ℝ⁺)
141	64, 140	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ ℝ⁺
142		0le1 11661	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 1
143		1lt6 12326	. . . . . . . . . . . . . . . 16 ⊢ 1 < 6
144		modid 13818	. . . . . . . . . . . . . . . 16 ⊢ (((1 ∈ ℝ ∧ 6 ∈ ℝ⁺) ∧ (0 ≤ 1 ∧ 1 < 6)) → (1 mod 6) = 1)
145	91, 141, 142, 143, 144	mp4an 693	. . . . . . . . . . . . . . 15 ⊢ (1 mod 6) = 1
146	145	eqeq2i 2742	. . . . . . . . . . . . . 14 ⊢ ((𝑘 mod 6) = (1 mod 6) ↔ (𝑘 mod 6) = 1)
147		1z 12523	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
148		moddvds 16192	. . . . . . . . . . . . . . 15 ⊢ ((6 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑘 mod 6) = (1 mod 6) ↔ 6 ∥ (𝑘 − 1)))
149	64, 147, 148	mp3an13 1454	. . . . . . . . . . . . . 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 3400	. . . . . . . . . . 11 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)}
153	152	fveq2i 6829	. . . . . . . . . 10 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)})
154	64	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 6 ∈ ℕ)
155		4z 12527	. . . . . . . . . . . 12 ⊢ 4 ∈ ℤ
156	155	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 4 ∈ ℤ)
157		4m1e3 12270	. . . . . . . . . . . . 13 ⊢ (4 − 1) = 3
158	157	fveq2i 6829	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘(4 − 1)) = (ℤ_≥‘3)
159	35, 158	eleqtrrdi 2839	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ (ℤ_≥‘(4 − 1)))
160	147	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 1 ∈ ℤ)
161	154, 156, 159, 160	hashdvds 16704	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))))
162	153, 161	eqtrid 2776	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))))
163		2cn 12221	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
164		ax-1cn 11086	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
165		df-3 12210	. . . . . . . . . . . . . . . 16 ⊢ 3 = (2 + 1)
166	157, 165	eqtri 2752	. . . . . . . . . . . . . . 15 ⊢ (4 − 1) = (2 + 1)
167	163, 164, 166	mvrraddi 11398	. . . . . . . . . . . . . 14 ⊢ ((4 − 1) − 1) = 2
168	167	oveq1i 7363	. . . . . . . . . . . . 13 ⊢ (((4 − 1) − 1) / 6) = (2 / 6)
169	168	fveq2i 6829	. . . . . . . . . . . 12 ⊢ (⌊‘(((4 − 1) − 1) / 6)) = (⌊‘(2 / 6))
170		0re 11136	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
171	64	nnne0i 12186	. . . . . . . . . . . . . . 15 ⊢ 6 ≠ 0
172	7, 96, 171	redivcli 11909	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ∈ ℝ
173		2pos 12249	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
174	7, 96, 173, 98	divgt0ii 12060	. . . . . . . . . . . . . 14 ⊢ 0 < (2 / 6)
175	170, 172, 174	ltleii 11257	. . . . . . . . . . . . 13 ⊢ 0 ≤ (2 / 6)
176		2lt6 12325	. . . . . . . . . . . . . . . 16 ⊢ 2 < 6
177		6cn 12237	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℂ
178	177	mulridi 11138	. . . . . . . . . . . . . . . 16 ⊢ (6 · 1) = 6
179	176, 178	breqtrri 5122	. . . . . . . . . . . . . . 15 ⊢ 2 < (6 · 1)
180	96, 98	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ (6 ∈ ℝ ∧ 0 < 6)
181		ltdivmul 12018	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ ∧ 1 ∈ ℝ ∧ (6 ∈ ℝ ∧ 0 < 6)) → ((2 / 6) < 1 ↔ 2 < (6 · 1)))
182	7, 91, 180, 181	mp3an 1463	. . . . . . . . . . . . . . 15 ⊢ ((2 / 6) < 1 ↔ 2 < (6 · 1))
183	179, 182	mpbir 231	. . . . . . . . . . . . . 14 ⊢ (2 / 6) < 1
184		1e0p1 12651	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
185	183, 184	breqtri 5120	. . . . . . . . . . . . 13 ⊢ (2 / 6) < (0 + 1)
186		0z 12500	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℤ
187		flbi 13738	. . . . . . . . . . . . . 14 ⊢ (((2 / 6) ∈ ℝ ∧ 0 ∈ ℤ) → ((⌊‘(2 / 6)) = 0 ↔ (0 ≤ (2 / 6) ∧ (2 / 6) < (0 + 1))))
188	172, 186, 187	mp2an 692	. . . . . . . . . . . . 13 ⊢ ((⌊‘(2 / 6)) = 0 ↔ (0 ≤ (2 / 6) ∧ (2 / 6) < (0 + 1)))
189	175, 185, 188	mpbir2an 711	. . . . . . . . . . . 12 ⊢ (⌊‘(2 / 6)) = 0
190	169, 189	eqtri 2752	. . . . . . . . . . 11 ⊢ (⌊‘(((4 − 1) − 1) / 6)) = 0
191	190	oveq2i 7364	. . . . . . . . . 10 ⊢ ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − 0)
192	66	flcld 13720	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℤ)
193	192	zcnd 12599	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℂ)
194	193	subid1d 11482	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) − 0) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
195	191, 194	eqtrid 2776	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
196	162, 195	eqtrd 2764	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
197		5pos 12255	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 5
198	170, 69, 197	ltleii 11257	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 5
199		5lt6 12322	. . . . . . . . . . . . . . . 16 ⊢ 5 < 6
200		modid 13818	. . . . . . . . . . . . . . . 16 ⊢ (((5 ∈ ℝ ∧ 6 ∈ ℝ⁺) ∧ (0 ≤ 5 ∧ 5 < 6)) → (5 mod 6) = 5)
201	69, 141, 198, 199, 200	mp4an 693	. . . . . . . . . . . . . . 15 ⊢ (5 mod 6) = 5
202	201	eqeq2i 2742	. . . . . . . . . . . . . 14 ⊢ ((𝑘 mod 6) = (5 mod 6) ↔ (𝑘 mod 6) = 5)
203		5nn 12232	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ ℕ
204	203	nnzi 12517	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℤ
205		moddvds 16192	. . . . . . . . . . . . . . 15 ⊢ ((6 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 5 ∈ ℤ) → ((𝑘 mod 6) = (5 mod 6) ↔ 6 ∥ (𝑘 − 5)))
206	64, 204, 205	mp3an13 1454	. . . . . . . . . . . . . 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 3400	. . . . . . . . . . 11 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)}
210	209	fveq2i 6829	. . . . . . . . . 10 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)})
211	204	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 5 ∈ ℤ)
212	154, 156, 159, 211	hashdvds 16704	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))))
213	210, 212	eqtrid 2776	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))))
214	157	oveq1i 7363	. . . . . . . . . . . . . . . 16 ⊢ ((4 − 1) − 5) = (3 − 5)
215		5cn 12234	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℂ
216		3cn 12227	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℂ
217	215, 216	negsubdi2i 11468	. . . . . . . . . . . . . . . 16 ⊢ -(5 − 3) = (3 − 5)
218		3p2e5 12292	. . . . . . . . . . . . . . . . . . 19 ⊢ (3 + 2) = 5
219	218	oveq1i 7363	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 + 2) − 3) = (5 − 3)
220		pncan2 11388	. . . . . . . . . . . . . . . . . . 19 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
221	216, 163, 220	mp2an 692	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 + 2) − 3) = 2
222	219, 221	eqtr3i 2754	. . . . . . . . . . . . . . . . 17 ⊢ (5 − 3) = 2
223	222	negeqi 11374	. . . . . . . . . . . . . . . 16 ⊢ -(5 − 3) = -2
224	214, 217, 223	3eqtr2i 2758	. . . . . . . . . . . . . . 15 ⊢ ((4 − 1) − 5) = -2
225	224	oveq1i 7363	. . . . . . . . . . . . . 14 ⊢ (((4 − 1) − 5) / 6) = (-2 / 6)
226		divneg 11834	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 6 ∈ ℂ ∧ 6 ≠ 0) → -(2 / 6) = (-2 / 6))
227	163, 177, 171, 226	mp3an 1463	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) = (-2 / 6)
228	225, 227	eqtr4i 2755	. . . . . . . . . . . . 13 ⊢ (((4 − 1) − 5) / 6) = -(2 / 6)
229	228	fveq2i 6829	. . . . . . . . . . . 12 ⊢ (⌊‘(((4 − 1) − 5) / 6)) = (⌊‘-(2 / 6))
230	172, 91, 183	ltleii 11257	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ≤ 1
231	172, 91	lenegi 11683	. . . . . . . . . . . . . 14 ⊢ ((2 / 6) ≤ 1 ↔ -1 ≤ -(2 / 6))
232	230, 231	mpbi 230	. . . . . . . . . . . . 13 ⊢ -1 ≤ -(2 / 6)
233	170, 172	ltnegi 11682	. . . . . . . . . . . . . . 15 ⊢ (0 < (2 / 6) ↔ -(2 / 6) < -0)
234	174, 233	mpbi 230	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) < -0
235		neg0 11428	. . . . . . . . . . . . . . . 16 ⊢ -0 = 0
236		1pneg1e0 12260	. . . . . . . . . . . . . . . 16 ⊢ (1 + -1) = 0
237	235, 236	eqtr4i 2755	. . . . . . . . . . . . . . 15 ⊢ -0 = (1 + -1)
238		neg1cn 12131	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℂ
239	238, 164	addcomi 11325	. . . . . . . . . . . . . . 15 ⊢ (-1 + 1) = (1 + -1)
240	237, 239	eqtr4i 2755	. . . . . . . . . . . . . 14 ⊢ -0 = (-1 + 1)
241	234, 240	breqtri 5120	. . . . . . . . . . . . 13 ⊢ -(2 / 6) < (-1 + 1)
242	172	renegcli 11443	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) ∈ ℝ
243		neg1z 12529	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℤ
244		flbi 13738	. . . . . . . . . . . . . 14 ⊢ ((-(2 / 6) ∈ ℝ ∧ -1 ∈ ℤ) → ((⌊‘-(2 / 6)) = -1 ↔ (-1 ≤ -(2 / 6) ∧ -(2 / 6) < (-1 + 1))))
245	242, 243, 244	mp2an 692	. . . . . . . . . . . . 13 ⊢ ((⌊‘-(2 / 6)) = -1 ↔ (-1 ≤ -(2 / 6) ∧ -(2 / 6) < (-1 + 1)))
246	232, 241, 245	mpbir2an 711	. . . . . . . . . . . 12 ⊢ (⌊‘-(2 / 6)) = -1
247	229, 246	eqtri 2752	. . . . . . . . . . 11 ⊢ (⌊‘(((4 − 1) − 5) / 6)) = -1
248	247	oveq2i 7364	. . . . . . . . . 10 ⊢ ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1)
249	73	flcld 13720	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℤ)
250	249	zcnd 12599	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℂ)
251		subneg 11431	. . . . . . . . . . 11 ⊢ (((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℂ ∧ 1 ∈ ℂ) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
252	250, 164, 251	sylancl 586	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
253	248, 252	eqtrid 2776	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
254	213, 253	eqtrd 2764	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
255	196, 254	oveq12d 7371	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)))
256	138, 255	eqtrid 2776	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)))
257	82	recnd 11162	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℂ)
258	257	2timesd 12385	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (2 · 𝑁) = (𝑁 + 𝑁))
259		df-6 12213	. . . . . . . . . . . . . 14 ⊢ 6 = (5 + 1)
260	215, 164	addcomi 11325	. . . . . . . . . . . . . 14 ⊢ (5 + 1) = (1 + 5)
261	259, 260	eqtri 2752	. . . . . . . . . . . . 13 ⊢ 6 = (1 + 5)
262	261	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 6 = (1 + 5))
263	258, 262	oveq12d 7371	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) − 6) = ((𝑁 + 𝑁) − (1 + 5)))
264		addsub4 11425	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ (1 ∈ ℂ ∧ 5 ∈ ℂ)) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
265	164, 215, 264	mpanr12 705	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
266	257, 257, 265	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
267	263, 266	eqtrd 2764	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) − 6) = ((𝑁 − 1) + (𝑁 − 5)))
268	267	oveq1d 7368	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = (((𝑁 − 1) + (𝑁 − 5)) / 6))
269		mulcl 11112	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) ∈ ℂ)
270	163, 257, 269	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (2 · 𝑁) ∈ ℂ)
271	177, 171	pm3.2i 470	. . . . . . . . . . . 12 ⊢ (6 ∈ ℂ ∧ 6 ≠ 0)
272		divsubdir 11836	. . . . . . . . . . . 12 ⊢ (((2 · 𝑁) ∈ ℂ ∧ 6 ∈ ℂ ∧ (6 ∈ ℂ ∧ 6 ≠ 0)) → (((2 · 𝑁) − 6) / 6) = (((2 · 𝑁) / 6) − (6 / 6)))
273	177, 271, 272	mp3an23 1455	. . . . . . . . . . 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 12307	. . . . . . . . . . . . . 14 ⊢ (3 · 2) = 6
276	216, 163	mulcomi 11142	. . . . . . . . . . . . . 14 ⊢ (3 · 2) = (2 · 3)
277	275, 276	eqtr3i 2754	. . . . . . . . . . . . 13 ⊢ 6 = (2 · 3)
278	277	oveq2i 7364	. . . . . . . . . . . 12 ⊢ ((2 · 𝑁) / 6) = ((2 · 𝑁) / (2 · 3))
279		3ne0 12252	. . . . . . . . . . . . . . 15 ⊢ 3 ≠ 0
280	216, 279	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℂ ∧ 3 ≠ 0)
281		2cnne0 12351	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
282		divcan5 11844	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 𝑁) / (2 · 3)) = (𝑁 / 3))
283	280, 281, 282	mp3an23 1455	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℂ → ((2 · 𝑁) / (2 · 3)) = (𝑁 / 3))
284	257, 283	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) / (2 · 3)) = (𝑁 / 3))
285	278, 284	eqtrid 2776	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) / 6) = (𝑁 / 3))
286	177, 171	dividi 11875	. . . . . . . . . . . 12 ⊢ (6 / 6) = 1
287	286	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (6 / 6) = 1)
288	285, 287	oveq12d 7371	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) / 6) − (6 / 6)) = ((𝑁 / 3) − 1))
289	274, 288	eqtrd 2764	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = ((𝑁 / 3) − 1))
290	79	recnd 11162	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℂ)
291	84	recnd 11162	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 5) ∈ ℂ)
292		divdir 11822	. . . . . . . . . . 11 ⊢ (((𝑁 − 1) ∈ ℂ ∧ (𝑁 − 5) ∈ ℂ ∧ (6 ∈ ℂ ∧ 6 ≠ 0)) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
293	271, 292	mp3an3 1452	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℂ ∧ (𝑁 − 5) ∈ ℂ) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
294	290, 291, 293	syl2anc 584	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
295	268, 289, 294	3eqtr3d 2772	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 / 3) − 1) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
296	295	oveq1d 7368	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 / 3) − 1) + 1) = ((((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)) + 1))
297	21	recnd 11162	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 / 3) ∈ ℂ)
298		npcan 11390	. . . . . . . 8 ⊢ (((𝑁 / 3) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3))
299	297, 164, 298	sylancl 586	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3))
300	81	recnd 11162	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 1) / 6) ∈ ℂ)
301	86	recnd 11162	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 5) / 6) ∈ ℂ)
302	164	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 1 ∈ ℂ)
303	300, 301, 302	addassd 11156	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)) + 1) = (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
304	296, 299, 303	3eqtr3d 2772	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 / 3) = (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
305	113, 256, 304	3brtr4d 5127	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ≤ (𝑁 / 3))
306	9, 17, 21, 59, 305	letrd 11291	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ≤ (𝑁 / 3))
307	7	a1i 11	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 2 ∈ ℝ)
308	6, 307, 21	lesubaddd 11735	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((π‘𝑁) − 2) ≤ (𝑁 / 3) ↔ (π‘𝑁) ≤ ((𝑁 / 3) + 2)))
309	306, 308	mpbid 232	. . 3 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
310	309	adantlr 715	. 2 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 3 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
311	5	ad2antrr 726	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ∈ ℝ)
312	7	a1i 11	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → 2 ∈ ℝ)
313	20	ad2antrr 726	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (𝑁 / 3) ∈ ℝ)
314		readdcl 11111	. . . 4 ⊢ (((𝑁 / 3) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑁 / 3) + 2) ∈ ℝ)
315	313, 7, 314	sylancl 586	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → ((𝑁 / 3) + 2) ∈ ℝ)
316		ppiwordi 27088	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
317	1, 316	mp3an2 1451	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
318	317	adantlr 715	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
319	318, 24	breqtrdi 5136	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ 2)
320		3pos 12251	. . . . . 6 ⊢ 0 < 3
321		divge0 12012	. . . . . 6 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ (3 ∈ ℝ ∧ 0 < 3)) → 0 ≤ (𝑁 / 3))
322	1, 320, 321	mpanr12 705	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → 0 ≤ (𝑁 / 3))
323	322	adantr 480	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → 0 ≤ (𝑁 / 3))
324		addge02 11649	. . . . 5 ⊢ ((2 ∈ ℝ ∧ (𝑁 / 3) ∈ ℝ) → (0 ≤ (𝑁 / 3) ↔ 2 ≤ ((𝑁 / 3) + 2)))
325	7, 313, 324	sylancr 587	. . . 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 11291	. 2 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
328	2, 3, 310, 327	lecasei 11240	1 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 {crab 3396 ∪ cun 3903 ∩ cin 3904 ⊆ wss 3905 ∅c0 4286 {cpr 4581 class class class wbr 5095 ‘cfv 6486 (class class class)co 7353 ≼ cdom 8877 Fincfn 8879 ℂcc 11026 ℝcr 11027 0cc0 11028 1c1 11029 + caddc 11031 · cmul 11033 < clt 11168 ≤ cle 11169 − cmin 11365 -cneg 11366 / cdiv 11795 ℕcn 12146 2c2 12201 3c3 12202 4c4 12203 5c5 12204 6c6 12205 ℕ₀cn0 12402 ℤcz 12489 ℤ_≥cuz 12753 ℝ⁺crp 12911 ...cfz 13428 ⌊cfl 13712 mod cmo 13791 ♯chash 14255 ∥ cdvds 16181 ℙcprime 16600 πcppi 27020

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-oadd 8399 df-er 8632 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-sup 9351 df-inf 9352 df-dju 9816 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11367 df-neg 11368 df-div 11796 df-nn 12147 df-2 12209 df-3 12210 df-4 12211 df-5 12212 df-6 12213 df-n0 12403 df-xnn0 12476 df-z 12490 df-uz 12754 df-rp 12912 df-icc 13273 df-fz 13429 df-fl 13714 df-mod 13792 df-seq 13927 df-exp 13987 df-hash 14256 df-cj 15024 df-re 15025 df-im 15026 df-sqrt 15160 df-abs 15161 df-dvds 16182 df-prm 16601 df-ppi 27026

This theorem is referenced by: bposlem5 27215

W3C validator