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

Proof

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