Theorem bpos1lem

Description: Lemma for bpos1 . (Contributed by Mario Carneiro, 12-Mar-2014)

	Ref	Expression
Hypotheses	bpos1.1	$$⊢\exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\to \phi$$
	bpos1.2	$$⊢N\in {\mathbb{Z}}_{\ge P}\to \phi$$
	bpos1.3	$$⊢P\in \mathbb{P}$$
	bpos1.4	$$⊢A\in {\mathbb{N}}_0$$
	bpos1.5	$$⊢A\cdot 2=B$$
	bpos1.6	$$⊢A<P$$
	bpos1.7	$$⊢\left(P<B\vee P=B\right)$$
Assertion	bpos1lem	$$⊢N\in {\mathbb{Z}}_{\ge A}\to \phi$$

Proof

Step	Hyp	Ref	Expression
1		bpos1.1	$$⊢\exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\to \phi$$
2		bpos1.2	$$⊢N\in {\mathbb{Z}}_{\ge P}\to \phi$$
3		bpos1.3	$$⊢P\in \mathbb{P}$$
4		bpos1.4	$$⊢A\in {\mathbb{N}}_0$$
5		bpos1.5	$$⊢A\cdot 2=B$$
6		bpos1.6	$$⊢A<P$$
7		bpos1.7	$$⊢\left(P<B\vee P=B\right)$$
8		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
9	3 8	ax-mp	$$⊢P\in \mathbb{N}$$
10	9	nnzi	$$⊢P\in \mathbb{Z}$$
11		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge A}\to N\in \mathbb{Z}$$
12		eluz	$$⊢\left(P\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(N\in {\mathbb{Z}}_{\ge P}\leftrightarrow P\le N\right)$$
13	10 11 12	sylancr	$$⊢N\in {\mathbb{Z}}_{\ge A}\to \left(N\in {\mathbb{Z}}_{\ge P}\leftrightarrow P\le N\right)$$
14	13 2	syl6bir	$$⊢N\in {\mathbb{Z}}_{\ge A}\to \left(P\le N\to \phi \right)$$
15	9	nnrei	$$⊢P\in ℝ$$
16	15	a1i	$$⊢N\in {\mathbb{Z}}_{\ge A}\to P\in ℝ$$
17	4	nn0rei	$$⊢A\in ℝ$$
18		2re	$$⊢2\in ℝ$$
19	17 18	remulcli	$$⊢A\cdot 2\in ℝ$$
20	5 19	eqeltrri	$$⊢B\in ℝ$$
21	20	a1i	$$⊢N\in {\mathbb{Z}}_{\ge A}\to B\in ℝ$$
22		eluzelre	$$⊢N\in {\mathbb{Z}}_{\ge A}\to N\in ℝ$$
23		remulcl	$$⊢\left(2\in ℝ\wedge N\in ℝ\right)\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
24	18 22 23	sylancr	$$⊢N\in {\mathbb{Z}}_{\ge A}\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
25	15 20	leloei	$$⊢P\le B\leftrightarrow \left(P<B\vee P=B\right)$$
26	7 25	mpbir	$$⊢P\le B$$
27	26	a1i	$$⊢N\in {\mathbb{Z}}_{\ge A}\to P\le B$$
28	4	nn0cni	$$⊢A\in ℂ$$
29		2cn	$$⊢2\in ℂ$$
30	28 29 5	mulcomli	$$⊢2A=B$$
31		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge A}\to A\le N$$
32		2pos	$$⊢0<2$$
33	18 32	pm3.2i	$$⊢\left(2\in ℝ\wedge 0<2\right)$$
34		lemul2	$$⊢\left(A\in ℝ\wedge N\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(A\le N\leftrightarrow 2A\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
35	17 33 34	mp3an13	$$⊢N\in ℝ\to \left(A\le N\leftrightarrow 2A\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
36	22 35	syl	$$⊢N\in {\mathbb{Z}}_{\ge A}\to \left(A\le N\leftrightarrow 2A\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
37	31 36	mpbid	$$⊢N\in {\mathbb{Z}}_{\ge A}\to 2A\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
38	30 37	eqbrtrrid	$$⊢N\in {\mathbb{Z}}_{\ge A}\to B\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
39	16 21 24 27 38	letrd	$$⊢N\in {\mathbb{Z}}_{\ge A}\to P\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
40	39	anim2i	$$⊢\left(N<P\wedge N\in {\mathbb{Z}}_{\ge A}\right)\to \left(N<P\wedge P\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
41		breq2	$$⊢p=P\to \left(N<p\leftrightarrow N<P\right)$$
42		breq1	$$⊢p=P\to \left(p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\leftrightarrow P\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
43	41 42	anbi12d	$$⊢p=P\to \left(\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\leftrightarrow \left(N<P\wedge P\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
44	43	rspcev	$$⊢\left(P\in \mathbb{P}\wedge \left(N<P\wedge P\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\to \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
45	3 40 44	sylancr	$$⊢\left(N<P\wedge N\in {\mathbb{Z}}_{\ge A}\right)\to \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
46	45 1	syl	$$⊢\left(N<P\wedge N\in {\mathbb{Z}}_{\ge A}\right)\to \phi$$
47	46	expcom	$$⊢N\in {\mathbb{Z}}_{\ge A}\to \left(N<P\to \phi \right)$$
48		lelttric	$$⊢\left(P\in ℝ\wedge N\in ℝ\right)\to \left(P\le N\vee N<P\right)$$
49	15 22 48	sylancr	$$⊢N\in {\mathbb{Z}}_{\ge A}\to \left(P\le N\vee N<P\right)$$
50	14 47 49	mpjaod	$$⊢N\in {\mathbb{Z}}_{\ge A}\to \phi$$