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

Proof

Step Hyp Ref Expression
1 1nn0 ⊢ 1 ∈ ℕ0
2 6nn0 ⊢ 6 ∈ ℕ0
3 1 2 deccl ⊢ 1 6 ∈ ℕ0
4 3nn ⊢ 3 ∈ ℕ
5 3 4 decnncl ⊢ 1 6 3 ∈ ℕ
6 8nn0 ⊢ 8 ∈ ℕ0
7 4nn0 ⊢ 4 ∈ ℕ0
8 3nn0 ⊢ 3 ∈ ℕ0
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 ∈ ℕ
14 1 13 decnncl ⊢ 1 6 ∈ ℕ
15 1lt10 ⊢ 1 < 1 0
16 14 8 1 15 declti ⊢ 1 < 1 6 3
17 2cn ⊢ 2 ∈ ℂ
18 17 mulid2i ⊢ ( 1 · 2 ) = 2
19 df-3 ⊢ 3 = ( 2 + 1 )
20 3 1 18 19 dec2dvds ⊢ ¬ 2 ∥ 1 6 3
21 5nn0 ⊢ 5 ∈ ℕ0
22 21 7 deccl ⊢ 5 4 ∈ ℕ0
23 1nn ⊢ 1 ∈ ℕ
24 0nn0 ⊢ 0 ∈ ℕ0
25 eqid ⊢ 5 4 = 5 4
26 1 dec0h ⊢ 1 = 0 1
27 ax-1cn ⊢ 1 ∈ ℂ
28 27 addid2i ⊢ ( 0 + 1 ) = 1
29 28 oveq2i ⊢ ( ( 3 · 5 ) + ( 0 + 1 ) ) = ( ( 3 · 5 ) + 1 )
30 5p1e6 ⊢ ( 5 + 1 ) = 6
31 5cn ⊢ 5 ∈ ℂ
32 3cn ⊢ 3 ∈ ℂ
33 5t3e15 ⊢ ( 5 · 3 ) = 1 5
34 31 32 33 mulcomli ⊢ ( 3 · 5 ) = 1 5
35 1 21 30 34 decsuc ⊢ ( ( 3 · 5 ) + 1 ) = 1 6
36 29 35 eqtri ⊢ ( ( 3 · 5 ) + ( 0 + 1 ) ) = 1 6
37 2nn0 ⊢ 2 ∈ ℕ0
38 2p1e3 ⊢ ( 2 + 1 ) = 3
39 4cn ⊢ 4 ∈ ℂ
40 4t3e12 ⊢ ( 4 · 3 ) = 1 2
41 39 32 40 mulcomli ⊢ ( 3 · 4 ) = 1 2
42 1 37 38 41 decsuc ⊢ ( ( 3 · 4 ) + 1 ) = 1 3
43 21 7 24 1 25 26 8 8 1 36 42 decma2c ⊢ ( ( 3 · 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 ∈ ℕ
49 37 8 deccl ⊢ 2 3 ∈ ℕ0
50 2nn ⊢ 2 ∈ ℕ
51 eqid ⊢ 2 3 = 2 3
52 37 dec0h ⊢ 2 = 0 2
53 7nn0 ⊢ 7 ∈ ℕ0
54 17 addid2i ⊢ ( 0 + 2 ) = 2
55 54 oveq2i ⊢ ( ( 7 · 2 ) + ( 0 + 2 ) ) = ( ( 7 · 2 ) + 2 )
56 7t2e14 ⊢ ( 7 · 2 ) = 1 4
57 4p2e6 ⊢ ( 4 + 2 ) = 6
58 1 7 37 56 57 decaddi ⊢ ( ( 7 · 2 ) + 2 ) = 1 6
59 55 58 eqtri ⊢ ( ( 7 · 2 ) + ( 0 + 2 ) ) = 1 6
60 7t3e21 ⊢ ( 7 · 3 ) = 2 1
61 1p2e3 ⊢ ( 1 + 2 ) = 3
62 37 1 37 60 61 decaddi ⊢ ( ( 7 · 3 ) + 2 ) = 2 3
63 37 8 24 37 51 52 53 8 37 59 62 decma2c ⊢ ( ( 7 · 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 ∈ ℕ
67 1 7 deccl ⊢ 1 4 ∈ ℕ0
68 9nn ⊢ 9 ∈ ℕ
69 9nn0 ⊢ 9 ∈ ℕ0
70 eqid ⊢ 1 4 = 1 4
71 69 dec0h ⊢ 9 = 0 9
72 1 1 deccl ⊢ 1 1 ∈ ℕ0
73 31 addid2i ⊢ ( 0 + 5 ) = 5
74 73 oveq2i ⊢ ( ( 1 1 · 1 ) + ( 0 + 5 ) ) = ( ( 1 1 · 1 ) + 5 )
75 66 nncni ⊢ 1 1 ∈ ℂ
76 75 mulid1i ⊢ ( 1 1 · 1 ) = 1 1
77 31 27 30 addcomli ⊢ ( 1 + 5 ) = 6
78 1 1 21 76 77 decaddi ⊢ ( ( 1 1 · 1 ) + 5 ) = 1 6
79 74 78 eqtri ⊢ ( ( 1 1 · 1 ) + ( 0 + 5 ) ) = 1 6
80 eqid ⊢ 1 1 = 1 1
81 39 mulid2i ⊢ ( 1 · 4 ) = 4
82 81 28 oveq12i ⊢ ( ( 1 · 4 ) + ( 0 + 1 ) ) = ( 4 + 1 )
83 4p1e5 ⊢ ( 4 + 1 ) = 5
84 82 83 eqtri ⊢ ( ( 1 · 4 ) + ( 0 + 1 ) ) = 5
85 81 oveq1i ⊢ ( ( 1 · 4 ) + 9 ) = ( 4 + 9 )
86 9cn ⊢ 9 ∈ ℂ
87 9p4e13 ⊢ ( 9 + 4 ) = 1 3
88 86 39 87 addcomli ⊢ ( 4 + 9 ) = 1 3
89 85 88 eqtri ⊢ ( ( 1 · 4 ) + 9 ) = 1 3
90 1 1 24 69 80 71 7 8 1 84 89 decmac ⊢ ( ( 1 1 · 4 ) + 9 ) = 5 3
91 1 7 24 69 70 71 72 8 21 79 90 decma2c ⊢ ( ( 1 1 · 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 ∈ ℕ
96 1 37 deccl ⊢ 1 2 ∈ ℕ0
97 eqid ⊢ 1 2 = 1 2
98 53 dec0h ⊢ 7 = 0 7
99 1 8 deccl ⊢ 1 3 ∈ ℕ0
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 · 1 ) = 1
105 00id ⊢ ( 0 + 0 ) = 0
106 104 105 oveq12i ⊢ ( ( 1 · 1 ) + ( 0 + 0 ) ) = ( 1 + 0 )
107 27 addid1i ⊢ ( 1 + 0 ) = 1
108 106 107 eqtri ⊢ ( ( 1 · 1 ) + ( 0 + 0 ) ) = 1
109 32 mulid1i ⊢ ( 3 · 1 ) = 3
110 109 oveq1i ⊢ ( ( 3 · 1 ) + 3 ) = ( 3 + 3 )
111 3p3e6 ⊢ ( 3 + 3 ) = 6
112 110 111 eqtri ⊢ ( ( 3 · 1 ) + 3 ) = 6
113 2 dec0h ⊢ 6 = 0 6
114 112 113 eqtri ⊢ ( ( 3 · 1 ) + 3 ) = 0 6
115 1 8 24 8 100 103 1 2 24 108 114 decmac ⊢ ( ( 1 3 · 1 ) + ( 0 + 3 ) ) = 1 6
116 18 28 oveq12i ⊢ ( ( 1 · 2 ) + ( 0 + 1 ) ) = ( 2 + 1 )
117 116 38 eqtri ⊢ ( ( 1 · 2 ) + ( 0 + 1 ) ) = 3
118 3t2e6 ⊢ ( 3 · 2 ) = 6
119 118 oveq1i ⊢ ( ( 3 · 2 ) + 7 ) = ( 6 + 7 )
120 7cn ⊢ 7 ∈ ℂ
121 6cn ⊢ 6 ∈ ℂ
122 7p6e13 ⊢ ( 7 + 6 ) = 1 3
123 120 121 122 addcomli ⊢ ( 6 + 7 ) = 1 3
124 119 123 eqtri ⊢ ( ( 3 · 2 ) + 7 ) = 1 3
125 1 8 24 53 100 98 37 8 1 117 124 decmac ⊢ ( ( 1 3 · 2 ) + 7 ) = 3 3
126 1 37 24 53 97 98 99 8 8 115 125 decma2c ⊢ ( ( 1 3 · 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 ∈ ℕ
131 10nn ⊢ 1 0 ∈ ℕ
132 eqid ⊢ 1 7 = 1 7
133 eqid ⊢ 1 0 = 1 0
134 86 mulid2i ⊢ ( 1 · 9 ) = 9
135 6p1e7 ⊢ ( 6 + 1 ) = 7
136 121 27 135 addcomli ⊢ ( 1 + 6 ) = 7
137 134 136 oveq12i ⊢ ( ( 1 · 9 ) + ( 1 + 6 ) ) = ( 9 + 7 )
138 9p7e16 ⊢ ( 9 + 7 ) = 1 6
139 137 138 eqtri ⊢ ( ( 1 · 9 ) + ( 1 + 6 ) ) = 1 6
140 9t7e63 ⊢ ( 9 · 7 ) = 6 3
141 86 120 140 mulcomli ⊢ ( 7 · 9 ) = 6 3
142 141 oveq1i ⊢ ( ( 7 · 9 ) + 0 ) = ( 6 3 + 0 )
143 2 8 deccl ⊢ 6 3 ∈ ℕ0
144 143 nn0cni ⊢ 6 3 ∈ ℂ
145 144 addid1i ⊢ ( 6 3 + 0 ) = 6 3
146 142 145 eqtri ⊢ ( ( 7 · 9 ) + 0 ) = 6 3
147 1 53 1 24 132 133 69 8 2 139 146 decmac ⊢ ( ( 1 7 · 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 ∈ ℕ
152 eqid ⊢ 1 9 = 1 9
153 8cn ⊢ 8 ∈ ℂ
154 153 mulid2i ⊢ ( 1 · 8 ) = 8
155 7p1e8 ⊢ ( 7 + 1 ) = 8
156 120 27 155 addcomli ⊢ ( 1 + 7 ) = 8
157 154 156 oveq12i ⊢ ( ( 1 · 8 ) + ( 1 + 7 ) ) = ( 8 + 8 )
158 8p8e16 ⊢ ( 8 + 8 ) = 1 6
159 157 158 eqtri ⊢ ( ( 1 · 8 ) + ( 1 + 7 ) ) = 1 6
160 9t8e72 ⊢ ( 9 · 8 ) = 7 2
161 53 37 38 160 decsuc ⊢ ( ( 9 · 8 ) + 1 ) = 7 3
162 1 69 1 1 152 80 6 8 53 159 161 decmac ⊢ ( ( 1 9 · 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 ∈ ℕ
167 120 17 56 mulcomli ⊢ ( 2 · 7 ) = 1 4
168 1 7 37 167 57 decaddi ⊢ ( ( 2 · 7 ) + 2 ) = 1 6
169 120 32 60 mulcomli ⊢ ( 3 · 7 ) = 2 1
170 37 1 37 169 61 decaddi ⊢ ( ( 3 · 7 ) + 2 ) = 2 3
171 37 8 37 51 53 8 37 168 170 decrmac ⊢ ( ( 2 3 · 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 ∈ ℙ