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 26039

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 11875	. . 3 ⊢ 3 ∈ ℝ
2	1	a1i 11	. 2 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → 3 ∈ ℝ)
3		simpl 486	. 2 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → 𝑁 ∈ ℝ)
4		ppicl 25967	. . . . . . . 8 ⊢ (𝑁 ∈ ℝ → (π‘𝑁) ∈ ℕ₀)
5	4	nn0red 12116	. . . . . . 7 ⊢ (𝑁 ∈ ℝ → (π‘𝑁) ∈ ℝ)
6	5	adantr 484	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘𝑁) ∈ ℝ)
7		2re 11869	. . . . . 6 ⊢ 2 ∈ ℝ
8		resubcl 11107	. . . . . 6 ⊢ (((π‘𝑁) ∈ ℝ ∧ 2 ∈ ℝ) → ((π‘𝑁) − 2) ∈ ℝ)
9	6, 7, 8	sylancl 589	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ∈ ℝ)
10		fzfi 13510	. . . . . . . . 9 ⊢ (4...(⌊‘𝑁)) ∈ Fin
11		ssrab2 3979	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} ⊆ (4...(⌊‘𝑁))
12		ssfi 8829	. . . . . . . . 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 13888	. . . . . . . 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 12066	. . . . . 6 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℝ
17	16	a1i 11	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ∈ ℝ)
18		3nn 11874	. . . . . . 7 ⊢ 3 ∈ ℕ
19		nndivre 11836	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℕ) → (𝑁 / 3) ∈ ℝ)
20	18, 19	mpan2 691	. . . . . 6 ⊢ (𝑁 ∈ ℝ → (𝑁 / 3) ∈ ℝ)
21	20	adantr 484	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 / 3) ∈ ℝ)
22		ppifl 25996	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ → (π‘(⌊‘𝑁)) = (π‘𝑁))
23	22	adantr 484	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘(⌊‘𝑁)) = (π‘𝑁))
24		ppi3 26007	. . . . . . . . 9 ⊢ (π‘3) = 2
25	24	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (π‘3) = 2)
26	23, 25	oveq12d 7209	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = ((π‘𝑁) − 2))
27		3z 12175	. . . . . . . . . . 11 ⊢ 3 ∈ ℤ
28	27	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 3 ∈ ℤ)
29		flcl 13335	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (⌊‘𝑁) ∈ ℤ)
30	29	adantr 484	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ ℤ)
31		flge 13345	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℤ) → (3 ≤ 𝑁 ↔ 3 ≤ (⌊‘𝑁)))
32	27, 31	mpan2 691	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (3 ≤ 𝑁 ↔ 3 ≤ (⌊‘𝑁)))
33	32	biimpa 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 3 ≤ (⌊‘𝑁))
34		eluz2 12409	. . . . . . . . . 10 ⊢ ((⌊‘𝑁) ∈ (ℤ_≥‘3) ↔ (3 ∈ ℤ ∧ (⌊‘𝑁) ∈ ℤ ∧ 3 ≤ (⌊‘𝑁)))
35	28, 30, 33, 34	syl3anbrc 1345	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ (ℤ_≥‘3))
36		ppidif 25999	. . . . . . . . 9 ⊢ ((⌊‘𝑁) ∈ (ℤ_≥‘3) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ)))
37	35, 36	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ)))
38		df-4 11860	. . . . . . . . . . 11 ⊢ 4 = (3 + 1)
39	38	oveq1i 7201	. . . . . . . . . 10 ⊢ (4...(⌊‘𝑁)) = ((3 + 1)...(⌊‘𝑁))
40	39	ineq1i 4109	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) = (((3 + 1)...(⌊‘𝑁)) ∩ ℙ)
41	40	fveq2i 6698	. . . . . . . 8 ⊢ (♯‘((4...(⌊‘𝑁)) ∩ ℙ)) = (♯‘(((3 + 1)...(⌊‘𝑁)) ∩ ℙ))
42	37, 41	eqtr4di 2789	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘(⌊‘𝑁)) − (π‘3)) = (♯‘((4...(⌊‘𝑁)) ∩ ℙ)))
43	26, 42	eqtr3d 2773	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) = (♯‘((4...(⌊‘𝑁)) ∩ ℙ)))
44		dfin5 3861	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 𝑘 ∈ ℙ}
45		elfzle1 13080	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 4 ≤ 𝑘)
46		ppiublem2 26038	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℙ ∧ 4 ≤ 𝑘) → (𝑘 mod 6) ∈ {1, 5})
47	46	expcom 417	. . . . . . . . . . 11 ⊢ (4 ≤ 𝑘 → (𝑘 ∈ ℙ → (𝑘 mod 6) ∈ {1, 5}))
48	45, 47	syl 17	. . . . . . . . . 10 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → (𝑘 ∈ ℙ → (𝑘 mod 6) ∈ {1, 5}))
49	48	ss2rabi 3976	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 𝑘 ∈ ℙ} ⊆ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}
50	44, 49	eqsstri 3921	. . . . . . . 8 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}
51		ssdomg 8652	. . . . . . . 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 4129	. . . . . . . . 9 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ (4...(⌊‘𝑁))
54		ssfi 8829	. . . . . . . . 9 ⊢ (((4...(⌊‘𝑁)) ∈ Fin ∧ ((4...(⌊‘𝑁)) ∩ ℙ) ⊆ (4...(⌊‘𝑁))) → ((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin)
55	10, 53, 54	mp2an 692	. . . . . . . 8 ⊢ ((4...(⌊‘𝑁)) ∩ ℙ) ∈ Fin
56		hashdom 13911	. . . . . . . 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 234	. . . . . 6 ⊢ (♯‘((4...(⌊‘𝑁)) ∩ ℙ)) ≤ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}})
59	43, 58	eqbrtrdi 5078	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ≤ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}))
60		reflcl 13336	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (⌊‘𝑁) ∈ ℝ)
61	60	adantr 484	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ ℝ)
62		peano2rem 11110	. . . . . . . . . 10 ⊢ ((⌊‘𝑁) ∈ ℝ → ((⌊‘𝑁) − 1) ∈ ℝ)
63	61, 62	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ∈ ℝ)
64		6nn 11884	. . . . . . . . 9 ⊢ 6 ∈ ℕ
65		nndivre 11836	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 1) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 1) / 6) ∈ ℝ)
66	63, 64, 65	sylancl 589	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) / 6) ∈ ℝ)
67		reflcl 13336	. . . . . . . 8 ⊢ ((((⌊‘𝑁) − 1) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℝ)
68	66, 67	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℝ)
69		5re 11882	. . . . . . . . . . 11 ⊢ 5 ∈ ℝ
70		resubcl 11107	. . . . . . . . . . 11 ⊢ (((⌊‘𝑁) ∈ ℝ ∧ 5 ∈ ℝ) → ((⌊‘𝑁) − 5) ∈ ℝ)
71	61, 69, 70	sylancl 589	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ∈ ℝ)
72		nndivre 11836	. . . . . . . . . 10 ⊢ ((((⌊‘𝑁) − 5) ∈ ℝ ∧ 6 ∈ ℕ) → (((⌊‘𝑁) − 5) / 6) ∈ ℝ)
73	71, 64, 72	sylancl 589	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) / 6) ∈ ℝ)
74		reflcl 13336	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 5) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ)
75	73, 74	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ)
76		peano2re 10970	. . . . . . . 8 ⊢ ((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℝ → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈ ℝ)
77	75, 76	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ∈ ℝ)
78		peano2rem 11110	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
79	78	adantr 484	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℝ)
80		nndivre 11836	. . . . . . . 8 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝑁 − 1) / 6) ∈ ℝ)
81	79, 64, 80	sylancl 589	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 1) / 6) ∈ ℝ)
82		simpl 486	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℝ)
83		resubcl 11107	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 5 ∈ ℝ) → (𝑁 − 5) ∈ ℝ)
84	82, 69, 83	sylancl 589	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 5) ∈ ℝ)
85		nndivre 11836	. . . . . . . . 9 ⊢ (((𝑁 − 5) ∈ ℝ ∧ 6 ∈ ℕ) → ((𝑁 − 5) / 6) ∈ ℝ)
86	84, 64, 85	sylancl 589	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 5) / 6) ∈ ℝ)
87		peano2re 10970	. . . . . . . 8 ⊢ (((𝑁 − 5) / 6) ∈ ℝ → (((𝑁 − 5) / 6) + 1) ∈ ℝ)
88	86, 87	syl 17	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 − 5) / 6) + 1) ∈ ℝ)
89		flle 13339	. . . . . . . . 9 ⊢ ((((⌊‘𝑁) − 1) / 6) ∈ ℝ → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ (((⌊‘𝑁) − 1) / 6))
90	66, 89	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ (((⌊‘𝑁) − 1) / 6))
91		1re 10798	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
92	91	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 1 ∈ ℝ)
93		flle 13339	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (⌊‘𝑁) ≤ 𝑁)
94	93	adantr 484	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ≤ 𝑁)
95	61, 82, 92, 94	lesub1dd 11413	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 1) ≤ (𝑁 − 1))
96		6re 11885	. . . . . . . . . . 11 ⊢ 6 ∈ ℝ
97	96	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 6 ∈ ℝ)
98		6pos 11905	. . . . . . . . . . 11 ⊢ 0 < 6
99	98	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 0 < 6)
100		lediv1 11662	. . . . . . . . . 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 235	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 1) / 6) ≤ ((𝑁 − 1) / 6))
103	68, 66, 81, 90, 102	letrd 10954	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ≤ ((𝑁 − 1) / 6))
104		flle 13339	. . . . . . . . . 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 11413	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘𝑁) − 5) ≤ (𝑁 − 5))
108		lediv1 11662	. . . . . . . . . . 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 235	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((⌊‘𝑁) − 5) / 6) ≤ ((𝑁 − 5) / 6))
111	75, 73, 86, 105, 110	letrd 10954	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ≤ ((𝑁 − 5) / 6))
112	75, 86, 92, 111	leadd1dd 11411	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1) ≤ (((𝑁 − 5) / 6) + 1))
113	68, 77, 81, 88, 103, 112	le2addd 11416	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)) ≤ (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
114		ovex 7224	. . . . . . . . . . . 12 ⊢ (𝑘 mod 6) ∈ V
115	114	elpr 4550	. . . . . . . . . . 11 ⊢ ((𝑘 mod 6) ∈ {1, 5} ↔ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5))
116	115	rabbii 3373	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)}
117		unrab 4206	. . . . . . . . . 10 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∨ (𝑘 mod 6) = 5)}
118	116, 117	eqtr4i 2762	. . . . . . . . 9 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}} = ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})
119	118	fveq2i 6698	. . . . . . . 8 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = (♯‘({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∪ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}))
120		ssrab2 3979	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ⊆ (4...(⌊‘𝑁))
121		ssfi 8829	. . . . . . . . . 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 3979	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} ⊆ (4...(⌊‘𝑁))
124		ssfi 8829	. . . . . . . . . 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 4207	. . . . . . . . . 10 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∩ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)}
127		rabeq0 4285	. . . . . . . . . . 11 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)} = ∅ ↔ ∀𝑘 ∈ (4...(⌊‘𝑁)) ¬ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5))
128		1lt5 11975	. . . . . . . . . . . . . 14 ⊢ 1 < 5
129	91, 128	ltneii 10910	. . . . . . . . . . . . 13 ⊢ 1 ≠ 5
130		eqtr2 2757	. . . . . . . . . . . . . 14 ⊢ (((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5) → 1 = 5)
131	130	necon3ai 2957	. . . . . . . . . . . . 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 3066	. . . . . . . . . 10 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ ((𝑘 mod 6) = 1 ∧ (𝑘 mod 6) = 5)} = ∅
135	126, 134	eqtri 2759	. . . . . . . . 9 ⊢ ({𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} ∩ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ∅
136		hashun 13914	. . . . . . . . 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 2759	. . . . . . 7 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = ((♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}))
139		elfzelz 13077	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → 𝑘 ∈ ℤ)
140		nnrp 12562	. . . . . . . . . . . . . . . . 17 ⊢ (6 ∈ ℕ → 6 ∈ ℝ⁺)
141	64, 140	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 6 ∈ ℝ⁺
142		0le1 11320	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 1
143		1lt6 11980	. . . . . . . . . . . . . . . 16 ⊢ 1 < 6
144		modid 13434	. . . . . . . . . . . . . . . 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 2749	. . . . . . . . . . . . . 14 ⊢ ((𝑘 mod 6) = (1 mod 6) ↔ (𝑘 mod 6) = 1)
147		1z 12172	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
148		moddvds 15789	. . . . . . . . . . . . . . 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 288	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = 1 ↔ 6 ∥ (𝑘 − 1)))
151	139, 150	syl 17	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → ((𝑘 mod 6) = 1 ↔ 6 ∥ (𝑘 − 1)))
152	151	rabbiia 3372	. . . . . . . . . . 11 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)}
153	152	fveq2i 6698	. . . . . . . . . 10 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)})
154	64	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 6 ∈ ℕ)
155		4z 12176	. . . . . . . . . . . 12 ⊢ 4 ∈ ℤ
156	155	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 4 ∈ ℤ)
157		4m1e3 11924	. . . . . . . . . . . . 13 ⊢ (4 − 1) = 3
158	157	fveq2i 6698	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘(4 − 1)) = (ℤ_≥‘3)
159	35, 158	eleqtrrdi 2842	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘𝑁) ∈ (ℤ_≥‘(4 − 1)))
160	147	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 1 ∈ ℤ)
161	154, 156, 159, 160	hashdvds 16291	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 1)}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))))
162	153, 161	syl5eq 2783	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))))
163		2cn 11870	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
164		ax-1cn 10752	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
165		df-3 11859	. . . . . . . . . . . . . . . 16 ⊢ 3 = (2 + 1)
166	157, 165	eqtri 2759	. . . . . . . . . . . . . . 15 ⊢ (4 − 1) = (2 + 1)
167	163, 164, 166	mvrraddi 11060	. . . . . . . . . . . . . 14 ⊢ ((4 − 1) − 1) = 2
168	167	oveq1i 7201	. . . . . . . . . . . . 13 ⊢ (((4 − 1) − 1) / 6) = (2 / 6)
169	168	fveq2i 6698	. . . . . . . . . . . 12 ⊢ (⌊‘(((4 − 1) − 1) / 6)) = (⌊‘(2 / 6))
170		0re 10800	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
171	64	nnne0i 11835	. . . . . . . . . . . . . . 15 ⊢ 6 ≠ 0
172	7, 96, 171	redivcli 11564	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ∈ ℝ
173		2pos 11898	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
174	7, 96, 173, 98	divgt0ii 11714	. . . . . . . . . . . . . 14 ⊢ 0 < (2 / 6)
175	170, 172, 174	ltleii 10920	. . . . . . . . . . . . 13 ⊢ 0 ≤ (2 / 6)
176		2lt6 11979	. . . . . . . . . . . . . . . 16 ⊢ 2 < 6
177		6cn 11886	. . . . . . . . . . . . . . . . 17 ⊢ 6 ∈ ℂ
178	177	mulid1i 10802	. . . . . . . . . . . . . . . 16 ⊢ (6 · 1) = 6
179	176, 178	breqtrri 5066	. . . . . . . . . . . . . . 15 ⊢ 2 < (6 · 1)
180	96, 98	pm3.2i 474	. . . . . . . . . . . . . . . 16 ⊢ (6 ∈ ℝ ∧ 0 < 6)
181		ltdivmul 11672	. . . . . . . . . . . . . . . 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 234	. . . . . . . . . . . . . 14 ⊢ (2 / 6) < 1
184		1e0p1 12300	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
185	183, 184	breqtri 5064	. . . . . . . . . . . . 13 ⊢ (2 / 6) < (0 + 1)
186		0z 12152	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℤ
187		flbi 13356	. . . . . . . . . . . . . 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 2759	. . . . . . . . . . 11 ⊢ (⌊‘(((4 − 1) − 1) / 6)) = 0
191	190	oveq2i 7202	. . . . . . . . . 10 ⊢ ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) − 0)
192	66	flcld 13338	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℤ)
193	192	zcnd 12248	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 1) / 6)) ∈ ℂ)
194	193	subid1d 11143	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) − 0) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
195	191, 194	syl5eq 2783	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 1) / 6)) − (⌊‘(((4 − 1) − 1) / 6))) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
196	162, 195	eqtrd 2771	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) = (⌊‘(((⌊‘𝑁) − 1) / 6)))
197		5pos 11904	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 5
198	170, 69, 197	ltleii 10920	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 5
199		5lt6 11976	. . . . . . . . . . . . . . . 16 ⊢ 5 < 6
200		modid 13434	. . . . . . . . . . . . . . . 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 2749	. . . . . . . . . . . . . 14 ⊢ ((𝑘 mod 6) = (5 mod 6) ↔ (𝑘 mod 6) = 5)
203		5nn 11881	. . . . . . . . . . . . . . . 16 ⊢ 5 ∈ ℕ
204	203	nnzi 12166	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℤ
205		moddvds 15789	. . . . . . . . . . . . . . 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 288	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℤ → ((𝑘 mod 6) = 5 ↔ 6 ∥ (𝑘 − 5)))
208	139, 207	syl 17	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (4...(⌊‘𝑁)) → ((𝑘 mod 6) = 5 ↔ 6 ∥ (𝑘 − 5)))
209	208	rabbiia 3372	. . . . . . . . . . 11 ⊢ {𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5} = {𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)}
210	209	fveq2i 6698	. . . . . . . . . 10 ⊢ (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)})
211	204	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 5 ∈ ℤ)
212	154, 156, 159, 211	hashdvds 16291	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ 6 ∥ (𝑘 − 5)}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))))
213	210, 212	syl5eq 2783	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))))
214	157	oveq1i 7201	. . . . . . . . . . . . . . . 16 ⊢ ((4 − 1) − 5) = (3 − 5)
215		5cn 11883	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℂ
216		3cn 11876	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℂ
217	215, 216	negsubdi2i 11129	. . . . . . . . . . . . . . . 16 ⊢ -(5 − 3) = (3 − 5)
218		3p2e5 11946	. . . . . . . . . . . . . . . . . . 19 ⊢ (3 + 2) = 5
219	218	oveq1i 7201	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 + 2) − 3) = (5 − 3)
220		pncan2 11050	. . . . . . . . . . . . . . . . . . 19 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℂ) → ((3 + 2) − 3) = 2)
221	216, 163, 220	mp2an 692	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 + 2) − 3) = 2
222	219, 221	eqtr3i 2761	. . . . . . . . . . . . . . . . 17 ⊢ (5 − 3) = 2
223	222	negeqi 11036	. . . . . . . . . . . . . . . 16 ⊢ -(5 − 3) = -2
224	214, 217, 223	3eqtr2i 2765	. . . . . . . . . . . . . . 15 ⊢ ((4 − 1) − 5) = -2
225	224	oveq1i 7201	. . . . . . . . . . . . . 14 ⊢ (((4 − 1) − 5) / 6) = (-2 / 6)
226		divneg 11489	. . . . . . . . . . . . . . 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 2762	. . . . . . . . . . . . 13 ⊢ (((4 − 1) − 5) / 6) = -(2 / 6)
229	228	fveq2i 6698	. . . . . . . . . . . 12 ⊢ (⌊‘(((4 − 1) − 5) / 6)) = (⌊‘-(2 / 6))
230	172, 91, 183	ltleii 10920	. . . . . . . . . . . . . 14 ⊢ (2 / 6) ≤ 1
231	172, 91	lenegi 11342	. . . . . . . . . . . . . 14 ⊢ ((2 / 6) ≤ 1 ↔ -1 ≤ -(2 / 6))
232	230, 231	mpbi 233	. . . . . . . . . . . . 13 ⊢ -1 ≤ -(2 / 6)
233	170, 172	ltnegi 11341	. . . . . . . . . . . . . . 15 ⊢ (0 < (2 / 6) ↔ -(2 / 6) < -0)
234	174, 233	mpbi 233	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) < -0
235		neg0 11089	. . . . . . . . . . . . . . . 16 ⊢ -0 = 0
236		1pneg1e0 11914	. . . . . . . . . . . . . . . 16 ⊢ (1 + -1) = 0
237	235, 236	eqtr4i 2762	. . . . . . . . . . . . . . 15 ⊢ -0 = (1 + -1)
238		neg1cn 11909	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℂ
239	238, 164	addcomi 10988	. . . . . . . . . . . . . . 15 ⊢ (-1 + 1) = (1 + -1)
240	237, 239	eqtr4i 2762	. . . . . . . . . . . . . 14 ⊢ -0 = (-1 + 1)
241	234, 240	breqtri 5064	. . . . . . . . . . . . 13 ⊢ -(2 / 6) < (-1 + 1)
242	172	renegcli 11104	. . . . . . . . . . . . . 14 ⊢ -(2 / 6) ∈ ℝ
243		neg1z 12178	. . . . . . . . . . . . . 14 ⊢ -1 ∈ ℤ
244		flbi 13356	. . . . . . . . . . . . . 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 2759	. . . . . . . . . . 11 ⊢ (⌊‘(((4 − 1) − 5) / 6)) = -1
248	247	oveq2i 7202	. . . . . . . . . 10 ⊢ ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1)
249	73	flcld 13338	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℤ)
250	249	zcnd 12248	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℂ)
251		subneg 11092	. . . . . . . . . . 11 ⊢ (((⌊‘(((⌊‘𝑁) − 5) / 6)) ∈ ℂ ∧ 1 ∈ ℂ) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
252	250, 164, 251	sylancl 589	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − -1) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
253	248, 252	syl5eq 2783	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((⌊‘(((⌊‘𝑁) − 5) / 6)) − (⌊‘(((4 − 1) − 5) / 6))) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
254	213, 253	eqtrd 2771	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5}) = ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1))
255	196, 254	oveq12d 7209	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 1}) + (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) = 5})) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)))
256	138, 255	syl5eq 2783	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) = ((⌊‘(((⌊‘𝑁) − 1) / 6)) + ((⌊‘(((⌊‘𝑁) − 5) / 6)) + 1)))
257	82	recnd 10826	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℂ)
258	257	2timesd 12038	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (2 · 𝑁) = (𝑁 + 𝑁))
259		df-6 11862	. . . . . . . . . . . . . 14 ⊢ 6 = (5 + 1)
260	215, 164	addcomi 10988	. . . . . . . . . . . . . 14 ⊢ (5 + 1) = (1 + 5)
261	259, 260	eqtri 2759	. . . . . . . . . . . . 13 ⊢ 6 = (1 + 5)
262	261	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 6 = (1 + 5))
263	258, 262	oveq12d 7209	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) − 6) = ((𝑁 + 𝑁) − (1 + 5)))
264		addsub4 11086	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ) ∧ (1 ∈ ℂ ∧ 5 ∈ ℂ)) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
265	164, 215, 264	mpanr12 705	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
266	257, 257, 265	syl2anc 587	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 + 𝑁) − (1 + 5)) = ((𝑁 − 1) + (𝑁 − 5)))
267	263, 266	eqtrd 2771	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) − 6) = ((𝑁 − 1) + (𝑁 − 5)))
268	267	oveq1d 7206	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = (((𝑁 − 1) + (𝑁 − 5)) / 6))
269		mulcl 10778	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (2 · 𝑁) ∈ ℂ)
270	163, 257, 269	sylancr 590	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (2 · 𝑁) ∈ ℂ)
271	177, 171	pm3.2i 474	. . . . . . . . . . . 12 ⊢ (6 ∈ ℂ ∧ 6 ≠ 0)
272		divsubdir 11491	. . . . . . . . . . . 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 11961	. . . . . . . . . . . . . 14 ⊢ (3 · 2) = 6
276	216, 163	mulcomi 10806	. . . . . . . . . . . . . 14 ⊢ (3 · 2) = (2 · 3)
277	275, 276	eqtr3i 2761	. . . . . . . . . . . . 13 ⊢ 6 = (2 · 3)
278	277	oveq2i 7202	. . . . . . . . . . . 12 ⊢ ((2 · 𝑁) / 6) = ((2 · 𝑁) / (2 · 3))
279		3ne0 11901	. . . . . . . . . . . . . . 15 ⊢ 3 ≠ 0
280	216, 279	pm3.2i 474	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℂ ∧ 3 ≠ 0)
281		2cnne0 12005	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
282		divcan5 11499	. . . . . . . . . . . . . 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	syl5eq 2783	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((2 · 𝑁) / 6) = (𝑁 / 3))
286	177, 171	dividi 11530	. . . . . . . . . . . 12 ⊢ (6 / 6) = 1
287	286	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (6 / 6) = 1)
288	285, 287	oveq12d 7209	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) / 6) − (6 / 6)) = ((𝑁 / 3) − 1))
289	274, 288	eqtrd 2771	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((2 · 𝑁) − 6) / 6) = ((𝑁 / 3) − 1))
290	79	recnd 10826	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℂ)
291	84	recnd 10826	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 − 5) ∈ ℂ)
292		divdir 11480	. . . . . . . . . . 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 587	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 − 1) + (𝑁 − 5)) / 6) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
295	268, 289, 294	3eqtr3d 2779	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 / 3) − 1) = (((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)))
296	295	oveq1d 7206	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 / 3) − 1) + 1) = ((((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)) + 1))
297	21	recnd 10826	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 / 3) ∈ ℂ)
298		npcan 11052	. . . . . . . 8 ⊢ (((𝑁 / 3) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3))
299	297, 164, 298	sylancl 589	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((𝑁 / 3) − 1) + 1) = (𝑁 / 3))
300	81	recnd 10826	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 1) / 6) ∈ ℂ)
301	86	recnd 10826	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((𝑁 − 5) / 6) ∈ ℂ)
302	164	a1i 11	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 1 ∈ ℂ)
303	300, 301, 302	addassd 10820	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((((𝑁 − 1) / 6) + ((𝑁 − 5) / 6)) + 1) = (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
304	296, 299, 303	3eqtr3d 2779	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (𝑁 / 3) = (((𝑁 − 1) / 6) + (((𝑁 − 5) / 6) + 1)))
305	113, 256, 304	3brtr4d 5071	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (♯‘{𝑘 ∈ (4...(⌊‘𝑁)) ∣ (𝑘 mod 6) ∈ {1, 5}}) ≤ (𝑁 / 3))
306	9, 17, 21, 59, 305	letrd 10954	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → ((π‘𝑁) − 2) ≤ (𝑁 / 3))
307	7	a1i 11	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → 2 ∈ ℝ)
308	6, 307, 21	lesubaddd 11394	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ 3 ≤ 𝑁) → (((π‘𝑁) − 2) ≤ (𝑁 / 3) ↔ (π‘𝑁) ≤ ((𝑁 / 3) + 2)))
309	306, 308	mpbid 235	. . 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 10777	. . . 4 ⊢ (((𝑁 / 3) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑁 / 3) + 2) ∈ ℝ)
315	313, 7, 314	sylancl 589	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → ((𝑁 / 3) + 2) ∈ ℝ)
316		ppiwordi 25998	. . . . . 6 ⊢ ((𝑁 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
317	1, 316	mp3an2 1451	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
318	317	adantlr 715	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ (π‘3))
319	318, 24	breqtrdi 5080	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ 2)
320		3pos 11900	. . . . . 6 ⊢ 0 < 3
321		divge0 11666	. . . . . 6 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ (3 ∈ ℝ ∧ 0 < 3)) → 0 ≤ (𝑁 / 3))
322	1, 320, 321	mpanr12 705	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → 0 ≤ (𝑁 / 3))
323	322	adantr 484	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → 0 ≤ (𝑁 / 3))
324		addge02 11308	. . . . 5 ⊢ ((2 ∈ ℝ ∧ (𝑁 / 3) ∈ ℝ) → (0 ≤ (𝑁 / 3) ↔ 2 ≤ ((𝑁 / 3) + 2)))
325	7, 313, 324	sylancr 590	. . . 4 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (0 ≤ (𝑁 / 3) ↔ 2 ≤ ((𝑁 / 3) + 2)))
326	323, 325	mpbid 235	. . 3 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → 2 ≤ ((𝑁 / 3) + 2))
327	311, 312, 315, 319, 326	letrd 10954	. 2 ⊢ (((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) ∧ 𝑁 ≤ 3) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))
328	2, 3, 310, 327	lecasei 10903	1 ⊢ ((𝑁 ∈ ℝ ∧ 0 ≤ 𝑁) → (π‘𝑁) ≤ ((𝑁 / 3) + 2))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 847 = wceq 1543 ∈ wcel 2112 ≠ wne 2932 {crab 3055 ∪ cun 3851 ∩ cin 3852 ⊆ wss 3853 ∅c0 4223 {cpr 4529 class class class wbr 5039 ‘cfv 6358 (class class class)co 7191 ≼ cdom 8602 Fincfn 8604 ℂcc 10692 ℝcr 10693 0cc0 10694 1c1 10695 + caddc 10697 · cmul 10699 < clt 10832 ≤ cle 10833 − cmin 11027 -cneg 11028 / cdiv 11454 ℕcn 11795 2c2 11850 3c3 11851 4c4 11852 5c5 11853 6c6 11854 ℕ₀cn0 12055 ℤcz 12141 ℤ_≥cuz 12403 ℝ⁺crp 12551 ...cfz 13060 ⌊cfl 13330 mod cmo 13407 ♯chash 13861 ∥ cdvds 15778 ℙcprime 16191 πcppi 25930

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-sep 5177 ax-nul 5184 ax-pow 5243 ax-pr 5307 ax-un 7501 ax-cnex 10750 ax-resscn 10751 ax-1cn 10752 ax-icn 10753 ax-addcl 10754 ax-addrcl 10755 ax-mulcl 10756 ax-mulrcl 10757 ax-mulcom 10758 ax-addass 10759 ax-mulass 10760 ax-distr 10761 ax-i2m1 10762 ax-1ne0 10763 ax-1rid 10764 ax-rnegex 10765 ax-rrecex 10766 ax-cnre 10767 ax-pre-lttri 10768 ax-pre-lttrn 10769 ax-pre-ltadd 10770 ax-pre-mulgt0 10771 ax-pre-sup 10772

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-nfc 2879 df-ne 2933 df-nel 3037 df-ral 3056 df-rex 3057 df-reu 3058 df-rmo 3059 df-rab 3060 df-v 3400 df-sbc 3684 df-csb 3799 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-pss 3872 df-nul 4224 df-if 4426 df-pw 4501 df-sn 4528 df-pr 4530 df-tp 4532 df-op 4534 df-uni 4806 df-int 4846 df-iun 4892 df-br 5040 df-opab 5102 df-mpt 5121 df-tr 5147 df-id 5440 df-eprel 5445 df-po 5453 df-so 5454 df-fr 5494 df-we 5496 df-xp 5542 df-rel 5543 df-cnv 5544 df-co 5545 df-dm 5546 df-rn 5547 df-res 5548 df-ima 5549 df-pred 6140 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6316 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-riota 7148 df-ov 7194 df-oprab 7195 df-mpo 7196 df-om 7623 df-1st 7739 df-2nd 7740 df-wrecs 8025 df-recs 8086 df-rdg 8124 df-1o 8180 df-2o 8181 df-oadd 8184 df-er 8369 df-en 8605 df-dom 8606 df-sdom 8607 df-fin 8608 df-sup 9036 df-inf 9037 df-dju 9482 df-card 9520 df-pnf 10834 df-mnf 10835 df-xr 10836 df-ltxr 10837 df-le 10838 df-sub 11029 df-neg 11030 df-div 11455 df-nn 11796 df-2 11858 df-3 11859 df-4 11860 df-5 11861 df-6 11862 df-n0 12056 df-xnn0 12128 df-z 12142 df-uz 12404 df-rp 12552 df-icc 12907 df-fz 13061 df-fl 13332 df-mod 13408 df-seq 13540 df-exp 13601 df-hash 13862 df-cj 14627 df-re 14628 df-im 14629 df-sqrt 14763 df-abs 14764 df-dvds 15779 df-prm 16192 df-ppi 25936

This theorem is referenced by: bposlem5 26123

W3C validator