Metamath Proof Explorer

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 7cn 
 |-  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 6nn0 
 |-  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 11nn 
 |-  ; 1 1 e. NN
61 1nn 
 |-  1 e. NN
62 7 61 decnncl 
 |-  ; 1 1 e. NN
63 62 nncni 
 |-  ; 1 1 e. CC
64 63 31 mulcomi 
 |-  ( ; 1 1 x. 7 ) = ( 7 x. ; 1 1 )
65 64 oveq1i 
 |-  ( ( ; 1 1 x. 7 ) + 6 ) = ( ( 7 x. ; 1 1 ) + 6 )
66 65 57 eqtri 
 |-  ( ( ; 1 1 x. 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 e. NN
71 5nn 
 |-  5 e. NN
72 5nn0 
 |-  5 e. NN0
73 eqid 
 |-  ; 1 3 = ; 1 3
74 72 dec0h 
 |-  5 = ; 0 5
75 6cn 
 |-  6 e. CC
76 75 mullidi 
 |-  ( 1 x. 6 ) = 6
77 76 27 oveq12i 
 |-  ( ( 1 x. 6 ) + ( 0 + 2 ) ) = ( 6 + 2 )
78 77 29 eqtri 
 |-  ( ( 1 x. 6 ) + ( 0 + 2 ) ) = 8
79 6t3e18 
 |-  ( 6 x. 3 ) = ; 1 8
80 75 32 79 mulcomli 
 |-  ( 3 x. 6 ) = ; 1 8
81 1p1e2 
 |-  ( 1 + 1 ) = 2
82 8p5e13 
 |-  ( 8 + 5 ) = ; 1 3
83 7 1 72 80 81 6 82 decaddci 
 |-  ( ( 3 x. 6 ) + 5 ) = ; 2 3
84 7 6 23 72 73 74 45 6 19 78 83 decmac 
 |-  ( ( ; 1 3 x. 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 e. NN
89 7 71 decnncl 
 |-  ; 1 5 e. NN
90 eqid 
 |-  ; 1 7 = ; 1 7
91 eqid 
 |-  ; 1 5 = ; 1 5
92 4cn 
 |-  4 e. CC
93 92 mullidi 
 |-  ( 1 x. 4 ) = 4
94 3p1e4 
 |-  ( 3 + 1 ) = 4
95 32 49 94 addcomli 
 |-  ( 1 + 3 ) = 4
96 93 95 oveq12i 
 |-  ( ( 1 x. 4 ) + ( 1 + 3 ) ) = ( 4 + 4 )
97 4p4e8 
 |-  ( 4 + 4 ) = 8
98 96 97 eqtri 
 |-  ( ( 1 x. 4 ) + ( 1 + 3 ) ) = 8
99 7t4e28 
 |-  ( 7 x. 4 ) = ; 2 8
100 2p1e3 
 |-  ( 2 + 1 ) = 3
101 19 1 72 99 100 6 82 decaddci 
 |-  ( ( 7 x. 4 ) + 5 ) = ; 3 3
102 7 20 7 72 90 91 4 6 6 98 101 decmac 
 |-  ( ( ; 1 7 x. 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 e. NN
107 7 106 decnncl 
 |-  ; 1 9 e. NN
108 9nn0 
 |-  9 e. NN0
109 eqid 
 |-  ; 1 9 = ; 1 9
110 20 dec0h 
 |-  7 = ; 0 7
111 92 addlidi 
 |-  ( 0 + 4 ) = 4
112 93 111 oveq12i 
 |-  ( ( 1 x. 4 ) + ( 0 + 4 ) ) = ( 4 + 4 )
113 112 97 eqtri 
 |-  ( ( 1 x. 4 ) + ( 0 + 4 ) ) = 8
114 9t4e36 
 |-  ( 9 x. 4 ) = ; 3 6
115 31 75 55 addcomli 
 |-  ( 6 + 7 ) = ; 1 3
116 6 45 20 114 94 6 115 decaddci 
 |-  ( ( 9 x. 4 ) + 7 ) = ; 4 3
117 7 108 23 20 109 110 4 6 4 113 116 decmac 
 |-  ( ( ; 1 9 x. 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 e. NN
122 4nn 
 |-  4 e. NN
123 7 122 decnncl 
 |-  ; 1 4 e. NN
124 eqid 
 |-  ; 2 3 = ; 2 3
125 eqid 
 |-  ; 1 4 = ; 1 4
126 2t3e6 
 |-  ( 2 x. 3 ) = 6
127 126 81 oveq12i 
 |-  ( ( 2 x. 3 ) + ( 1 + 1 ) ) = ( 6 + 2 )
128 127 29 eqtri 
 |-  ( ( 2 x. 3 ) + ( 1 + 1 ) ) = 8
129 3t3e9 
 |-  ( 3 x. 3 ) = 9
130 129 oveq1i 
 |-  ( ( 3 x. 3 ) + 4 ) = ( 9 + 4 )
131 9p4e13 
 |-  ( 9 + 4 ) = ; 1 3
132 130 131 eqtri 
 |-  ( ( 3 x. 3 ) + 4 ) = ; 1 3
133 19 6 7 4 124 125 6 6 7 128 132 decmac 
 |-  ( ( ; 2 3 x. 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 e. Prime