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 \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		3nn0	$$⊢3\in {\mathbb{N}}_0$$
2		1nn0	$$⊢1\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢31\in {\mathbb{N}}_0$$
4		7nn	$$⊢7\in \mathbb{N}$$
5	3 4	decnncl	$$⊢317\in \mathbb{N}$$
6		8nn0	$$⊢8\in {\mathbb{N}}_0$$
7		4nn0	$$⊢4\in {\mathbb{N}}_0$$
8		7nn0	$$⊢7\in {\mathbb{N}}_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 \mathbb{N}$$
14	1 13	decnncl	$$⊢31\in \mathbb{N}$$
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	$$⊢\neg 2\parallel 317$$
19		3nn	$$⊢3\in \mathbb{N}$$
20		10nn0	$$⊢10\in {\mathbb{N}}_0$$
21		5nn0	$$⊢5\in {\mathbb{N}}_0$$
22	20 21	deccl	$$⊢105\in {\mathbb{N}}_0$$
23		2nn	$$⊢2\in \mathbb{N}$$
24		0nn0	$$⊢0\in {\mathbb{N}}_0$$
25		2nn0	$$⊢2\in {\mathbb{N}}_0$$
26		eqid	$$⊢105=105$$
27	25	dec0h	$$⊢2=02$$
28		eqid	$$⊢10=10$$
29		ax-1cn	$$⊢1\in ℂ$$
30	29	addlidi	$$⊢0+1=1$$
31	2	dec0h	$$⊢1=01$$
32	30 31	eqtri	$$⊢0+1=01$$
33		3cn	$$⊢3\in ℂ$$
34	33	mulridi	$$⊢3\cdot 1=3$$
35		00id	$$⊢0+0=0$$
36	34 35	oveq12i	$$⊢3\cdot 1+0+0=3+0$$
37	33	addridi	$$⊢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	$$⊢\neg 3\parallel 317$$
52		2lt5	$$⊢2<5$$
53	3 23 52 47	dec5dvds2	$$⊢\neg 5\parallel 317$$
54	7 21	deccl	$$⊢45\in {\mathbb{N}}_0$$
55		eqid	$$⊢45=45$$
56	33	addlidi	$$⊢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	$$⊢\neg 7\parallel 317$$
68	2 13	decnncl	$$⊢11\in \mathbb{N}$$
69	25 6	deccl	$$⊢28\in {\mathbb{N}}_0$$
70		9nn	$$⊢9\in \mathbb{N}$$
71		9nn0	$$⊢9\in {\mathbb{N}}_0$$
72		eqid	$$⊢28=28$$
73	71	dec0h	$$⊢9=09$$
74	2 2	deccl	$$⊢11\in {\mathbb{N}}_0$$
75		eqid	$$⊢11=11$$
76		9cn	$$⊢9\in ℂ$$
77	76	addlidi	$$⊢0+9=9$$
78	77 73	eqtri	$$⊢0+9=09$$
79		2cn	$$⊢2\in ℂ$$
80	79	mullidi	$$⊢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	mullidi	$$⊢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	$$⊢\neg 11\parallel 317$$
102	2 19	decnncl	$$⊢13\in \mathbb{N}$$
103	25 7	deccl	$$⊢24\in {\mathbb{N}}_0$$
104		5nn	$$⊢5\in \mathbb{N}$$
105		eqid	$$⊢24=24$$
106	21	dec0h	$$⊢5=05$$
107	2 1	deccl	$$⊢13\in {\mathbb{N}}_0$$
108		eqid	$$⊢13=13$$
109	44	addlidi	$$⊢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	mullidi	$$⊢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	$$⊢\neg 13\parallel 317$$
129	2 4	decnncl	$$⊢17\in \mathbb{N}$$
130	2 6	deccl	$$⊢18\in {\mathbb{N}}_0$$
131		eqid	$$⊢18=18$$
132	2 8	deccl	$$⊢17\in {\mathbb{N}}_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	mulridi	$$⊢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	mulridi	$$⊢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 {\mathbb{N}}_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	$$⊢\neg 17\parallel 317$$
161	2 70	decnncl	$$⊢19\in \mathbb{N}$$
162	2 151	deccl	$$⊢16\in {\mathbb{N}}_0$$
163		eqid	$$⊢16=16$$
164	2 71	deccl	$$⊢19\in {\mathbb{N}}_0$$
165		eqid	$$⊢19=19$$
166	24 2 2 2 31 75 30 138	decadd	$$⊢1+11=12$$
167	76	mulridi	$$⊢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	mullidi	$$⊢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	$$⊢\neg 19\parallel 317$$
184	25 19	decnncl	$$⊢23\in \mathbb{N}$$
185	102	nnnn0i	$$⊢13\in {\mathbb{N}}_0$$
186		8nn	$$⊢8\in \mathbb{N}$$
187	2 186	decnncl	$$⊢18\in \mathbb{N}$$
188	25 1	deccl	$$⊢23\in {\mathbb{N}}_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	mulridi	$$⊢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	$$⊢\neg 23\parallel 317$$
213	5 12 15 18 51 53 67 101 128 160 183 212	prmlem2	$$⊢317\in \mathbb{P}$$