Metamath Proof Explorer

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 
|- ( ( N e. NN /\ N <_ ; 6 4 ) -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )

Proof

Step Hyp Ref Expression
1 elnnuz 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
2 ax-1 
 |-  ( E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) -> ( N <_ ; 6 4 -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) ) )
3 6nn0 
 |-  6 e. NN0
4 4nn0 
 |-  4 e. NN0
5 3 4 deccl 
 |-  ; 6 4 e. NN0
6 5 nn0rei 
 |-  ; 6 4 e. RR
7 6 a1i 
 |-  ( N e. ( ZZ>= ` ; 8 3 ) -> ; 6 4 e. RR )
8 8nn0 
 |-  8 e. NN0
9 3nn0 
 |-  3 e. NN0
10 8 9 deccl 
 |-  ; 8 3 e. NN0
11 10 nn0rei 
 |-  ; 8 3 e. RR
12 11 a1i 
 |-  ( N e. ( ZZ>= ` ; 8 3 ) -> ; 8 3 e. RR )
13 eluzelre 
 |-  ( N e. ( ZZ>= ` ; 8 3 ) -> N e. RR )
14 4lt10 
 |-  4 < ; 1 0
15 6lt8 
 |-  6 < 8
16 3 8 4 9 14 15 decltc 
 |-  ; 6 4 < ; 8 3
17 16 a1i 
 |-  ( N e. ( ZZ>= ` ; 8 3 ) -> ; 6 4 < ; 8 3 )
18 eluzle 
 |-  ( N e. ( ZZ>= ` ; 8 3 ) -> ; 8 3 <_ N )
19 7 12 13 17 18 ltletrd 
 |-  ( N e. ( ZZ>= ` ; 8 3 ) -> ; 6 4 < N )
20 ltnle 
 |-  ( ( ; 6 4 e. RR /\ N e. RR ) -> ( ; 6 4 < N <-> -. N <_ ; 6 4 ) )
21 6 13 20 sylancr 
 |-  ( N e. ( ZZ>= ` ; 8 3 ) -> ( ; 6 4 < N <-> -. N <_ ; 6 4 ) )
22 19 21 mpbid 
 |-  ( N e. ( ZZ>= ` ; 8 3 ) -> -. N <_ ; 6 4 )
23 22 pm2.21d 
 |-  ( N e. ( ZZ>= ` ; 8 3 ) -> ( N <_ ; 6 4 -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) ) )
24 83prm 
 |-  ; 8 3 e. Prime
25 4 9 deccl 
 |-  ; 4 3 e. NN0
26 2nn0 
 |-  2 e. NN0
27 eqid 
 |-  ; 4 3 = ; 4 3
28 4t2e8 
 |-  ( 4 x. 2 ) = 8
29 3t2e6 
 |-  ( 3 x. 2 ) = 6
30 26 4 9 27 28 29 decmul1 
 |-  ( ; 4 3 x. 2 ) = ; 8 6
31 3lt10 
 |-  3 < ; 1 0
32 4lt8 
 |-  4 < 8
33 4 8 9 9 31 32 decltc 
 |-  ; 4 3 < ; 8 3
34 6nn 
 |-  6 e. NN
35 3lt6 
 |-  3 < 6
36 8 9 34 35 declt 
 |-  ; 8 3 < ; 8 6
37 36 orci 
 |-  ( ; 8 3 < ; 8 6 \/ ; 8 3 = ; 8 6 )
38 2 23 24 25 30 33 37 bpos1lem 
 |-  ( N e. ( ZZ>= ` ; 4 3 ) -> ( N <_ ; 6 4 -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) ) )
39 43prm 
 |-  ; 4 3 e. Prime
40 26 9 deccl 
 |-  ; 2 3 e. NN0
41 eqid 
 |-  ; 2 3 = ; 2 3
42 2t2e4 
 |-  ( 2 x. 2 ) = 4
43 26 26 9 41 42 29 decmul1 
 |-  ( ; 2 3 x. 2 ) = ; 4 6
44 2lt4 
 |-  2 < 4
45 26 4 9 9 31 44 decltc 
 |-  ; 2 3 < ; 4 3
46 4 9 34 35 declt 
 |-  ; 4 3 < ; 4 6
47 46 orci 
 |-  ( ; 4 3 < ; 4 6 \/ ; 4 3 = ; 4 6 )
48 2 38 39 40 43 45 47 bpos1lem 
 |-  ( N e. ( ZZ>= ` ; 2 3 ) -> ( N <_ ; 6 4 -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) ) )
49 23prm 
 |-  ; 2 3 e. Prime
50 1nn0 
 |-  1 e. NN0
51 50 9 deccl 
 |-  ; 1 3 e. NN0
52 eqid 
 |-  ; 1 3 = ; 1 3
53 2cn 
 |-  2 e. CC
54 53 mulid2i 
 |-  ( 1 x. 2 ) = 2
55 26 50 9 52 54 29 decmul1 
 |-  ( ; 1 3 x. 2 ) = ; 2 6
56 1lt2 
 |-  1 < 2
57 50 26 9 9 31 56 decltc 
 |-  ; 1 3 < ; 2 3
58 26 9 34 35 declt 
 |-  ; 2 3 < ; 2 6
59 58 orci 
 |-  ( ; 2 3 < ; 2 6 \/ ; 2 3 = ; 2 6 )
60 2 48 49 51 55 57 59 bpos1lem 
 |-  ( N e. ( ZZ>= ` ; 1 3 ) -> ( N <_ ; 6 4 -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) ) )
61 13prm 
 |-  ; 1 3 e. Prime
62 7nn0 
 |-  7 e. NN0
63 7t2e14 
 |-  ( 7 x. 2 ) = ; 1 4
64 1nn 
 |-  1 e. NN
65 7lt10 
 |-  7 < ; 1 0
66 64 9 62 65 declti 
 |-  7 < ; 1 3
67 4nn 
 |-  4 e. NN
68 3lt4 
 |-  3 < 4
69 50 9 67 68 declt 
 |-  ; 1 3 < ; 1 4
70 69 orci 
 |-  ( ; 1 3 < ; 1 4 \/ ; 1 3 = ; 1 4 )
71 2 60 61 62 63 66 70 bpos1lem 
 |-  ( N e. ( ZZ>= ` 7 ) -> ( N <_ ; 6 4 -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) ) )
72 7prm 
 |-  7 e. Prime
73 5nn0 
 |-  5 e. NN0
74 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
75 5lt7 
 |-  5 < 7
76 65 orci 
 |-  ( 7 < ; 1 0 \/ 7 = ; 1 0 )
77 2 71 72 73 74 75 76 bpos1lem 
 |-  ( N e. ( ZZ>= ` 5 ) -> ( N <_ ; 6 4 -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) ) )
78 5prm 
 |-  5 e. Prime
79 3lt5 
 |-  3 < 5
80 5lt6 
 |-  5 < 6
81 80 orci 
 |-  ( 5 < 6 \/ 5 = 6 )
82 2 77 78 9 29 79 81 bpos1lem 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N <_ ; 6 4 -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) ) )
83 3prm 
 |-  3 e. Prime
84 2lt3 
 |-  2 < 3
85 68 orci 
 |-  ( 3 < 4 \/ 3 = 4 )
86 2 82 83 26 42 84 85 bpos1lem 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N <_ ; 6 4 -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) ) )
87 2prm 
 |-  2 e. Prime
88 eqid 
 |-  2 = 2
89 88 olci 
 |-  ( 2 < 2 \/ 2 = 2 )
90 2 86 87 50 54 56 89 bpos1lem 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( N <_ ; 6 4 -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) ) )
91 1 90 sylbi 
 |-  ( N e. NN -> ( N <_ ; 6 4 -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) ) )
92 91 imp 
 |-  ( ( N e. NN /\ N <_ ; 6 4 ) -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )