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 ∈ ℙ

Proof

Step	Hyp	Ref	Expression
1		8nn0	⊢ 8 ∈ ℕ0
2		3nn	⊢ 3 ∈ ℕ
3	1 2	decnncl	⊢ ; 8 3 ∈ ℕ
4		4nn0	⊢ 4 ∈ ℕ0
5	1 4	deccl	⊢ ; 8 4 ∈ ℕ0
6		3nn0	⊢ 3 ∈ ℕ0
7		1nn0	⊢ 1 ∈ ℕ0
8		3lt10	⊢ 3 < ; 1 0
9		8nn	⊢ 8 ∈ ℕ
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 ∈ ℂ
16	15	mulid2i	⊢ ( 1 · 2 ) = 2
17		df-3	⊢ 3 = ( 2 + 1 )
18	1 7 16 17	dec2dvds	⊢ ¬ 2 ∥ ; 8 3
19		2nn0	⊢ 2 ∈ ℕ0
20		7nn0	⊢ 7 ∈ ℕ0
21	19 20	deccl	⊢ ; 2 7 ∈ ℕ0
22		2nn	⊢ 2 ∈ ℕ
23		0nn0	⊢ 0 ∈ ℕ0
24		eqid	⊢ ; 2 7 = ; 2 7
25	19	dec0h	⊢ 2 = ; 0 2
26		3t2e6	⊢ ( 3 · 2 ) = 6
27	15	addid2i	⊢ ( 0 + 2 ) = 2
28	26 27	oveq12i	⊢ ( ( 3 · 2 ) + ( 0 + 2 ) ) = ( 6 + 2 )
29		6p2e8	⊢ ( 6 + 2 ) = 8
30	28 29	eqtri	⊢ ( ( 3 · 2 ) + ( 0 + 2 ) ) = 8
31	20	nn0cni	⊢ 7 ∈ ℂ
32		3cn	⊢ 3 ∈ ℂ
33		7t3e21	⊢ ( 7 · 3 ) = ; 2 1
34	31 32 33	mulcomli	⊢ ( 3 · 7 ) = ; 2 1
35		1p2e3	⊢ ( 1 + 2 ) = 3
36	19 7 19 34 35	decaddi	⊢ ( ( 3 · 7 ) + 2 ) = ; 2 3
37	19 20 23 19 24 25 6 6 19 30 36	decma2c	⊢ ( ( 3 · ; 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 ∈ ℕ
43	7 7	deccl	⊢ ; 1 1 ∈ ℕ0
44		6nn	⊢ 6 ∈ ℕ
45	44	nnnn0i	⊢ 6 ∈ ℕ0
46		eqid	⊢ ; 1 1 = ; 1 1
47	45	dec0h	⊢ 6 = ; 0 6
48	31	mulid1i	⊢ ( 7 · 1 ) = 7
49		ax-1cn	⊢ 1 ∈ ℂ
50	49	addid2i	⊢ ( 0 + 1 ) = 1
51	48 50	oveq12i	⊢ ( ( 7 · 1 ) + ( 0 + 1 ) ) = ( 7 + 1 )
52		7p1e8	⊢ ( 7 + 1 ) = 8
53	51 52	eqtri	⊢ ( ( 7 · 1 ) + ( 0 + 1 ) ) = 8
54	48	oveq1i	⊢ ( ( 7 · 1 ) + 6 ) = ( 7 + 6 )
55		7p6e13	⊢ ( 7 + 6 ) = ; 1 3
56	54 55	eqtri	⊢ ( ( 7 · 1 ) + 6 ) = ; 1 3
57	7 7 23 45 46 47 20 6 7 53 56	decma2c	⊢ ( ( 7 · ; 1 1 ) + 6 ) = ; 8 3
58		6lt7	⊢ 6 < 7
59	42 43 44 57 58	ndvdsi	⊢ ¬ 7 ∥ ; 8 3
60		1nn	⊢ 1 ∈ ℕ
61	7 60	decnncl	⊢ ; 1 1 ∈ ℕ
62	61	nncni	⊢ ; 1 1 ∈ ℂ
63	62 31	mulcomi	⊢ ( ; 1 1 · 7 ) = ( 7 · ; 1 1 )
64	63	oveq1i	⊢ ( ( ; 1 1 · 7 ) + 6 ) = ( ( 7 · ; 1 1 ) + 6 )
65	64 57	eqtri	⊢ ( ( ; 1 1 · 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 ∈ ℕ
70		5nn	⊢ 5 ∈ ℕ
71	70	nnnn0i	⊢ 5 ∈ ℕ0
72		eqid	⊢ ; 1 3 = ; 1 3
73	71	dec0h	⊢ 5 = ; 0 5
74		6cn	⊢ 6 ∈ ℂ
75	74	mulid2i	⊢ ( 1 · 6 ) = 6
76	75 27	oveq12i	⊢ ( ( 1 · 6 ) + ( 0 + 2 ) ) = ( 6 + 2 )
77	76 29	eqtri	⊢ ( ( 1 · 6 ) + ( 0 + 2 ) ) = 8
78		6t3e18	⊢ ( 6 · 3 ) = ; 1 8
79	74 32 78	mulcomli	⊢ ( 3 · 6 ) = ; 1 8
80		1p1e2	⊢ ( 1 + 1 ) = 2
81		8p5e13	⊢ ( 8 + 5 ) = ; 1 3
82	7 1 71 79 80 6 81	decaddci	⊢ ( ( 3 · 6 ) + 5 ) = ; 2 3
83	7 6 23 71 72 73 45 6 19 77 82	decmac	⊢ ( ( ; 1 3 · 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 ∈ ℕ
88	7 70	decnncl	⊢ ; 1 5 ∈ ℕ
89		eqid	⊢ ; 1 7 = ; 1 7
90		eqid	⊢ ; 1 5 = ; 1 5
91	4	nn0cni	⊢ 4 ∈ ℂ
92	91	mulid2i	⊢ ( 1 · 4 ) = 4
93		3p1e4	⊢ ( 3 + 1 ) = 4
94	32 49 93	addcomli	⊢ ( 1 + 3 ) = 4
95	92 94	oveq12i	⊢ ( ( 1 · 4 ) + ( 1 + 3 ) ) = ( 4 + 4 )
96		4p4e8	⊢ ( 4 + 4 ) = 8
97	95 96	eqtri	⊢ ( ( 1 · 4 ) + ( 1 + 3 ) ) = 8
98		7t4e28	⊢ ( 7 · 4 ) = ; 2 8
99		2p1e3	⊢ ( 2 + 1 ) = 3
100	19 1 71 98 99 6 81	decaddci	⊢ ( ( 7 · 4 ) + 5 ) = ; 3 3
101	7 20 7 71 89 90 4 6 6 97 100	decmac	⊢ ( ( ; 1 7 · 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 ∈ ℕ
106	7 105	decnncl	⊢ ; 1 9 ∈ ℕ
107		9nn0	⊢ 9 ∈ ℕ0
108		eqid	⊢ ; 1 9 = ; 1 9
109	20	dec0h	⊢ 7 = ; 0 7
110	91	addid2i	⊢ ( 0 + 4 ) = 4
111	92 110	oveq12i	⊢ ( ( 1 · 4 ) + ( 0 + 4 ) ) = ( 4 + 4 )
112	111 96	eqtri	⊢ ( ( 1 · 4 ) + ( 0 + 4 ) ) = 8
113		9t4e36	⊢ ( 9 · 4 ) = ; 3 6
114	31 74 55	addcomli	⊢ ( 6 + 7 ) = ; 1 3
115	6 45 20 113 93 6 114	decaddci	⊢ ( ( 9 · 4 ) + 7 ) = ; 4 3
116	7 107 23 20 108 109 4 6 4 112 115	decmac	⊢ ( ( ; 1 9 · 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 ∈ ℕ
121		4nn	⊢ 4 ∈ ℕ
122	7 121	decnncl	⊢ ; 1 4 ∈ ℕ
123		eqid	⊢ ; 2 3 = ; 2 3
124		eqid	⊢ ; 1 4 = ; 1 4
125	32 15 26	mulcomli	⊢ ( 2 · 3 ) = 6
126	125 80	oveq12i	⊢ ( ( 2 · 3 ) + ( 1 + 1 ) ) = ( 6 + 2 )
127	126 29	eqtri	⊢ ( ( 2 · 3 ) + ( 1 + 1 ) ) = 8
128		3t3e9	⊢ ( 3 · 3 ) = 9
129	128	oveq1i	⊢ ( ( 3 · 3 ) + 4 ) = ( 9 + 4 )
130		9p4e13	⊢ ( 9 + 4 ) = ; 1 3
131	129 130	eqtri	⊢ ( ( 3 · 3 ) + 4 ) = ; 1 3
132	19 6 7 4 123 124 6 6 7 127 131	decmac	⊢ ( ( ; 2 3 · 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 ∈ ℙ