Metamath Proof Explorer

Theorem 631prm

Description: 631 is a prime number. (Contributed by Mario Carneiro, 1-Mar-2014) (Proof shortened by Mario Carneiro, 20-Apr-2015)

Ref Expression
Assertion 631prm 6 3 1 ∈ ℙ

Proof

Step Hyp Ref Expression
1 6nn0 ⊢ 6 ∈ ℕ0
2 3nn0 ⊢ 3 ∈ ℕ0
3 1 2 deccl ⊢ 6 3 ∈ ℕ0
4 1nn ⊢ 1 ∈ ℕ
5 3 4 decnncl ⊢ 6 3 1 ∈ ℕ
6 8nn0 ⊢ 8 ∈ ℕ0
7 4nn0 ⊢ 4 ∈ ℕ0
8 1nn0 ⊢ 1 ∈ ℕ0
9 6lt8 ⊢ 6 < 8
10 3lt10 ⊢ 3 < 1 0
11 1lt10 ⊢ 1 < 1 0
12 1 6 2 7 8 8 9 10 11 3decltc ⊢ 6 3 1 < 8 4 1
13 3nn ⊢ 3 ∈ ℕ
14 1 13 decnncl ⊢ 6 3 ∈ ℕ
15 14 8 8 11 declti ⊢ 1 < 6 3 1
16 0nn0 ⊢ 0 ∈ ℕ0
17 2cn ⊢ 2 ∈ ℂ
18 17 mul02i ⊢ ( 0 · 2 ) = 0
19 1e0p1 ⊢ 1 = ( 0 + 1 )
20 3 16 18 19 dec2dvds ⊢ ¬ 2 ∥ 6 3 1
21 2nn0 ⊢ 2 ∈ ℕ0
22 21 8 deccl ⊢ 2 1 ∈ ℕ0
23 22 16 deccl ⊢ 2 1 0 ∈ ℕ0
24 eqid ⊢ 2 1 0 = 2 1 0
25 8 dec0h ⊢ 1 = 0 1
26 eqid ⊢ 2 1 = 2 1
27 00id ⊢ ( 0 + 0 ) = 0
28 16 dec0h ⊢ 0 = 0 0
29 27 28 eqtri ⊢ ( 0 + 0 ) = 0 0
30 3t2e6 ⊢ ( 3 · 2 ) = 6
31 30 27 oveq12i ⊢ ( ( 3 · 2 ) + ( 0 + 0 ) ) = ( 6 + 0 )
32 6cn ⊢ 6 ∈ ℂ
33 32 addid1i ⊢ ( 6 + 0 ) = 6
34 31 33 eqtri ⊢ ( ( 3 · 2 ) + ( 0 + 0 ) ) = 6
35 3t1e3 ⊢ ( 3 · 1 ) = 3
36 35 oveq1i ⊢ ( ( 3 · 1 ) + 0 ) = ( 3 + 0 )
37 3cn ⊢ 3 ∈ ℂ
38 37 addid1i ⊢ ( 3 + 0 ) = 3
39 2 dec0h ⊢ 3 = 0 3
40 36 38 39 3eqtri ⊢ ( ( 3 · 1 ) + 0 ) = 0 3
41 21 8 16 16 26 29 2 2 16 34 40 decma2c ⊢ ( ( 3 · 2 1 ) + ( 0 + 0 ) ) = 6 3
42 37 mul01i ⊢ ( 3 · 0 ) = 0
43 42 oveq1i ⊢ ( ( 3 · 0 ) + 1 ) = ( 0 + 1 )
44 0p1e1 ⊢ ( 0 + 1 ) = 1
45 43 44 25 3eqtri ⊢ ( ( 3 · 0 ) + 1 ) = 0 1
46 22 16 16 8 24 25 2 8 16 41 45 decma2c ⊢ ( ( 3 · 2 1 0 ) + 1 ) = 6 3 1
47 1lt3 ⊢ 1 < 3
48 13 23 4 46 47 ndvdsi ⊢ ¬ 3 ∥ 6 3 1
49 1lt5 ⊢ 1 < 5
50 3 4 49 dec5dvds ⊢ ¬ 5 ∥ 6 3 1
51 7nn ⊢ 7 ∈ ℕ
52 9nn0 ⊢ 9 ∈ ℕ0
53 52 16 deccl ⊢ 9 0 ∈ ℕ0
54 eqid ⊢ 9 0 = 9 0
55 7nn0 ⊢ 7 ∈ ℕ0
56 27 oveq2i ⊢ ( ( 7 · 9 ) + ( 0 + 0 ) ) = ( ( 7 · 9 ) + 0 )
57 9cn ⊢ 9 ∈ ℂ
58 7cn ⊢ 7 ∈ ℂ
59 9t7e63 ⊢ ( 9 · 7 ) = 6 3
60 57 58 59 mulcomli ⊢ ( 7 · 9 ) = 6 3
61 60 oveq1i ⊢ ( ( 7 · 9 ) + 0 ) = ( 6 3 + 0 )
62 3 nn0cni ⊢ 6 3 ∈ ℂ
63 62 addid1i ⊢ ( 6 3 + 0 ) = 6 3
64 56 61 63 3eqtri ⊢ ( ( 7 · 9 ) + ( 0 + 0 ) ) = 6 3
65 58 mul01i ⊢ ( 7 · 0 ) = 0
66 65 oveq1i ⊢ ( ( 7 · 0 ) + 1 ) = ( 0 + 1 )
67 66 44 25 3eqtri ⊢ ( ( 7 · 0 ) + 1 ) = 0 1
68 52 16 16 8 54 25 55 8 16 64 67 decma2c ⊢ ( ( 7 · 9 0 ) + 1 ) = 6 3 1
69 1lt7 ⊢ 1 < 7
70 51 53 4 68 69 ndvdsi ⊢ ¬ 7 ∥ 6 3 1
71 8 4 decnncl ⊢ 1 1 ∈ ℕ
72 5nn0 ⊢ 5 ∈ ℕ0
73 72 55 deccl ⊢ 5 7 ∈ ℕ0
74 4nn ⊢ 4 ∈ ℕ
75 eqid ⊢ 5 7 = 5 7
76 7 dec0h ⊢ 4 = 0 4
77 8 8 deccl ⊢ 1 1 ∈ ℕ0
78 eqid ⊢ 1 1 = 1 1
79 8cn ⊢ 8 ∈ ℂ
80 79 addid2i ⊢ ( 0 + 8 ) = 8
81 6 dec0h ⊢ 8 = 0 8
82 80 81 eqtri ⊢ ( 0 + 8 ) = 0 8
83 5cn ⊢ 5 ∈ ℂ
84 83 mulid2i ⊢ ( 1 · 5 ) = 5
85 84 44 oveq12i ⊢ ( ( 1 · 5 ) + ( 0 + 1 ) ) = ( 5 + 1 )
86 5p1e6 ⊢ ( 5 + 1 ) = 6
87 85 86 eqtri ⊢ ( ( 1 · 5 ) + ( 0 + 1 ) ) = 6
88 84 oveq1i ⊢ ( ( 1 · 5 ) + 8 ) = ( 5 + 8 )
89 8p5e13 ⊢ ( 8 + 5 ) = 1 3
90 79 83 89 addcomli ⊢ ( 5 + 8 ) = 1 3
91 88 90 eqtri ⊢ ( ( 1 · 5 ) + 8 ) = 1 3
92 8 8 16 6 78 82 72 2 8 87 91 decmac ⊢ ( ( 1 1 · 5 ) + ( 0 + 8 ) ) = 6 3
93 58 mulid2i ⊢ ( 1 · 7 ) = 7
94 93 44 oveq12i ⊢ ( ( 1 · 7 ) + ( 0 + 1 ) ) = ( 7 + 1 )
95 7p1e8 ⊢ ( 7 + 1 ) = 8
96 94 95 eqtri ⊢ ( ( 1 · 7 ) + ( 0 + 1 ) ) = 8
97 93 oveq1i ⊢ ( ( 1 · 7 ) + 4 ) = ( 7 + 4 )
98 7p4e11 ⊢ ( 7 + 4 ) = 1 1
99 97 98 eqtri ⊢ ( ( 1 · 7 ) + 4 ) = 1 1
100 8 8 16 7 78 76 55 8 8 96 99 decmac ⊢ ( ( 1 1 · 7 ) + 4 ) = 8 1
101 72 55 16 7 75 76 77 8 6 92 100 decma2c ⊢ ( ( 1 1 · 5 7 ) + 4 ) = 6 3 1
102 4lt10 ⊢ 4 < 1 0
103 4 8 7 102 declti ⊢ 4 < 1 1
104 71 73 74 101 103 ndvdsi ⊢ ¬ 1 1 ∥ 6 3 1
105 8 13 decnncl ⊢ 1 3 ∈ ℕ
106 7 6 deccl ⊢ 4 8 ∈ ℕ0
107 eqid ⊢ 4 8 = 4 8
108 55 dec0h ⊢ 7 = 0 7
109 8 2 deccl ⊢ 1 3 ∈ ℕ0
110 eqid ⊢ 1 3 = 1 3
111 77 nn0cni ⊢ 1 1 ∈ ℂ
112 111 addid2i ⊢ ( 0 + 1 1 ) = 1 1
113 4cn ⊢ 4 ∈ ℂ
114 113 mulid2i ⊢ ( 1 · 4 ) = 4
115 1p1e2 ⊢ ( 1 + 1 ) = 2
116 114 115 oveq12i ⊢ ( ( 1 · 4 ) + ( 1 + 1 ) ) = ( 4 + 2 )
117 4p2e6 ⊢ ( 4 + 2 ) = 6
118 116 117 eqtri ⊢ ( ( 1 · 4 ) + ( 1 + 1 ) ) = 6
119 4t3e12 ⊢ ( 4 · 3 ) = 1 2
120 113 37 119 mulcomli ⊢ ( 3 · 4 ) = 1 2
121 2p1e3 ⊢ ( 2 + 1 ) = 3
122 8 21 8 120 121 decaddi ⊢ ( ( 3 · 4 ) + 1 ) = 1 3
123 8 2 8 8 110 112 7 2 8 118 122 decmac ⊢ ( ( 1 3 · 4 ) + ( 0 + 1 1 ) ) = 6 3
124 79 mulid2i ⊢ ( 1 · 8 ) = 8
125 37 addid2i ⊢ ( 0 + 3 ) = 3
126 124 125 oveq12i ⊢ ( ( 1 · 8 ) + ( 0 + 3 ) ) = ( 8 + 3 )
127 8p3e11 ⊢ ( 8 + 3 ) = 1 1
128 126 127 eqtri ⊢ ( ( 1 · 8 ) + ( 0 + 3 ) ) = 1 1
129 8t3e24 ⊢ ( 8 · 3 ) = 2 4
130 79 37 129 mulcomli ⊢ ( 3 · 8 ) = 2 4
131 58 113 98 addcomli ⊢ ( 4 + 7 ) = 1 1
132 21 7 55 130 121 8 131 decaddci ⊢ ( ( 3 · 8 ) + 7 ) = 3 1
133 8 2 16 55 110 108 6 8 2 128 132 decmac ⊢ ( ( 1 3 · 8 ) + 7 ) = 1 1 1
134 7 6 16 55 107 108 109 8 77 123 133 decma2c ⊢ ( ( 1 3 · 4 8 ) + 7 ) = 6 3 1
135 7lt10 ⊢ 7 < 1 0
136 4 2 55 135 declti ⊢ 7 < 1 3
137 105 106 51 134 136 ndvdsi ⊢ ¬ 1 3 ∥ 6 3 1
138 8 51 decnncl ⊢ 1 7 ∈ ℕ
139 2 55 deccl ⊢ 3 7 ∈ ℕ0
140 2nn ⊢ 2 ∈ ℕ
141 eqid ⊢ 3 7 = 3 7
142 21 dec0h ⊢ 2 = 0 2
143 8 55 deccl ⊢ 1 7 ∈ ℕ0
144 8 21 deccl ⊢ 1 2 ∈ ℕ0
145 eqid ⊢ 1 7 = 1 7
146 144 nn0cni ⊢ 1 2 ∈ ℂ
147 146 addid2i ⊢ ( 0 + 1 2 ) = 1 2
148 37 mulid2i ⊢ ( 1 · 3 ) = 3
149 1p2e3 ⊢ ( 1 + 2 ) = 3
150 148 149 oveq12i ⊢ ( ( 1 · 3 ) + ( 1 + 2 ) ) = ( 3 + 3 )
151 3p3e6 ⊢ ( 3 + 3 ) = 6
152 150 151 eqtri ⊢ ( ( 1 · 3 ) + ( 1 + 2 ) ) = 6
153 7t3e21 ⊢ ( 7 · 3 ) = 2 1
154 21 8 21 153 149 decaddi ⊢ ( ( 7 · 3 ) + 2 ) = 2 3
155 8 55 8 21 145 147 2 2 21 152 154 decmac ⊢ ( ( 1 7 · 3 ) + ( 0 + 1 2 ) ) = 6 3
156 83 addid2i ⊢ ( 0 + 5 ) = 5
157 93 156 oveq12i ⊢ ( ( 1 · 7 ) + ( 0 + 5 ) ) = ( 7 + 5 )
158 7p5e12 ⊢ ( 7 + 5 ) = 1 2
159 157 158 eqtri ⊢ ( ( 1 · 7 ) + ( 0 + 5 ) ) = 1 2
160 7t7e49 ⊢ ( 7 · 7 ) = 4 9
161 4p1e5 ⊢ ( 4 + 1 ) = 5
162 9p2e11 ⊢ ( 9 + 2 ) = 1 1
163 7 52 21 160 161 8 162 decaddci ⊢ ( ( 7 · 7 ) + 2 ) = 5 1
164 8 55 16 21 145 142 55 8 72 159 163 decmac ⊢ ( ( 1 7 · 7 ) + 2 ) = 1 2 1
165 2 55 16 21 141 142 143 8 144 155 164 decma2c ⊢ ( ( 1 7 · 3 7 ) + 2 ) = 6 3 1
166 2lt10 ⊢ 2 < 1 0
167 4 55 21 166 declti ⊢ 2 < 1 7
168 138 139 140 165 167 ndvdsi ⊢ ¬ 1 7 ∥ 6 3 1
169 9nn ⊢ 9 ∈ ℕ
170 8 169 decnncl ⊢ 1 9 ∈ ℕ
171 2 2 deccl ⊢ 3 3 ∈ ℕ0
172 eqid ⊢ 3 3 = 3 3
173 8 52 deccl ⊢ 1 9 ∈ ℕ0
174 eqid ⊢ 1 9 = 1 9
175 32 addid2i ⊢ ( 0 + 6 ) = 6
176 1 dec0h ⊢ 6 = 0 6
177 175 176 eqtri ⊢ ( 0 + 6 ) = 0 6
178 148 125 oveq12i ⊢ ( ( 1 · 3 ) + ( 0 + 3 ) ) = ( 3 + 3 )
179 178 151 eqtri ⊢ ( ( 1 · 3 ) + ( 0 + 3 ) ) = 6
180 9t3e27 ⊢ ( 9 · 3 ) = 2 7
181 7p6e13 ⊢ ( 7 + 6 ) = 1 3
182 21 55 1 180 121 2 181 decaddci ⊢ ( ( 9 · 3 ) + 6 ) = 3 3
183 8 52 16 1 174 177 2 2 2 179 182 decmac ⊢ ( ( 1 9 · 3 ) + ( 0 + 6 ) ) = 6 3
184 21 55 7 180 121 8 98 decaddci ⊢ ( ( 9 · 3 ) + 4 ) = 3 1
185 8 52 16 7 174 76 2 8 2 179 184 decmac ⊢ ( ( 1 9 · 3 ) + 4 ) = 6 1
186 2 2 16 7 172 76 173 8 1 183 185 decma2c ⊢ ( ( 1 9 · 3 3 ) + 4 ) = 6 3 1
187 4 52 7 102 declti ⊢ 4 < 1 9
188 170 171 74 186 187 ndvdsi ⊢ ¬ 1 9 ∥ 6 3 1
189 21 13 decnncl ⊢ 2 3 ∈ ℕ
190 21 55 deccl ⊢ 2 7 ∈ ℕ0
191 10nn ⊢ 1 0 ∈ ℕ
192 eqid ⊢ 2 7 = 2 7
193 eqid ⊢ 1 0 = 1 0
194 21 2 deccl ⊢ 2 3 ∈ ℕ0
195 8 1 deccl ⊢ 1 6 ∈ ℕ0
196 eqid ⊢ 2 3 = 2 3
197 eqid ⊢ 1 6 = 1 6
198 ax-1cn ⊢ 1 ∈ ℂ
199 6p1e7 ⊢ ( 6 + 1 ) = 7
200 32 198 199 addcomli ⊢ ( 1 + 6 ) = 7
201 16 8 8 1 25 197 44 200 decadd ⊢ ( 1 + 1 6 ) = 1 7
202 2t2e4 ⊢ ( 2 · 2 ) = 4
203 202 115 oveq12i ⊢ ( ( 2 · 2 ) + ( 1 + 1 ) ) = ( 4 + 2 )
204 203 117 eqtri ⊢ ( ( 2 · 2 ) + ( 1 + 1 ) ) = 6
205 30 oveq1i ⊢ ( ( 3 · 2 ) + 7 ) = ( 6 + 7 )
206 58 32 181 addcomli ⊢ ( 6 + 7 ) = 1 3
207 205 206 eqtri ⊢ ( ( 3 · 2 ) + 7 ) = 1 3
208 21 2 8 55 196 201 21 2 8 204 207 decmac ⊢ ( ( 2 3 · 2 ) + ( 1 + 1 6 ) ) = 6 3
209 7t2e14 ⊢ ( 7 · 2 ) = 1 4
210 58 17 209 mulcomli ⊢ ( 2 · 7 ) = 1 4
211 8 7 21 210 117 decaddi ⊢ ( ( 2 · 7 ) + 2 ) = 1 6
212 58 37 153 mulcomli ⊢ ( 3 · 7 ) = 2 1
213 55 21 2 196 8 21 211 212 decmul1c ⊢ ( 2 3 · 7 ) = 1 6 1
214 213 oveq1i ⊢ ( ( 2 3 · 7 ) + 0 ) = ( 1 6 1 + 0 )
215 195 8 deccl ⊢ 1 6 1 ∈ ℕ0
216 215 nn0cni ⊢ 1 6 1 ∈ ℂ
217 216 addid1i ⊢ ( 1 6 1 + 0 ) = 1 6 1
218 214 217 eqtri ⊢ ( ( 2 3 · 7 ) + 0 ) = 1 6 1
219 21 55 8 16 192 193 194 8 195 208 218 decma2c ⊢ ( ( 2 3 · 2 7 ) + 1 0 ) = 6 3 1
220 10pos ⊢ 0 < 1 0
221 1lt2 ⊢ 1 < 2
222 8 21 16 2 220 221 decltc ⊢ 1 0 < 2 3
223 189 190 191 219 222 ndvdsi ⊢ ¬ 2 3 ∥ 6 3 1
224 5 12 15 20 48 50 70 104 137 168 188 223 prmlem2 ⊢ 6 3 1 ∈ ℙ