Theorem 83prm

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

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

Proof

Step	Hyp	Ref	Expression
1		8nn0	$$⊢8\in {\mathbb{N}}_0$$
2		3nn	$$⊢3\in \mathbb{N}$$
3	1 2	decnncl	$$⊢83\in \mathbb{N}$$
4		4nn0	$$⊢4\in {\mathbb{N}}_0$$
5	1 4	deccl	$$⊢84\in {\mathbb{N}}_0$$
6		3nn0	$$⊢3\in {\mathbb{N}}_0$$
7		1nn0	$$⊢1\in {\mathbb{N}}_0$$
8		3lt10	$$⊢3<10$$
9		8nn	$$⊢8\in \mathbb{N}$$
10		8lt10	$$⊢8<10$$
11	9 4 1 10	declti	$$⊢8<84$$
12	1 5 6 7 8 11	decltc	$$⊢83<841$$
13		1lt10	$$⊢1<10$$
14	9 6 7 13	declti	$$⊢1<83$$
15		2cn	$$⊢2\in ℂ$$
16	15	mullidi	$$⊢1\cdot 2=2$$
17		df-3	$$⊢3=2+1$$
18	1 7 16 17	dec2dvds	$$⊢\neg 2\parallel 83$$
19		2nn0	$$⊢2\in {\mathbb{N}}_0$$
20		7nn0	$$⊢7\in {\mathbb{N}}_0$$
21	19 20	deccl	$$⊢27\in {\mathbb{N}}_0$$
22		2nn	$$⊢2\in \mathbb{N}$$
23		0nn0	$$⊢0\in {\mathbb{N}}_0$$
24		eqid	$$⊢27=27$$
25	19	dec0h	$$⊢2=02$$
26		3t2e6	$$⊢3\cdot 2=6$$
27	15	addlidi	$$⊢0+2=2$$
28	26 27	oveq12i	$$⊢3\cdot 2+0+2=6+2$$
29		6p2e8	$$⊢6+2=8$$
30	28 29	eqtri	$$⊢3\cdot 2+0+2=8$$
31		7cn	$$⊢7\in ℂ$$
32		3cn	$$⊢3\in ℂ$$
33		7t3e21	$$⊢7\cdot 3=21$$
34	31 32 33	mulcomli	$$⊢3\cdot 7=21$$
35		1p2e3	$$⊢1+2=3$$
36	19 7 19 34 35	decaddi	$$⊢3\cdot 7+2=23$$
37	19 20 23 19 24 25 6 6 19 30 36	decma2c	$$⊢3\cdot 27+2=83$$
38		2lt3	$$⊢2<3$$
39	2 21 22 37 38	ndvdsi	$$⊢\neg 3\parallel 83$$
40		3lt5	$$⊢3<5$$
41	1 2 40	dec5dvds	$$⊢\neg 5\parallel 83$$
42		7nn	$$⊢7\in \mathbb{N}$$
43	7 7	deccl	$$⊢11\in {\mathbb{N}}_0$$
44		6nn	$$⊢6\in \mathbb{N}$$
45		6nn0	$$⊢6\in {\mathbb{N}}_0$$
46		eqid	$$⊢11=11$$
47	45	dec0h	$$⊢6=06$$
48	31	mulridi	$$⊢7\cdot 1=7$$
49		ax-1cn	$$⊢1\in ℂ$$
50	49	addlidi	$$⊢0+1=1$$
51	48 50	oveq12i	$$⊢7\cdot 1+0+1=7+1$$
52		7p1e8	$$⊢7+1=8$$
53	51 52	eqtri	$$⊢7\cdot 1+0+1=8$$
54	48	oveq1i	$$⊢7\cdot 1+6=7+6$$
55		7p6e13	$$⊢7+6=13$$
56	54 55	eqtri	$$⊢7\cdot 1+6=13$$
57	7 7 23 45 46 47 20 6 7 53 56	decma2c	$$⊢7\cdot 11+6=83$$
58		6lt7	$$⊢6<7$$
59	42 43 44 57 58	ndvdsi	$$⊢\neg 7\parallel 83$$
60		11nn	$$⊢11\in \mathbb{N}$$
61		1nn	$$⊢1\in \mathbb{N}$$
62	7 61	decnncl	$$⊢11\in \mathbb{N}$$
63	62	nncni	$$⊢11\in ℂ$$
64	63 31	mulcomi	$$⊢11\cdot 7=7\cdot 11$$
65	64	oveq1i	$$⊢11\cdot 7+6=7\cdot 11+6$$
66	65 57	eqtri	$$⊢11\cdot 7+6=83$$
67		6lt10	$$⊢6<10$$
68	61 7 45 67	declti	$$⊢6<11$$
69	60 20 44 66 68	ndvdsi	$$⊢\neg 11\parallel 83$$
70	7 2	decnncl	$$⊢13\in \mathbb{N}$$
71		5nn	$$⊢5\in \mathbb{N}$$
72		5nn0	$$⊢5\in {\mathbb{N}}_0$$
73		eqid	$$⊢13=13$$
74	72	dec0h	$$⊢5=05$$
75		6cn	$$⊢6\in ℂ$$
76	75	mullidi	$$⊢1\cdot 6=6$$
77	76 27	oveq12i	$$⊢1\cdot 6+0+2=6+2$$
78	77 29	eqtri	$$⊢1\cdot 6+0+2=8$$
79		6t3e18	$$⊢6\cdot 3=18$$
80	75 32 79	mulcomli	$$⊢3\cdot 6=18$$
81		1p1e2	$$⊢1+1=2$$
82		8p5e13	$$⊢8+5=13$$
83	7 1 72 80 81 6 82	decaddci	$$⊢3\cdot 6+5=23$$
84	7 6 23 72 73 74 45 6 19 78 83	decmac	$$⊢13\cdot 6+5=83$$
85		5lt10	$$⊢5<10$$
86	61 6 72 85	declti	$$⊢5<13$$
87	70 45 71 84 86	ndvdsi	$$⊢\neg 13\parallel 83$$
88	7 42	decnncl	$$⊢17\in \mathbb{N}$$
89	7 71	decnncl	$$⊢15\in \mathbb{N}$$
90		eqid	$$⊢17=17$$
91		eqid	$$⊢15=15$$
92		4cn	$$⊢4\in ℂ$$
93	92	mullidi	$$⊢1\cdot 4=4$$
94		3p1e4	$$⊢3+1=4$$
95	32 49 94	addcomli	$$⊢1+3=4$$
96	93 95	oveq12i	$$⊢1\cdot 4+1+3=4+4$$
97		4p4e8	$$⊢4+4=8$$
98	96 97	eqtri	$$⊢1\cdot 4+1+3=8$$
99		7t4e28	$$⊢7\cdot 4=28$$
100		2p1e3	$$⊢2+1=3$$
101	19 1 72 99 100 6 82	decaddci	$$⊢7\cdot 4+5=33$$
102	7 20 7 72 90 91 4 6 6 98 101	decmac	$$⊢17\cdot 4+15=83$$
103		5lt7	$$⊢5<7$$
104	7 72 42 103	declt	$$⊢15<17$$
105	88 4 89 102 104	ndvdsi	$$⊢\neg 17\parallel 83$$
106		9nn	$$⊢9\in \mathbb{N}$$
107	7 106	decnncl	$$⊢19\in \mathbb{N}$$
108		9nn0	$$⊢9\in {\mathbb{N}}_0$$
109		eqid	$$⊢19=19$$
110	20	dec0h	$$⊢7=07$$
111	92	addlidi	$$⊢0+4=4$$
112	93 111	oveq12i	$$⊢1\cdot 4+0+4=4+4$$
113	112 97	eqtri	$$⊢1\cdot 4+0+4=8$$
114		9t4e36	$$⊢9\cdot 4=36$$
115	31 75 55	addcomli	$$⊢6+7=13$$
116	6 45 20 114 94 6 115	decaddci	$$⊢9\cdot 4+7=43$$
117	7 108 23 20 109 110 4 6 4 113 116	decmac	$$⊢19\cdot 4+7=83$$
118		7lt10	$$⊢7<10$$
119	61 108 20 118	declti	$$⊢7<19$$
120	107 4 42 117 119	ndvdsi	$$⊢\neg 19\parallel 83$$
121	19 2	decnncl	$$⊢23\in \mathbb{N}$$
122		4nn	$$⊢4\in \mathbb{N}$$
123	7 122	decnncl	$$⊢14\in \mathbb{N}$$
124		eqid	$$⊢23=23$$
125		eqid	$$⊢14=14$$
126		2t3e6	$$⊢2\cdot 3=6$$
127	126 81	oveq12i	$$⊢2\cdot 3+1+1=6+2$$
128	127 29	eqtri	$$⊢2\cdot 3+1+1=8$$
129		3t3e9	$$⊢3\cdot 3=9$$
130	129	oveq1i	$$⊢3\cdot 3+4=9+4$$
131		9p4e13	$$⊢9+4=13$$
132	130 131	eqtri	$$⊢3\cdot 3+4=13$$
133	19 6 7 4 124 125 6 6 7 128 132	decmac	$$⊢23\cdot 3+14=83$$
134		4lt10	$$⊢4<10$$
135		1lt2	$$⊢1<2$$
136	7 19 4 6 134 135	decltc	$$⊢14<23$$
137	121 6 123 133 136	ndvdsi	$$⊢\neg 23\parallel 83$$
138	3 12 14 18 39 41 59 69 87 105 120 137	prmlem2	$$⊢83\in \mathbb{P}$$