Metamath Proof Explorer

Theorem 31prm

Description: 31 is a prime number. In contrast to 37prm , the proof of this theorem is not based on the "blanket" prmlem2 , but on isprm7 . Although the checks for non-divisibility by the primes 7 to 23 are not needed, the proof is much longer (regarding size) than the proof of 37prm (1810 characters compared with 1213 for 37prm ). The number of essential steps, however, is much smaller (138 compared with 213 for 37prm ). (Contributed by AV, 17-Aug-2021) (Proof modification is discouraged.)

Ref Expression
Assertion 31prm 3 1 ∈ ℙ

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 3nn0 ⊢ 3 ∈ ℕ0
3 1nn0 ⊢ 1 ∈ ℕ0
4 2 3 deccl ⊢ 3 1 ∈ ℕ0
5 4 nn0zi ⊢ 3 1 ∈ ℤ
6 3nn ⊢ 3 ∈ ℕ
7 2nn0 ⊢ 2 ∈ ℕ0
8 2re ⊢ 2 ∈ ℝ
9 9re ⊢ 9 ∈ ℝ
10 2lt9 ⊢ 2 < 9
11 8 9 10 ltleii ⊢ 2 ≤ 9
12 6 3 7 11 declei ⊢ 2 ≤ 3 1
13 eluz2 ⊢ ( 3 1 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 3 1 ∈ ℤ ∧ 2 ≤ 3 1 ) )
14 1 5 12 13 mpbir3an ⊢ 3 1 ∈ ( ℤ≥ ‘ 2 )
15 elun ⊢ ( 𝑛 ∈ ( ( { 2 , 3 } ∩ ℙ ) ∪ ( { 4 , 5 } ∩ ℙ ) ) ↔ ( 𝑛 ∈ ( { 2 , 3 } ∩ ℙ ) ∨ 𝑛 ∈ ( { 4 , 5 } ∩ ℙ ) ) )
16 elin ⊢ ( 𝑛 ∈ ( { 2 , 3 } ∩ ℙ ) ↔ ( 𝑛 ∈ { 2 , 3 } ∧ 𝑛 ∈ ℙ ) )
17 vex ⊢ 𝑛 ∈ V
18 17 elpr ⊢ ( 𝑛 ∈ { 2 , 3 } ↔ ( 𝑛 = 2 ∨ 𝑛 = 3 ) )
19 0nn0 ⊢ 0 ∈ ℕ0
20 2cn ⊢ 2 ∈ ℂ
21 20 mul02i ⊢ ( 0 · 2 ) = 0
22 1e0p1 ⊢ 1 = ( 0 + 1 )
23 2 19 21 22 dec2dvds ⊢ ¬ 2 ∥ 3 1
24 breq1 ⊢ ( 𝑛 = 2 → ( 𝑛 ∥ 3 1 ↔ 2 ∥ 3 1 ) )
25 23 24 mtbiri ⊢ ( 𝑛 = 2 → ¬ 𝑛 ∥ 3 1 )
26 3ndvds4 ⊢ ¬ 3 ∥ 4
27 2 3 3dvdsdec ⊢ ( 3 ∥ 3 1 ↔ 3 ∥ ( 3 + 1 ) )
28 3p1e4 ⊢ ( 3 + 1 ) = 4
29 28 breq2i ⊢ ( 3 ∥ ( 3 + 1 ) ↔ 3 ∥ 4 )
30 27 29 bitri ⊢ ( 3 ∥ 3 1 ↔ 3 ∥ 4 )
31 26 30 mtbir ⊢ ¬ 3 ∥ 3 1
32 breq1 ⊢ ( 𝑛 = 3 → ( 𝑛 ∥ 3 1 ↔ 3 ∥ 3 1 ) )
33 31 32 mtbiri ⊢ ( 𝑛 = 3 → ¬ 𝑛 ∥ 3 1 )
34 25 33 jaoi ⊢ ( ( 𝑛 = 2 ∨ 𝑛 = 3 ) → ¬ 𝑛 ∥ 3 1 )
35 18 34 sylbi ⊢ ( 𝑛 ∈ { 2 , 3 } → ¬ 𝑛 ∥ 3 1 )
36 35 adantr ⊢ ( ( 𝑛 ∈ { 2 , 3 } ∧ 𝑛 ∈ ℙ ) → ¬ 𝑛 ∥ 3 1 )
37 16 36 sylbi ⊢ ( 𝑛 ∈ ( { 2 , 3 } ∩ ℙ ) → ¬ 𝑛 ∥ 3 1 )
38 elin ⊢ ( 𝑛 ∈ ( { 4 , 5 } ∩ ℙ ) ↔ ( 𝑛 ∈ { 4 , 5 } ∧ 𝑛 ∈ ℙ ) )
39 17 elpr ⊢ ( 𝑛 ∈ { 4 , 5 } ↔ ( 𝑛 = 4 ∨ 𝑛 = 5 ) )
40 eleq1 ⊢ ( 𝑛 = 4 → ( 𝑛 ∈ ℙ ↔ 4 ∈ ℙ ) )
41 4nprm ⊢ ¬ 4 ∈ ℙ
42 41 pm2.21i ⊢ ( 4 ∈ ℙ → ¬ 𝑛 ∥ 3 1 )
43 40 42 syl6bi ⊢ ( 𝑛 = 4 → ( 𝑛 ∈ ℙ → ¬ 𝑛 ∥ 3 1 ) )
44 1nn ⊢ 1 ∈ ℕ
45 1lt5 ⊢ 1 < 5
46 2 44 45 dec5dvds ⊢ ¬ 5 ∥ 3 1
47 breq1 ⊢ ( 𝑛 = 5 → ( 𝑛 ∥ 3 1 ↔ 5 ∥ 3 1 ) )
48 46 47 mtbiri ⊢ ( 𝑛 = 5 → ¬ 𝑛 ∥ 3 1 )
49 48 a1d ⊢ ( 𝑛 = 5 → ( 𝑛 ∈ ℙ → ¬ 𝑛 ∥ 3 1 ) )
50 43 49 jaoi ⊢ ( ( 𝑛 = 4 ∨ 𝑛 = 5 ) → ( 𝑛 ∈ ℙ → ¬ 𝑛 ∥ 3 1 ) )
51 39 50 sylbi ⊢ ( 𝑛 ∈ { 4 , 5 } → ( 𝑛 ∈ ℙ → ¬ 𝑛 ∥ 3 1 ) )
52 51 imp ⊢ ( ( 𝑛 ∈ { 4 , 5 } ∧ 𝑛 ∈ ℙ ) → ¬ 𝑛 ∥ 3 1 )
53 38 52 sylbi ⊢ ( 𝑛 ∈ ( { 4 , 5 } ∩ ℙ ) → ¬ 𝑛 ∥ 3 1 )
54 37 53 jaoi ⊢ ( ( 𝑛 ∈ ( { 2 , 3 } ∩ ℙ ) ∨ 𝑛 ∈ ( { 4 , 5 } ∩ ℙ ) ) → ¬ 𝑛 ∥ 3 1 )
55 15 54 sylbi ⊢ ( 𝑛 ∈ ( ( { 2 , 3 } ∩ ℙ ) ∪ ( { 4 , 5 } ∩ ℙ ) ) → ¬ 𝑛 ∥ 3 1 )
56 indir ⊢ ( ( { 2 , 3 } ∪ { 4 , 5 } ) ∩ ℙ ) = ( ( { 2 , 3 } ∩ ℙ ) ∪ ( { 4 , 5 } ∩ ℙ ) )
57 55 56 eleq2s ⊢ ( 𝑛 ∈ ( ( { 2 , 3 } ∪ { 4 , 5 } ) ∩ ℙ ) → ¬ 𝑛 ∥ 3 1 )
58 5nn0 ⊢ 5 ∈ ℕ0
59 5re ⊢ 5 ∈ ℝ
60 5lt9 ⊢ 5 < 9
61 59 9 60 ltleii ⊢ 5 ≤ 9
62 2lt3 ⊢ 2 < 3
63 7 2 58 3 61 62 decleh ⊢ 2 5 ≤ 3 1
64 6nn ⊢ 6 ∈ ℕ
65 1lt6 ⊢ 1 < 6
66 2 3 64 65 declt ⊢ 3 1 < 3 6
67 4 nn0rei ⊢ 3 1 ∈ ℝ
68 0re ⊢ 0 ∈ ℝ
69 9pos ⊢ 0 < 9
70 68 9 69 ltleii ⊢ 0 ≤ 9
71 6 3 19 70 declei ⊢ 0 ≤ 3 1
72 67 71 pm3.2i ⊢ ( 3 1 ∈ ℝ ∧ 0 ≤ 3 1 )
73 flsqrt5 ⊢ ( ( 3 1 ∈ ℝ ∧ 0 ≤ 3 1 ) → ( ( 2 5 ≤ 3 1 ∧ 3 1 < 3 6 ) ↔ ( ⌊ ‘ ( √ ‘ 3 1 ) ) = 5 ) )
74 73 bicomd ⊢ ( ( 3 1 ∈ ℝ ∧ 0 ≤ 3 1 ) → ( ( ⌊ ‘ ( √ ‘ 3 1 ) ) = 5 ↔ ( 2 5 ≤ 3 1 ∧ 3 1 < 3 6 ) ) )
75 72 74 ax-mp ⊢ ( ( ⌊ ‘ ( √ ‘ 3 1 ) ) = 5 ↔ ( 2 5 ≤ 3 1 ∧ 3 1 < 3 6 ) )
76 63 66 75 mpbir2an ⊢ ( ⌊ ‘ ( √ ‘ 3 1 ) ) = 5
77 76 oveq2i ⊢ ( 2 ... ( ⌊ ‘ ( √ ‘ 3 1 ) ) ) = ( 2 ... 5 )
78 5nn ⊢ 5 ∈ ℕ
79 78 nnzi ⊢ 5 ∈ ℤ
80 3z ⊢ 3 ∈ ℤ
81 1 79 80 3pm3.2i ⊢ ( 2 ∈ ℤ ∧ 5 ∈ ℤ ∧ 3 ∈ ℤ )
82 3re ⊢ 3 ∈ ℝ
83 8 82 62 ltleii ⊢ 2 ≤ 3
84 3lt5 ⊢ 3 < 5
85 82 59 84 ltleii ⊢ 3 ≤ 5
86 83 85 pm3.2i ⊢ ( 2 ≤ 3 ∧ 3 ≤ 5 )
87 elfz2 ⊢ ( 3 ∈ ( 2 ... 5 ) ↔ ( ( 2 ∈ ℤ ∧ 5 ∈ ℤ ∧ 3 ∈ ℤ ) ∧ ( 2 ≤ 3 ∧ 3 ≤ 5 ) ) )
88 81 86 87 mpbir2an ⊢ 3 ∈ ( 2 ... 5 )
89 fzsplit ⊢ ( 3 ∈ ( 2 ... 5 ) → ( 2 ... 5 ) = ( ( 2 ... 3 ) ∪ ( ( 3 + 1 ) ... 5 ) ) )
90 88 89 ax-mp ⊢ ( 2 ... 5 ) = ( ( 2 ... 3 ) ∪ ( ( 3 + 1 ) ... 5 ) )
91 df-3 ⊢ 3 = ( 2 + 1 )
92 91 oveq2i ⊢ ( 2 ... 3 ) = ( 2 ... ( 2 + 1 ) )
93 fzpr ⊢ ( 2 ∈ ℤ → ( 2 ... ( 2 + 1 ) ) = { 2 , ( 2 + 1 ) } )
94 1 93 ax-mp ⊢ ( 2 ... ( 2 + 1 ) ) = { 2 , ( 2 + 1 ) }
95 2p1e3 ⊢ ( 2 + 1 ) = 3
96 95 preq2i ⊢ { 2 , ( 2 + 1 ) } = { 2 , 3 }
97 92 94 96 3eqtri ⊢ ( 2 ... 3 ) = { 2 , 3 }
98 28 oveq1i ⊢ ( ( 3 + 1 ) ... 5 ) = ( 4 ... 5 )
99 df-5 ⊢ 5 = ( 4 + 1 )
100 99 oveq2i ⊢ ( 4 ... 5 ) = ( 4 ... ( 4 + 1 ) )
101 4z ⊢ 4 ∈ ℤ
102 fzpr ⊢ ( 4 ∈ ℤ → ( 4 ... ( 4 + 1 ) ) = { 4 , ( 4 + 1 ) } )
103 101 102 ax-mp ⊢ ( 4 ... ( 4 + 1 ) ) = { 4 , ( 4 + 1 ) }
104 4p1e5 ⊢ ( 4 + 1 ) = 5
105 104 preq2i ⊢ { 4 , ( 4 + 1 ) } = { 4 , 5 }
106 103 105 eqtri ⊢ ( 4 ... ( 4 + 1 ) ) = { 4 , 5 }
107 98 100 106 3eqtri ⊢ ( ( 3 + 1 ) ... 5 ) = { 4 , 5 }
108 97 107 uneq12i ⊢ ( ( 2 ... 3 ) ∪ ( ( 3 + 1 ) ... 5 ) ) = ( { 2 , 3 } ∪ { 4 , 5 } )
109 77 90 108 3eqtri ⊢ ( 2 ... ( ⌊ ‘ ( √ ‘ 3 1 ) ) ) = ( { 2 , 3 } ∪ { 4 , 5 } )
110 109 ineq1i ⊢ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 3 1 ) ) ) ∩ ℙ ) = ( ( { 2 , 3 } ∪ { 4 , 5 } ) ∩ ℙ )
111 57 110 eleq2s ⊢ ( 𝑛 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 3 1 ) ) ) ∩ ℙ ) → ¬ 𝑛 ∥ 3 1 )
112 111 rgen ⊢ ∀ 𝑛 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 3 1 ) ) ) ∩ ℙ ) ¬ 𝑛 ∥ 3 1
113 isprm7 ⊢ ( 3 1 ∈ ℙ ↔ ( 3 1 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑛 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 3 1 ) ) ) ∩ ℙ ) ¬ 𝑛 ∥ 3 1 ) )
114 14 112 113 mpbir2an ⊢ 3 1 ∈ ℙ