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	mulid2i	$$⊢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	addid2i	$$⊢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	20	nn0cni	$$⊢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	44	nnnn0i	$$⊢6\in {\mathbb{N}}_0$$
46		eqid	$$⊢11=11$$
47	45	dec0h	$$⊢6=06$$
48	31	mulid1i	$$⊢7\cdot 1=7$$
49		ax-1cn	$$⊢1\in ℂ$$
50	49	addid2i	$$⊢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		1nn	$$⊢1\in \mathbb{N}$$
61	7 60	decnncl	$$⊢11\in \mathbb{N}$$
62	61	nncni	$$⊢11\in ℂ$$
63	62 31	mulcomi	$$⊢11\cdot 7=7\cdot 11$$
64	63	oveq1i	$$⊢11\cdot 7+6=7\cdot 11+6$$
65	64 57	eqtri	$$⊢11\cdot 7+6=83$$
66		6lt10	$$⊢6<10$$
67	60 7 45 66	declti	$$⊢6<11$$
68	61 20 44 65 67	ndvdsi	$$⊢\neg 11\parallel 83$$
69	7 2	decnncl	$$⊢13\in \mathbb{N}$$
70		5nn	$$⊢5\in \mathbb{N}$$
71	70	nnnn0i	$$⊢5\in {\mathbb{N}}_0$$
72		eqid	$$⊢13=13$$
73	71	dec0h	$$⊢5=05$$
74		6cn	$$⊢6\in ℂ$$
75	74	mulid2i	$$⊢1\cdot 6=6$$
76	75 27	oveq12i	$$⊢1\cdot 6+0+2=6+2$$
77	76 29	eqtri	$$⊢1\cdot 6+0+2=8$$
78		6t3e18	$$⊢6\cdot 3=18$$
79	74 32 78	mulcomli	$$⊢3\cdot 6=18$$
80		1p1e2	$$⊢1+1=2$$
81		8p5e13	$$⊢8+5=13$$
82	7 1 71 79 80 6 81	decaddci	$$⊢3\cdot 6+5=23$$
83	7 6 23 71 72 73 45 6 19 77 82	decmac	$$⊢13\cdot 6+5=83$$
84		5lt10	$$⊢5<10$$
85	60 6 71 84	declti	$$⊢5<13$$
86	69 45 70 83 85	ndvdsi	$$⊢\neg 13\parallel 83$$
87	7 42	decnncl	$$⊢17\in \mathbb{N}$$
88	7 70	decnncl	$$⊢15\in \mathbb{N}$$
89		eqid	$$⊢17=17$$
90		eqid	$$⊢15=15$$
91	4	nn0cni	$$⊢4\in ℂ$$
92	91	mulid2i	$$⊢1\cdot 4=4$$
93		3p1e4	$$⊢3+1=4$$
94	32 49 93	addcomli	$$⊢1+3=4$$
95	92 94	oveq12i	$$⊢1\cdot 4+1+3=4+4$$
96		4p4e8	$$⊢4+4=8$$
97	95 96	eqtri	$$⊢1\cdot 4+1+3=8$$
98		7t4e28	$$⊢7\cdot 4=28$$
99		2p1e3	$$⊢2+1=3$$
100	19 1 71 98 99 6 81	decaddci	$$⊢7\cdot 4+5=33$$
101	7 20 7 71 89 90 4 6 6 97 100	decmac	$$⊢17\cdot 4+15=83$$
102		5lt7	$$⊢5<7$$
103	7 71 42 102	declt	$$⊢15<17$$
104	87 4 88 101 103	ndvdsi	$$⊢\neg 17\parallel 83$$
105		9nn	$$⊢9\in \mathbb{N}$$
106	7 105	decnncl	$$⊢19\in \mathbb{N}$$
107		9nn0	$$⊢9\in {\mathbb{N}}_0$$
108		eqid	$$⊢19=19$$
109	20	dec0h	$$⊢7=07$$
110	91	addid2i	$$⊢0+4=4$$
111	92 110	oveq12i	$$⊢1\cdot 4+0+4=4+4$$
112	111 96	eqtri	$$⊢1\cdot 4+0+4=8$$
113		9t4e36	$$⊢9\cdot 4=36$$
114	31 74 55	addcomli	$$⊢6+7=13$$
115	6 45 20 113 93 6 114	decaddci	$$⊢9\cdot 4+7=43$$
116	7 107 23 20 108 109 4 6 4 112 115	decmac	$$⊢19\cdot 4+7=83$$
117		7lt10	$$⊢7<10$$
118	60 107 20 117	declti	$$⊢7<19$$
119	106 4 42 116 118	ndvdsi	$$⊢\neg 19\parallel 83$$
120	19 2	decnncl	$$⊢23\in \mathbb{N}$$
121		4nn	$$⊢4\in \mathbb{N}$$
122	7 121	decnncl	$$⊢14\in \mathbb{N}$$
123		eqid	$$⊢23=23$$
124		eqid	$$⊢14=14$$
125	32 15 26	mulcomli	$$⊢2\cdot 3=6$$
126	125 80	oveq12i	$$⊢2\cdot 3+1+1=6+2$$
127	126 29	eqtri	$$⊢2\cdot 3+1+1=8$$
128		3t3e9	$$⊢3\cdot 3=9$$
129	128	oveq1i	$$⊢3\cdot 3+4=9+4$$
130		9p4e13	$$⊢9+4=13$$
131	129 130	eqtri	$$⊢3\cdot 3+4=13$$
132	19 6 7 4 123 124 6 6 7 127 131	decmac	$$⊢23\cdot 3+14=83$$
133		4lt10	$$⊢4<10$$
134		1lt2	$$⊢1<2$$
135	7 19 4 6 133 134	decltc	$$⊢14<23$$
136	120 6 122 132 135	ndvdsi	$$⊢\neg 23\parallel 83$$
137	3 12 14 18 39 41 59 68 86 104 119 136	prmlem2	$$⊢83\in \mathbb{P}$$