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	|- ; 8 3 e. Prime

Proof

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