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	mullidi	⊢ ( 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	addlidi	⊢ ( 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		7cn	⊢ 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		6nn0	⊢ 6 ∈ ℕ0
46		eqid	⊢ ; 1 1 = ; 1 1
47	45	dec0h	⊢ 6 = ; 0 6
48	31	mulridi	⊢ ( 7 · 1 ) = 7
49		ax-1cn	⊢ 1 ∈ ℂ
50	49	addlidi	⊢ ( 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		11nn	⊢ ; 1 1 ∈ ℕ
61		1nn	⊢ 1 ∈ ℕ
62	7 61	decnncl	⊢ ; 1 1 ∈ ℕ
63	62	nncni	⊢ ; 1 1 ∈ ℂ
64	63 31	mulcomi	⊢ ( ; 1 1 · 7 ) = ( 7 · ; 1 1 )
65	64	oveq1i	⊢ ( ( ; 1 1 · 7 ) + 6 ) = ( ( 7 · ; 1 1 ) + 6 )
66	65 57	eqtri	⊢ ( ( ; 1 1 · 7 ) + 6 ) = ; 8 3
67		6lt10	⊢ 6 < ; 1 0
68	61 7 45 67	declti	⊢ 6 < ; 1 1
69	60 20 44 66 68	ndvdsi	⊢ ¬ ; 1 1 ∥ ; 8 3
70	7 2	decnncl	⊢ ; 1 3 ∈ ℕ
71		5nn	⊢ 5 ∈ ℕ
72		5nn0	⊢ 5 ∈ ℕ0
73		eqid	⊢ ; 1 3 = ; 1 3
74	72	dec0h	⊢ 5 = ; 0 5
75		6cn	⊢ 6 ∈ ℂ
76	75	mullidi	⊢ ( 1 · 6 ) = 6
77	76 27	oveq12i	⊢ ( ( 1 · 6 ) + ( 0 + 2 ) ) = ( 6 + 2 )
78	77 29	eqtri	⊢ ( ( 1 · 6 ) + ( 0 + 2 ) ) = 8
79		6t3e18	⊢ ( 6 · 3 ) = ; 1 8
80	75 32 79	mulcomli	⊢ ( 3 · 6 ) = ; 1 8
81		1p1e2	⊢ ( 1 + 1 ) = 2
82		8p5e13	⊢ ( 8 + 5 ) = ; 1 3
83	7 1 72 80 81 6 82	decaddci	⊢ ( ( 3 · 6 ) + 5 ) = ; 2 3
84	7 6 23 72 73 74 45 6 19 78 83	decmac	⊢ ( ( ; 1 3 · 6 ) + 5 ) = ; 8 3
85		5lt10	⊢ 5 < ; 1 0
86	61 6 72 85	declti	⊢ 5 < ; 1 3
87	70 45 71 84 86	ndvdsi	⊢ ¬ ; 1 3 ∥ ; 8 3
88	7 42	decnncl	⊢ ; 1 7 ∈ ℕ
89	7 71	decnncl	⊢ ; 1 5 ∈ ℕ
90		eqid	⊢ ; 1 7 = ; 1 7
91		eqid	⊢ ; 1 5 = ; 1 5
92		4cn	⊢ 4 ∈ ℂ
93	92	mullidi	⊢ ( 1 · 4 ) = 4
94		3p1e4	⊢ ( 3 + 1 ) = 4
95	32 49 94	addcomli	⊢ ( 1 + 3 ) = 4
96	93 95	oveq12i	⊢ ( ( 1 · 4 ) + ( 1 + 3 ) ) = ( 4 + 4 )
97		4p4e8	⊢ ( 4 + 4 ) = 8
98	96 97	eqtri	⊢ ( ( 1 · 4 ) + ( 1 + 3 ) ) = 8
99		7t4e28	⊢ ( 7 · 4 ) = ; 2 8
100		2p1e3	⊢ ( 2 + 1 ) = 3
101	19 1 72 99 100 6 82	decaddci	⊢ ( ( 7 · 4 ) + 5 ) = ; 3 3
102	7 20 7 72 90 91 4 6 6 98 101	decmac	⊢ ( ( ; 1 7 · 4 ) + ; 1 5 ) = ; 8 3
103		5lt7	⊢ 5 < 7
104	7 72 42 103	declt	⊢ ; 1 5 < ; 1 7
105	88 4 89 102 104	ndvdsi	⊢ ¬ ; 1 7 ∥ ; 8 3
106		9nn	⊢ 9 ∈ ℕ
107	7 106	decnncl	⊢ ; 1 9 ∈ ℕ
108		9nn0	⊢ 9 ∈ ℕ0
109		eqid	⊢ ; 1 9 = ; 1 9
110	20	dec0h	⊢ 7 = ; 0 7
111	92	addlidi	⊢ ( 0 + 4 ) = 4
112	93 111	oveq12i	⊢ ( ( 1 · 4 ) + ( 0 + 4 ) ) = ( 4 + 4 )
113	112 97	eqtri	⊢ ( ( 1 · 4 ) + ( 0 + 4 ) ) = 8
114		9t4e36	⊢ ( 9 · 4 ) = ; 3 6
115	31 75 55	addcomli	⊢ ( 6 + 7 ) = ; 1 3
116	6 45 20 114 94 6 115	decaddci	⊢ ( ( 9 · 4 ) + 7 ) = ; 4 3
117	7 108 23 20 109 110 4 6 4 113 116	decmac	⊢ ( ( ; 1 9 · 4 ) + 7 ) = ; 8 3
118		7lt10	⊢ 7 < ; 1 0
119	61 108 20 118	declti	⊢ 7 < ; 1 9
120	107 4 42 117 119	ndvdsi	⊢ ¬ ; 1 9 ∥ ; 8 3
121	19 2	decnncl	⊢ ; 2 3 ∈ ℕ
122		4nn	⊢ 4 ∈ ℕ
123	7 122	decnncl	⊢ ; 1 4 ∈ ℕ
124		eqid	⊢ ; 2 3 = ; 2 3
125		eqid	⊢ ; 1 4 = ; 1 4
126		2t3e6	⊢ ( 2 · 3 ) = 6
127	126 81	oveq12i	⊢ ( ( 2 · 3 ) + ( 1 + 1 ) ) = ( 6 + 2 )
128	127 29	eqtri	⊢ ( ( 2 · 3 ) + ( 1 + 1 ) ) = 8
129		3t3e9	⊢ ( 3 · 3 ) = 9
130	129	oveq1i	⊢ ( ( 3 · 3 ) + 4 ) = ( 9 + 4 )
131		9p4e13	⊢ ( 9 + 4 ) = ; 1 3
132	130 131	eqtri	⊢ ( ( 3 · 3 ) + 4 ) = ; 1 3
133	19 6 7 4 124 125 6 6 7 128 132	decmac	⊢ ( ( ; 2 3 · 3 ) + ; 1 4 ) = ; 8 3
134		4lt10	⊢ 4 < ; 1 0
135		1lt2	⊢ 1 < 2
136	7 19 4 6 134 135	decltc	⊢ ; 1 4 < ; 2 3
137	121 6 123 133 136	ndvdsi	⊢ ¬ ; 2 3 ∥ ; 8 3
138	3 12 14 18 39 41 59 69 87 105 120 137	prmlem2	⊢ ; 8 3 ∈ ℙ