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 e. Prime

Proof

Step Hyp Ref Expression
1 3nn0 
 |-  3 e. NN0
2 1nn0 
 |-  1 e. NN0
3 1 2 deccl 
 |-  ; 3 1 e. NN0
4 7nn 
 |-  7 e. NN
5 3 4 decnncl 
 |-  ; ; 3 1 7 e. NN
6 8nn0 
 |-  8 e. NN0
7 4nn0 
 |-  4 e. NN0
8 7nn0 
 |-  7 e. NN0
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 e. NN
14 1 13 decnncl 
 |-  ; 3 1 e. NN
15 14 8 2 10 declti 
 |-  1 < ; ; 3 1 7
16 3t2e6 
 |-  ( 3 x. 2 ) = 6
17 df-7 
 |-  7 = ( 6 + 1 )
18 3 1 16 17 dec2dvds 
 |-  -. 2 || ; ; 3 1 7
19 3nn 
 |-  3 e. NN
20 10nn0 
 |-  ; 1 0 e. NN0
21 5nn0 
 |-  5 e. NN0
22 20 21 deccl 
 |-  ; ; 1 0 5 e. NN0
23 2nn 
 |-  2 e. NN
24 0nn0 
 |-  0 e. NN0
25 2nn0 
 |-  2 e. NN0
26 eqid 
 |-  ; ; 1 0 5 = ; ; 1 0 5
27 25 dec0h 
 |-  2 = ; 0 2
28 eqid 
 |-  ; 1 0 = ; 1 0
29 ax-1cn 
 |-  1 e. CC
30 29 addid2i 
 |-  ( 0 + 1 ) = 1
31 2 dec0h 
 |-  1 = ; 0 1
32 30 31 eqtri 
 |-  ( 0 + 1 ) = ; 0 1
33 3cn 
 |-  3 e. CC
34 33 mulid1i 
 |-  ( 3 x. 1 ) = 3
35 00id 
 |-  ( 0 + 0 ) = 0
36 34 35 oveq12i 
 |-  ( ( 3 x. 1 ) + ( 0 + 0 ) ) = ( 3 + 0 )
37 33 addid1i 
 |-  ( 3 + 0 ) = 3
38 36 37 eqtri 
 |-  ( ( 3 x. 1 ) + ( 0 + 0 ) ) = 3
39 33 mul01i 
 |-  ( 3 x. 0 ) = 0
40 39 oveq1i 
 |-  ( ( 3 x. 0 ) + 1 ) = ( 0 + 1 )
41 40 30 eqtri 
 |-  ( ( 3 x. 0 ) + 1 ) = 1
42 41 31 eqtri 
 |-  ( ( 3 x. 0 ) + 1 ) = ; 0 1
43 2 24 24 2 28 32 1 2 24 38 42 decma2c 
 |-  ( ( 3 x. ; 1 0 ) + ( 0 + 1 ) ) = ; 3 1
44 5cn 
 |-  5 e. CC
45 5t3e15 
 |-  ( 5 x. 3 ) = ; 1 5
46 44 33 45 mulcomli 
 |-  ( 3 x. 5 ) = ; 1 5
47 5p2e7 
 |-  ( 5 + 2 ) = 7
48 2 21 25 46 47 decaddi 
 |-  ( ( 3 x. 5 ) + 2 ) = ; 1 7
49 20 21 24 25 26 27 1 8 2 43 48 decma2c 
 |-  ( ( 3 x. ; ; 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 e. NN0
55 eqid 
 |-  ; 4 5 = ; 4 5
56 33 addid2i 
 |-  ( 0 + 3 ) = 3
57 56 oveq2i 
 |-  ( ( 7 x. 4 ) + ( 0 + 3 ) ) = ( ( 7 x. 4 ) + 3 )
58 7t4e28 
 |-  ( 7 x. 4 ) = ; 2 8
59 2p1e3 
 |-  ( 2 + 1 ) = 3
60 8p3e11 
 |-  ( 8 + 3 ) = ; 1 1
61 25 6 1 58 59 2 60 decaddci 
 |-  ( ( 7 x. 4 ) + 3 ) = ; 3 1
62 57 61 eqtri 
 |-  ( ( 7 x. 4 ) + ( 0 + 3 ) ) = ; 3 1
63 7t5e35 
 |-  ( 7 x. 5 ) = ; 3 5
64 1 21 25 63 47 decaddi 
 |-  ( ( 7 x. 5 ) + 2 ) = ; 3 7
65 7 21 24 25 55 27 8 8 1 62 64 decma2c 
 |-  ( ( 7 x. ; 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 e. NN
69 25 6 deccl 
 |-  ; 2 8 e. NN0
70 9nn 
 |-  9 e. NN
71 9nn0 
 |-  9 e. NN0
72 eqid 
 |-  ; 2 8 = ; 2 8
73 71 dec0h 
 |-  9 = ; 0 9
74 2 2 deccl 
 |-  ; 1 1 e. NN0
75 eqid 
 |-  ; 1 1 = ; 1 1
76 9cn 
 |-  9 e. CC
77 76 addid2i 
 |-  ( 0 + 9 ) = 9
78 77 73 eqtri 
 |-  ( 0 + 9 ) = ; 0 9
79 2cn 
 |-  2 e. CC
80 79 mulid2i 
 |-  ( 1 x. 2 ) = 2
81 80 30 oveq12i 
 |-  ( ( 1 x. 2 ) + ( 0 + 1 ) ) = ( 2 + 1 )
82 81 59 eqtri 
 |-  ( ( 1 x. 2 ) + ( 0 + 1 ) ) = 3
83 80 oveq1i 
 |-  ( ( 1 x. 2 ) + 9 ) = ( 2 + 9 )
84 9p2e11 
 |-  ( 9 + 2 ) = ; 1 1
85 76 79 84 addcomli 
 |-  ( 2 + 9 ) = ; 1 1
86 83 85 eqtri 
 |-  ( ( 1 x. 2 ) + 9 ) = ; 1 1
87 2 2 24 71 75 78 25 2 2 82 86 decmac 
 |-  ( ( ; 1 1 x. 2 ) + ( 0 + 9 ) ) = ; 3 1
88 8cn 
 |-  8 e. CC
89 88 mulid2i 
 |-  ( 1 x. 8 ) = 8
90 89 30 oveq12i 
 |-  ( ( 1 x. 8 ) + ( 0 + 1 ) ) = ( 8 + 1 )
91 8p1e9 
 |-  ( 8 + 1 ) = 9
92 90 91 eqtri 
 |-  ( ( 1 x. 8 ) + ( 0 + 1 ) ) = 9
93 89 oveq1i 
 |-  ( ( 1 x. 8 ) + 9 ) = ( 8 + 9 )
94 9p8e17 
 |-  ( 9 + 8 ) = ; 1 7
95 76 88 94 addcomli 
 |-  ( 8 + 9 ) = ; 1 7
96 93 95 eqtri 
 |-  ( ( 1 x. 8 ) + 9 ) = ; 1 7
97 2 2 24 71 75 73 6 8 2 92 96 decmac 
 |-  ( ( ; 1 1 x. 8 ) + 9 ) = ; 9 7
98 25 6 24 71 72 73 74 8 71 87 97 decma2c 
 |-  ( ( ; 1 1 x. ; 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 e. NN
103 25 7 deccl 
 |-  ; 2 4 e. NN0
104 5nn 
 |-  5 e. NN
105 eqid 
 |-  ; 2 4 = ; 2 4
106 21 dec0h 
 |-  5 = ; 0 5
107 2 1 deccl 
 |-  ; 1 3 e. NN0
108 eqid 
 |-  ; 1 3 = ; 1 3
109 44 addid2i 
 |-  ( 0 + 5 ) = 5
110 109 106 eqtri 
 |-  ( 0 + 5 ) = ; 0 5
111 16 oveq1i 
 |-  ( ( 3 x. 2 ) + 5 ) = ( 6 + 5 )
112 6p5e11 
 |-  ( 6 + 5 ) = ; 1 1
113 111 112 eqtri 
 |-  ( ( 3 x. 2 ) + 5 ) = ; 1 1
114 2 1 24 21 108 110 25 2 2 82 113 decmac 
 |-  ( ( ; 1 3 x. 2 ) + ( 0 + 5 ) ) = ; 3 1
115 4cn 
 |-  4 e. CC
116 115 mulid2i 
 |-  ( 1 x. 4 ) = 4
117 116 30 oveq12i 
 |-  ( ( 1 x. 4 ) + ( 0 + 1 ) ) = ( 4 + 1 )
118 4p1e5 
 |-  ( 4 + 1 ) = 5
119 117 118 eqtri 
 |-  ( ( 1 x. 4 ) + ( 0 + 1 ) ) = 5
120 4t3e12 
 |-  ( 4 x. 3 ) = ; 1 2
121 115 33 120 mulcomli 
 |-  ( 3 x. 4 ) = ; 1 2
122 44 79 47 addcomli 
 |-  ( 2 + 5 ) = 7
123 2 25 21 121 122 decaddi 
 |-  ( ( 3 x. 4 ) + 5 ) = ; 1 7
124 2 1 24 21 108 106 7 8 2 119 123 decmac 
 |-  ( ( ; 1 3 x. 4 ) + 5 ) = ; 5 7
125 25 7 24 21 105 106 107 8 21 114 124 decma2c 
 |-  ( ( ; 1 3 x. ; 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 e. NN
130 2 6 deccl 
 |-  ; 1 8 e. NN0
131 eqid 
 |-  ; 1 8 = ; 1 8
132 2 8 deccl 
 |-  ; 1 7 e. NN0
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 x. 1 ) = 1
138 1p1e2 
 |-  ( 1 + 1 ) = 2
139 137 138 oveq12i 
 |-  ( ( 1 x. 1 ) + ( 1 + 1 ) ) = ( 1 + 2 )
140 1p2e3 
 |-  ( 1 + 2 ) = 3
141 139 140 eqtri 
 |-  ( ( 1 x. 1 ) + ( 1 + 1 ) ) = 3
142 7cn 
 |-  7 e. CC
143 142 mulid1i 
 |-  ( 7 x. 1 ) = 7
144 143 oveq1i 
 |-  ( ( 7 x. 1 ) + 4 ) = ( 7 + 4 )
145 7p4e11 
 |-  ( 7 + 4 ) = ; 1 1
146 144 145 eqtri 
 |-  ( ( 7 x. 1 ) + 4 ) = ; 1 1
147 2 8 2 7 133 136 2 2 2 141 146 decmac 
 |-  ( ( ; 1 7 x. 1 ) + ( 1 + ; 1 3 ) ) = ; 3 1
148 89 109 oveq12i 
 |-  ( ( 1 x. 8 ) + ( 0 + 5 ) ) = ( 8 + 5 )
149 8p5e13 
 |-  ( 8 + 5 ) = ; 1 3
150 148 149 eqtri 
 |-  ( ( 1 x. 8 ) + ( 0 + 5 ) ) = ; 1 3
151 6nn0 
 |-  6 e. NN0
152 6p1e7 
 |-  ( 6 + 1 ) = 7
153 8t7e56 
 |-  ( 8 x. 7 ) = ; 5 6
154 88 142 153 mulcomli 
 |-  ( 7 x. 8 ) = ; 5 6
155 21 151 152 154 decsuc 
 |-  ( ( 7 x. 8 ) + 1 ) = ; 5 7
156 2 8 24 2 133 31 6 8 21 150 155 decmac 
 |-  ( ( ; 1 7 x. 8 ) + 1 ) = ; ; 1 3 7
157 2 6 2 2 131 75 132 8 107 147 156 decma2c 
 |-  ( ( ; 1 7 x. ; 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 e. NN
162 2 151 deccl 
 |-  ; 1 6 e. NN0
163 eqid 
 |-  ; 1 6 = ; 1 6
164 2 71 deccl 
 |-  ; 1 9 e. NN0
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 x. 1 ) = 9
168 167 oveq1i 
 |-  ( ( 9 x. 1 ) + 2 ) = ( 9 + 2 )
169 168 84 eqtri 
 |-  ( ( 9 x. 1 ) + 2 ) = ; 1 1
170 2 71 2 25 165 166 2 2 2 141 169 decmac 
 |-  ( ( ; 1 9 x. 1 ) + ( 1 + ; 1 1 ) ) = ; 3 1
171 1 dec0h 
 |-  3 = ; 0 3
172 6cn 
 |-  6 e. CC
173 172 mulid2i 
 |-  ( 1 x. 6 ) = 6
174 173 109 oveq12i 
 |-  ( ( 1 x. 6 ) + ( 0 + 5 ) ) = ( 6 + 5 )
175 174 112 eqtri 
 |-  ( ( 1 x. 6 ) + ( 0 + 5 ) ) = ; 1 1
176 9t6e54 
 |-  ( 9 x. 6 ) = ; 5 4
177 4p3e7 
 |-  ( 4 + 3 ) = 7
178 21 7 1 176 177 decaddi 
 |-  ( ( 9 x. 6 ) + 3 ) = ; 5 7
179 2 71 24 1 165 171 151 8 21 175 178 decmac 
 |-  ( ( ; 1 9 x. 6 ) + 3 ) = ; ; 1 1 7
180 2 151 2 1 163 108 164 8 74 170 179 decma2c 
 |-  ( ( ; 1 9 x. ; 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 e. NN
185 102 nnnn0i 
 |-  ; 1 3 e. NN0
186 8nn 
 |-  8 e. NN
187 2 186 decnncl 
 |-  ; 1 8 e. NN
188 25 1 deccl 
 |-  ; 2 3 e. NN0
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 x. 1 ) = 2
195 194 30 oveq12i 
 |-  ( ( 2 x. 1 ) + ( 0 + 1 ) ) = ( 2 + 1 )
196 195 59 eqtri 
 |-  ( ( 2 x. 1 ) + ( 0 + 1 ) ) = 3
197 34 oveq1i 
 |-  ( ( 3 x. 1 ) + 8 ) = ( 3 + 8 )
198 88 33 60 addcomli 
 |-  ( 3 + 8 ) = ; 1 1
199 197 198 eqtri 
 |-  ( ( 3 x. 1 ) + 8 ) = ; 1 1
200 25 1 24 6 189 193 2 2 2 196 199 decmac 
 |-  ( ( ; 2 3 x. 1 ) + ( 1 + 7 ) ) = ; 3 1
201 33 79 16 mulcomli 
 |-  ( 2 x. 3 ) = 6
202 201 30 oveq12i 
 |-  ( ( 2 x. 3 ) + ( 0 + 1 ) ) = ( 6 + 1 )
203 202 152 eqtri 
 |-  ( ( 2 x. 3 ) + ( 0 + 1 ) ) = 7
204 3t3e9 
 |-  ( 3 x. 3 ) = 9
205 204 oveq1i 
 |-  ( ( 3 x. 3 ) + 8 ) = ( 9 + 8 )
206 205 94 eqtri 
 |-  ( ( 3 x. 3 ) + 8 ) = ; 1 7
207 25 1 24 6 189 192 1 8 2 203 206 decmac 
 |-  ( ( ; 2 3 x. 3 ) + 8 ) = ; 7 7
208 2 1 2 6 108 131 188 8 8 200 207 decma2c 
 |-  ( ( ; 2 3 x. ; 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 e. Prime