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 e. Prime

Proof

Step Hyp Ref Expression
1 6nn0 
 |-  6 e. NN0
2 3nn0 
 |-  3 e. NN0
3 1 2 deccl 
 |-  ; 6 3 e. NN0
4 1nn 
 |-  1 e. NN
5 3 4 decnncl 
 |-  ; ; 6 3 1 e. NN
6 8nn0 
 |-  8 e. NN0
7 4nn0 
 |-  4 e. NN0
8 1nn0 
 |-  1 e. NN0
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 e. NN
14 1 13 decnncl 
 |-  ; 6 3 e. NN
15 14 8 8 11 declti 
 |-  1 < ; ; 6 3 1
16 0nn0 
 |-  0 e. NN0
17 2cn 
 |-  2 e. CC
18 17 mul02i 
 |-  ( 0 x. 2 ) = 0
19 1e0p1 
 |-  1 = ( 0 + 1 )
20 3 16 18 19 dec2dvds 
 |-  -. 2 || ; ; 6 3 1
21 2nn0 
 |-  2 e. NN0
22 21 8 deccl 
 |-  ; 2 1 e. NN0
23 22 16 deccl 
 |-  ; ; 2 1 0 e. NN0
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 x. 2 ) = 6
31 30 27 oveq12i 
 |-  ( ( 3 x. 2 ) + ( 0 + 0 ) ) = ( 6 + 0 )
32 6cn 
 |-  6 e. CC
33 32 addid1i 
 |-  ( 6 + 0 ) = 6
34 31 33 eqtri 
 |-  ( ( 3 x. 2 ) + ( 0 + 0 ) ) = 6
35 3t1e3 
 |-  ( 3 x. 1 ) = 3
36 35 oveq1i 
 |-  ( ( 3 x. 1 ) + 0 ) = ( 3 + 0 )
37 3cn 
 |-  3 e. CC
38 37 addid1i 
 |-  ( 3 + 0 ) = 3
39 2 dec0h 
 |-  3 = ; 0 3
40 36 38 39 3eqtri 
 |-  ( ( 3 x. 1 ) + 0 ) = ; 0 3
41 21 8 16 16 26 29 2 2 16 34 40 decma2c 
 |-  ( ( 3 x. ; 2 1 ) + ( 0 + 0 ) ) = ; 6 3
42 37 mul01i 
 |-  ( 3 x. 0 ) = 0
43 42 oveq1i 
 |-  ( ( 3 x. 0 ) + 1 ) = ( 0 + 1 )
44 0p1e1 
 |-  ( 0 + 1 ) = 1
45 43 44 25 3eqtri 
 |-  ( ( 3 x. 0 ) + 1 ) = ; 0 1
46 22 16 16 8 24 25 2 8 16 41 45 decma2c 
 |-  ( ( 3 x. ; ; 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 e. NN
52 9nn0 
 |-  9 e. NN0
53 52 16 deccl 
 |-  ; 9 0 e. NN0
54 eqid 
 |-  ; 9 0 = ; 9 0
55 7nn0 
 |-  7 e. NN0
56 27 oveq2i 
 |-  ( ( 7 x. 9 ) + ( 0 + 0 ) ) = ( ( 7 x. 9 ) + 0 )
57 9cn 
 |-  9 e. CC
58 7cn 
 |-  7 e. CC
59 9t7e63 
 |-  ( 9 x. 7 ) = ; 6 3
60 57 58 59 mulcomli 
 |-  ( 7 x. 9 ) = ; 6 3
61 60 oveq1i 
 |-  ( ( 7 x. 9 ) + 0 ) = ( ; 6 3 + 0 )
62 3 nn0cni 
 |-  ; 6 3 e. CC
63 62 addid1i 
 |-  ( ; 6 3 + 0 ) = ; 6 3
64 56 61 63 3eqtri 
 |-  ( ( 7 x. 9 ) + ( 0 + 0 ) ) = ; 6 3
65 58 mul01i 
 |-  ( 7 x. 0 ) = 0
66 65 oveq1i 
 |-  ( ( 7 x. 0 ) + 1 ) = ( 0 + 1 )
67 66 44 25 3eqtri 
 |-  ( ( 7 x. 0 ) + 1 ) = ; 0 1
68 52 16 16 8 54 25 55 8 16 64 67 decma2c 
 |-  ( ( 7 x. ; 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 e. NN
72 5nn0 
 |-  5 e. NN0
73 72 55 deccl 
 |-  ; 5 7 e. NN0
74 4nn 
 |-  4 e. NN
75 eqid 
 |-  ; 5 7 = ; 5 7
76 7 dec0h 
 |-  4 = ; 0 4
77 8 8 deccl 
 |-  ; 1 1 e. NN0
78 eqid 
 |-  ; 1 1 = ; 1 1
79 8cn 
 |-  8 e. CC
80 79 addid2i 
 |-  ( 0 + 8 ) = 8
81 6 dec0h 
 |-  8 = ; 0 8
82 80 81 eqtri 
 |-  ( 0 + 8 ) = ; 0 8
83 5cn 
 |-  5 e. CC
84 83 mulid2i 
 |-  ( 1 x. 5 ) = 5
85 84 44 oveq12i 
 |-  ( ( 1 x. 5 ) + ( 0 + 1 ) ) = ( 5 + 1 )
86 5p1e6 
 |-  ( 5 + 1 ) = 6
87 85 86 eqtri 
 |-  ( ( 1 x. 5 ) + ( 0 + 1 ) ) = 6
88 84 oveq1i 
 |-  ( ( 1 x. 5 ) + 8 ) = ( 5 + 8 )
89 8p5e13 
 |-  ( 8 + 5 ) = ; 1 3
90 79 83 89 addcomli 
 |-  ( 5 + 8 ) = ; 1 3
91 88 90 eqtri 
 |-  ( ( 1 x. 5 ) + 8 ) = ; 1 3
92 8 8 16 6 78 82 72 2 8 87 91 decmac 
 |-  ( ( ; 1 1 x. 5 ) + ( 0 + 8 ) ) = ; 6 3
93 58 mulid2i 
 |-  ( 1 x. 7 ) = 7
94 93 44 oveq12i 
 |-  ( ( 1 x. 7 ) + ( 0 + 1 ) ) = ( 7 + 1 )
95 7p1e8 
 |-  ( 7 + 1 ) = 8
96 94 95 eqtri 
 |-  ( ( 1 x. 7 ) + ( 0 + 1 ) ) = 8
97 93 oveq1i 
 |-  ( ( 1 x. 7 ) + 4 ) = ( 7 + 4 )
98 7p4e11 
 |-  ( 7 + 4 ) = ; 1 1
99 97 98 eqtri 
 |-  ( ( 1 x. 7 ) + 4 ) = ; 1 1
100 8 8 16 7 78 76 55 8 8 96 99 decmac 
 |-  ( ( ; 1 1 x. 7 ) + 4 ) = ; 8 1
101 72 55 16 7 75 76 77 8 6 92 100 decma2c 
 |-  ( ( ; 1 1 x. ; 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 e. NN
106 7 6 deccl 
 |-  ; 4 8 e. NN0
107 eqid 
 |-  ; 4 8 = ; 4 8
108 55 dec0h 
 |-  7 = ; 0 7
109 8 2 deccl 
 |-  ; 1 3 e. NN0
110 eqid 
 |-  ; 1 3 = ; 1 3
111 77 nn0cni 
 |-  ; 1 1 e. CC
112 111 addid2i 
 |-  ( 0 + ; 1 1 ) = ; 1 1
113 4cn 
 |-  4 e. CC
114 113 mulid2i 
 |-  ( 1 x. 4 ) = 4
115 1p1e2 
 |-  ( 1 + 1 ) = 2
116 114 115 oveq12i 
 |-  ( ( 1 x. 4 ) + ( 1 + 1 ) ) = ( 4 + 2 )
117 4p2e6 
 |-  ( 4 + 2 ) = 6
118 116 117 eqtri 
 |-  ( ( 1 x. 4 ) + ( 1 + 1 ) ) = 6
119 4t3e12 
 |-  ( 4 x. 3 ) = ; 1 2
120 113 37 119 mulcomli 
 |-  ( 3 x. 4 ) = ; 1 2
121 2p1e3 
 |-  ( 2 + 1 ) = 3
122 8 21 8 120 121 decaddi 
 |-  ( ( 3 x. 4 ) + 1 ) = ; 1 3
123 8 2 8 8 110 112 7 2 8 118 122 decmac 
 |-  ( ( ; 1 3 x. 4 ) + ( 0 + ; 1 1 ) ) = ; 6 3
124 79 mulid2i 
 |-  ( 1 x. 8 ) = 8
125 37 addid2i 
 |-  ( 0 + 3 ) = 3
126 124 125 oveq12i 
 |-  ( ( 1 x. 8 ) + ( 0 + 3 ) ) = ( 8 + 3 )
127 8p3e11 
 |-  ( 8 + 3 ) = ; 1 1
128 126 127 eqtri 
 |-  ( ( 1 x. 8 ) + ( 0 + 3 ) ) = ; 1 1
129 8t3e24 
 |-  ( 8 x. 3 ) = ; 2 4
130 79 37 129 mulcomli 
 |-  ( 3 x. 8 ) = ; 2 4
131 58 113 98 addcomli 
 |-  ( 4 + 7 ) = ; 1 1
132 21 7 55 130 121 8 131 decaddci 
 |-  ( ( 3 x. 8 ) + 7 ) = ; 3 1
133 8 2 16 55 110 108 6 8 2 128 132 decmac 
 |-  ( ( ; 1 3 x. 8 ) + 7 ) = ; ; 1 1 1
134 7 6 16 55 107 108 109 8 77 123 133 decma2c 
 |-  ( ( ; 1 3 x. ; 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 e. NN
139 2 55 deccl 
 |-  ; 3 7 e. NN0
140 2nn 
 |-  2 e. NN
141 eqid 
 |-  ; 3 7 = ; 3 7
142 21 dec0h 
 |-  2 = ; 0 2
143 8 55 deccl 
 |-  ; 1 7 e. NN0
144 8 21 deccl 
 |-  ; 1 2 e. NN0
145 eqid 
 |-  ; 1 7 = ; 1 7
146 144 nn0cni 
 |-  ; 1 2 e. CC
147 146 addid2i 
 |-  ( 0 + ; 1 2 ) = ; 1 2
148 37 mulid2i 
 |-  ( 1 x. 3 ) = 3
149 1p2e3 
 |-  ( 1 + 2 ) = 3
150 148 149 oveq12i 
 |-  ( ( 1 x. 3 ) + ( 1 + 2 ) ) = ( 3 + 3 )
151 3p3e6 
 |-  ( 3 + 3 ) = 6
152 150 151 eqtri 
 |-  ( ( 1 x. 3 ) + ( 1 + 2 ) ) = 6
153 7t3e21 
 |-  ( 7 x. 3 ) = ; 2 1
154 21 8 21 153 149 decaddi 
 |-  ( ( 7 x. 3 ) + 2 ) = ; 2 3
155 8 55 8 21 145 147 2 2 21 152 154 decmac 
 |-  ( ( ; 1 7 x. 3 ) + ( 0 + ; 1 2 ) ) = ; 6 3
156 83 addid2i 
 |-  ( 0 + 5 ) = 5
157 93 156 oveq12i 
 |-  ( ( 1 x. 7 ) + ( 0 + 5 ) ) = ( 7 + 5 )
158 7p5e12 
 |-  ( 7 + 5 ) = ; 1 2
159 157 158 eqtri 
 |-  ( ( 1 x. 7 ) + ( 0 + 5 ) ) = ; 1 2
160 7t7e49 
 |-  ( 7 x. 7 ) = ; 4 9
161 4p1e5 
 |-  ( 4 + 1 ) = 5
162 9p2e11 
 |-  ( 9 + 2 ) = ; 1 1
163 7 52 21 160 161 8 162 decaddci 
 |-  ( ( 7 x. 7 ) + 2 ) = ; 5 1
164 8 55 16 21 145 142 55 8 72 159 163 decmac 
 |-  ( ( ; 1 7 x. 7 ) + 2 ) = ; ; 1 2 1
165 2 55 16 21 141 142 143 8 144 155 164 decma2c 
 |-  ( ( ; 1 7 x. ; 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 e. NN
170 8 169 decnncl 
 |-  ; 1 9 e. NN
171 2 2 deccl 
 |-  ; 3 3 e. NN0
172 eqid 
 |-  ; 3 3 = ; 3 3
173 8 52 deccl 
 |-  ; 1 9 e. NN0
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 x. 3 ) + ( 0 + 3 ) ) = ( 3 + 3 )
179 178 151 eqtri 
 |-  ( ( 1 x. 3 ) + ( 0 + 3 ) ) = 6
180 9t3e27 
 |-  ( 9 x. 3 ) = ; 2 7
181 7p6e13 
 |-  ( 7 + 6 ) = ; 1 3
182 21 55 1 180 121 2 181 decaddci 
 |-  ( ( 9 x. 3 ) + 6 ) = ; 3 3
183 8 52 16 1 174 177 2 2 2 179 182 decmac 
 |-  ( ( ; 1 9 x. 3 ) + ( 0 + 6 ) ) = ; 6 3
184 21 55 7 180 121 8 98 decaddci 
 |-  ( ( 9 x. 3 ) + 4 ) = ; 3 1
185 8 52 16 7 174 76 2 8 2 179 184 decmac 
 |-  ( ( ; 1 9 x. 3 ) + 4 ) = ; 6 1
186 2 2 16 7 172 76 173 8 1 183 185 decma2c 
 |-  ( ( ; 1 9 x. ; 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 e. NN
190 21 55 deccl 
 |-  ; 2 7 e. NN0
191 10nn 
 |-  ; 1 0 e. NN
192 eqid 
 |-  ; 2 7 = ; 2 7
193 eqid 
 |-  ; 1 0 = ; 1 0
194 21 2 deccl 
 |-  ; 2 3 e. NN0
195 8 1 deccl 
 |-  ; 1 6 e. NN0
196 eqid 
 |-  ; 2 3 = ; 2 3
197 eqid 
 |-  ; 1 6 = ; 1 6
198 ax-1cn 
 |-  1 e. CC
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 x. 2 ) = 4
203 202 115 oveq12i 
 |-  ( ( 2 x. 2 ) + ( 1 + 1 ) ) = ( 4 + 2 )
204 203 117 eqtri 
 |-  ( ( 2 x. 2 ) + ( 1 + 1 ) ) = 6
205 30 oveq1i 
 |-  ( ( 3 x. 2 ) + 7 ) = ( 6 + 7 )
206 58 32 181 addcomli 
 |-  ( 6 + 7 ) = ; 1 3
207 205 206 eqtri 
 |-  ( ( 3 x. 2 ) + 7 ) = ; 1 3
208 21 2 8 55 196 201 21 2 8 204 207 decmac 
 |-  ( ( ; 2 3 x. 2 ) + ( 1 + ; 1 6 ) ) = ; 6 3
209 7t2e14 
 |-  ( 7 x. 2 ) = ; 1 4
210 58 17 209 mulcomli 
 |-  ( 2 x. 7 ) = ; 1 4
211 8 7 21 210 117 decaddi 
 |-  ( ( 2 x. 7 ) + 2 ) = ; 1 6
212 58 37 153 mulcomli 
 |-  ( 3 x. 7 ) = ; 2 1
213 55 21 2 196 8 21 211 212 decmul1c 
 |-  ( ; 2 3 x. 7 ) = ; ; 1 6 1
214 213 oveq1i 
 |-  ( ( ; 2 3 x. 7 ) + 0 ) = ( ; ; 1 6 1 + 0 )
215 195 8 deccl 
 |-  ; ; 1 6 1 e. NN0
216 215 nn0cni 
 |-  ; ; 1 6 1 e. CC
217 216 addid1i 
 |-  ( ; ; 1 6 1 + 0 ) = ; ; 1 6 1
218 214 217 eqtri 
 |-  ( ( ; 2 3 x. 7 ) + 0 ) = ; ; 1 6 1
219 21 55 8 16 192 193 194 8 195 208 218 decma2c 
 |-  ( ( ; 2 3 x. ; 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 e. Prime