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