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

Proof

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