Theorem bposlem4

Description: Lemma for bpos . (Contributed by Mario Carneiro, 13-Mar-2014)

	Ref	Expression
Hypotheses	bpos.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 5}$$
	bpos.2	$$⊢\phi \to \neg \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
	bpos.3	$$⊢F=\left(n\in \mathbb{N}⟼if\left(n\in \mathbb{P},n^{n\mathrm{pCnt}\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{N}\right)},1\right)\right)$$
	bpos.4	$$⊢K=⌊\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}⌋$$
	bpos.5	$$⊢M=⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋$$
Assertion	bposlem4	$$⊢\phi \to M\in \left(3\dots K\right)$$

Proof

Step	Hyp	Ref	Expression
1		bpos.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 5}$$
2		bpos.2	$$⊢\phi \to \neg \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
3		bpos.3	$$⊢F=\left(n\in \mathbb{N}⟼if\left(n\in \mathbb{P},n^{n\mathrm{pCnt}\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{N}\right)},1\right)\right)$$
4		bpos.4	$$⊢K=⌊\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}⌋$$
5		bpos.5	$$⊢M=⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋$$
6		2nn	$$⊢2\in \mathbb{N}$$
7		5nn	$$⊢5\in \mathbb{N}$$
8		eluznn	$$⊢\left(5\in \mathbb{N}\wedge N\in {\mathbb{Z}}_{\ge 5}\right)\to N\in \mathbb{N}$$
9	7 1 8	sylancr	$$⊢\phi \to N\in \mathbb{N}$$
10		nnmulcl	$$⊢\left(2\in \mathbb{N}\wedge N\in \mathbb{N}\right)\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{N}$$
11	6 9 10	sylancr	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{N}$$
12	11	nnred	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
13	11	nnrpd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {ℝ}^{+}$$
14	13	rpge0d	$$⊢\phi \to 0\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
15	12 14	resqrtcld	$$⊢\phi \to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in ℝ$$
16	15	flcld	$$⊢\phi \to ⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋\in \mathbb{Z}$$
17		sqrt9	$$⊢\sqrt{9}=3$$
18		9re	$$⊢9\in ℝ$$
19	18	a1i	$$⊢\phi \to 9\in ℝ$$
20		10re	$$⊢10\in ℝ$$
21	20	a1i	$$⊢\phi \to 10\in ℝ$$
22		lep1	$$⊢9\in ℝ\to 9\le 9+1$$
23	18 22	ax-mp	$$⊢9\le 9+1$$
24		9p1e10	$$⊢9+1=10$$
25	23 24	breqtri	$$⊢9\le 10$$
26	25	a1i	$$⊢\phi \to 9\le 10$$
27		5cn	$$⊢5\in ℂ$$
28		2cn	$$⊢2\in ℂ$$
29		5t2e10	$$⊢5\cdot 2=10$$
30	27 28 29	mulcomli	$$⊢2\cdot 5=10$$
31		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge 5}\to 5\le N$$
32	1 31	syl	$$⊢\phi \to 5\le N$$
33	9	nnred	$$⊢\phi \to N\in ℝ$$
34		5re	$$⊢5\in ℝ$$
35		2re	$$⊢2\in ℝ$$
36		2pos	$$⊢0<2$$
37	35 36	pm3.2i	$$⊢\left(2\in ℝ\wedge 0<2\right)$$
38		lemul2	$$⊢\left(5\in ℝ\wedge N\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(5\le N\leftrightarrow 2\cdot 5\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
39	34 37 38	mp3an13	$$⊢N\in ℝ\to \left(5\le N\leftrightarrow 2\cdot 5\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
40	33 39	syl	$$⊢\phi \to \left(5\le N\leftrightarrow 2\cdot 5\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
41	32 40	mpbid	$$⊢\phi \to 2\cdot 5\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
42	30 41	eqbrtrrid	$$⊢\phi \to 10\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
43	19 21 12 26 42	letrd	$$⊢\phi \to 9\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
44		0re	$$⊢0\in ℝ$$
45		9pos	$$⊢0<9$$
46	44 18 45	ltleii	$$⊢0\le 9$$
47	18 46	pm3.2i	$$⊢\left(9\in ℝ\wedge 0\le 9\right)$$
48	13	rprege0d	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ\wedge 0\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
49		sqrtle	$$⊢\left(\left(9\in ℝ\wedge 0\le 9\right)\wedge \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ\wedge 0\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\to \left(9\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\leftrightarrow \sqrt{9}\le \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\right)$$
50	47 48 49	sylancr	$$⊢\phi \to \left(9\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\leftrightarrow \sqrt{9}\le \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\right)$$
51	43 50	mpbid	$$⊢\phi \to \sqrt{9}\le \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}$$
52	17 51	eqbrtrrid	$$⊢\phi \to 3\le \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}$$
53		3z	$$⊢3\in \mathbb{Z}$$
54		flge	$$⊢\left(\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in ℝ\wedge 3\in \mathbb{Z}\right)\to \left(3\le \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\leftrightarrow 3\le ⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋\right)$$
55	15 53 54	sylancl	$$⊢\phi \to \left(3\le \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\leftrightarrow 3\le ⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋\right)$$
56	52 55	mpbid	$$⊢\phi \to 3\le ⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋$$
57	53	eluz1i	$$⊢⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋\in {\mathbb{Z}}_{\ge 3}\leftrightarrow \left(⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋\in \mathbb{Z}\wedge 3\le ⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋\right)$$
58	16 56 57	sylanbrc	$$⊢\phi \to ⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋\in {\mathbb{Z}}_{\ge 3}$$
59		3nn	$$⊢3\in \mathbb{N}$$
60		nndivre	$$⊢\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ\wedge 3\in \mathbb{N}\right)\to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\in ℝ$$
61	12 59 60	sylancl	$$⊢\phi \to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\in ℝ$$
62		3re	$$⊢3\in ℝ$$
63	62	a1i	$$⊢\phi \to 3\in ℝ$$
64	13	sqrtgt0d	$$⊢\phi \to 0<\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}$$
65		lemul2	$$⊢\left(3\in ℝ\wedge \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in ℝ\wedge \left(\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in ℝ\wedge 0<\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\right)\right)\to \left(3\le \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\leftrightarrow \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\cdot 3\le \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\right)$$
66	63 15 15 64 65	syl112anc	$$⊢\phi \to \left(3\le \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\leftrightarrow \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\cdot 3\le \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\right)$$
67	52 66	mpbid	$$⊢\phi \to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\cdot 3\le \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}$$
68		remsqsqrt	$$⊢\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ\wedge 0\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
69	12 14 68	syl2anc	$$⊢\phi \to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
70	67 69	breqtrd	$$⊢\phi \to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\cdot 3\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
71		3pos	$$⊢0<3$$
72	62 71	pm3.2i	$$⊢\left(3\in ℝ\wedge 0<3\right)$$
73	72	a1i	$$⊢\phi \to \left(3\in ℝ\wedge 0<3\right)$$
74		lemuldiv	$$⊢\left(\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in ℝ\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ\wedge \left(3\in ℝ\wedge 0<3\right)\right)\to \left(\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\cdot 3\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\leftrightarrow \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\le \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)$$
75	15 12 73 74	syl3anc	$$⊢\phi \to \left(\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\cdot 3\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\leftrightarrow \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\le \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)$$
76	70 75	mpbid	$$⊢\phi \to \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\le \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}$$
77		flword2	$$⊢\left(\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in ℝ\wedge \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\in ℝ\wedge \sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\le \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}\right)\to ⌊\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}⌋\in {\mathbb{Z}}_{\ge ⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋}$$
78	15 61 76 77	syl3anc	$$⊢\phi \to ⌊\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}⌋\in {\mathbb{Z}}_{\ge ⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋}$$
79		elfzuzb	$$⊢⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋\in \left(3\dots ⌊\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}⌋\right)\leftrightarrow \left(⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋\in {\mathbb{Z}}_{\ge 3}\wedge ⌊\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}⌋\in {\mathbb{Z}}_{\ge ⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋}\right)$$
80	58 78 79	sylanbrc	$$⊢\phi \to ⌊\sqrt{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}⌋\in \left(3\dots ⌊\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}⌋\right)$$
81	4	oveq2i	$$⊢\left(3\dots K\right)=\left(3\dots ⌊\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{3}⌋\right)$$
82	80 5 81	3eltr4g	$$⊢\phi \to M\in \left(3\dots K\right)$$