ppiub

Description: An upper bound on the prime-counting function ppi , which counts the number of primes less than N . (Contributed by Mario Carneiro, 13-Mar-2014)

		Ref	Expression
	Assertion	ppiub	$⊢ (N \in ℝ \land 0 \leq N) \to \underline{π} (N) \leq (\frac{N}{3}) + 2$

Proof

Step	Hyp	Ref	Expression
1		3re	$⊢ 3 \in ℝ$
2	1	a1i	$⊢ (N \in ℝ \land 0 \leq N) \to 3 \in ℝ$
3		simpl	$⊢ (N \in ℝ \land 0 \leq N) \to N \in ℝ$
4		ppicl	$⊢ N \in ℝ \to \underline{π} (N) \in ℕ_{0}$
5	4	nn0red	$⊢ N \in ℝ \to \underline{π} (N) \in ℝ$
6	5	adantr	$⊢ (N \in ℝ \land 3 \leq N) \to \underline{π} (N) \in ℝ$
7		2re	$⊢ 2 \in ℝ$
8		resubcl	$⊢ (\underline{π} (N) \in ℝ \land 2 \in ℝ) \to \underline{π} (N) - 2 \in ℝ$
9	6 7 8	sylancl	$⊢ (N \in ℝ \land 3 \leq N) \to \underline{π} (N) - 2 \in ℝ$
10		fzfi	$⊢ (4 \dots ⌊N⌋) \in Fin$
11		ssrab2	$⊢ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\} \subseteq (4 \dots ⌊N⌋)$
12		ssfi	$⊢ ((4 \dots ⌊N⌋) \in Fin \land \{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\} \subseteq (4 \dots ⌊N⌋)) \to \{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\} \in Fin$
13	10 11 12	mp2an	$⊢ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\} \in Fin$
14		hashcl	$⊢ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\} \in Fin \to \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\}\| \in ℕ_{0}$
15	13 14	ax-mp	$⊢ \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\}\| \in ℕ_{0}$
16	15	nn0rei	$⊢ \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\}\| \in ℝ$
17	16	a1i	$⊢ (N \in ℝ \land 3 \leq N) \to \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\}\| \in ℝ$
18		3nn	$⊢ 3 \in ℕ$
19		nndivre	$⊢ (N \in ℝ \land 3 \in ℕ) \to \frac{N}{3} \in ℝ$
20	18 19	mpan2	$⊢ N \in ℝ \to \frac{N}{3} \in ℝ$
21	20	adantr	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{N}{3} \in ℝ$
22		ppifl	$⊢ N \in ℝ \to \underline{π} (⌊N⌋) = \underline{π} (N)$
23	22	adantr	$⊢ (N \in ℝ \land 3 \leq N) \to \underline{π} (⌊N⌋) = \underline{π} (N)$
24		ppi3	$⊢ \underline{π} (3) = 2$
25	24	a1i	$⊢ (N \in ℝ \land 3 \leq N) \to \underline{π} (3) = 2$
26	23 25	oveq12d	$⊢ (N \in ℝ \land 3 \leq N) \to \underline{π} (⌊N⌋) - \underline{π} (3) = \underline{π} (N) - 2$
27		3z	$⊢ 3 \in ℤ$
28	27	a1i	$⊢ (N \in ℝ \land 3 \leq N) \to 3 \in ℤ$
29		flcl	$⊢ N \in ℝ \to ⌊N⌋ \in ℤ$
30	29	adantr	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊N⌋ \in ℤ$
31		flge	$⊢ (N \in ℝ \land 3 \in ℤ) \to (3 \leq N \leftrightarrow 3 \leq ⌊N⌋)$
32	27 31	mpan2	$⊢ N \in ℝ \to (3 \leq N \leftrightarrow 3 \leq ⌊N⌋)$
33	32	biimpa	$⊢ (N \in ℝ \land 3 \leq N) \to 3 \leq ⌊N⌋$
34		eluz2	$⊢ ⌊N⌋ \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land ⌊N⌋ \in ℤ \land 3 \leq ⌊N⌋)$
35	28 30 33 34	syl3anbrc	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊N⌋ \in ℤ_{\geq 3}$
36		ppidif	$⊢ ⌊N⌋ \in ℤ_{\geq 3} \to \underline{π} (⌊N⌋) - \underline{π} (3) = \|(3 + 1 \dots ⌊N⌋) \cap ℙ\|$
37	35 36	syl	$⊢ (N \in ℝ \land 3 \leq N) \to \underline{π} (⌊N⌋) - \underline{π} (3) = \|(3 + 1 \dots ⌊N⌋) \cap ℙ\|$
38		df-4	$⊢ 4 = 3 + 1$
39	38	oveq1i	$⊢ (4 \dots ⌊N⌋) = (3 + 1 \dots ⌊N⌋)$
40	39	ineq1i	$⊢ (4 \dots ⌊N⌋) \cap ℙ = (3 + 1 \dots ⌊N⌋) \cap ℙ$
41	40	fveq2i	$⊢ \|(4 \dots ⌊N⌋) \cap ℙ\| = \|(3 + 1 \dots ⌊N⌋) \cap ℙ\|$
42	37 41	eqtr4di	$⊢ (N \in ℝ \land 3 \leq N) \to \underline{π} (⌊N⌋) - \underline{π} (3) = \|(4 \dots ⌊N⌋) \cap ℙ\|$
43	26 42	eqtr3d	$⊢ (N \in ℝ \land 3 \leq N) \to \underline{π} (N) - 2 = \|(4 \dots ⌊N⌋) \cap ℙ\|$
44		dfin5	$⊢ (4 \dots ⌊N⌋) \cap ℙ = \{k \in (4 \dots ⌊N⌋) \| k \in ℙ\}$
45		elfzle1	$⊢ k \in (4 \dots ⌊N⌋) \to 4 \leq k$
46		ppiublem2	$⊢ (k \in ℙ \land 4 \leq k) \to k \mod 6 \in \{1, 5\}$
47	46	expcom	$⊢ 4 \leq k \to (k \in ℙ \to k \mod 6 \in \{1, 5\})$
48	45 47	syl	$⊢ k \in (4 \dots ⌊N⌋) \to (k \in ℙ \to k \mod 6 \in \{1, 5\})$
49	48	ss2rabi	$⊢ \{k \in (4 \dots ⌊N⌋) \| k \in ℙ\} \subseteq \{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\}$
50	44 49	eqsstri	$⊢ (4 \dots ⌊N⌋) \cap ℙ \subseteq \{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\}$
51		ssdomg	$⊢ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\} \in Fin \to ((4 \dots ⌊N⌋) \cap ℙ \subseteq \{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\} \to ((4 \dots ⌊N⌋) \cap ℙ) ≼ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\})$
52	13 50 51	mp2	$⊢ ((4 \dots ⌊N⌋) \cap ℙ) ≼ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\}$
53		inss1	$⊢ (4 \dots ⌊N⌋) \cap ℙ \subseteq (4 \dots ⌊N⌋)$
54		ssfi	$⊢ ((4 \dots ⌊N⌋) \in Fin \land (4 \dots ⌊N⌋) \cap ℙ \subseteq (4 \dots ⌊N⌋)) \to (4 \dots ⌊N⌋) \cap ℙ \in Fin$
55	10 53 54	mp2an	$⊢ (4 \dots ⌊N⌋) \cap ℙ \in Fin$
56		hashdom	$⊢ ((4 \dots ⌊N⌋) \cap ℙ \in Fin \land \{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\} \in Fin) \to (\|(4 \dots ⌊N⌋) \cap ℙ\| \leq \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\}\| \leftrightarrow ((4 \dots ⌊N⌋) \cap ℙ) ≼ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\})$
57	55 13 56	mp2an	$⊢ \|(4 \dots ⌊N⌋) \cap ℙ\| \leq \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\}\| \leftrightarrow ((4 \dots ⌊N⌋) \cap ℙ) ≼ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\}$
58	52 57	mpbir	$⊢ \|(4 \dots ⌊N⌋) \cap ℙ\| \leq \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\}\|$
59	43 58	eqbrtrdi	$⊢ (N \in ℝ \land 3 \leq N) \to \underline{π} (N) - 2 \leq \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\}\|$
60		reflcl	$⊢ N \in ℝ \to ⌊N⌋ \in ℝ$
61	60	adantr	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊N⌋ \in ℝ$
62		peano2rem	$⊢ ⌊N⌋ \in ℝ \to ⌊N⌋ - 1 \in ℝ$
63	61 62	syl	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊N⌋ - 1 \in ℝ$
64		6nn	$⊢ 6 \in ℕ$
65		nndivre	$⊢ (⌊N⌋ - 1 \in ℝ \land 6 \in ℕ) \to \frac{⌊N⌋ - 1}{6} \in ℝ$
66	63 64 65	sylancl	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{⌊N⌋ - 1}{6} \in ℝ$
67		reflcl	$⊢ \frac{⌊N⌋ - 1}{6} \in ℝ \to ⌊\frac{⌊N⌋ - 1}{6}⌋ \in ℝ$
68	66 67	syl	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 1}{6}⌋ \in ℝ$
69		5re	$⊢ 5 \in ℝ$
70		resubcl	$⊢ (⌊N⌋ \in ℝ \land 5 \in ℝ) \to ⌊N⌋ - 5 \in ℝ$
71	61 69 70	sylancl	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊N⌋ - 5 \in ℝ$
72		nndivre	$⊢ (⌊N⌋ - 5 \in ℝ \land 6 \in ℕ) \to \frac{⌊N⌋ - 5}{6} \in ℝ$
73	71 64 72	sylancl	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{⌊N⌋ - 5}{6} \in ℝ$
74		reflcl	$⊢ \frac{⌊N⌋ - 5}{6} \in ℝ \to ⌊\frac{⌊N⌋ - 5}{6}⌋ \in ℝ$
75	73 74	syl	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 5}{6}⌋ \in ℝ$
76		peano2re	$⊢ ⌊\frac{⌊N⌋ - 5}{6}⌋ \in ℝ \to ⌊\frac{⌊N⌋ - 5}{6}⌋ + 1 \in ℝ$
77	75 76	syl	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 5}{6}⌋ + 1 \in ℝ$
78		peano2rem	$⊢ N \in ℝ \to N - 1 \in ℝ$
79	78	adantr	$⊢ (N \in ℝ \land 3 \leq N) \to N - 1 \in ℝ$
80		nndivre	$⊢ (N - 1 \in ℝ \land 6 \in ℕ) \to \frac{N - 1}{6} \in ℝ$
81	79 64 80	sylancl	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{N - 1}{6} \in ℝ$
82		simpl	$⊢ (N \in ℝ \land 3 \leq N) \to N \in ℝ$
83		resubcl	$⊢ (N \in ℝ \land 5 \in ℝ) \to N - 5 \in ℝ$
84	82 69 83	sylancl	$⊢ (N \in ℝ \land 3 \leq N) \to N - 5 \in ℝ$
85		nndivre	$⊢ (N - 5 \in ℝ \land 6 \in ℕ) \to \frac{N - 5}{6} \in ℝ$
86	84 64 85	sylancl	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{N - 5}{6} \in ℝ$
87		peano2re	$⊢ \frac{N - 5}{6} \in ℝ \to (\frac{N - 5}{6}) + 1 \in ℝ$
88	86 87	syl	$⊢ (N \in ℝ \land 3 \leq N) \to (\frac{N - 5}{6}) + 1 \in ℝ$
89		flle	$⊢ \frac{⌊N⌋ - 1}{6} \in ℝ \to ⌊\frac{⌊N⌋ - 1}{6}⌋ \leq \frac{⌊N⌋ - 1}{6}$
90	66 89	syl	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 1}{6}⌋ \leq \frac{⌊N⌋ - 1}{6}$
91		1re	$⊢ 1 \in ℝ$
92	91	a1i	$⊢ (N \in ℝ \land 3 \leq N) \to 1 \in ℝ$
93		flle	$⊢ N \in ℝ \to ⌊N⌋ \leq N$
94	93	adantr	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊N⌋ \leq N$
95	61 82 92 94	lesub1dd	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊N⌋ - 1 \leq N - 1$
96		6re	$⊢ 6 \in ℝ$
97	96	a1i	$⊢ (N \in ℝ \land 3 \leq N) \to 6 \in ℝ$
98		6pos	$⊢ 0 < 6$
99	98	a1i	$⊢ (N \in ℝ \land 3 \leq N) \to 0 < 6$
100		lediv1	$⊢ (⌊N⌋ - 1 \in ℝ \land N - 1 \in ℝ \land (6 \in ℝ \land 0 < 6)) \to (⌊N⌋ - 1 \leq N - 1 \leftrightarrow \frac{⌊N⌋ - 1}{6} \leq \frac{N - 1}{6})$
101	63 79 97 99 100	syl112anc	$⊢ (N \in ℝ \land 3 \leq N) \to (⌊N⌋ - 1 \leq N - 1 \leftrightarrow \frac{⌊N⌋ - 1}{6} \leq \frac{N - 1}{6})$
102	95 101	mpbid	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{⌊N⌋ - 1}{6} \leq \frac{N - 1}{6}$
103	68 66 81 90 102	letrd	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 1}{6}⌋ \leq \frac{N - 1}{6}$
104		flle	$⊢ \frac{⌊N⌋ - 5}{6} \in ℝ \to ⌊\frac{⌊N⌋ - 5}{6}⌋ \leq \frac{⌊N⌋ - 5}{6}$
105	73 104	syl	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 5}{6}⌋ \leq \frac{⌊N⌋ - 5}{6}$
106	69	a1i	$⊢ (N \in ℝ \land 3 \leq N) \to 5 \in ℝ$
107	61 82 106 94	lesub1dd	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊N⌋ - 5 \leq N - 5$
108		lediv1	$⊢ (⌊N⌋ - 5 \in ℝ \land N - 5 \in ℝ \land (6 \in ℝ \land 0 < 6)) \to (⌊N⌋ - 5 \leq N - 5 \leftrightarrow \frac{⌊N⌋ - 5}{6} \leq \frac{N - 5}{6})$
109	71 84 97 99 108	syl112anc	$⊢ (N \in ℝ \land 3 \leq N) \to (⌊N⌋ - 5 \leq N - 5 \leftrightarrow \frac{⌊N⌋ - 5}{6} \leq \frac{N - 5}{6})$
110	107 109	mpbid	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{⌊N⌋ - 5}{6} \leq \frac{N - 5}{6}$
111	75 73 86 105 110	letrd	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 5}{6}⌋ \leq \frac{N - 5}{6}$
112	75 86 92 111	leadd1dd	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 5}{6}⌋ + 1 \leq (\frac{N - 5}{6}) + 1$
113	68 77 81 88 103 112	le2addd	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 1}{6}⌋ + ⌊\frac{⌊N⌋ - 5}{6}⌋ + 1 \leq (\frac{N - 1}{6}) + (\frac{N - 5}{6}) + 1$
114		ovex	$⊢ k \mod 6 \in V$
115	114	elpr	$⊢ k \mod 6 \in \{1, 5\} \leftrightarrow (k \mod 6 = 1 \lor k \mod 6 = 5)$
116	115	rabbii	$⊢ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\} = \{k \in (4 \dots ⌊N⌋) \| (k \mod 6 = 1 \lor k \mod 6 = 5)\}$
117		unrab	$⊢ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\} \cup \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\} = \{k \in (4 \dots ⌊N⌋) \| (k \mod 6 = 1 \lor k \mod 6 = 5)\}$
118	116 117	eqtr4i	$⊢ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\} = \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\} \cup \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\}$
119	118	fveq2i	$⊢ \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\}\| = \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\} \cup \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\}\|$
120		ssrab2	$⊢ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\} \subseteq (4 \dots ⌊N⌋)$
121		ssfi	$⊢ ((4 \dots ⌊N⌋) \in Fin \land \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\} \subseteq (4 \dots ⌊N⌋)) \to \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\} \in Fin$
122	10 120 121	mp2an	$⊢ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\} \in Fin$
123		ssrab2	$⊢ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\} \subseteq (4 \dots ⌊N⌋)$
124		ssfi	$⊢ ((4 \dots ⌊N⌋) \in Fin \land \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\} \subseteq (4 \dots ⌊N⌋)) \to \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\} \in Fin$
125	10 123 124	mp2an	$⊢ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\} \in Fin$
126		inrab	$⊢ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\} \cap \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\} = \{k \in (4 \dots ⌊N⌋) \| (k \mod 6 = 1 \land k \mod 6 = 5)\}$
127		rabeq0	$⊢ \{k \in (4 \dots ⌊N⌋) \| (k \mod 6 = 1 \land k \mod 6 = 5)\} = \emptyset \leftrightarrow \forall k \in (4 \dots ⌊N⌋) \neg (k \mod 6 = 1 \land k \mod 6 = 5)$
128		1lt5	$⊢ 1 < 5$
129	91 128	ltneii	$⊢ 1 \neq 5$
130		eqtr2	$⊢ (k \mod 6 = 1 \land k \mod 6 = 5) \to 1 = 5$
131	130	necon3ai	$⊢ 1 \neq 5 \to \neg (k \mod 6 = 1 \land k \mod 6 = 5)$
132	129 131	ax-mp	$⊢ \neg (k \mod 6 = 1 \land k \mod 6 = 5)$
133	132	a1i	$⊢ k \in (4 \dots ⌊N⌋) \to \neg (k \mod 6 = 1 \land k \mod 6 = 5)$
134	127 133	mprgbir	$⊢ \{k \in (4 \dots ⌊N⌋) \| (k \mod 6 = 1 \land k \mod 6 = 5)\} = \emptyset$
135	126 134	eqtri	$⊢ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\} \cap \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\} = \emptyset$
136		hashun	$⊢ (\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\} \in Fin \land \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\} \in Fin \land \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\} \cap \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\} = \emptyset) \to \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\} \cup \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\}\| = \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\}\| + \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\}\|$
137	122 125 135 136	mp3an	$⊢ \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\} \cup \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\}\| = \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\}\| + \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\}\|$
138	119 137	eqtri	$⊢ \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\}\| = \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\}\| + \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\}\|$
139		elfzelz	$⊢ k \in (4 \dots ⌊N⌋) \to k \in ℤ$
140		nnrp	$⊢ 6 \in ℕ \to 6 \in ℝ^{+}$
141	64 140	ax-mp	$⊢ 6 \in ℝ^{+}$
142		0le1	$⊢ 0 \leq 1$
143		1lt6	$⊢ 1 < 6$
144		modid	$⊢ ((1 \in ℝ \land 6 \in ℝ^{+}) \land (0 \leq 1 \land 1 < 6)) \to 1 \mod 6 = 1$
145	91 141 142 143 144	mp4an	$⊢ 1 \mod 6 = 1$
146	145	eqeq2i	$⊢ k \mod 6 = 1 \mod 6 \leftrightarrow k \mod 6 = 1$
147		1z	$⊢ 1 \in ℤ$
148		moddvds	$⊢ (6 \in ℕ \land k \in ℤ \land 1 \in ℤ) \to (k \mod 6 = 1 \mod 6 \leftrightarrow 6 ∥ (k - 1))$
149	64 147 148	mp3an13	$⊢ k \in ℤ \to (k \mod 6 = 1 \mod 6 \leftrightarrow 6 ∥ (k - 1))$
150	146 149	bitr3id	$⊢ k \in ℤ \to (k \mod 6 = 1 \leftrightarrow 6 ∥ (k - 1))$
151	139 150	syl	$⊢ k \in (4 \dots ⌊N⌋) \to (k \mod 6 = 1 \leftrightarrow 6 ∥ (k - 1))$
152	151	rabbiia	$⊢ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\} = \{k \in (4 \dots ⌊N⌋) \| 6 ∥ (k - 1)\}$
153	152	fveq2i	$⊢ \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\}\| = \|\{k \in (4 \dots ⌊N⌋) \| 6 ∥ (k - 1)\}\|$
154	64	a1i	$⊢ (N \in ℝ \land 3 \leq N) \to 6 \in ℕ$
155		4z	$⊢ 4 \in ℤ$
156	155	a1i	$⊢ (N \in ℝ \land 3 \leq N) \to 4 \in ℤ$
157		4m1e3	$⊢ 4 - 1 = 3$
158	157	fveq2i	$⊢ ℤ_{\geq (4 - 1)} = ℤ_{\geq 3}$
159	35 158	eleqtrrdi	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊N⌋ \in ℤ_{\geq (4 - 1)}$
160	147	a1i	$⊢ (N \in ℝ \land 3 \leq N) \to 1 \in ℤ$
161	154 156 159 160	hashdvds	$⊢ (N \in ℝ \land 3 \leq N) \to \|\{k \in (4 \dots ⌊N⌋) \| 6 ∥ (k - 1)\}\| = ⌊\frac{⌊N⌋ - 1}{6}⌋ - ⌊\frac{4 - 1 - 1}{6}⌋$
162	153 161	syl5eq	$⊢ (N \in ℝ \land 3 \leq N) \to \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\}\| = ⌊\frac{⌊N⌋ - 1}{6}⌋ - ⌊\frac{4 - 1 - 1}{6}⌋$
163		2cn	$⊢ 2 \in ℂ$
164		ax-1cn	$⊢ 1 \in ℂ$
165		df-3	$⊢ 3 = 2 + 1$
166	157 165	eqtri	$⊢ 4 - 1 = 2 + 1$
167	163 164 166	mvrraddi	$⊢ 4 - 1 - 1 = 2$
168	167	oveq1i	$⊢ \frac{4 - 1 - 1}{6} = \frac{2}{6}$
169	168	fveq2i	$⊢ ⌊\frac{4 - 1 - 1}{6}⌋ = ⌊\frac{2}{6}⌋$
170		0re	$⊢ 0 \in ℝ$
171	64	nnne0i	$⊢ 6 \neq 0$
172	7 96 171	redivcli	$⊢ \frac{2}{6} \in ℝ$
173		2pos	$⊢ 0 < 2$
174	7 96 173 98	divgt0ii	$⊢ 0 < \frac{2}{6}$
175	170 172 174	ltleii	$⊢ 0 \leq \frac{2}{6}$
176		2lt6	$⊢ 2 < 6$
177		6cn	$⊢ 6 \in ℂ$
178	177	mulid1i	$⊢ 6 \cdot 1 = 6$
179	176 178	breqtrri	$⊢ 2 < 6 \cdot 1$
180	96 98	pm3.2i	$⊢ (6 \in ℝ \land 0 < 6)$
181		ltdivmul	$⊢ (2 \in ℝ \land 1 \in ℝ \land (6 \in ℝ \land 0 < 6)) \to (\frac{2}{6} < 1 \leftrightarrow 2 < 6 \cdot 1)$
182	7 91 180 181	mp3an	$⊢ \frac{2}{6} < 1 \leftrightarrow 2 < 6 \cdot 1$
183	179 182	mpbir	$⊢ \frac{2}{6} < 1$
184		1e0p1	$⊢ 1 = 0 + 1$
185	183 184	breqtri	$⊢ \frac{2}{6} < 0 + 1$
186		0z	$⊢ 0 \in ℤ$
187		flbi	$⊢ (\frac{2}{6} \in ℝ \land 0 \in ℤ) \to (⌊\frac{2}{6}⌋ = 0 \leftrightarrow (0 \leq \frac{2}{6} \land \frac{2}{6} < 0 + 1))$
188	172 186 187	mp2an	$⊢ ⌊\frac{2}{6}⌋ = 0 \leftrightarrow (0 \leq \frac{2}{6} \land \frac{2}{6} < 0 + 1)$
189	175 185 188	mpbir2an	$⊢ ⌊\frac{2}{6}⌋ = 0$
190	169 189	eqtri	$⊢ ⌊\frac{4 - 1 - 1}{6}⌋ = 0$
191	190	oveq2i	$⊢ ⌊\frac{⌊N⌋ - 1}{6}⌋ - ⌊\frac{4 - 1 - 1}{6}⌋ = ⌊\frac{⌊N⌋ - 1}{6}⌋ - 0$
192	66	flcld	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 1}{6}⌋ \in ℤ$
193	192	zcnd	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 1}{6}⌋ \in ℂ$
194	193	subid1d	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 1}{6}⌋ - 0 = ⌊\frac{⌊N⌋ - 1}{6}⌋$
195	191 194	syl5eq	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 1}{6}⌋ - ⌊\frac{4 - 1 - 1}{6}⌋ = ⌊\frac{⌊N⌋ - 1}{6}⌋$
196	162 195	eqtrd	$⊢ (N \in ℝ \land 3 \leq N) \to \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\}\| = ⌊\frac{⌊N⌋ - 1}{6}⌋$
197		5pos	$⊢ 0 < 5$
198	170 69 197	ltleii	$⊢ 0 \leq 5$
199		5lt6	$⊢ 5 < 6$
200		modid	$⊢ ((5 \in ℝ \land 6 \in ℝ^{+}) \land (0 \leq 5 \land 5 < 6)) \to 5 \mod 6 = 5$
201	69 141 198 199 200	mp4an	$⊢ 5 \mod 6 = 5$
202	201	eqeq2i	$⊢ k \mod 6 = 5 \mod 6 \leftrightarrow k \mod 6 = 5$
203		5nn	$⊢ 5 \in ℕ$
204	203	nnzi	$⊢ 5 \in ℤ$
205		moddvds	$⊢ (6 \in ℕ \land k \in ℤ \land 5 \in ℤ) \to (k \mod 6 = 5 \mod 6 \leftrightarrow 6 ∥ (k - 5))$
206	64 204 205	mp3an13	$⊢ k \in ℤ \to (k \mod 6 = 5 \mod 6 \leftrightarrow 6 ∥ (k - 5))$
207	202 206	bitr3id	$⊢ k \in ℤ \to (k \mod 6 = 5 \leftrightarrow 6 ∥ (k - 5))$
208	139 207	syl	$⊢ k \in (4 \dots ⌊N⌋) \to (k \mod 6 = 5 \leftrightarrow 6 ∥ (k - 5))$
209	208	rabbiia	$⊢ \{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\} = \{k \in (4 \dots ⌊N⌋) \| 6 ∥ (k - 5)\}$
210	209	fveq2i	$⊢ \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\}\| = \|\{k \in (4 \dots ⌊N⌋) \| 6 ∥ (k - 5)\}\|$
211	204	a1i	$⊢ (N \in ℝ \land 3 \leq N) \to 5 \in ℤ$
212	154 156 159 211	hashdvds	$⊢ (N \in ℝ \land 3 \leq N) \to \|\{k \in (4 \dots ⌊N⌋) \| 6 ∥ (k - 5)\}\| = ⌊\frac{⌊N⌋ - 5}{6}⌋ - ⌊\frac{4 - 1 - 5}{6}⌋$
213	210 212	syl5eq	$⊢ (N \in ℝ \land 3 \leq N) \to \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\}\| = ⌊\frac{⌊N⌋ - 5}{6}⌋ - ⌊\frac{4 - 1 - 5}{6}⌋$
214	157	oveq1i	$⊢ 4 - 1 - 5 = 3 - 5$
215		5cn	$⊢ 5 \in ℂ$
216		3cn	$⊢ 3 \in ℂ$
217	215 216	negsubdi2i	$⊢ - (5 - 3) = 3 - 5$
218		3p2e5	$⊢ 3 + 2 = 5$
219	218	oveq1i	$⊢ 3 + 2 - 3 = 5 - 3$
220		pncan2	$⊢ (3 \in ℂ \land 2 \in ℂ) \to 3 + 2 - 3 = 2$
221	216 163 220	mp2an	$⊢ 3 + 2 - 3 = 2$
222	219 221	eqtr3i	$⊢ 5 - 3 = 2$
223	222	negeqi	$⊢ - (5 - 3) = - 2$
224	214 217 223	3eqtr2i	$⊢ 4 - 1 - 5 = - 2$
225	224	oveq1i	$⊢ \frac{4 - 1 - 5}{6} = \frac{- 2}{6}$
226		divneg	$⊢ (2 \in ℂ \land 6 \in ℂ \land 6 \neq 0) \to - \frac{2}{6} = \frac{- 2}{6}$
227	163 177 171 226	mp3an	$⊢ - \frac{2}{6} = \frac{- 2}{6}$
228	225 227	eqtr4i	$⊢ \frac{4 - 1 - 5}{6} = - \frac{2}{6}$
229	228	fveq2i	$⊢ ⌊\frac{4 - 1 - 5}{6}⌋ = ⌊- \frac{2}{6}⌋$
230	172 91 183	ltleii	$⊢ \frac{2}{6} \leq 1$
231	172 91	lenegi	$⊢ \frac{2}{6} \leq 1 \leftrightarrow - 1 \leq - \frac{2}{6}$
232	230 231	mpbi	$⊢ - 1 \leq - \frac{2}{6}$
233	170 172	ltnegi	$⊢ 0 < \frac{2}{6} \leftrightarrow - \frac{2}{6} < - 0$
234	174 233	mpbi	$⊢ - \frac{2}{6} < - 0$
235		neg0	$⊢ - 0 = 0$
236		1pneg1e0	$⊢ 1 + -1 = 0$
237	235 236	eqtr4i	$⊢ - 0 = 1 + -1$
238		neg1cn	$⊢ - 1 \in ℂ$
239	238 164	addcomi	$⊢ - 1 + 1 = 1 + -1$
240	237 239	eqtr4i	$⊢ - 0 = - 1 + 1$
241	234 240	breqtri	$⊢ - \frac{2}{6} < - 1 + 1$
242	172	renegcli	$⊢ - \frac{2}{6} \in ℝ$
243		neg1z	$⊢ - 1 \in ℤ$
244		flbi	$⊢ (- \frac{2}{6} \in ℝ \land - 1 \in ℤ) \to (⌊- \frac{2}{6}⌋ = - 1 \leftrightarrow (- 1 \leq - \frac{2}{6} \land - \frac{2}{6} < - 1 + 1))$
245	242 243 244	mp2an	$⊢ ⌊- \frac{2}{6}⌋ = - 1 \leftrightarrow (- 1 \leq - \frac{2}{6} \land - \frac{2}{6} < - 1 + 1)$
246	232 241 245	mpbir2an	$⊢ ⌊- \frac{2}{6}⌋ = - 1$
247	229 246	eqtri	$⊢ ⌊\frac{4 - 1 - 5}{6}⌋ = - 1$
248	247	oveq2i	$⊢ ⌊\frac{⌊N⌋ - 5}{6}⌋ - ⌊\frac{4 - 1 - 5}{6}⌋ = ⌊\frac{⌊N⌋ - 5}{6}⌋ - -1$
249	73	flcld	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 5}{6}⌋ \in ℤ$
250	249	zcnd	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 5}{6}⌋ \in ℂ$
251		subneg	$⊢ (⌊\frac{⌊N⌋ - 5}{6}⌋ \in ℂ \land 1 \in ℂ) \to ⌊\frac{⌊N⌋ - 5}{6}⌋ - -1 = ⌊\frac{⌊N⌋ - 5}{6}⌋ + 1$
252	250 164 251	sylancl	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 5}{6}⌋ - -1 = ⌊\frac{⌊N⌋ - 5}{6}⌋ + 1$
253	248 252	syl5eq	$⊢ (N \in ℝ \land 3 \leq N) \to ⌊\frac{⌊N⌋ - 5}{6}⌋ - ⌊\frac{4 - 1 - 5}{6}⌋ = ⌊\frac{⌊N⌋ - 5}{6}⌋ + 1$
254	213 253	eqtrd	$⊢ (N \in ℝ \land 3 \leq N) \to \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\}\| = ⌊\frac{⌊N⌋ - 5}{6}⌋ + 1$
255	196 254	oveq12d	$⊢ (N \in ℝ \land 3 \leq N) \to \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 1\}\| + \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 = 5\}\| = ⌊\frac{⌊N⌋ - 1}{6}⌋ + ⌊\frac{⌊N⌋ - 5}{6}⌋ + 1$
256	138 255	syl5eq	$⊢ (N \in ℝ \land 3 \leq N) \to \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\}\| = ⌊\frac{⌊N⌋ - 1}{6}⌋ + ⌊\frac{⌊N⌋ - 5}{6}⌋ + 1$
257	82	recnd	$⊢ (N \in ℝ \land 3 \leq N) \to N \in ℂ$
258	257	2timesd	$⊢ (N \in ℝ \land 3 \leq N) \to 2 \cdot N = N + N$
259		df-6	$⊢ 6 = 5 + 1$
260	215 164	addcomi	$⊢ 5 + 1 = 1 + 5$
261	259 260	eqtri	$⊢ 6 = 1 + 5$
262	261	a1i	$⊢ (N \in ℝ \land 3 \leq N) \to 6 = 1 + 5$
263	258 262	oveq12d	$⊢ (N \in ℝ \land 3 \leq N) \to 2 \cdot N - 6 = N + N - (1 + 5)$
264		addsub4	$⊢ ((N \in ℂ \land N \in ℂ) \land (1 \in ℂ \land 5 \in ℂ)) \to N + N - (1 + 5) = (N - 1) + N - 5$
265	164 215 264	mpanr12	$⊢ (N \in ℂ \land N \in ℂ) \to N + N - (1 + 5) = (N - 1) + N - 5$
266	257 257 265	syl2anc	$⊢ (N \in ℝ \land 3 \leq N) \to N + N - (1 + 5) = (N - 1) + N - 5$
267	263 266	eqtrd	$⊢ (N \in ℝ \land 3 \leq N) \to 2 \cdot N - 6 = (N - 1) + N - 5$
268	267	oveq1d	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{2 \cdot N - 6}{6} = \frac{(N - 1) + N - 5}{6}$
269		mulcl	$⊢ (2 \in ℂ \land N \in ℂ) \to 2 \cdot N \in ℂ$
270	163 257 269	sylancr	$⊢ (N \in ℝ \land 3 \leq N) \to 2 \cdot N \in ℂ$
271	177 171	pm3.2i	$⊢ (6 \in ℂ \land 6 \neq 0)$
272		divsubdir	$⊢ (2 \cdot N \in ℂ \land 6 \in ℂ \land (6 \in ℂ \land 6 \neq 0)) \to \frac{2 \cdot N - 6}{6} = (\frac{2 \cdot N}{6}) - (\frac{6}{6})$
273	177 271 272	mp3an23	$⊢ 2 \cdot N \in ℂ \to \frac{2 \cdot N - 6}{6} = (\frac{2 \cdot N}{6}) - (\frac{6}{6})$
274	270 273	syl	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{2 \cdot N - 6}{6} = (\frac{2 \cdot N}{6}) - (\frac{6}{6})$
275		3t2e6	$⊢ 3 \cdot 2 = 6$
276	216 163	mulcomi	$⊢ 3 \cdot 2 = 2 \cdot 3$
277	275 276	eqtr3i	$⊢ 6 = 2 \cdot 3$
278	277	oveq2i	$⊢ \frac{2 \cdot N}{6} = \frac{2 \cdot N}{2 \cdot 3}$
279		3ne0	$⊢ 3 \neq 0$
280	216 279	pm3.2i	$⊢ (3 \in ℂ \land 3 \neq 0)$
281		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
282		divcan5	$⊢ (N \in ℂ \land (3 \in ℂ \land 3 \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{2 \cdot N}{2 \cdot 3} = \frac{N}{3}$
283	280 281 282	mp3an23	$⊢ N \in ℂ \to \frac{2 \cdot N}{2 \cdot 3} = \frac{N}{3}$
284	257 283	syl	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{2 \cdot N}{2 \cdot 3} = \frac{N}{3}$
285	278 284	syl5eq	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{2 \cdot N}{6} = \frac{N}{3}$
286	177 171	dividi	$⊢ \frac{6}{6} = 1$
287	286	a1i	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{6}{6} = 1$
288	285 287	oveq12d	$⊢ (N \in ℝ \land 3 \leq N) \to (\frac{2 \cdot N}{6}) - (\frac{6}{6}) = (\frac{N}{3}) - 1$
289	274 288	eqtrd	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{2 \cdot N - 6}{6} = (\frac{N}{3}) - 1$
290	79	recnd	$⊢ (N \in ℝ \land 3 \leq N) \to N - 1 \in ℂ$
291	84	recnd	$⊢ (N \in ℝ \land 3 \leq N) \to N - 5 \in ℂ$
292		divdir	$⊢ (N - 1 \in ℂ \land N - 5 \in ℂ \land (6 \in ℂ \land 6 \neq 0)) \to \frac{(N - 1) + N - 5}{6} = (\frac{N - 1}{6}) + (\frac{N - 5}{6})$
293	271 292	mp3an3	$⊢ (N - 1 \in ℂ \land N - 5 \in ℂ) \to \frac{(N - 1) + N - 5}{6} = (\frac{N - 1}{6}) + (\frac{N - 5}{6})$
294	290 291 293	syl2anc	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{(N - 1) + N - 5}{6} = (\frac{N - 1}{6}) + (\frac{N - 5}{6})$
295	268 289 294	3eqtr3d	$⊢ (N \in ℝ \land 3 \leq N) \to (\frac{N}{3}) - 1 = (\frac{N - 1}{6}) + (\frac{N - 5}{6})$
296	295	oveq1d	$⊢ (N \in ℝ \land 3 \leq N) \to (\frac{N}{3}) - 1 + 1 = (\frac{N - 1}{6}) + (\frac{N - 5}{6}) + 1$
297	21	recnd	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{N}{3} \in ℂ$
298		npcan	$⊢ (\frac{N}{3} \in ℂ \land 1 \in ℂ) \to (\frac{N}{3}) - 1 + 1 = \frac{N}{3}$
299	297 164 298	sylancl	$⊢ (N \in ℝ \land 3 \leq N) \to (\frac{N}{3}) - 1 + 1 = \frac{N}{3}$
300	81	recnd	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{N - 1}{6} \in ℂ$
301	86	recnd	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{N - 5}{6} \in ℂ$
302	164	a1i	$⊢ (N \in ℝ \land 3 \leq N) \to 1 \in ℂ$
303	300 301 302	addassd	$⊢ (N \in ℝ \land 3 \leq N) \to (\frac{N - 1}{6}) + (\frac{N - 5}{6}) + 1 = (\frac{N - 1}{6}) + (\frac{N - 5}{6}) + 1$
304	296 299 303	3eqtr3d	$⊢ (N \in ℝ \land 3 \leq N) \to \frac{N}{3} = (\frac{N - 1}{6}) + (\frac{N - 5}{6}) + 1$
305	113 256 304	3brtr4d	$⊢ (N \in ℝ \land 3 \leq N) \to \|\{k \in (4 \dots ⌊N⌋) \| k \mod 6 \in \{1, 5\}\}\| \leq \frac{N}{3}$
306	9 17 21 59 305	letrd	$⊢ (N \in ℝ \land 3 \leq N) \to \underline{π} (N) - 2 \leq \frac{N}{3}$
307	7	a1i	$⊢ (N \in ℝ \land 3 \leq N) \to 2 \in ℝ$
308	6 307 21	lesubaddd	$⊢ (N \in ℝ \land 3 \leq N) \to (\underline{π} (N) - 2 \leq \frac{N}{3} \leftrightarrow \underline{π} (N) \leq (\frac{N}{3}) + 2)$
309	306 308	mpbid	$⊢ (N \in ℝ \land 3 \leq N) \to \underline{π} (N) \leq (\frac{N}{3}) + 2$
310	309	adantlr	$⊢ ((N \in ℝ \land 0 \leq N) \land 3 \leq N) \to \underline{π} (N) \leq (\frac{N}{3}) + 2$
311	5	ad2antrr	$⊢ ((N \in ℝ \land 0 \leq N) \land N \leq 3) \to \underline{π} (N) \in ℝ$
312	7	a1i	$⊢ ((N \in ℝ \land 0 \leq N) \land N \leq 3) \to 2 \in ℝ$
313	20	ad2antrr	$⊢ ((N \in ℝ \land 0 \leq N) \land N \leq 3) \to \frac{N}{3} \in ℝ$
314		readdcl	$⊢ (\frac{N}{3} \in ℝ \land 2 \in ℝ) \to (\frac{N}{3}) + 2 \in ℝ$
315	313 7 314	sylancl	$⊢ ((N \in ℝ \land 0 \leq N) \land N \leq 3) \to (\frac{N}{3}) + 2 \in ℝ$
316		ppiwordi	$⊢ (N \in ℝ \land 3 \in ℝ \land N \leq 3) \to \underline{π} (N) \leq \underline{π} (3)$
317	1 316	mp3an2	$⊢ (N \in ℝ \land N \leq 3) \to \underline{π} (N) \leq \underline{π} (3)$
318	317	adantlr	$⊢ ((N \in ℝ \land 0 \leq N) \land N \leq 3) \to \underline{π} (N) \leq \underline{π} (3)$
319	318 24	breqtrdi	$⊢ ((N \in ℝ \land 0 \leq N) \land N \leq 3) \to \underline{π} (N) \leq 2$
320		3pos	$⊢ 0 < 3$
321		divge0	$⊢ ((N \in ℝ \land 0 \leq N) \land (3 \in ℝ \land 0 < 3)) \to 0 \leq \frac{N}{3}$
322	1 320 321	mpanr12	$⊢ (N \in ℝ \land 0 \leq N) \to 0 \leq \frac{N}{3}$
323	322	adantr	$⊢ ((N \in ℝ \land 0 \leq N) \land N \leq 3) \to 0 \leq \frac{N}{3}$
324		addge02	$⊢ (2 \in ℝ \land \frac{N}{3} \in ℝ) \to (0 \leq \frac{N}{3} \leftrightarrow 2 \leq (\frac{N}{3}) + 2)$
325	7 313 324	sylancr	$⊢ ((N \in ℝ \land 0 \leq N) \land N \leq 3) \to (0 \leq \frac{N}{3} \leftrightarrow 2 \leq (\frac{N}{3}) + 2)$
326	323 325	mpbid	$⊢ ((N \in ℝ \land 0 \leq N) \land N \leq 3) \to 2 \leq (\frac{N}{3}) + 2$
327	311 312 315 319 326	letrd	$⊢ ((N \in ℝ \land 0 \leq N) \land N \leq 3) \to \underline{π} (N) \leq (\frac{N}{3}) + 2$
328	2 3 310 327	lecasei	$⊢ (N \in ℝ \land 0 \leq N) \to \underline{π} (N) \leq (\frac{N}{3}) + 2$

Metamath Proof Explorer

Theorem ppiub

Proof