Theorem 163prm

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

	Ref	Expression
Assertion	163prm	$$⊢163\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		1nn0	$$⊢1\in {\mathbb{N}}_0$$
2		6nn0	$$⊢6\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢16\in {\mathbb{N}}_0$$
4		3nn	$$⊢3\in \mathbb{N}$$
5	3 4	decnncl	$$⊢163\in \mathbb{N}$$
6		8nn0	$$⊢8\in {\mathbb{N}}_0$$
7		4nn0	$$⊢4\in {\mathbb{N}}_0$$
8		3nn0	$$⊢3\in {\mathbb{N}}_0$$
9		1lt8	$$⊢1<8$$
10		6lt10	$$⊢6<10$$
11		3lt10	$$⊢3<10$$
12	1 6 2 7 8 1 9 10 11	3decltc	$$⊢163<841$$
13		6nn	$$⊢6\in \mathbb{N}$$
14	1 13	decnncl	$$⊢16\in \mathbb{N}$$
15		1lt10	$$⊢1<10$$
16	14 8 1 15	declti	$$⊢1<163$$
17		2cn	$$⊢2\in ℂ$$
18	17	mullidi	$$⊢1\cdot 2=2$$
19		df-3	$$⊢3=2+1$$
20	3 1 18 19	dec2dvds	$$⊢\neg 2\parallel 163$$
21		5nn0	$$⊢5\in {\mathbb{N}}_0$$
22	21 7	deccl	$$⊢54\in {\mathbb{N}}_0$$
23		1nn	$$⊢1\in \mathbb{N}$$
24		0nn0	$$⊢0\in {\mathbb{N}}_0$$
25		eqid	$$⊢54=54$$
26	1	dec0h	$$⊢1=01$$
27		ax-1cn	$$⊢1\in ℂ$$
28	27	addlidi	$$⊢0+1=1$$
29	28	oveq2i	$$⊢3\cdot 5+0+1=3\cdot 5+1$$
30		5p1e6	$$⊢5+1=6$$
31		5cn	$$⊢5\in ℂ$$
32		3cn	$$⊢3\in ℂ$$
33		5t3e15	$$⊢5\cdot 3=15$$
34	31 32 33	mulcomli	$$⊢3\cdot 5=15$$
35	1 21 30 34	decsuc	$$⊢3\cdot 5+1=16$$
36	29 35	eqtri	$$⊢3\cdot 5+0+1=16$$
37		2nn0	$$⊢2\in {\mathbb{N}}_0$$
38		2p1e3	$$⊢2+1=3$$
39		4cn	$$⊢4\in ℂ$$
40		4t3e12	$$⊢4\cdot 3=12$$
41	39 32 40	mulcomli	$$⊢3\cdot 4=12$$
42	1 37 38 41	decsuc	$$⊢3\cdot 4+1=13$$
43	21 7 24 1 25 26 8 8 1 36 42	decma2c	$$⊢3\cdot 54+1=163$$
44		1lt3	$$⊢1<3$$
45	4 22 23 43 44	ndvdsi	$$⊢\neg 3\parallel 163$$
46		3lt5	$$⊢3<5$$
47	3 4 46	dec5dvds	$$⊢\neg 5\parallel 163$$
48		7nn	$$⊢7\in \mathbb{N}$$
49	37 8	deccl	$$⊢23\in {\mathbb{N}}_0$$
50		2nn	$$⊢2\in \mathbb{N}$$
51		eqid	$$⊢23=23$$
52	37	dec0h	$$⊢2=02$$
53		7nn0	$$⊢7\in {\mathbb{N}}_0$$
54	17	addlidi	$$⊢0+2=2$$
55	54	oveq2i	$$⊢7\cdot 2+0+2=7\cdot 2+2$$
56		7t2e14	$$⊢7\cdot 2=14$$
57		4p2e6	$$⊢4+2=6$$
58	1 7 37 56 57	decaddi	$$⊢7\cdot 2+2=16$$
59	55 58	eqtri	$$⊢7\cdot 2+0+2=16$$
60		7t3e21	$$⊢7\cdot 3=21$$
61		1p2e3	$$⊢1+2=3$$
62	37 1 37 60 61	decaddi	$$⊢7\cdot 3+2=23$$
63	37 8 24 37 51 52 53 8 37 59 62	decma2c	$$⊢7\cdot 23+2=163$$
64		2lt7	$$⊢2<7$$
65	48 49 50 63 64	ndvdsi	$$⊢\neg 7\parallel 163$$
66	1 23	decnncl	$$⊢11\in \mathbb{N}$$
67	1 7	deccl	$$⊢14\in {\mathbb{N}}_0$$
68		9nn	$$⊢9\in \mathbb{N}$$
69		9nn0	$$⊢9\in {\mathbb{N}}_0$$
70		eqid	$$⊢14=14$$
71	69	dec0h	$$⊢9=09$$
72	1 1	deccl	$$⊢11\in {\mathbb{N}}_0$$
73	31	addlidi	$$⊢0+5=5$$
74	73	oveq2i	$$⊢11\cdot 1+0+5=11\cdot 1+5$$
75	66	nncni	$$⊢11\in ℂ$$
76	75	mulridi	$$⊢11\cdot 1=11$$
77	31 27 30	addcomli	$$⊢1+5=6$$
78	1 1 21 76 77	decaddi	$$⊢11\cdot 1+5=16$$
79	74 78	eqtri	$$⊢11\cdot 1+0+5=16$$
80		eqid	$$⊢11=11$$
81	39	mullidi	$$⊢1\cdot 4=4$$
82	81 28	oveq12i	$$⊢1\cdot 4+0+1=4+1$$
83		4p1e5	$$⊢4+1=5$$
84	82 83	eqtri	$$⊢1\cdot 4+0+1=5$$
85	81	oveq1i	$$⊢1\cdot 4+9=4+9$$
86		9cn	$$⊢9\in ℂ$$
87		9p4e13	$$⊢9+4=13$$
88	86 39 87	addcomli	$$⊢4+9=13$$
89	85 88	eqtri	$$⊢1\cdot 4+9=13$$
90	1 1 24 69 80 71 7 8 1 84 89	decmac	$$⊢11\cdot 4+9=53$$
91	1 7 24 69 70 71 72 8 21 79 90	decma2c	$$⊢11\cdot 14+9=163$$
92		9lt10	$$⊢9<10$$
93	23 1 69 92	declti	$$⊢9<11$$
94	66 67 68 91 93	ndvdsi	$$⊢\neg 11\parallel 163$$
95	1 4	decnncl	$$⊢13\in \mathbb{N}$$
96	1 37	deccl	$$⊢12\in {\mathbb{N}}_0$$
97		eqid	$$⊢12=12$$
98	53	dec0h	$$⊢7=07$$
99	1 8	deccl	$$⊢13\in {\mathbb{N}}_0$$
100		eqid	$$⊢13=13$$
101	32	addlidi	$$⊢0+3=3$$
102	8	dec0h	$$⊢3=03$$
103	101 102	eqtri	$$⊢0+3=03$$
104	27	mulridi	$$⊢1\cdot 1=1$$
105		00id	$$⊢0+0=0$$
106	104 105	oveq12i	$$⊢1\cdot 1+0+0=1+0$$
107	27	addridi	$$⊢1+0=1$$
108	106 107	eqtri	$$⊢1\cdot 1+0+0=1$$
109	32	mulridi	$$⊢3\cdot 1=3$$
110	109	oveq1i	$$⊢3\cdot 1+3=3+3$$
111		3p3e6	$$⊢3+3=6$$
112	110 111	eqtri	$$⊢3\cdot 1+3=6$$
113	2	dec0h	$$⊢6=06$$
114	112 113	eqtri	$$⊢3\cdot 1+3=06$$
115	1 8 24 8 100 103 1 2 24 108 114	decmac	$$⊢13\cdot 1+0+3=16$$
116	18 28	oveq12i	$$⊢1\cdot 2+0+1=2+1$$
117	116 38	eqtri	$$⊢1\cdot 2+0+1=3$$
118		3t2e6	$$⊢3\cdot 2=6$$
119	118	oveq1i	$$⊢3\cdot 2+7=6+7$$
120		7cn	$$⊢7\in ℂ$$
121		6cn	$$⊢6\in ℂ$$
122		7p6e13	$$⊢7+6=13$$
123	120 121 122	addcomli	$$⊢6+7=13$$
124	119 123	eqtri	$$⊢3\cdot 2+7=13$$
125	1 8 24 53 100 98 37 8 1 117 124	decmac	$$⊢13\cdot 2+7=33$$
126	1 37 24 53 97 98 99 8 8 115 125	decma2c	$$⊢13\cdot 12+7=163$$
127		7lt10	$$⊢7<10$$
128	23 8 53 127	declti	$$⊢7<13$$
129	95 96 48 126 128	ndvdsi	$$⊢\neg 13\parallel 163$$
130	1 48	decnncl	$$⊢17\in \mathbb{N}$$
131		10nn	$$⊢10\in \mathbb{N}$$
132		eqid	$$⊢17=17$$
133		eqid	$$⊢10=10$$
134	86	mullidi	$$⊢1\cdot 9=9$$
135		6p1e7	$$⊢6+1=7$$
136	121 27 135	addcomli	$$⊢1+6=7$$
137	134 136	oveq12i	$$⊢1\cdot 9+1+6=9+7$$
138		9p7e16	$$⊢9+7=16$$
139	137 138	eqtri	$$⊢1\cdot 9+1+6=16$$
140		9t7e63	$$⊢9\cdot 7=63$$
141	86 120 140	mulcomli	$$⊢7\cdot 9=63$$
142	141	oveq1i	$$⊢7\cdot 9+0=63+0$$
143	2 8	deccl	$$⊢63\in {\mathbb{N}}_0$$
144	143	nn0cni	$$⊢63\in ℂ$$
145	144	addridi	$$⊢63+0=63$$
146	142 145	eqtri	$$⊢7\cdot 9+0=63$$
147	1 53 1 24 132 133 69 8 2 139 146	decmac	$$⊢17\cdot 9+10=163$$
148		7pos	$$⊢0<7$$
149	1 24 48 148	declt	$$⊢10<17$$
150	130 69 131 147 149	ndvdsi	$$⊢\neg 17\parallel 163$$
151	1 68	decnncl	$$⊢19\in \mathbb{N}$$
152		eqid	$$⊢19=19$$
153		8cn	$$⊢8\in ℂ$$
154	153	mullidi	$$⊢1\cdot 8=8$$
155		7p1e8	$$⊢7+1=8$$
156	120 27 155	addcomli	$$⊢1+7=8$$
157	154 156	oveq12i	$$⊢1\cdot 8+1+7=8+8$$
158		8p8e16	$$⊢8+8=16$$
159	157 158	eqtri	$$⊢1\cdot 8+1+7=16$$
160		9t8e72	$$⊢9\cdot 8=72$$
161	53 37 38 160	decsuc	$$⊢9\cdot 8+1=73$$
162	1 69 1 1 152 80 6 8 53 159 161	decmac	$$⊢19\cdot 8+11=163$$
163		1lt9	$$⊢1<9$$
164	1 1 68 163	declt	$$⊢11<19$$
165	151 6 66 162 164	ndvdsi	$$⊢\neg 19\parallel 163$$
166	37 4	decnncl	$$⊢23\in \mathbb{N}$$
167	120 17 56	mulcomli	$$⊢2\cdot 7=14$$
168	1 7 37 167 57	decaddi	$$⊢2\cdot 7+2=16$$
169	120 32 60	mulcomli	$$⊢3\cdot 7=21$$
170	37 1 37 169 61	decaddi	$$⊢3\cdot 7+2=23$$
171	37 8 37 51 53 8 37 168 170	decrmac	$$⊢23\cdot 7+2=163$$
172		2lt10	$$⊢2<10$$
173	50 8 37 172	declti	$$⊢2<23$$
174	166 53 50 171 173	ndvdsi	$$⊢\neg 23\parallel 163$$
175	5 12 16 20 45 47 65 94 129 150 165 174	prmlem2	$$⊢163\in \mathbb{P}$$