# Metamath Proof Explorer

## Theorem 317prm

Description: 317 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014) (Proof shortened by Mario Carneiro, 20-Apr-2015)

Ref Expression
Assertion 317prm ${⊢}317\in ℙ$

### Proof

Step Hyp Ref Expression
1 3nn0 ${⊢}3\in {ℕ}_{0}$
2 1nn0 ${⊢}1\in {ℕ}_{0}$
3 1 2 deccl ${⊢}31\in {ℕ}_{0}$
4 7nn ${⊢}7\in ℕ$
5 3 4 decnncl ${⊢}317\in ℕ$
6 8nn0 ${⊢}8\in {ℕ}_{0}$
7 4nn0 ${⊢}4\in {ℕ}_{0}$
8 7nn0 ${⊢}7\in {ℕ}_{0}$
9 3lt8 ${⊢}3<8$
10 1lt10 ${⊢}1<10$
11 7lt10 ${⊢}7<10$
12 1 6 2 7 8 2 9 10 11 3decltc ${⊢}317<841$
13 1nn ${⊢}1\in ℕ$
14 1 13 decnncl ${⊢}31\in ℕ$
15 14 8 2 10 declti ${⊢}1<317$
16 3t2e6 ${⊢}3\cdot 2=6$
17 df-7 ${⊢}7=6+1$
18 3 1 16 17 dec2dvds ${⊢}¬2\parallel 317$
19 3nn ${⊢}3\in ℕ$
20 10nn0 ${⊢}10\in {ℕ}_{0}$
21 5nn0 ${⊢}5\in {ℕ}_{0}$
22 20 21 deccl ${⊢}105\in {ℕ}_{0}$
23 2nn ${⊢}2\in ℕ$
24 0nn0 ${⊢}0\in {ℕ}_{0}$
25 2nn0 ${⊢}2\in {ℕ}_{0}$
26 eqid ${⊢}105=105$
27 25 dec0h ${⊢}2=02$
28 eqid ${⊢}10=10$
29 ax-1cn ${⊢}1\in ℂ$
30 29 addid2i ${⊢}0+1=1$
31 2 dec0h ${⊢}1=01$
32 30 31 eqtri ${⊢}0+1=01$
33 3cn ${⊢}3\in ℂ$
34 33 mulid1i ${⊢}3\cdot 1=3$
35 00id ${⊢}0+0=0$
36 34 35 oveq12i ${⊢}3\cdot 1+0+0=3+0$
37 33 addid1i ${⊢}3+0=3$
38 36 37 eqtri ${⊢}3\cdot 1+0+0=3$
39 33 mul01i ${⊢}3\cdot 0=0$
40 39 oveq1i ${⊢}3\cdot 0+1=0+1$
41 40 30 eqtri ${⊢}3\cdot 0+1=1$
42 41 31 eqtri ${⊢}3\cdot 0+1=01$
43 2 24 24 2 28 32 1 2 24 38 42 decma2c ${⊢}3\cdot 10+0+1=31$
44 5cn ${⊢}5\in ℂ$
45 5t3e15 ${⊢}5\cdot 3=15$
46 44 33 45 mulcomli ${⊢}3\cdot 5=15$
47 5p2e7 ${⊢}5+2=7$
48 2 21 25 46 47 decaddi ${⊢}3\cdot 5+2=17$
49 20 21 24 25 26 27 1 8 2 43 48 decma2c ${⊢}3\cdot 105+2=317$
50 2lt3 ${⊢}2<3$
51 19 22 23 49 50 ndvdsi ${⊢}¬3\parallel 317$
52 2lt5 ${⊢}2<5$
53 3 23 52 47 dec5dvds2 ${⊢}¬5\parallel 317$
54 7 21 deccl ${⊢}45\in {ℕ}_{0}$
55 eqid ${⊢}45=45$
56 33 addid2i ${⊢}0+3=3$
57 56 oveq2i ${⊢}7\cdot 4+0+3=7\cdot 4+3$
58 7t4e28 ${⊢}7\cdot 4=28$
59 2p1e3 ${⊢}2+1=3$
60 8p3e11 ${⊢}8+3=11$
61 25 6 1 58 59 2 60 decaddci ${⊢}7\cdot 4+3=31$
62 57 61 eqtri ${⊢}7\cdot 4+0+3=31$
63 7t5e35 ${⊢}7\cdot 5=35$
64 1 21 25 63 47 decaddi ${⊢}7\cdot 5+2=37$
65 7 21 24 25 55 27 8 8 1 62 64 decma2c ${⊢}7\cdot 45+2=317$
66 2lt7 ${⊢}2<7$
67 4 54 23 65 66 ndvdsi ${⊢}¬7\parallel 317$
68 2 13 decnncl ${⊢}11\in ℕ$
69 25 6 deccl ${⊢}28\in {ℕ}_{0}$
70 9nn ${⊢}9\in ℕ$
71 9nn0 ${⊢}9\in {ℕ}_{0}$
72 eqid ${⊢}28=28$
73 71 dec0h ${⊢}9=09$
74 2 2 deccl ${⊢}11\in {ℕ}_{0}$
75 eqid ${⊢}11=11$
76 9cn ${⊢}9\in ℂ$
77 76 addid2i ${⊢}0+9=9$
78 77 73 eqtri ${⊢}0+9=09$
79 2cn ${⊢}2\in ℂ$
80 79 mulid2i ${⊢}1\cdot 2=2$
81 80 30 oveq12i ${⊢}1\cdot 2+0+1=2+1$
82 81 59 eqtri ${⊢}1\cdot 2+0+1=3$
83 80 oveq1i ${⊢}1\cdot 2+9=2+9$
84 9p2e11 ${⊢}9+2=11$
85 76 79 84 addcomli ${⊢}2+9=11$
86 83 85 eqtri ${⊢}1\cdot 2+9=11$
87 2 2 24 71 75 78 25 2 2 82 86 decmac ${⊢}11\cdot 2+0+9=31$
88 8cn ${⊢}8\in ℂ$
89 88 mulid2i ${⊢}1\cdot 8=8$
90 89 30 oveq12i ${⊢}1\cdot 8+0+1=8+1$
91 8p1e9 ${⊢}8+1=9$
92 90 91 eqtri ${⊢}1\cdot 8+0+1=9$
93 89 oveq1i ${⊢}1\cdot 8+9=8+9$
94 9p8e17 ${⊢}9+8=17$
95 76 88 94 addcomli ${⊢}8+9=17$
96 93 95 eqtri ${⊢}1\cdot 8+9=17$
97 2 2 24 71 75 73 6 8 2 92 96 decmac ${⊢}11\cdot 8+9=97$
98 25 6 24 71 72 73 74 8 71 87 97 decma2c ${⊢}11\cdot 28+9=317$
99 9lt10 ${⊢}9<10$
100 13 2 71 99 declti ${⊢}9<11$
101 68 69 70 98 100 ndvdsi ${⊢}¬11\parallel 317$
102 2 19 decnncl ${⊢}13\in ℕ$
103 25 7 deccl ${⊢}24\in {ℕ}_{0}$
104 5nn ${⊢}5\in ℕ$
105 eqid ${⊢}24=24$
106 21 dec0h ${⊢}5=05$
107 2 1 deccl ${⊢}13\in {ℕ}_{0}$
108 eqid ${⊢}13=13$
109 44 addid2i ${⊢}0+5=5$
110 109 106 eqtri ${⊢}0+5=05$
111 16 oveq1i ${⊢}3\cdot 2+5=6+5$
112 6p5e11 ${⊢}6+5=11$
113 111 112 eqtri ${⊢}3\cdot 2+5=11$
114 2 1 24 21 108 110 25 2 2 82 113 decmac ${⊢}13\cdot 2+0+5=31$
115 4cn ${⊢}4\in ℂ$
116 115 mulid2i ${⊢}1\cdot 4=4$
117 116 30 oveq12i ${⊢}1\cdot 4+0+1=4+1$
118 4p1e5 ${⊢}4+1=5$
119 117 118 eqtri ${⊢}1\cdot 4+0+1=5$
120 4t3e12 ${⊢}4\cdot 3=12$
121 115 33 120 mulcomli ${⊢}3\cdot 4=12$
122 44 79 47 addcomli ${⊢}2+5=7$
123 2 25 21 121 122 decaddi ${⊢}3\cdot 4+5=17$
124 2 1 24 21 108 106 7 8 2 119 123 decmac ${⊢}13\cdot 4+5=57$
125 25 7 24 21 105 106 107 8 21 114 124 decma2c ${⊢}13\cdot 24+5=317$
126 5lt10 ${⊢}5<10$
127 13 1 21 126 declti ${⊢}5<13$
128 102 103 104 125 127 ndvdsi ${⊢}¬13\parallel 317$
129 2 4 decnncl ${⊢}17\in ℕ$
130 2 6 deccl ${⊢}18\in {ℕ}_{0}$
131 eqid ${⊢}18=18$
132 2 8 deccl ${⊢}17\in {ℕ}_{0}$
133 eqid ${⊢}17=17$
134 3p1e4 ${⊢}3+1=4$
135 33 29 134 addcomli ${⊢}1+3=4$
136 24 2 2 1 31 108 30 135 decadd ${⊢}1+13=14$
137 29 mulid1i ${⊢}1\cdot 1=1$
138 1p1e2 ${⊢}1+1=2$
139 137 138 oveq12i ${⊢}1\cdot 1+1+1=1+2$
140 1p2e3 ${⊢}1+2=3$
141 139 140 eqtri ${⊢}1\cdot 1+1+1=3$
142 7cn ${⊢}7\in ℂ$
143 142 mulid1i ${⊢}7\cdot 1=7$
144 143 oveq1i ${⊢}7\cdot 1+4=7+4$
145 7p4e11 ${⊢}7+4=11$
146 144 145 eqtri ${⊢}7\cdot 1+4=11$
147 2 8 2 7 133 136 2 2 2 141 146 decmac ${⊢}17\cdot 1+1+13=31$
148 89 109 oveq12i ${⊢}1\cdot 8+0+5=8+5$
149 8p5e13 ${⊢}8+5=13$
150 148 149 eqtri ${⊢}1\cdot 8+0+5=13$
151 6nn0 ${⊢}6\in {ℕ}_{0}$
152 6p1e7 ${⊢}6+1=7$
153 8t7e56 ${⊢}8\cdot 7=56$
154 88 142 153 mulcomli ${⊢}7\cdot 8=56$
155 21 151 152 154 decsuc ${⊢}7\cdot 8+1=57$
156 2 8 24 2 133 31 6 8 21 150 155 decmac ${⊢}17\cdot 8+1=137$
157 2 6 2 2 131 75 132 8 107 147 156 decma2c ${⊢}17\cdot 18+11=317$
158 1lt7 ${⊢}1<7$
159 2 2 4 158 declt ${⊢}11<17$
160 129 130 68 157 159 ndvdsi ${⊢}¬17\parallel 317$
161 2 70 decnncl ${⊢}19\in ℕ$
162 2 151 deccl ${⊢}16\in {ℕ}_{0}$
163 eqid ${⊢}16=16$
164 2 71 deccl ${⊢}19\in {ℕ}_{0}$
165 eqid ${⊢}19=19$
166 24 2 2 2 31 75 30 138 decadd ${⊢}1+11=12$
167 76 mulid1i ${⊢}9\cdot 1=9$
168 167 oveq1i ${⊢}9\cdot 1+2=9+2$
169 168 84 eqtri ${⊢}9\cdot 1+2=11$
170 2 71 2 25 165 166 2 2 2 141 169 decmac ${⊢}19\cdot 1+1+11=31$
171 1 dec0h ${⊢}3=03$
172 6cn ${⊢}6\in ℂ$
173 172 mulid2i ${⊢}1\cdot 6=6$
174 173 109 oveq12i ${⊢}1\cdot 6+0+5=6+5$
175 174 112 eqtri ${⊢}1\cdot 6+0+5=11$
176 9t6e54 ${⊢}9\cdot 6=54$
177 4p3e7 ${⊢}4+3=7$
178 21 7 1 176 177 decaddi ${⊢}9\cdot 6+3=57$
179 2 71 24 1 165 171 151 8 21 175 178 decmac ${⊢}19\cdot 6+3=117$
180 2 151 2 1 163 108 164 8 74 170 179 decma2c ${⊢}19\cdot 16+13=317$
181 3lt9 ${⊢}3<9$
182 2 1 70 181 declt ${⊢}13<19$
183 161 162 102 180 182 ndvdsi ${⊢}¬19\parallel 317$
184 25 19 decnncl ${⊢}23\in ℕ$
185 102 nnnn0i ${⊢}13\in {ℕ}_{0}$
186 8nn ${⊢}8\in ℕ$
187 2 186 decnncl ${⊢}18\in ℕ$
188 25 1 deccl ${⊢}23\in {ℕ}_{0}$
189 eqid ${⊢}23=23$
190 7p1e8 ${⊢}7+1=8$
191 142 29 190 addcomli ${⊢}1+7=8$
192 6 dec0h ${⊢}8=08$
193 191 192 eqtri ${⊢}1+7=08$
194 79 mulid1i ${⊢}2\cdot 1=2$
195 194 30 oveq12i ${⊢}2\cdot 1+0+1=2+1$
196 195 59 eqtri ${⊢}2\cdot 1+0+1=3$
197 34 oveq1i ${⊢}3\cdot 1+8=3+8$
198 88 33 60 addcomli ${⊢}3+8=11$
199 197 198 eqtri ${⊢}3\cdot 1+8=11$
200 25 1 24 6 189 193 2 2 2 196 199 decmac ${⊢}23\cdot 1+1+7=31$
201 33 79 16 mulcomli ${⊢}2\cdot 3=6$
202 201 30 oveq12i ${⊢}2\cdot 3+0+1=6+1$
203 202 152 eqtri ${⊢}2\cdot 3+0+1=7$
204 3t3e9 ${⊢}3\cdot 3=9$
205 204 oveq1i ${⊢}3\cdot 3+8=9+8$
206 205 94 eqtri ${⊢}3\cdot 3+8=17$
207 25 1 24 6 189 192 1 8 2 203 206 decmac ${⊢}23\cdot 3+8=77$
208 2 1 2 6 108 131 188 8 8 200 207 decma2c ${⊢}23\cdot 13+18=317$
209 8lt10 ${⊢}8<10$
210 1lt2 ${⊢}1<2$
211 2 25 6 1 209 210 decltc ${⊢}18<23$
212 184 185 187 208 211 ndvdsi ${⊢}¬23\parallel 317$
213 5 12 15 18 51 53 67 101 128 160 183 212 prmlem2 ${⊢}317\in ℙ$