Theorem bpos1

Description: Bertrand's postulate, checked numerically for N <_ 6 4 , using the prime sequence 2 , 3 , 5 , 7 , 1 3 , 2 3 , 4 3 , 8 3 . (Contributed by Mario Carneiro, 12-Mar-2014) (Proof shortened by Mario Carneiro, 20-Apr-2015) (Proof shortened by AV, 15-Sep-2021)

	Ref	Expression
Assertion	bpos1	$$⊢\left(N\in \mathbb{N}\wedge N\le 64\right)\to \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$

Proof

Step	Hyp	Ref	Expression
1		elnnuz	$$⊢N\in \mathbb{N}\leftrightarrow N\in {\mathbb{Z}}_{\ge 1}$$
2		ax-1	$$⊢\exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\to \left(N\le 64\to \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
3		6nn0	$$⊢6\in {\mathbb{N}}_0$$
4		4nn0	$$⊢4\in {\mathbb{N}}_0$$
5	3 4	deccl	$$⊢64\in {\mathbb{N}}_0$$
6	5	nn0rei	$$⊢64\in ℝ$$
7	6	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 83}\to 64\in ℝ$$
8		8nn0	$$⊢8\in {\mathbb{N}}_0$$
9		3nn0	$$⊢3\in {\mathbb{N}}_0$$
10	8 9	deccl	$$⊢83\in {\mathbb{N}}_0$$
11	10	nn0rei	$$⊢83\in ℝ$$
12	11	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 83}\to 83\in ℝ$$
13		eluzelre	$$⊢N\in {\mathbb{Z}}_{\ge 83}\to N\in ℝ$$
14		4lt10	$$⊢4<10$$
15		6lt8	$$⊢6<8$$
16	3 8 4 9 14 15	decltc	$$⊢64<83$$
17	16	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 83}\to 64<83$$
18		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge 83}\to 83\le N$$
19	7 12 13 17 18	ltletrd	$$⊢N\in {\mathbb{Z}}_{\ge 83}\to 64<N$$
20		ltnle	$$⊢\left(64\in ℝ\wedge N\in ℝ\right)\to \left(64<N\leftrightarrow \neg N\le 64\right)$$
21	6 13 20	sylancr	$$⊢N\in {\mathbb{Z}}_{\ge 83}\to \left(64<N\leftrightarrow \neg N\le 64\right)$$
22	19 21	mpbid	$$⊢N\in {\mathbb{Z}}_{\ge 83}\to \neg N\le 64$$
23	22	pm2.21d	$$⊢N\in {\mathbb{Z}}_{\ge 83}\to \left(N\le 64\to \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
24		83prm	$$⊢83\in \mathbb{P}$$
25	4 9	deccl	$$⊢43\in {\mathbb{N}}_0$$
26		2nn0	$$⊢2\in {\mathbb{N}}_0$$
27		eqid	$$⊢43=43$$
28		4t2e8	$$⊢4\cdot 2=8$$
29		3t2e6	$$⊢3\cdot 2=6$$
30	26 4 9 27 28 29	decmul1	$$⊢43\cdot 2=86$$
31		3lt10	$$⊢3<10$$
32		4lt8	$$⊢4<8$$
33	4 8 9 9 31 32	decltc	$$⊢43<83$$
34		6nn	$$⊢6\in \mathbb{N}$$
35		3lt6	$$⊢3<6$$
36	8 9 34 35	declt	$$⊢83<86$$
37	36	orci	$$⊢\left(83<86\vee 83=86\right)$$
38	2 23 24 25 30 33 37	bpos1lem	$$⊢N\in {\mathbb{Z}}_{\ge 43}\to \left(N\le 64\to \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
39		43prm	$$⊢43\in \mathbb{P}$$
40	26 9	deccl	$$⊢23\in {\mathbb{N}}_0$$
41		eqid	$$⊢23=23$$
42		2t2e4	$$⊢2\cdot 2=4$$
43	26 26 9 41 42 29	decmul1	$$⊢23\cdot 2=46$$
44		2lt4	$$⊢2<4$$
45	26 4 9 9 31 44	decltc	$$⊢23<43$$
46	4 9 34 35	declt	$$⊢43<46$$
47	46	orci	$$⊢\left(43<46\vee 43=46\right)$$
48	2 38 39 40 43 45 47	bpos1lem	$$⊢N\in {\mathbb{Z}}_{\ge 23}\to \left(N\le 64\to \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
49		23prm	$$⊢23\in \mathbb{P}$$
50		1nn0	$$⊢1\in {\mathbb{N}}_0$$
51	50 9	deccl	$$⊢13\in {\mathbb{N}}_0$$
52		eqid	$$⊢13=13$$
53		2cn	$$⊢2\in ℂ$$
54	53	mullidi	$$⊢1\cdot 2=2$$
55	26 50 9 52 54 29	decmul1	$$⊢13\cdot 2=26$$
56		1lt2	$$⊢1<2$$
57	50 26 9 9 31 56	decltc	$$⊢13<23$$
58	26 9 34 35	declt	$$⊢23<26$$
59	58	orci	$$⊢\left(23<26\vee 23=26\right)$$
60	2 48 49 51 55 57 59	bpos1lem	$$⊢N\in {\mathbb{Z}}_{\ge 13}\to \left(N\le 64\to \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
61		13prm	$$⊢13\in \mathbb{P}$$
62		7nn0	$$⊢7\in {\mathbb{N}}_0$$
63		7t2e14	$$⊢7\cdot 2=14$$
64		1nn	$$⊢1\in \mathbb{N}$$
65		7lt10	$$⊢7<10$$
66	64 9 62 65	declti	$$⊢7<13$$
67		4nn	$$⊢4\in \mathbb{N}$$
68		3lt4	$$⊢3<4$$
69	50 9 67 68	declt	$$⊢13<14$$
70	69	orci	$$⊢\left(13<14\vee 13=14\right)$$
71	2 60 61 62 63 66 70	bpos1lem	$$⊢N\in {\mathbb{Z}}_{\ge 7}\to \left(N\le 64\to \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
72		7prm	$$⊢7\in \mathbb{P}$$
73		5nn0	$$⊢5\in {\mathbb{N}}_0$$
74		5t2e10	$$⊢5\cdot 2=10$$
75		5lt7	$$⊢5<7$$
76	65	orci	$$⊢\left(7<10\vee 7=10\right)$$
77	2 71 72 73 74 75 76	bpos1lem	$$⊢N\in {\mathbb{Z}}_{\ge 5}\to \left(N\le 64\to \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
78		5prm	$$⊢5\in \mathbb{P}$$
79		3lt5	$$⊢3<5$$
80		5lt6	$$⊢5<6$$
81	80	orci	$$⊢\left(5<6\vee 5=6\right)$$
82	2 77 78 9 29 79 81	bpos1lem	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(N\le 64\to \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
83		3prm	$$⊢3\in \mathbb{P}$$
84		2lt3	$$⊢2<3$$
85	68	orci	$$⊢\left(3<4\vee 3=4\right)$$
86	2 82 83 26 42 84 85	bpos1lem	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(N\le 64\to \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
87		2prm	$$⊢2\in \mathbb{P}$$
88		eqid	$$⊢2=2$$
89	88	olci	$$⊢\left(2<2\vee 2=2\right)$$
90	2 86 87 50 54 56 89	bpos1lem	$$⊢N\in {\mathbb{Z}}_{\ge 1}\to \left(N\le 64\to \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
91	1 90	sylbi	$$⊢N\in \mathbb{N}\to \left(N\le 64\to \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
92	91	imp	$$⊢\left(N\in \mathbb{N}\wedge N\le 64\right)\to \exists p\in \mathbb{P}\left(N<p\wedge p\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$