Metamath Proof Explorer

Theorem 163prm

Description: 163 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014) (Proof shortened by Mario Carneiro, 20-Apr-2015)

Ref Expression
Assertion 163prm 
|- ; ; 1 6 3 e. Prime

Proof

Step Hyp Ref Expression
1 1nn0 
 |-  1 e. NN0
2 6nn0 
 |-  6 e. NN0
3 1 2 deccl 
 |-  ; 1 6 e. NN0
4 3nn 
 |-  3 e. NN
5 3 4 decnncl 
 |-  ; ; 1 6 3 e. NN
6 8nn0 
 |-  8 e. NN0
7 4nn0 
 |-  4 e. NN0
8 3nn0 
 |-  3 e. NN0
9 1lt8 
 |-  1 < 8
10 6lt10 
 |-  6 < ; 1 0
11 3lt10 
 |-  3 < ; 1 0
12 1 6 2 7 8 1 9 10 11 3decltc 
 |-  ; ; 1 6 3 < ; ; 8 4 1
13 6nn 
 |-  6 e. NN
14 1 13 decnncl 
 |-  ; 1 6 e. NN
15 1lt10 
 |-  1 < ; 1 0
16 14 8 1 15 declti 
 |-  1 < ; ; 1 6 3
17 2cn 
 |-  2 e. CC
18 17 mulid2i 
 |-  ( 1 x. 2 ) = 2
19 df-3 
 |-  3 = ( 2 + 1 )
20 3 1 18 19 dec2dvds 
 |-  -. 2 || ; ; 1 6 3
21 5nn0 
 |-  5 e. NN0
22 21 7 deccl 
 |-  ; 5 4 e. NN0
23 1nn 
 |-  1 e. NN
24 0nn0 
 |-  0 e. NN0
25 eqid 
 |-  ; 5 4 = ; 5 4
26 1 dec0h 
 |-  1 = ; 0 1
27 ax-1cn 
 |-  1 e. CC
28 27 addid2i 
 |-  ( 0 + 1 ) = 1
29 28 oveq2i 
 |-  ( ( 3 x. 5 ) + ( 0 + 1 ) ) = ( ( 3 x. 5 ) + 1 )
30 5p1e6 
 |-  ( 5 + 1 ) = 6
31 5cn 
 |-  5 e. CC
32 3cn 
 |-  3 e. CC
33 5t3e15 
 |-  ( 5 x. 3 ) = ; 1 5
34 31 32 33 mulcomli 
 |-  ( 3 x. 5 ) = ; 1 5
35 1 21 30 34 decsuc 
 |-  ( ( 3 x. 5 ) + 1 ) = ; 1 6
36 29 35 eqtri 
 |-  ( ( 3 x. 5 ) + ( 0 + 1 ) ) = ; 1 6
37 2nn0 
 |-  2 e. NN0
38 2p1e3 
 |-  ( 2 + 1 ) = 3
39 4cn 
 |-  4 e. CC
40 4t3e12 
 |-  ( 4 x. 3 ) = ; 1 2
41 39 32 40 mulcomli 
 |-  ( 3 x. 4 ) = ; 1 2
42 1 37 38 41 decsuc 
 |-  ( ( 3 x. 4 ) + 1 ) = ; 1 3
43 21 7 24 1 25 26 8 8 1 36 42 decma2c 
 |-  ( ( 3 x. ; 5 4 ) + 1 ) = ; ; 1 6 3
44 1lt3 
 |-  1 < 3
45 4 22 23 43 44 ndvdsi 
 |-  -. 3 || ; ; 1 6 3
46 3lt5 
 |-  3 < 5
47 3 4 46 dec5dvds 
 |-  -. 5 || ; ; 1 6 3
48 7nn 
 |-  7 e. NN
49 37 8 deccl 
 |-  ; 2 3 e. NN0
50 2nn 
 |-  2 e. NN
51 eqid 
 |-  ; 2 3 = ; 2 3
52 37 dec0h 
 |-  2 = ; 0 2
53 7nn0 
 |-  7 e. NN0
54 17 addid2i 
 |-  ( 0 + 2 ) = 2
55 54 oveq2i 
 |-  ( ( 7 x. 2 ) + ( 0 + 2 ) ) = ( ( 7 x. 2 ) + 2 )
56 7t2e14 
 |-  ( 7 x. 2 ) = ; 1 4
57 4p2e6 
 |-  ( 4 + 2 ) = 6
58 1 7 37 56 57 decaddi 
 |-  ( ( 7 x. 2 ) + 2 ) = ; 1 6
59 55 58 eqtri 
 |-  ( ( 7 x. 2 ) + ( 0 + 2 ) ) = ; 1 6
60 7t3e21 
 |-  ( 7 x. 3 ) = ; 2 1
61 1p2e3 
 |-  ( 1 + 2 ) = 3
62 37 1 37 60 61 decaddi 
 |-  ( ( 7 x. 3 ) + 2 ) = ; 2 3
63 37 8 24 37 51 52 53 8 37 59 62 decma2c 
 |-  ( ( 7 x. ; 2 3 ) + 2 ) = ; ; 1 6 3
64 2lt7 
 |-  2 < 7
65 48 49 50 63 64 ndvdsi 
 |-  -. 7 || ; ; 1 6 3
66 1 23 decnncl 
 |-  ; 1 1 e. NN
67 1 7 deccl 
 |-  ; 1 4 e. NN0
68 9nn 
 |-  9 e. NN
69 9nn0 
 |-  9 e. NN0
70 eqid 
 |-  ; 1 4 = ; 1 4
71 69 dec0h 
 |-  9 = ; 0 9
72 1 1 deccl 
 |-  ; 1 1 e. NN0
73 31 addid2i 
 |-  ( 0 + 5 ) = 5
74 73 oveq2i 
 |-  ( ( ; 1 1 x. 1 ) + ( 0 + 5 ) ) = ( ( ; 1 1 x. 1 ) + 5 )
75 66 nncni 
 |-  ; 1 1 e. CC
76 75 mulid1i 
 |-  ( ; 1 1 x. 1 ) = ; 1 1
77 31 27 30 addcomli 
 |-  ( 1 + 5 ) = 6
78 1 1 21 76 77 decaddi 
 |-  ( ( ; 1 1 x. 1 ) + 5 ) = ; 1 6
79 74 78 eqtri 
 |-  ( ( ; 1 1 x. 1 ) + ( 0 + 5 ) ) = ; 1 6
80 eqid 
 |-  ; 1 1 = ; 1 1
81 39 mulid2i 
 |-  ( 1 x. 4 ) = 4
82 81 28 oveq12i 
 |-  ( ( 1 x. 4 ) + ( 0 + 1 ) ) = ( 4 + 1 )
83 4p1e5 
 |-  ( 4 + 1 ) = 5
84 82 83 eqtri 
 |-  ( ( 1 x. 4 ) + ( 0 + 1 ) ) = 5
85 81 oveq1i 
 |-  ( ( 1 x. 4 ) + 9 ) = ( 4 + 9 )
86 9cn 
 |-  9 e. CC
87 9p4e13 
 |-  ( 9 + 4 ) = ; 1 3
88 86 39 87 addcomli 
 |-  ( 4 + 9 ) = ; 1 3
89 85 88 eqtri 
 |-  ( ( 1 x. 4 ) + 9 ) = ; 1 3
90 1 1 24 69 80 71 7 8 1 84 89 decmac 
 |-  ( ( ; 1 1 x. 4 ) + 9 ) = ; 5 3
91 1 7 24 69 70 71 72 8 21 79 90 decma2c 
 |-  ( ( ; 1 1 x. ; 1 4 ) + 9 ) = ; ; 1 6 3
92 9lt10 
 |-  9 < ; 1 0
93 23 1 69 92 declti 
 |-  9 < ; 1 1
94 66 67 68 91 93 ndvdsi 
 |-  -. ; 1 1 || ; ; 1 6 3
95 1 4 decnncl 
 |-  ; 1 3 e. NN
96 1 37 deccl 
 |-  ; 1 2 e. NN0
97 eqid 
 |-  ; 1 2 = ; 1 2
98 53 dec0h 
 |-  7 = ; 0 7
99 1 8 deccl 
 |-  ; 1 3 e. NN0
100 eqid 
 |-  ; 1 3 = ; 1 3
101 32 addid2i 
 |-  ( 0 + 3 ) = 3
102 8 dec0h 
 |-  3 = ; 0 3
103 101 102 eqtri 
 |-  ( 0 + 3 ) = ; 0 3
104 27 mulid1i 
 |-  ( 1 x. 1 ) = 1
105 00id 
 |-  ( 0 + 0 ) = 0
106 104 105 oveq12i 
 |-  ( ( 1 x. 1 ) + ( 0 + 0 ) ) = ( 1 + 0 )
107 27 addid1i 
 |-  ( 1 + 0 ) = 1
108 106 107 eqtri 
 |-  ( ( 1 x. 1 ) + ( 0 + 0 ) ) = 1
109 32 mulid1i 
 |-  ( 3 x. 1 ) = 3
110 109 oveq1i 
 |-  ( ( 3 x. 1 ) + 3 ) = ( 3 + 3 )
111 3p3e6 
 |-  ( 3 + 3 ) = 6
112 110 111 eqtri 
 |-  ( ( 3 x. 1 ) + 3 ) = 6
113 2 dec0h 
 |-  6 = ; 0 6
114 112 113 eqtri 
 |-  ( ( 3 x. 1 ) + 3 ) = ; 0 6
115 1 8 24 8 100 103 1 2 24 108 114 decmac 
 |-  ( ( ; 1 3 x. 1 ) + ( 0 + 3 ) ) = ; 1 6
116 18 28 oveq12i 
 |-  ( ( 1 x. 2 ) + ( 0 + 1 ) ) = ( 2 + 1 )
117 116 38 eqtri 
 |-  ( ( 1 x. 2 ) + ( 0 + 1 ) ) = 3
118 3t2e6 
 |-  ( 3 x. 2 ) = 6
119 118 oveq1i 
 |-  ( ( 3 x. 2 ) + 7 ) = ( 6 + 7 )
120 7cn 
 |-  7 e. CC
121 6cn 
 |-  6 e. CC
122 7p6e13 
 |-  ( 7 + 6 ) = ; 1 3
123 120 121 122 addcomli 
 |-  ( 6 + 7 ) = ; 1 3
124 119 123 eqtri 
 |-  ( ( 3 x. 2 ) + 7 ) = ; 1 3
125 1 8 24 53 100 98 37 8 1 117 124 decmac 
 |-  ( ( ; 1 3 x. 2 ) + 7 ) = ; 3 3
126 1 37 24 53 97 98 99 8 8 115 125 decma2c 
 |-  ( ( ; 1 3 x. ; 1 2 ) + 7 ) = ; ; 1 6 3
127 7lt10 
 |-  7 < ; 1 0
128 23 8 53 127 declti 
 |-  7 < ; 1 3
129 95 96 48 126 128 ndvdsi 
 |-  -. ; 1 3 || ; ; 1 6 3
130 1 48 decnncl 
 |-  ; 1 7 e. NN
131 10nn 
 |-  ; 1 0 e. NN
132 eqid 
 |-  ; 1 7 = ; 1 7
133 eqid 
 |-  ; 1 0 = ; 1 0
134 86 mulid2i 
 |-  ( 1 x. 9 ) = 9
135 6p1e7 
 |-  ( 6 + 1 ) = 7
136 121 27 135 addcomli 
 |-  ( 1 + 6 ) = 7
137 134 136 oveq12i 
 |-  ( ( 1 x. 9 ) + ( 1 + 6 ) ) = ( 9 + 7 )
138 9p7e16 
 |-  ( 9 + 7 ) = ; 1 6
139 137 138 eqtri 
 |-  ( ( 1 x. 9 ) + ( 1 + 6 ) ) = ; 1 6
140 9t7e63 
 |-  ( 9 x. 7 ) = ; 6 3
141 86 120 140 mulcomli 
 |-  ( 7 x. 9 ) = ; 6 3
142 141 oveq1i 
 |-  ( ( 7 x. 9 ) + 0 ) = ( ; 6 3 + 0 )
143 2 8 deccl 
 |-  ; 6 3 e. NN0
144 143 nn0cni 
 |-  ; 6 3 e. CC
145 144 addid1i 
 |-  ( ; 6 3 + 0 ) = ; 6 3
146 142 145 eqtri 
 |-  ( ( 7 x. 9 ) + 0 ) = ; 6 3
147 1 53 1 24 132 133 69 8 2 139 146 decmac 
 |-  ( ( ; 1 7 x. 9 ) + ; 1 0 ) = ; ; 1 6 3
148 7pos 
 |-  0 < 7
149 1 24 48 148 declt 
 |-  ; 1 0 < ; 1 7
150 130 69 131 147 149 ndvdsi 
 |-  -. ; 1 7 || ; ; 1 6 3
151 1 68 decnncl 
 |-  ; 1 9 e. NN
152 eqid 
 |-  ; 1 9 = ; 1 9
153 8cn 
 |-  8 e. CC
154 153 mulid2i 
 |-  ( 1 x. 8 ) = 8
155 7p1e8 
 |-  ( 7 + 1 ) = 8
156 120 27 155 addcomli 
 |-  ( 1 + 7 ) = 8
157 154 156 oveq12i 
 |-  ( ( 1 x. 8 ) + ( 1 + 7 ) ) = ( 8 + 8 )
158 8p8e16 
 |-  ( 8 + 8 ) = ; 1 6
159 157 158 eqtri 
 |-  ( ( 1 x. 8 ) + ( 1 + 7 ) ) = ; 1 6
160 9t8e72 
 |-  ( 9 x. 8 ) = ; 7 2
161 53 37 38 160 decsuc 
 |-  ( ( 9 x. 8 ) + 1 ) = ; 7 3
162 1 69 1 1 152 80 6 8 53 159 161 decmac 
 |-  ( ( ; 1 9 x. 8 ) + ; 1 1 ) = ; ; 1 6 3
163 1lt9 
 |-  1 < 9
164 1 1 68 163 declt 
 |-  ; 1 1 < ; 1 9
165 151 6 66 162 164 ndvdsi 
 |-  -. ; 1 9 || ; ; 1 6 3
166 37 4 decnncl 
 |-  ; 2 3 e. NN
167 120 17 56 mulcomli 
 |-  ( 2 x. 7 ) = ; 1 4
168 1 7 37 167 57 decaddi 
 |-  ( ( 2 x. 7 ) + 2 ) = ; 1 6
169 120 32 60 mulcomli 
 |-  ( 3 x. 7 ) = ; 2 1
170 37 1 37 169 61 decaddi 
 |-  ( ( 3 x. 7 ) + 2 ) = ; 2 3
171 37 8 37 51 53 8 37 168 170 decrmac 
 |-  ( ( ; 2 3 x. 7 ) + 2 ) = ; ; 1 6 3
172 2lt10 
 |-  2 < ; 1 0
173 50 8 37 172 declti 
 |-  2 < ; 2 3
174 166 53 50 171 173 ndvdsi 
 |-  -. ; 2 3 || ; ; 1 6 3
175 5 12 16 20 45 47 65 94 129 150 165 174 prmlem2 
 |-  ; ; 1 6 3 e. Prime