Proof of Theorem 4001lem2
Step | Hyp | Ref
| Expression |
1 | | 4001prm.1 |
. . 3
;;;    |
2 | | 4nn0 10916 |
. . . . . 6
 |
3 | | 0nn0 10912 |
. . . . . 6
 |
4 | 2, 3 | deccl 11093 |
. . . . 5
;  |
5 | 4, 3 | deccl 11093 |
. . . 4
;;   |
6 | | 1nn 10647 |
. . . 4
 |
7 | 5, 6 | decnncl 11092 |
. . 3
;;;    |
8 | 1, 7 | eqeltri 2535 |
. 2
 |
9 | | 2nn 10795 |
. 2
 |
10 | | 9nn0 10921 |
. . . . 5
 |
11 | 2, 10 | deccl 11093 |
. . . 4
;  |
12 | 11, 3 | deccl 11093 |
. . 3
;;   |
13 | 12 | nn0zi 10990 |
. 2
;;   |
14 | | 1nn0 10913 |
. . . . 5
 |
15 | 14, 2 | deccl 11093 |
. . . 4
;  |
16 | 15, 3 | deccl 11093 |
. . 3
;;   |
17 | 16, 14 | deccl 11093 |
. 2
;;;    |
18 | | 2nn0 10914 |
. . . . 5
 |
19 | | 3nn0 10915 |
. . . . 5
 |
20 | 18, 19 | deccl 11093 |
. . . 4
;  |
21 | 20, 14 | deccl 11093 |
. . 3
;;   |
22 | 21, 14 | deccl 11093 |
. 2
;;;    |
23 | 18, 3 | deccl 11093 |
. . . 4
;  |
24 | 23, 3 | deccl 11093 |
. . 3
;;   |
25 | 23, 19 | deccl 11093 |
. . . 4
;;   |
26 | 25 | nn0zi 10990 |
. . 3
;;   |
27 | 10, 3 | deccl 11093 |
. . . 4
;  |
28 | 27, 18 | deccl 11093 |
. . 3
;;   |
29 | 1 | 4001lem1 15160 |
. . 3
   ;;    ;;    |
30 | | eqid 2461 |
. . . 4
;;  ;;   |
31 | | eqid 2461 |
. . . . . . 7
; ;  |
32 | | 2t2e4 10787 |
. . . . . . . . 9
   |
33 | 32 | oveq1i 6324 |
. . . . . . . 8
       |
34 | | 4cn 10714 |
. . . . . . . . 9
 |
35 | 34 | addid1i 9845 |
. . . . . . . 8
   |
36 | 33, 35 | eqtri 2483 |
. . . . . . 7
     |
37 | | 2cn 10707 |
. . . . . . . . 9
 |
38 | 37 | mul01i 9848 |
. . . . . . . 8
   |
39 | 3 | dec0h 11095 |
. . . . . . . 8
;  |
40 | 38, 39 | eqtri 2483 |
. . . . . . 7
  ;  |
41 | 18, 18, 3, 31, 3, 3,
36, 40 | decmul2c 11127 |
. . . . . 6
 ;  ;  |
42 | 41 | oveq1i 6324 |
. . . . 5
  ;   ;   |
43 | 4 | nn0cni 10909 |
. . . . . 6
;  |
44 | 43 | addid1i 9845 |
. . . . 5
;  ;  |
45 | 42, 44 | eqtri 2483 |
. . . 4
  ;   ;  |
46 | 18, 23, 3, 30, 3, 3,
45, 40 | decmul2c 11127 |
. . 3
 ;;   ;;   |
47 | | eqid 2461 |
. . . . 5
;;;   ;;;    |
48 | | 6nn0 10918 |
. . . . . . 7
 |
49 | 14, 48 | deccl 11093 |
. . . . . 6
;  |
50 | | eqid 2461 |
. . . . . 6
;;  ;;   |
51 | | eqid 2461 |
. . . . . . 7
;;  ;;   |
52 | | eqid 2461 |
. . . . . . . 8
; ;  |
53 | | 4p2e6 10772 |
. . . . . . . 8
   |
54 | 14, 2, 18, 52, 53 | decaddi 11123 |
. . . . . . 7
;  ;  |
55 | | 00id 9833 |
. . . . . . 7
   |
56 | 15, 3, 18, 3, 51, 31, 54, 55 | decadd 11120 |
. . . . . 6
;;  ;  ;;   |
57 | | eqid 2461 |
. . . . . . 7
; ;  |
58 | 49 | nn0cni 10909 |
. . . . . . . 8
;  |
59 | 58 | addid1i 9845 |
. . . . . . 7
;  ;  |
60 | | eqid 2461 |
. . . . . . . 8
;;  ;;   |
61 | | ax-1cn 9622 |
. . . . . . . . . 10
 |
62 | 61 | addid1i 9845 |
. . . . . . . . 9
   |
63 | 14 | dec0h 11095 |
. . . . . . . . 9
;  |
64 | 62, 63 | eqtri 2483 |
. . . . . . . 8
  ;  |
65 | 61 | addid2i 9846 |
. . . . . . . . . 10
   |
66 | 65, 63 | eqtri 2483 |
. . . . . . . . 9
  ;  |
67 | | 4t2e8 10791 |
. . . . . . . . . . . 12
   |
68 | 34, 37, 67 | mulcomli 9675 |
. . . . . . . . . . 11
   |
69 | 68, 55 | oveq12i 6326 |
. . . . . . . . . 10
         |
70 | | 8cn 10722 |
. . . . . . . . . . 11
 |
71 | 70 | addid1i 9845 |
. . . . . . . . . 10
   |
72 | 69, 71 | eqtri 2483 |
. . . . . . . . 9
       |
73 | 34 | mul02i 9847 |
. . . . . . . . . . 11
   |
74 | 73 | oveq1i 6324 |
. . . . . . . . . 10
       |
75 | 74, 65, 63 | 3eqtri 2487 |
. . . . . . . . 9
    ;  |
76 | 18, 3, 3, 14, 31, 66, 2, 14, 3, 72, 75 | decmac 11118 |
. . . . . . . 8
 ;     ;  |
77 | | 2p1e3 10761 |
. . . . . . . . 9
   |
78 | | 3cn 10711 |
. . . . . . . . . 10
 |
79 | | 4t3e12 11151 |
. . . . . . . . . 10
  ;  |
80 | 34, 78, 79 | mulcomli 9675 |
. . . . . . . . 9
  ;  |
81 | 14, 18, 77, 80 | decsuc 11102 |
. . . . . . . 8
    ;  |
82 | 23, 19, 3, 14, 60, 64, 2, 19, 14, 76, 81 | decmac 11118 |
. . . . . . 7
 ;;      ;;   |
83 | 25 | nn0cni 10909 |
. . . . . . . . . 10
;;   |
84 | 83 | mul01i 9848 |
. . . . . . . . 9
;;    |
85 | 84 | oveq1i 6324 |
. . . . . . . 8
 ;;       |
86 | | 6cn 10718 |
. . . . . . . . 9
 |
87 | 86 | addid2i 9846 |
. . . . . . . 8
   |
88 | 48 | dec0h 11095 |
. . . . . . . 8
;  |
89 | 85, 87, 88 | 3eqtri 2487 |
. . . . . . 7
 ;;    ;  |
90 | 2, 3, 14, 48, 57, 59, 25, 48, 3, 82, 89 | decma2c 11119 |
. . . . . 6
 ;;  ;  ;   ;;;    |
91 | 84 | oveq1i 6324 |
. . . . . . 7
 ;;       |
92 | 91, 55, 39 | 3eqtri 2487 |
. . . . . 6
 ;;    ;  |
93 | 4, 3, 49, 3, 50, 56, 25, 3, 3, 90, 92 | decma2c 11119 |
. . . . 5
 ;;  ;;   ;;  ;   ;;;;     |
94 | 55, 39 | eqtri 2483 |
. . . . . . 7
  ;  |
95 | 37 | mulid1i 9670 |
. . . . . . . . 9
   |
96 | 95, 55 | oveq12i 6326 |
. . . . . . . 8
         |
97 | 37 | addid1i 9845 |
. . . . . . . 8
   |
98 | 96, 97 | eqtri 2483 |
. . . . . . 7
       |
99 | 61 | mul02i 9847 |
. . . . . . . . 9
   |
100 | 99 | oveq1i 6324 |
. . . . . . . 8
       |
101 | 100, 55, 39 | 3eqtri 2487 |
. . . . . . 7
    ;  |
102 | 18, 3, 3, 3, 31, 94, 14, 3, 3, 98, 101 | decmac 11118 |
. . . . . 6
 ;     ;  |
103 | 78 | mulid1i 9670 |
. . . . . . . 8
   |
104 | 103 | oveq1i 6324 |
. . . . . . 7
       |
105 | | 3p1e4 10763 |
. . . . . . 7
   |
106 | 2 | dec0h 11095 |
. . . . . . 7
;  |
107 | 104, 105,
106 | 3eqtri 2487 |
. . . . . 6
    ;  |
108 | 23, 19, 3, 14, 60, 63, 14, 2, 3, 102, 107 | decmac 11118 |
. . . . 5
 ;;    ;;   |
109 | 5, 14, 16, 14, 1, 47, 25, 2, 23, 93, 108 | decma2c 11119 |
. . . 4
 ;;   ;;;    ;;;;;      |
110 | | eqid 2461 |
. . . . 5
;;  ;;   |
111 | | 8nn0 10920 |
. . . . . . 7
 |
112 | 14, 111 | deccl 11093 |
. . . . . 6
;  |
113 | 112, 3 | deccl 11093 |
. . . . 5
;;   |
114 | | eqid 2461 |
. . . . . 6
; ;  |
115 | | eqid 2461 |
. . . . . 6
;;  ;;   |
116 | 112 | nn0cni 10909 |
. . . . . . . 8
;  |
117 | 116 | addid1i 9845 |
. . . . . . 7
;  ;  |
118 | | 1p2e3 10762 |
. . . . . . . . 9
   |
119 | 19 | dec0h 11095 |
. . . . . . . . 9
;  |
120 | 118, 119 | eqtri 2483 |
. . . . . . . 8
  ;  |
121 | | 9t9e81 11181 |
. . . . . . . . . 10
  ;  |
122 | 121 | oveq1i 6324 |
. . . . . . . . 9
    ;   |
123 | 111, 14 | deccl 11093 |
. . . . . . . . . . 11
;  |
124 | 123 | nn0cni 10909 |
. . . . . . . . . 10
;  |
125 | 124 | addid1i 9845 |
. . . . . . . . 9
;  ;  |
126 | 122, 125 | eqtri 2483 |
. . . . . . . 8
    ;  |
127 | | 9cn 10724 |
. . . . . . . . . . 11
 |
128 | 127 | mul02i 9847 |
. . . . . . . . . 10
   |
129 | 128 | oveq1i 6324 |
. . . . . . . . 9
       |
130 | 78 | addid2i 9846 |
. . . . . . . . 9
   |
131 | 129, 130 | eqtri 2483 |
. . . . . . . 8
     |
132 | 10, 3, 3, 19, 114, 120, 10, 126, 131 | decma 11117 |
. . . . . . 7
 ;     ;;   |
133 | | 9t2e18 11174 |
. . . . . . . . 9
  ;  |
134 | 127, 37, 133 | mulcomli 9675 |
. . . . . . . 8
  ;  |
135 | | 1p1e2 10750 |
. . . . . . . 8
   |
136 | | 8p8e16 11140 |
. . . . . . . 8
  ;  |
137 | 14, 111, 111, 134, 135, 48, 136 | decaddci 11124 |
. . . . . . 7
    ;  |
138 | 27, 18, 14, 111, 110, 117, 10, 48, 18, 132, 137 | decmac 11118 |
. . . . . 6
 ;;   ;   ;;;    |
139 | 28 | nn0cni 10909 |
. . . . . . . . 9
;;   |
140 | 139 | mul01i 9848 |
. . . . . . . 8
;;    |
141 | 140 | oveq1i 6324 |
. . . . . . 7
 ;;       |
142 | 141, 55, 39 | 3eqtri 2487 |
. . . . . 6
 ;;    ;  |
143 | 10, 3, 112, 3, 114, 115, 28, 3, 3, 138, 142 | decma2c 11119 |
. . . . 5
 ;;  ;  ;;   ;;;;     |
144 | 133 | oveq1i 6324 |
. . . . . . . . . 10
    ;   |
145 | 144, 117 | eqtri 2483 |
. . . . . . . . 9
    ;  |
146 | 37 | mul02i 9847 |
. . . . . . . . . 10
   |
147 | 146, 39 | eqtri 2483 |
. . . . . . . . 9
  ;  |
148 | 18, 10, 3, 114, 3, 3, 145, 147 | decmul1c 11126 |
. . . . . . . 8
;  ;;   |
149 | 148 | oveq1i 6324 |
. . . . . . 7
 ;   ;;    |
150 | 113 | nn0cni 10909 |
. . . . . . . 8
;;   |
151 | 150 | addid1i 9845 |
. . . . . . 7
;;   ;;   |
152 | 149, 151 | eqtri 2483 |
. . . . . 6
 ;   ;;   |
153 | 32, 106 | eqtri 2483 |
. . . . . 6
  ;  |
154 | 18, 27, 18, 110, 2, 3, 152, 153 | decmul1c 11126 |
. . . . 5
;;   ;;;    |
155 | 28, 27, 18, 110, 2, 113, 143, 154 | decmul2c 11127 |
. . . 4
;;  ;;   ;;;;;      |
156 | 109, 155 | eqtr4i 2486 |
. . 3
 ;;   ;;;    ;;  ;;    |
157 | 8, 9, 24, 26, 28, 17, 29, 46, 156 | mod2xi 15089 |
. 2
   ;;    ;;;     |
158 | 68 | oveq1i 6324 |
. . . . . . 7
       |
159 | 158, 71 | eqtri 2483 |
. . . . . 6
     |
160 | 18, 2, 3, 57, 3, 3,
159, 40 | decmul2c 11127 |
. . . . 5
 ;  ;  |
161 | 160 | oveq1i 6324 |
. . . 4
  ;   ;   |
162 | 111, 3 | deccl 11093 |
. . . . . 6
;  |
163 | 162 | nn0cni 10909 |
. . . . 5
;  |
164 | 163 | addid1i 9845 |
. . . 4
;  ;  |
165 | 161, 164 | eqtri 2483 |
. . 3
  ;   ;  |
166 | 18, 4, 3, 50, 3, 3,
165, 40 | decmul2c 11127 |
. 2
 ;;   ;;   |
167 | | eqid 2461 |
. . . 4
;;;   ;;;    |
168 | 18, 111 | deccl 11093 |
. . . . 5
;  |
169 | | eqid 2461 |
. . . . . 6
;;  ;;   |
170 | | eqid 2461 |
. . . . . 6
; ;  |
171 | | 7nn0 10919 |
. . . . . . 7
 |
172 | | 7p1e8 10767 |
. . . . . . 7
   |
173 | | eqid 2461 |
. . . . . . . 8
; ;  |
174 | | 4p3e7 10773 |
. . . . . . . . 9
   |
175 | 34, 78, 174 | addcomli 9850 |
. . . . . . . 8
   |
176 | 18, 19, 2, 173, 175 | decaddi 11123 |
. . . . . . 7
;  ;  |
177 | 18, 171, 172, 176 | decsuc 11102 |
. . . . . 6
 ;   ;  |
178 | | 9p1e10 10769 |
. . . . . . 7
   |
179 | 127, 61, 178 | addcomli 9850 |
. . . . . 6
   |
180 | 20, 14, 2, 10, 169, 170, 177, 179 | decaddc2 11122 |
. . . . 5
;;  ;  ;;   |
181 | 168 | nn0cni 10909 |
. . . . . . 7
;  |
182 | 181 | addid1i 9845 |
. . . . . 6
;  ;  |
183 | | eqid 2461 |
. . . . . . 7
;;  ;;   |
184 | 18 | dec0h 11095 |
. . . . . . . 8
;  |
185 | 97, 184 | eqtri 2483 |
. . . . . . 7
  ;  |
186 | 130 | oveq2i 6325 |
. . . . . . . . 9
           |
187 | | 4t4e16 11152 |
. . . . . . . . . 10
  ;  |
188 | | 6p3e9 10780 |
. . . . . . . . . 10
   |
189 | 14, 48, 19, 187, 188 | decaddi 11123 |
. . . . . . . . 9
    ;  |
190 | 186, 189 | eqtri 2483 |
. . . . . . . 8
      ;  |
191 | | 9t4e36 11176 |
. . . . . . . . . 10
  ;  |
192 | 191 | oveq1i 6324 |
. . . . . . . . 9
    ;   |
193 | 19, 48 | deccl 11093 |
. . . . . . . . . . 11
;  |
194 | 193 | nn0cni 10909 |
. . . . . . . . . 10
;  |
195 | 194 | addid1i 9845 |
. . . . . . . . 9
;  ;  |
196 | 192, 195 | eqtri 2483 |
. . . . . . . 8
    ;  |
197 | 2, 10, 3, 3, 170, 94, 2, 48, 19, 190, 196 | decmac 11118 |
. . . . . . 7
 ;     ;;   |
198 | 73 | oveq1i 6324 |
. . . . . . . 8
       |
199 | 37 | addid2i 9846 |
. . . . . . . 8
   |
200 | 198, 199,
184 | 3eqtri 2487 |
. . . . . . 7
    ;  |
201 | 11, 3, 3, 18, 183, 185, 2, 18, 3, 197, 200 | decmac 11118 |
. . . . . 6
 ;;      ;;;    |
202 | 12 | nn0cni 10909 |
. . . . . . . . 9
;;   |
203 | 202 | mul01i 9848 |
. . . . . . . 8
;;    |
204 | 203 | oveq1i 6324 |
. . . . . . 7
 ;;       |
205 | 70 | addid2i 9846 |
. . . . . . 7
   |
206 | 111 | dec0h 11095 |
. . . . . . 7
;  |
207 | 204, 205,
206 | 3eqtri 2487 |
. . . . . 6
 ;;    ;  |
208 | 2, 3, 18, 111, 57, 182, 12, 111, 3, 201, 207 | decma2c 11119 |
. . . . 5
 ;;  ;  ;   ;;;;     |
209 | 203 | oveq1i 6324 |
. . . . . 6
 ;;       |
210 | 209, 55, 39 | 3eqtri 2487 |
. . . . 5
 ;;    ;  |
211 | 4, 3, 168, 3, 50, 180, 12, 3, 3, 208, 210 | decma2c 11119 |
. . . 4
 ;;  ;;   ;;  ;   ;;;;;      |
212 | 34 | mulid1i 9670 |
. . . . . . . 8
   |
213 | 212, 55 | oveq12i 6326 |
. . . . . . 7
         |
214 | 213, 35 | eqtri 2483 |
. . . . . 6
       |
215 | 127 | mulid1i 9670 |
. . . . . . . 8
   |
216 | 215 | oveq1i 6324 |
. . . . . . 7
       |
217 | 127 | addid1i 9845 |
. . . . . . 7
   |
218 | 10 | dec0h 11095 |
. . . . . . 7
;  |
219 | 216, 217,
218 | 3eqtri 2487 |
. . . . . 6
    ;  |
220 | 2, 10, 3, 3, 170, 94, 14, 10, 3, 214, 219 | decmac 11118 |
. . . . 5
 ;     ;  |
221 | 99 | oveq1i 6324 |
. . . . . 6
       |
222 | 221, 65, 63 | 3eqtri 2487 |
. . . . 5
    ;  |
223 | 11, 3, 3, 14, 183, 63, 14, 14, 3, 220, 222 | decmac 11118 |
. . . 4
 ;;    ;;   |
224 | 5, 14, 21, 14, 1, 167, 12, 14, 11, 211, 223 | decma2c 11119 |
. . 3
 ;;   ;;;    ;;;;;;       |
225 | 15 | nn0cni 10909 |
. . . . . . 7
;  |
226 | 225 | addid1i 9845 |
. . . . . 6
;  ;  |
227 | | 5nn0 10917 |
. . . . . . . 8
 |
228 | 227, 48 | deccl 11093 |
. . . . . . 7
;  |
229 | 228, 3 | deccl 11093 |
. . . . . 6
;;   |
230 | | eqid 2461 |
. . . . . . . 8
;;  ;;   |
231 | 228 | nn0cni 10909 |
. . . . . . . . 9
;  |
232 | 231 | addid2i 9846 |
. . . . . . . 8
 ;  ;  |
233 | 3, 14, 228, 3, 63, 230, 232, 62 | decadd 11120 |
. . . . . . 7
 ;;   ;;   |
234 | 231 | addid1i 9845 |
. . . . . . . 8
;  ;  |
235 | | 5cn 10716 |
. . . . . . . . . . 11
 |
236 | 235 | addid1i 9845 |
. . . . . . . . . 10
   |
237 | 227 | dec0h 11095 |
. . . . . . . . . 10
;  |
238 | 236, 237 | eqtri 2483 |
. . . . . . . . 9
  ;  |
239 | 61 | mulid1i 9670 |
. . . . . . . . . . 11
   |
240 | 239, 55 | oveq12i 6326 |
. . . . . . . . . 10
         |
241 | 240, 62 | eqtri 2483 |
. . . . . . . . 9
       |
242 | 212 | oveq1i 6324 |
. . . . . . . . . 10
       |
243 | | 5p4e9 10777 |
. . . . . . . . . . 11
   |
244 | 235, 34, 243 | addcomli 9850 |
. . . . . . . . . 10
   |
245 | 242, 244,
218 | 3eqtri 2487 |
. . . . . . . . 9
    ;  |
246 | 14, 2, 3, 227, 52, 238, 14, 10, 3, 241, 245 | decmac 11118 |
. . . . . . . 8
 ;     ;  |
247 | 99 | oveq1i 6324 |
. . . . . . . . 9
       |
248 | 247, 87, 88 | 3eqtri 2487 |
. . . . . . . 8
    ;  |
249 | 15, 3, 227, 48, 51, 234, 14, 48, 3, 246, 248 | decmac 11118 |
. . . . . . 7
 ;;   ;   ;;   |
250 | 239 | oveq1i 6324 |
. . . . . . . 8
       |
251 | 250, 135,
184 | 3eqtri 2487 |
. . . . . . 7
    ;  |
252 | 16, 14, 228, 14, 47, 233, 14, 18, 3, 249, 251 | decmac 11118 |
. . . . . 6
 ;;;     ;;    ;;;    |
253 | 34 | mulid2i 9671 |
. . . . . . . . . . 11
   |
254 | 253, 65 | oveq12i 6326 |
. . . . . . . . . 10
         |
255 | | 4p1e5 10764 |
. . . . . . . . . 10
   |
256 | 254, 255 | eqtri 2483 |
. . . . . . . . 9
       |
257 | 187 | oveq1i 6324 |
. . . . . . . . . 10
    ;   |
258 | 257, 59 | eqtri 2483 |
. . . . . . . . 9
    ;  |
259 | 14, 2, 3, 3, 52, 94, 2, 48, 14, 256, 258 | decmac 11118 |
. . . . . . . 8
 ;     ;  |
260 | 73 | oveq1i 6324 |
. . . . . . . . 9
       |
261 | 260, 55, 39 | 3eqtri 2487 |
. . . . . . . 8
    ;  |
262 | 15, 3, 3, 3, 51, 94, 2, 3, 3,
259, 261 | decmac 11118 |
. . . . . . 7
 ;;      ;;   |
263 | 253 | oveq1i 6324 |
. . . . . . . 8
       |
264 | | 4p4e8 10774 |
. . . . . . . 8
   |
265 | 263, 264,
206 | 3eqtri 2487 |
. . . . . . 7
    ;  |
266 | 16, 14, 3, 2, 47, 106, 2, 111, 3, 262, 265 | decmac 11118 |
. . . . . 6
 ;;;     ;;;    |
267 | 14, 2, 14, 2, 52, 226, 17, 111, 229, 252, 266 | decma2c 11119 |
. . . . 5
 ;;;   ;  ;   ;;;;     |
268 | 17 | nn0cni 10909 |
. . . . . . . 8
;;;    |
269 | 268 | mul01i 9848 |
. . . . . . 7
;;;     |
270 | 269 | oveq1i 6324 |
. . . . . 6
 ;;;        |
271 | 270, 55, 39 | 3eqtri 2487 |
. . . . 5
 ;;;     ;  |
272 | 15, 3, 15, 3, 51, 51, 17, 3, 3, 267, 271 | decma2c 11119 |
. . . 4
 ;;;   ;;   ;;   ;;;;;      |
273 | 268 | mulid1i 9670 |
. . . 4
;;;    ;;;    |
274 | 17, 16, 14, 47, 14, 16, 272, 273 | decmul2c 11127 |
. . 3
;;;   ;;;    ;;;;;;       |
275 | 224, 274 | eqtr4i 2486 |
. 2
 ;;   ;;;    ;;;   ;;;     |
276 | 8, 9, 5, 13, 17, 22, 157, 166, 275 | mod2xi 15089 |
1
   ;;    ;;;     |