Metamath Proof Explorer

Theorem 317prm

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

Ref Expression
Assertion 317prm 3 1 7 ∈ ℙ

Proof

Step Hyp Ref Expression
1 3nn0 ⊢ 3 ∈ ℕ0
2 1nn0 ⊢ 1 ∈ ℕ0
3 1 2 deccl ⊢ 3 1 ∈ ℕ0
4 7nn ⊢ 7 ∈ ℕ
5 3 4 decnncl ⊢ 3 1 7 ∈ ℕ
6 8nn0 ⊢ 8 ∈ ℕ0
7 4nn0 ⊢ 4 ∈ ℕ0
8 7nn0 ⊢ 7 ∈ ℕ0
9 3lt8 ⊢ 3 < 8
10 1lt10 ⊢ 1 < 1 0
11 7lt10 ⊢ 7 < 1 0
12 1 6 2 7 8 2 9 10 11 3decltc ⊢ 3 1 7 < 8 4 1
13 1nn ⊢ 1 ∈ ℕ
14 1 13 decnncl ⊢ 3 1 ∈ ℕ
15 14 8 2 10 declti ⊢ 1 < 3 1 7
16 3t2e6 ⊢ ( 3 · 2 ) = 6
17 df-7 ⊢ 7 = ( 6 + 1 )
18 3 1 16 17 dec2dvds ⊢ ¬ 2 ∥ 3 1 7
19 3nn ⊢ 3 ∈ ℕ
20 10nn0 ⊢ 1 0 ∈ ℕ0
21 5nn0 ⊢ 5 ∈ ℕ0
22 20 21 deccl ⊢ 1 0 5 ∈ ℕ0
23 2nn ⊢ 2 ∈ ℕ
24 0nn0 ⊢ 0 ∈ ℕ0
25 2nn0 ⊢ 2 ∈ ℕ0
26 eqid ⊢ 1 0 5 = 1 0 5
27 25 dec0h ⊢ 2 = 0 2
28 eqid ⊢ 1 0 = 1 0
29 ax-1cn ⊢ 1 ∈ ℂ
30 29 addid2i ⊢ ( 0 + 1 ) = 1
31 2 dec0h ⊢ 1 = 0 1
32 30 31 eqtri ⊢ ( 0 + 1 ) = 0 1
33 3cn ⊢ 3 ∈ ℂ
34 33 mulid1i ⊢ ( 3 · 1 ) = 3
35 00id ⊢ ( 0 + 0 ) = 0
36 34 35 oveq12i ⊢ ( ( 3 · 1 ) + ( 0 + 0 ) ) = ( 3 + 0 )
37 33 addid1i ⊢ ( 3 + 0 ) = 3
38 36 37 eqtri ⊢ ( ( 3 · 1 ) + ( 0 + 0 ) ) = 3
39 33 mul01i ⊢ ( 3 · 0 ) = 0
40 39 oveq1i ⊢ ( ( 3 · 0 ) + 1 ) = ( 0 + 1 )
41 40 30 eqtri ⊢ ( ( 3 · 0 ) + 1 ) = 1
42 41 31 eqtri ⊢ ( ( 3 · 0 ) + 1 ) = 0 1
43 2 24 24 2 28 32 1 2 24 38 42 decma2c ⊢ ( ( 3 · 1 0 ) + ( 0 + 1 ) ) = 3 1
44 5cn ⊢ 5 ∈ ℂ
45 5t3e15 ⊢ ( 5 · 3 ) = 1 5
46 44 33 45 mulcomli ⊢ ( 3 · 5 ) = 1 5
47 5p2e7 ⊢ ( 5 + 2 ) = 7
48 2 21 25 46 47 decaddi ⊢ ( ( 3 · 5 ) + 2 ) = 1 7
49 20 21 24 25 26 27 1 8 2 43 48 decma2c ⊢ ( ( 3 · 1 0 5 ) + 2 ) = 3 1 7
50 2lt3 ⊢ 2 < 3
51 19 22 23 49 50 ndvdsi ⊢ ¬ 3 ∥ 3 1 7
52 2lt5 ⊢ 2 < 5
53 3 23 52 47 dec5dvds2 ⊢ ¬ 5 ∥ 3 1 7
54 7 21 deccl ⊢ 4 5 ∈ ℕ0
55 eqid ⊢ 4 5 = 4 5
56 33 addid2i ⊢ ( 0 + 3 ) = 3
57 56 oveq2i ⊢ ( ( 7 · 4 ) + ( 0 + 3 ) ) = ( ( 7 · 4 ) + 3 )
58 7t4e28 ⊢ ( 7 · 4 ) = 2 8
59 2p1e3 ⊢ ( 2 + 1 ) = 3
60 8p3e11 ⊢ ( 8 + 3 ) = 1 1
61 25 6 1 58 59 2 60 decaddci ⊢ ( ( 7 · 4 ) + 3 ) = 3 1
62 57 61 eqtri ⊢ ( ( 7 · 4 ) + ( 0 + 3 ) ) = 3 1
63 7t5e35 ⊢ ( 7 · 5 ) = 3 5
64 1 21 25 63 47 decaddi ⊢ ( ( 7 · 5 ) + 2 ) = 3 7
65 7 21 24 25 55 27 8 8 1 62 64 decma2c ⊢ ( ( 7 · 4 5 ) + 2 ) = 3 1 7
66 2lt7 ⊢ 2 < 7
67 4 54 23 65 66 ndvdsi ⊢ ¬ 7 ∥ 3 1 7
68 2 13 decnncl ⊢ 1 1 ∈ ℕ
69 25 6 deccl ⊢ 2 8 ∈ ℕ0
70 9nn ⊢ 9 ∈ ℕ
71 9nn0 ⊢ 9 ∈ ℕ0
72 eqid ⊢ 2 8 = 2 8
73 71 dec0h ⊢ 9 = 0 9
74 2 2 deccl ⊢ 1 1 ∈ ℕ0
75 eqid ⊢ 1 1 = 1 1
76 9cn ⊢ 9 ∈ ℂ
77 76 addid2i ⊢ ( 0 + 9 ) = 9
78 77 73 eqtri ⊢ ( 0 + 9 ) = 0 9
79 2cn ⊢ 2 ∈ ℂ
80 79 mulid2i ⊢ ( 1 · 2 ) = 2
81 80 30 oveq12i ⊢ ( ( 1 · 2 ) + ( 0 + 1 ) ) = ( 2 + 1 )
82 81 59 eqtri ⊢ ( ( 1 · 2 ) + ( 0 + 1 ) ) = 3
83 80 oveq1i ⊢ ( ( 1 · 2 ) + 9 ) = ( 2 + 9 )
84 9p2e11 ⊢ ( 9 + 2 ) = 1 1
85 76 79 84 addcomli ⊢ ( 2 + 9 ) = 1 1
86 83 85 eqtri ⊢ ( ( 1 · 2 ) + 9 ) = 1 1
87 2 2 24 71 75 78 25 2 2 82 86 decmac ⊢ ( ( 1 1 · 2 ) + ( 0 + 9 ) ) = 3 1
88 8cn ⊢ 8 ∈ ℂ
89 88 mulid2i ⊢ ( 1 · 8 ) = 8
90 89 30 oveq12i ⊢ ( ( 1 · 8 ) + ( 0 + 1 ) ) = ( 8 + 1 )
91 8p1e9 ⊢ ( 8 + 1 ) = 9
92 90 91 eqtri ⊢ ( ( 1 · 8 ) + ( 0 + 1 ) ) = 9
93 89 oveq1i ⊢ ( ( 1 · 8 ) + 9 ) = ( 8 + 9 )
94 9p8e17 ⊢ ( 9 + 8 ) = 1 7
95 76 88 94 addcomli ⊢ ( 8 + 9 ) = 1 7
96 93 95 eqtri ⊢ ( ( 1 · 8 ) + 9 ) = 1 7
97 2 2 24 71 75 73 6 8 2 92 96 decmac ⊢ ( ( 1 1 · 8 ) + 9 ) = 9 7
98 25 6 24 71 72 73 74 8 71 87 97 decma2c ⊢ ( ( 1 1 · 2 8 ) + 9 ) = 3 1 7
99 9lt10 ⊢ 9 < 1 0
100 13 2 71 99 declti ⊢ 9 < 1 1
101 68 69 70 98 100 ndvdsi ⊢ ¬ 1 1 ∥ 3 1 7
102 2 19 decnncl ⊢ 1 3 ∈ ℕ
103 25 7 deccl ⊢ 2 4 ∈ ℕ0
104 5nn ⊢ 5 ∈ ℕ
105 eqid ⊢ 2 4 = 2 4
106 21 dec0h ⊢ 5 = 0 5
107 2 1 deccl ⊢ 1 3 ∈ ℕ0
108 eqid ⊢ 1 3 = 1 3
109 44 addid2i ⊢ ( 0 + 5 ) = 5
110 109 106 eqtri ⊢ ( 0 + 5 ) = 0 5
111 16 oveq1i ⊢ ( ( 3 · 2 ) + 5 ) = ( 6 + 5 )
112 6p5e11 ⊢ ( 6 + 5 ) = 1 1
113 111 112 eqtri ⊢ ( ( 3 · 2 ) + 5 ) = 1 1
114 2 1 24 21 108 110 25 2 2 82 113 decmac ⊢ ( ( 1 3 · 2 ) + ( 0 + 5 ) ) = 3 1
115 4cn ⊢ 4 ∈ ℂ
116 115 mulid2i ⊢ ( 1 · 4 ) = 4
117 116 30 oveq12i ⊢ ( ( 1 · 4 ) + ( 0 + 1 ) ) = ( 4 + 1 )
118 4p1e5 ⊢ ( 4 + 1 ) = 5
119 117 118 eqtri ⊢ ( ( 1 · 4 ) + ( 0 + 1 ) ) = 5
120 4t3e12 ⊢ ( 4 · 3 ) = 1 2
121 115 33 120 mulcomli ⊢ ( 3 · 4 ) = 1 2
122 44 79 47 addcomli ⊢ ( 2 + 5 ) = 7
123 2 25 21 121 122 decaddi ⊢ ( ( 3 · 4 ) + 5 ) = 1 7
124 2 1 24 21 108 106 7 8 2 119 123 decmac ⊢ ( ( 1 3 · 4 ) + 5 ) = 5 7
125 25 7 24 21 105 106 107 8 21 114 124 decma2c ⊢ ( ( 1 3 · 2 4 ) + 5 ) = 3 1 7
126 5lt10 ⊢ 5 < 1 0
127 13 1 21 126 declti ⊢ 5 < 1 3
128 102 103 104 125 127 ndvdsi ⊢ ¬ 1 3 ∥ 3 1 7
129 2 4 decnncl ⊢ 1 7 ∈ ℕ
130 2 6 deccl ⊢ 1 8 ∈ ℕ0
131 eqid ⊢ 1 8 = 1 8
132 2 8 deccl ⊢ 1 7 ∈ ℕ0
133 eqid ⊢ 1 7 = 1 7
134 3p1e4 ⊢ ( 3 + 1 ) = 4
135 33 29 134 addcomli ⊢ ( 1 + 3 ) = 4
136 24 2 2 1 31 108 30 135 decadd ⊢ ( 1 + 1 3 ) = 1 4
137 29 mulid1i ⊢ ( 1 · 1 ) = 1
138 1p1e2 ⊢ ( 1 + 1 ) = 2
139 137 138 oveq12i ⊢ ( ( 1 · 1 ) + ( 1 + 1 ) ) = ( 1 + 2 )
140 1p2e3 ⊢ ( 1 + 2 ) = 3
141 139 140 eqtri ⊢ ( ( 1 · 1 ) + ( 1 + 1 ) ) = 3
142 7cn ⊢ 7 ∈ ℂ
143 142 mulid1i ⊢ ( 7 · 1 ) = 7
144 143 oveq1i ⊢ ( ( 7 · 1 ) + 4 ) = ( 7 + 4 )
145 7p4e11 ⊢ ( 7 + 4 ) = 1 1
146 144 145 eqtri ⊢ ( ( 7 · 1 ) + 4 ) = 1 1
147 2 8 2 7 133 136 2 2 2 141 146 decmac ⊢ ( ( 1 7 · 1 ) + ( 1 + 1 3 ) ) = 3 1
148 89 109 oveq12i ⊢ ( ( 1 · 8 ) + ( 0 + 5 ) ) = ( 8 + 5 )
149 8p5e13 ⊢ ( 8 + 5 ) = 1 3
150 148 149 eqtri ⊢ ( ( 1 · 8 ) + ( 0 + 5 ) ) = 1 3
151 6nn0 ⊢ 6 ∈ ℕ0
152 6p1e7 ⊢ ( 6 + 1 ) = 7
153 8t7e56 ⊢ ( 8 · 7 ) = 5 6
154 88 142 153 mulcomli ⊢ ( 7 · 8 ) = 5 6
155 21 151 152 154 decsuc ⊢ ( ( 7 · 8 ) + 1 ) = 5 7
156 2 8 24 2 133 31 6 8 21 150 155 decmac ⊢ ( ( 1 7 · 8 ) + 1 ) = 1 3 7
157 2 6 2 2 131 75 132 8 107 147 156 decma2c ⊢ ( ( 1 7 · 1 8 ) + 1 1 ) = 3 1 7
158 1lt7 ⊢ 1 < 7
159 2 2 4 158 declt ⊢ 1 1 < 1 7
160 129 130 68 157 159 ndvdsi ⊢ ¬ 1 7 ∥ 3 1 7
161 2 70 decnncl ⊢ 1 9 ∈ ℕ
162 2 151 deccl ⊢ 1 6 ∈ ℕ0
163 eqid ⊢ 1 6 = 1 6
164 2 71 deccl ⊢ 1 9 ∈ ℕ0
165 eqid ⊢ 1 9 = 1 9
166 24 2 2 2 31 75 30 138 decadd ⊢ ( 1 + 1 1 ) = 1 2
167 76 mulid1i ⊢ ( 9 · 1 ) = 9
168 167 oveq1i ⊢ ( ( 9 · 1 ) + 2 ) = ( 9 + 2 )
169 168 84 eqtri ⊢ ( ( 9 · 1 ) + 2 ) = 1 1
170 2 71 2 25 165 166 2 2 2 141 169 decmac ⊢ ( ( 1 9 · 1 ) + ( 1 + 1 1 ) ) = 3 1
171 1 dec0h ⊢ 3 = 0 3
172 6cn ⊢ 6 ∈ ℂ
173 172 mulid2i ⊢ ( 1 · 6 ) = 6
174 173 109 oveq12i ⊢ ( ( 1 · 6 ) + ( 0 + 5 ) ) = ( 6 + 5 )
175 174 112 eqtri ⊢ ( ( 1 · 6 ) + ( 0 + 5 ) ) = 1 1
176 9t6e54 ⊢ ( 9 · 6 ) = 5 4
177 4p3e7 ⊢ ( 4 + 3 ) = 7
178 21 7 1 176 177 decaddi ⊢ ( ( 9 · 6 ) + 3 ) = 5 7
179 2 71 24 1 165 171 151 8 21 175 178 decmac ⊢ ( ( 1 9 · 6 ) + 3 ) = 1 1 7
180 2 151 2 1 163 108 164 8 74 170 179 decma2c ⊢ ( ( 1 9 · 1 6 ) + 1 3 ) = 3 1 7
181 3lt9 ⊢ 3 < 9
182 2 1 70 181 declt ⊢ 1 3 < 1 9
183 161 162 102 180 182 ndvdsi ⊢ ¬ 1 9 ∥ 3 1 7
184 25 19 decnncl ⊢ 2 3 ∈ ℕ
185 102 nnnn0i ⊢ 1 3 ∈ ℕ0
186 8nn ⊢ 8 ∈ ℕ
187 2 186 decnncl ⊢ 1 8 ∈ ℕ
188 25 1 deccl ⊢ 2 3 ∈ ℕ0
189 eqid ⊢ 2 3 = 2 3
190 7p1e8 ⊢ ( 7 + 1 ) = 8
191 142 29 190 addcomli ⊢ ( 1 + 7 ) = 8
192 6 dec0h ⊢ 8 = 0 8
193 191 192 eqtri ⊢ ( 1 + 7 ) = 0 8
194 79 mulid1i ⊢ ( 2 · 1 ) = 2
195 194 30 oveq12i ⊢ ( ( 2 · 1 ) + ( 0 + 1 ) ) = ( 2 + 1 )
196 195 59 eqtri ⊢ ( ( 2 · 1 ) + ( 0 + 1 ) ) = 3
197 34 oveq1i ⊢ ( ( 3 · 1 ) + 8 ) = ( 3 + 8 )
198 88 33 60 addcomli ⊢ ( 3 + 8 ) = 1 1
199 197 198 eqtri ⊢ ( ( 3 · 1 ) + 8 ) = 1 1
200 25 1 24 6 189 193 2 2 2 196 199 decmac ⊢ ( ( 2 3 · 1 ) + ( 1 + 7 ) ) = 3 1
201 33 79 16 mulcomli ⊢ ( 2 · 3 ) = 6
202 201 30 oveq12i ⊢ ( ( 2 · 3 ) + ( 0 + 1 ) ) = ( 6 + 1 )
203 202 152 eqtri ⊢ ( ( 2 · 3 ) + ( 0 + 1 ) ) = 7
204 3t3e9 ⊢ ( 3 · 3 ) = 9
205 204 oveq1i ⊢ ( ( 3 · 3 ) + 8 ) = ( 9 + 8 )
206 205 94 eqtri ⊢ ( ( 3 · 3 ) + 8 ) = 1 7
207 25 1 24 6 189 192 1 8 2 203 206 decmac ⊢ ( ( 2 3 · 3 ) + 8 ) = 7 7
208 2 1 2 6 108 131 188 8 8 200 207 decma2c ⊢ ( ( 2 3 · 1 3 ) + 1 8 ) = 3 1 7
209 8lt10 ⊢ 8 < 1 0
210 1lt2 ⊢ 1 < 2
211 2 25 6 1 209 210 decltc ⊢ 1 8 < 2 3
212 184 185 187 208 211 ndvdsi ⊢ ¬ 2 3 ∥ 3 1 7
213 5 12 15 18 51 53 67 101 128 160 183 212 prmlem2 ⊢ 3 1 7 ∈ ℙ