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 | ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 ≤ ; 6 4 ) → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elnnuz | ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) ) | |
2 | ax-1 | ⊢ ( ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) → ( 𝑁 ≤ ; 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) ) | |
3 | 6nn0 | ⊢ 6 ∈ ℕ0 | |
4 | 4nn0 | ⊢ 4 ∈ ℕ0 | |
5 | 3 4 | deccl | ⊢ ; 6 4 ∈ ℕ0 |
6 | 5 | nn0rei | ⊢ ; 6 4 ∈ ℝ |
7 | 6 | a1i | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ; 8 3 ) → ; 6 4 ∈ ℝ ) |
8 | 8nn0 | ⊢ 8 ∈ ℕ0 | |
9 | 3nn0 | ⊢ 3 ∈ ℕ0 | |
10 | 8 9 | deccl | ⊢ ; 8 3 ∈ ℕ0 |
11 | 10 | nn0rei | ⊢ ; 8 3 ∈ ℝ |
12 | 11 | a1i | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ; 8 3 ) → ; 8 3 ∈ ℝ ) |
13 | eluzelre | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ; 8 3 ) → 𝑁 ∈ ℝ ) | |
14 | 4lt10 | ⊢ 4 < ; 1 0 | |
15 | 6lt8 | ⊢ 6 < 8 | |
16 | 3 8 4 9 14 15 | decltc | ⊢ ; 6 4 < ; 8 3 |
17 | 16 | a1i | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ; 8 3 ) → ; 6 4 < ; 8 3 ) |
18 | eluzle | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ; 8 3 ) → ; 8 3 ≤ 𝑁 ) | |
19 | 7 12 13 17 18 | ltletrd | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ; 8 3 ) → ; 6 4 < 𝑁 ) |
20 | ltnle | ⊢ ( ( ; 6 4 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ; 6 4 < 𝑁 ↔ ¬ 𝑁 ≤ ; 6 4 ) ) | |
21 | 6 13 20 | sylancr | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ; 8 3 ) → ( ; 6 4 < 𝑁 ↔ ¬ 𝑁 ≤ ; 6 4 ) ) |
22 | 19 21 | mpbid | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ; 8 3 ) → ¬ 𝑁 ≤ ; 6 4 ) |
23 | 22 | pm2.21d | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ; 8 3 ) → ( 𝑁 ≤ ; 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) ) |
24 | 83prm | ⊢ ; 8 3 ∈ ℙ | |
25 | 4 9 | deccl | ⊢ ; 4 3 ∈ ℕ0 |
26 | 2nn0 | ⊢ 2 ∈ ℕ0 | |
27 | eqid | ⊢ ; 4 3 = ; 4 3 | |
28 | 4t2e8 | ⊢ ( 4 · 2 ) = 8 | |
29 | 3t2e6 | ⊢ ( 3 · 2 ) = 6 | |
30 | 26 4 9 27 28 29 | decmul1 | ⊢ ( ; 4 3 · 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 ∈ ℕ | |
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 | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ; 4 3 ) → ( 𝑁 ≤ ; 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) ) |
39 | 43prm | ⊢ ; 4 3 ∈ ℙ | |
40 | 26 9 | deccl | ⊢ ; 2 3 ∈ ℕ0 |
41 | eqid | ⊢ ; 2 3 = ; 2 3 | |
42 | 2t2e4 | ⊢ ( 2 · 2 ) = 4 | |
43 | 26 26 9 41 42 29 | decmul1 | ⊢ ( ; 2 3 · 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 | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ; 2 3 ) → ( 𝑁 ≤ ; 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) ) |
49 | 23prm | ⊢ ; 2 3 ∈ ℙ | |
50 | 1nn0 | ⊢ 1 ∈ ℕ0 | |
51 | 50 9 | deccl | ⊢ ; 1 3 ∈ ℕ0 |
52 | eqid | ⊢ ; 1 3 = ; 1 3 | |
53 | 2cn | ⊢ 2 ∈ ℂ | |
54 | 53 | mulid2i | ⊢ ( 1 · 2 ) = 2 |
55 | 26 50 9 52 54 29 | decmul1 | ⊢ ( ; 1 3 · 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 | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ; 1 3 ) → ( 𝑁 ≤ ; 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) ) |
61 | 13prm | ⊢ ; 1 3 ∈ ℙ | |
62 | 7nn0 | ⊢ 7 ∈ ℕ0 | |
63 | 7t2e14 | ⊢ ( 7 · 2 ) = ; 1 4 | |
64 | 1nn | ⊢ 1 ∈ ℕ | |
65 | 7lt10 | ⊢ 7 < ; 1 0 | |
66 | 64 9 62 65 | declti | ⊢ 7 < ; 1 3 |
67 | 4nn | ⊢ 4 ∈ ℕ | |
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 | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 7 ) → ( 𝑁 ≤ ; 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) ) |
72 | 7prm | ⊢ 7 ∈ ℙ | |
73 | 5nn0 | ⊢ 5 ∈ ℕ0 | |
74 | 5t2e10 | ⊢ ( 5 · 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 | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → ( 𝑁 ≤ ; 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) ) |
78 | 5prm | ⊢ 5 ∈ ℙ | |
79 | 3lt5 | ⊢ 3 < 5 | |
80 | 5lt6 | ⊢ 5 < 6 | |
81 | 80 | orci | ⊢ ( 5 < 6 ∨ 5 = 6 ) |
82 | 2 77 78 9 29 79 81 | bpos1lem | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 ≤ ; 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) ) |
83 | 3prm | ⊢ 3 ∈ ℙ | |
84 | 2lt3 | ⊢ 2 < 3 | |
85 | 68 | orci | ⊢ ( 3 < 4 ∨ 3 = 4 ) |
86 | 2 82 83 26 42 84 85 | bpos1lem | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ≤ ; 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) ) |
87 | 2prm | ⊢ 2 ∈ ℙ | |
88 | eqid | ⊢ 2 = 2 | |
89 | 88 | olci | ⊢ ( 2 < 2 ∨ 2 = 2 ) |
90 | 2 86 87 50 54 56 89 | bpos1lem | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( 𝑁 ≤ ; 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) ) |
91 | 1 90 | sylbi | ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ≤ ; 6 4 → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) ) |
92 | 91 | imp | ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 ≤ ; 6 4 ) → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) |