Proof of Theorem 1259lem4
Step | Hyp | Ref
| Expression |
1 | | 2nn 10767 |
. 2
 |
2 | | 6nn0 10890 |
. . . 4
 |
3 | | 2nn0 10886 |
. . . 4
 |
4 | 2, 3 | deccl 11065 |
. . 3
;  |
5 | | 9nn0 10893 |
. . 3
 |
6 | 4, 5 | deccl 11065 |
. 2
;;   |
7 | | 0z 10948 |
. 2
 |
8 | | 1nn 10620 |
. 2
 |
9 | | 1nn0 10885 |
. 2
 |
10 | | 1259prm.1 |
. . . . . 6
;;;    |
11 | 9, 3 | deccl 11065 |
. . . . . . . 8
;  |
12 | | 5nn0 10889 |
. . . . . . . 8
 |
13 | 11, 12 | deccl 11065 |
. . . . . . 7
;;   |
14 | | 8nn0 10892 |
. . . . . . 7
 |
15 | | 8p1e9 10740 |
. . . . . . 7
   |
16 | | eqid 2451 |
. . . . . . 7
;;;   ;;;    |
17 | 13, 14, 15, 16 | decsuc 11074 |
. . . . . 6
;;;    ;;;    |
18 | 10, 17 | eqtr4i 2476 |
. . . . 5
;;;     |
19 | 18 | oveq1i 6300 |
. . . 4
   ;;;      |
20 | 13, 14 | deccl 11065 |
. . . . . 6
;;;    |
21 | 20 | nn0cni 10881 |
. . . . 5
;;;    |
22 | | ax-1cn 9597 |
. . . . 5
 |
23 | 21, 22 | pncan3oi 9891 |
. . . 4
 ;;;     ;;;    |
24 | 19, 23 | eqtri 2473 |
. . 3
  ;;;    |
25 | 24, 20 | eqeltri 2525 |
. 2
   |
26 | | 9nn 10774 |
. . . . 5
 |
27 | 13, 26 | decnncl 11064 |
. . . 4
;;;    |
28 | 10, 27 | eqeltri 2525 |
. . 3
 |
29 | 2, 9 | deccl 11065 |
. . . 4
;  |
30 | 29, 3 | deccl 11065 |
. . 3
;;   |
31 | | 3nn0 10887 |
. . . . 5
 |
32 | | 4nn0 10888 |
. . . . 5
 |
33 | 31, 32 | deccl 11065 |
. . . 4
;  |
34 | 33 | nn0zi 10962 |
. . 3
;  |
35 | 31, 3 | deccl 11065 |
. . . 4
;  |
36 | 35, 32 | deccl 11065 |
. . 3
;;   |
37 | | 7nn0 10891 |
. . . 4
 |
38 | 9, 37 | deccl 11065 |
. . 3
;  |
39 | 9, 31 | deccl 11065 |
. . . 4
;  |
40 | 39, 2 | deccl 11065 |
. . 3
;;   |
41 | | 0nn0 10884 |
. . . . . 6
 |
42 | 31, 41 | deccl 11065 |
. . . . 5
;  |
43 | 42, 2 | deccl 11065 |
. . . 4
;;   |
44 | | 8nn 10773 |
. . . . 5
 |
45 | 9, 44 | decnncl 11064 |
. . . 4
;  |
46 | 11, 32 | deccl 11065 |
. . . . 5
;;   |
47 | 46, 9 | deccl 11065 |
. . . 4
;;;    |
48 | 9, 12 | deccl 11065 |
. . . . . 6
;  |
49 | 48, 31 | deccl 11065 |
. . . . 5
;;   |
50 | | 1z 10967 |
. . . . 5
 |
51 | 12, 41 | deccl 11065 |
. . . . 5
;  |
52 | 48, 3 | deccl 11065 |
. . . . . 6
;;   |
53 | 3, 12 | deccl 11065 |
. . . . . 6
;  |
54 | 37, 2 | deccl 11065 |
. . . . . . 7
;  |
55 | 10 | 1259lem3 15104 |
. . . . . . 7
   ;      |
56 | | eqid 2451 |
. . . . . . . 8
; ;  |
57 | | 4p1e5 10736 |
. . . . . . . . 9
   |
58 | | 7cn 10693 |
. . . . . . . . . 10
 |
59 | | 2cn 10680 |
. . . . . . . . . 10
 |
60 | | 7t2e14 11133 |
. . . . . . . . . 10
  ;  |
61 | 58, 59, 60 | mulcomli 9650 |
. . . . . . . . 9
  ;  |
62 | 9, 32, 57, 61 | decsuc 11074 |
. . . . . . . 8
    ;  |
63 | | 6cn 10691 |
. . . . . . . . 9
 |
64 | | 6t2e12 11128 |
. . . . . . . . 9
  ;  |
65 | 63, 59, 64 | mulcomli 9650 |
. . . . . . . 8
  ;  |
66 | 3, 37, 2, 56, 3, 9,
62, 65 | decmul2c 11099 |
. . . . . . 7
 ;  ;;   |
67 | 53 | nn0cni 10881 |
. . . . . . . . 9
;  |
68 | 67 | addid2i 9821 |
. . . . . . . 8
 ;  ;  |
69 | 28 | nncni 10619 |
. . . . . . . . . 10
 |
70 | 69 | mul02i 9822 |
. . . . . . . . 9
   |
71 | 70 | oveq1i 6300 |
. . . . . . . 8
   ;   ;   |
72 | | 5t5e25 11127 |
. . . . . . . 8
  ;  |
73 | 68, 71, 72 | 3eqtr4i 2483 |
. . . . . . 7
   ;     |
74 | 28, 1, 54, 7, 12, 53, 55, 66, 73 | mod2xi 15041 |
. . . . . 6
   ;;    ;
  |
75 | | 2p1e3 10733 |
. . . . . . 7
   |
76 | | eqid 2451 |
. . . . . . 7
;;  ;;   |
77 | 48, 3, 75, 76 | decsuc 11074 |
. . . . . 6
;;   ;;   |
78 | 51 | nn0cni 10881 |
. . . . . . . 8
;  |
79 | 78 | addid2i 9821 |
. . . . . . 7
 ;  ;  |
80 | 70 | oveq1i 6300 |
. . . . . . 7
   ;   ;   |
81 | | eqid 2451 |
. . . . . . . 8
; ;  |
82 | | 2t2e4 10759 |
. . . . . . . . . 10
   |
83 | 82 | oveq1i 6300 |
. . . . . . . . 9
       |
84 | 83, 57 | eqtri 2473 |
. . . . . . . 8
     |
85 | | 5t2e10 10764 |
. . . . . . . . 9
   |
86 | | dec10 11081 |
. . . . . . . . 9
;  |
87 | 85, 86 | eqtri 2473 |
. . . . . . . 8
  ;  |
88 | 3, 3, 12, 81, 41, 9, 84, 87 | decmul1c 11098 |
. . . . . . 7
;  ;  |
89 | 79, 80, 88 | 3eqtr4i 2483 |
. . . . . 6
   ;  ;   |
90 | 28, 1, 52, 7, 53, 51, 74, 77, 89 | modxp1i 15042 |
. . . . 5
   ;;    ;
  |
91 | | eqid 2451 |
. . . . . 6
;;  ;;   |
92 | | eqid 2451 |
. . . . . . . . 9
; ;  |
93 | 59 | mulid1i 9645 |
. . . . . . . . . . 11
   |
94 | 93 | oveq1i 6300 |
. . . . . . . . . 10
       |
95 | 94, 75 | eqtri 2473 |
. . . . . . . . 9
     |
96 | | 5cn 10689 |
. . . . . . . . . . 11
 |
97 | 96, 59, 85 | mulcomli 9650 |
. . . . . . . . . 10
   |
98 | 97, 86 | eqtri 2473 |
. . . . . . . . 9
  ;  |
99 | 3, 9, 12, 92, 41, 9, 95, 98 | decmul2c 11099 |
. . . . . . . 8
 ;  ;  |
100 | 99 | oveq1i 6300 |
. . . . . . 7
  ;   ;   |
101 | 42 | nn0cni 10881 |
. . . . . . . 8
;  |
102 | 101 | addid1i 9820 |
. . . . . . 7
;  ;  |
103 | 100, 102 | eqtri 2473 |
. . . . . 6
  ;   ;  |
104 | | 3cn 10684 |
. . . . . . . 8
 |
105 | | 3t2e6 10761 |
. . . . . . . 8
   |
106 | 104, 59, 105 | mulcomli 9650 |
. . . . . . 7
   |
107 | 2 | dec0h 11067 |
. . . . . . 7
;  |
108 | 106, 107 | eqtri 2473 |
. . . . . 6
  ;  |
109 | 3, 48, 31, 91, 2, 41, 103, 108 | decmul2c 11099 |
. . . . 5
 ;;   ;;   |
110 | 69 | mulid2i 9646 |
. . . . . . . 8
   |
111 | 110, 10 | eqtri 2473 |
. . . . . . 7
  ;;;    |
112 | | eqid 2451 |
. . . . . . 7
;;;   ;;;    |
113 | 3, 32 | deccl 11065 |
. . . . . . . 8
;  |
114 | | eqid 2451 |
. . . . . . . . 9
; ;  |
115 | 3, 32, 57, 114 | decsuc 11074 |
. . . . . . . 8
;  ;  |
116 | | eqid 2451 |
. . . . . . . . 9
;;  ;;   |
117 | | eqid 2451 |
. . . . . . . . 9
;;  ;;   |
118 | | eqid 2451 |
. . . . . . . . . 10
; ;  |
119 | | 1p1e2 10723 |
. . . . . . . . . 10
   |
120 | | 2p2e4 10727 |
. . . . . . . . . 10
   |
121 | 9, 3, 9, 3, 118, 118, 119, 120 | decadd 11092 |
. . . . . . . . 9
; ;  ;  |
122 | | 5p4e9 10749 |
. . . . . . . . 9
   |
123 | 11, 12, 11, 32, 116, 117, 121, 122 | decadd 11092 |
. . . . . . . 8
;;  ;;   ;;   |
124 | 113, 115,
123 | decsucc 11078 |
. . . . . . 7
 ;;  ;;    ;;   |
125 | | 9p1e10 10741 |
. . . . . . 7
   |
126 | 13, 5, 46, 9, 111, 112, 124, 125 | decaddc2 11094 |
. . . . . 6
   ;;;    ;;;    |
127 | | eqid 2451 |
. . . . . . 7
; ;  |
128 | 72 | oveq1i 6300 |
. . . . . . . . . . 11
    ;   |
129 | 67 | addid1i 9820 |
. . . . . . . . . . 11
;  ;  |
130 | 128, 129 | eqtri 2473 |
. . . . . . . . . 10
    ;  |
131 | 96 | mul02i 9822 |
. . . . . . . . . . 11
   |
132 | 41 | dec0h 11067 |
. . . . . . . . . . 11
;  |
133 | 131, 132 | eqtri 2473 |
. . . . . . . . . 10
  ;  |
134 | 12, 12, 41, 127, 41, 41, 130, 133 | decmul1c 11098 |
. . . . . . . . 9
;  ;;   |
135 | 134 | oveq1i 6300 |
. . . . . . . 8
 ;   ;;    |
136 | 53, 41 | deccl 11065 |
. . . . . . . . . 10
;;   |
137 | 136 | nn0cni 10881 |
. . . . . . . . 9
;;   |
138 | 137 | addid1i 9820 |
. . . . . . . 8
;;   ;;   |
139 | 135, 138 | eqtri 2473 |
. . . . . . 7
 ;   ;;   |
140 | 78 | mul01i 9823 |
. . . . . . . 8
;   |
141 | 140, 132 | eqtri 2473 |
. . . . . . 7
;  ;  |
142 | 51, 12, 41, 127, 41, 41, 139, 141 | decmul2c 11099 |
. . . . . 6
; ;  ;;;    |
143 | 126, 142 | eqtr4i 2476 |
. . . . 5
   ;;;    ; ;   |
144 | 28, 1, 49, 50, 51, 47, 90, 109, 143 | mod2xi 15041 |
. . . 4
   ;;    ;;;     |
145 | | eqid 2451 |
. . . . 5
;;  ;;   |
146 | | eqid 2451 |
. . . . . 6
; ;  |
147 | 9 | dec0h 11067 |
. . . . . 6
;  |
148 | | 00id 9808 |
. . . . . . . 8
   |
149 | 106, 148 | oveq12i 6302 |
. . . . . . 7
         |
150 | 63 | addid1i 9820 |
. . . . . . 7
   |
151 | 149, 150 | eqtri 2473 |
. . . . . 6
       |
152 | 59 | mul01i 9823 |
. . . . . . . 8
   |
153 | 152 | oveq1i 6300 |
. . . . . . 7
       |
154 | | 0p1e1 10721 |
. . . . . . 7
   |
155 | 153, 154,
147 | 3eqtri 2477 |
. . . . . 6
    ;  |
156 | 31, 41, 41, 9, 146, 147, 3, 9, 41, 151, 155 | decma2c 11091 |
. . . . 5
  ;   ;  |
157 | 3, 42, 2, 145, 3, 9, 156, 65 | decmul2c 11099 |
. . . 4
 ;;   ;;   |
158 | | eqid 2451 |
. . . . . 6
; ;  |
159 | 11, 32, 57, 117 | decsuc 11074 |
. . . . . 6
;;   ;;   |
160 | | 8cn 10695 |
. . . . . . 7
 |
161 | 160, 22, 15 | addcomli 9825 |
. . . . . 6
   |
162 | 46, 9, 9, 14, 112, 158, 159, 161 | decadd 11092 |
. . . . 5
;;;   ;  ;;;    |
163 | 162, 10 | eqtr4i 2476 |
. . . 4
;;;   ;   |
164 | 36 | nn0cni 10881 |
. . . . . 6
;;   |
165 | 164 | addid2i 9821 |
. . . . 5
 ;;   ;;   |
166 | 70 | oveq1i 6300 |
. . . . 5
   ;;    ;;    |
167 | 9, 14 | deccl 11065 |
. . . . . 6
;  |
168 | 9, 32 | deccl 11065 |
. . . . . 6
;  |
169 | | eqid 2451 |
. . . . . . 7
; ;  |
170 | 22 | mulid1i 9645 |
. . . . . . . . 9
   |
171 | 170, 119 | oveq12i 6302 |
. . . . . . . 8
         |
172 | | 1p2e3 10734 |
. . . . . . . 8
   |
173 | 171, 172 | eqtri 2473 |
. . . . . . 7
       |
174 | 160 | mulid1i 9645 |
. . . . . . . . 9
   |
175 | 174 | oveq1i 6300 |
. . . . . . . 8
       |
176 | | 8p4e12 11108 |
. . . . . . . 8
  ;  |
177 | 175, 176 | eqtri 2473 |
. . . . . . 7
    ;  |
178 | 9, 14, 9, 32, 158, 169, 9, 3, 9, 173, 177 | decmac 11090 |
. . . . . 6
 ;  ;  ;  |
179 | 160 | mulid2i 9646 |
. . . . . . . . 9
   |
180 | 179 | oveq1i 6300 |
. . . . . . . 8
       |
181 | | 8p6e14 11110 |
. . . . . . . 8
  ;  |
182 | 180, 181 | eqtri 2473 |
. . . . . . 7
    ;  |
183 | | 8t8e64 11145 |
. . . . . . 7
  ;  |
184 | 14, 9, 14, 158, 32, 2, 182, 183 | decmul1c 11098 |
. . . . . 6
;  ;;   |
185 | 167, 9, 14, 158, 32, 168, 178, 184 | decmul2c 11099 |
. . . . 5
; ;  ;;   |
186 | 165, 166,
185 | 3eqtr4i 2483 |
. . . 4
   ;;   ; ;   |
187 | 1, 43, 7, 45, 36, 47, 144, 157, 163, 186 | mod2xnegi 15043 |
. . 3
   ;;    ;;    |
188 | 10 | 1259lem1 15102 |
. . 3
   ;   ;;    |
189 | | eqid 2451 |
. . . 4
;;  ;;   |
190 | | eqid 2451 |
. . . 4
; ;  |
191 | | eqid 2451 |
. . . . 5
; ;  |
192 | 2, 9, 119, 191 | decsuc 11074 |
. . . 4
;  ;  |
193 | | 7p2e9 10754 |
. . . . 5
   |
194 | 58, 59, 193 | addcomli 9825 |
. . . 4
   |
195 | 29, 3, 9, 37, 189, 190, 192, 194 | decadd 11092 |
. . 3
;;  ;  ;;   |
196 | 31, 9 | deccl 11065 |
. . . . 5
;  |
197 | | eqid 2451 |
. . . . . . 7
; ;  |
198 | | 3p2e5 10742 |
. . . . . . . . 9
   |
199 | 104, 59, 198 | addcomli 9825 |
. . . . . . . 8
   |
200 | 9, 3, 31, 118, 199 | decaddi 11095 |
. . . . . . 7
;  ;  |
201 | | 5p1e6 10737 |
. . . . . . 7
   |
202 | 11, 12, 31, 9, 116, 197, 200, 201 | decadd 11092 |
. . . . . 6
;;  ;  ;;   |
203 | 119 | oveq1i 6300 |
. . . . . . . . 9
       |
204 | 203, 75 | eqtri 2473 |
. . . . . . . 8
     |
205 | | 7p5e12 11104 |
. . . . . . . . 9
  ;  |
206 | 58, 96, 205 | addcomli 9825 |
. . . . . . . 8
  ;  |
207 | 9, 12, 9, 37, 92, 190, 204, 3, 206 | decaddc 11093 |
. . . . . . 7
; ;  ;  |
208 | | eqid 2451 |
. . . . . . . 8
; ;  |
209 | | 7p3e10 10755 |
. . . . . . . . . 10
   |
210 | 58, 104, 209 | addcomli 9825 |
. . . . . . . . 9
   |
211 | 210, 86 | eqtri 2473 |
. . . . . . . 8
  ;  |
212 | 104 | mulid1i 9645 |
. . . . . . . . . 10
   |
213 | 22 | addid1i 9820 |
. . . . . . . . . 10
   |
214 | 212, 213 | oveq12i 6302 |
. . . . . . . . 9
         |
215 | | 3p1e4 10735 |
. . . . . . . . 9
   |
216 | 214, 215 | eqtri 2473 |
. . . . . . . 8
       |
217 | | 4cn 10687 |
. . . . . . . . . . 11
 |
218 | 217 | mulid1i 9645 |
. . . . . . . . . 10
   |
219 | 218 | oveq1i 6300 |
. . . . . . . . 9
       |
220 | 217 | addid1i 9820 |
. . . . . . . . 9
   |
221 | 32 | dec0h 11067 |
. . . . . . . . 9
;  |
222 | 219, 220,
221 | 3eqtri 2477 |
. . . . . . . 8
    ;  |
223 | 31, 32, 9, 41, 208, 211, 9, 32, 41, 216, 222 | decmac 11090 |
. . . . . . 7
 ;     ;  |
224 | 3 | dec0h 11067 |
. . . . . . . 8
;  |
225 | 105, 154 | oveq12i 6302 |
. . . . . . . . 9
         |
226 | | 6p1e7 10738 |
. . . . . . . . 9
   |
227 | 225, 226 | eqtri 2473 |
. . . . . . . 8
       |
228 | | 4t2e8 10763 |
. . . . . . . . . 10
   |
229 | 228 | oveq1i 6300 |
. . . . . . . . 9
       |
230 | | 8p2e10 10756 |
. . . . . . . . 9
   |
231 | 229, 230,
86 | 3eqtri 2477 |
. . . . . . . 8
    ;  |
232 | 31, 32, 41, 3, 208, 224, 3, 41, 9, 227, 231 | decmac 11090 |
. . . . . . 7
 ;   ;  |
233 | 9, 3, 31, 3, 118, 207, 33, 41, 37, 223, 232 | decma2c 11091 |
. . . . . 6
 ; ;  ; ;   ;;   |
234 | 59 | addid2i 9821 |
. . . . . . . . 9
   |
235 | 234 | oveq2i 6301 |
. . . . . . . 8
           |
236 | | 5t3e15 11125 |
. . . . . . . . . 10
  ;  |
237 | 96, 104, 236 | mulcomli 9650 |
. . . . . . . . 9
  ;  |
238 | | 5p2e7 10747 |
. . . . . . . . 9
   |
239 | 9, 12, 3, 237, 238 | decaddi 11095 |
. . . . . . . 8
    ;  |
240 | 235, 239 | eqtri 2473 |
. . . . . . 7
      ;  |
241 | | 5t4e20 11126 |
. . . . . . . . 9
  ;  |
242 | 96, 217, 241 | mulcomli 9650 |
. . . . . . . 8
  ;  |
243 | 63 | addid2i 9821 |
. . . . . . . 8
   |
244 | 3, 41, 2, 242, 243 | decaddi 11095 |
. . . . . . 7
    ;  |
245 | 31, 32, 41, 2, 208, 107, 12, 2, 3, 240, 244 | decmac 11090 |
. . . . . 6
 ;   ;;   |
246 | 11, 12, 48, 2, 116, 202, 33, 2, 38, 233, 245 | decma2c 11091 |
. . . . 5
 ; ;;   ;;  ;   ;;;    |
247 | 14 | dec0h 11067 |
. . . . . 6
;  |
248 | 217 | addid2i 9821 |
. . . . . . . 8
   |
249 | 248 | oveq2i 6301 |
. . . . . . 7
           |
250 | | 9cn 10697 |
. . . . . . . . 9
 |
251 | | 9t3e27 11147 |
. . . . . . . . 9
  ;  |
252 | 250, 104,
251 | mulcomli 9650 |
. . . . . . . 8
  ;  |
253 | | 7p4e11 11103 |
. . . . . . . 8
  ;  |
254 | 3, 37, 32, 252, 75, 9, 253 | decaddci 11096 |
. . . . . . 7
    ;  |
255 | 249, 254 | eqtri 2473 |
. . . . . 6
      ;  |
256 | | 9t4e36 11148 |
. . . . . . . 8
  ;  |
257 | 250, 217,
256 | mulcomli 9650 |
. . . . . . 7
  ;  |
258 | 160, 63, 181 | addcomli 9825 |
. . . . . . 7
  ;  |
259 | 31, 2, 14, 257, 215, 32, 258 | decaddci 11096 |
. . . . . 6
    ;  |
260 | 31, 32, 41, 14, 208, 247, 5, 32, 32, 255, 259 | decmac 11090 |
. . . . 5
 ;   ;;   |
261 | 13, 5, 13, 14, 10, 24, 33, 32, 196, 246, 260 | decma2c 11091 |
. . . 4
 ;     ;;;;     |
262 | | eqid 2451 |
. . . . 5
;;  ;;   |
263 | 9, 5 | deccl 11065 |
. . . . . 6
;  |
264 | 263, 32 | deccl 11065 |
. . . . 5
;;   |
265 | | eqid 2451 |
. . . . . 6
; ;  |
266 | | eqid 2451 |
. . . . . 6
;;  ;;   |
267 | 5, 37 | deccl 11065 |
. . . . . 6
;  |
268 | 9, 9 | deccl 11065 |
. . . . . . 7
;  |
269 | | eqid 2451 |
. . . . . . 7
;;  ;;   |
270 | | eqid 2451 |
. . . . . . . 8
; ;  |
271 | | eqid 2451 |
. . . . . . . 8
; ;  |
272 | 250, 22, 125 | addcomli 9825 |
. . . . . . . . . 10
   |
273 | 272, 86 | eqtri 2473 |
. . . . . . . . 9
  ;  |
274 | 9, 41, 154, 273 | decsuc 11074 |
. . . . . . . 8
    ;  |
275 | | 9p7e16 11118 |
. . . . . . . 8
  ;  |
276 | 9, 5, 5, 37, 270, 271, 274, 2, 275 | decaddc 11093 |
. . . . . . 7
; ;  ;;   |
277 | | eqid 2451 |
. . . . . . . 8
; ;  |
278 | | eqid 2451 |
. . . . . . . . 9
; ;  |
279 | 9, 9, 119, 278 | decsuc 11074 |
. . . . . . . 8
;  ;  |
280 | 93 | oveq1i 6300 |
. . . . . . . . 9
       |
281 | 280, 120,
221 | 3eqtri 2477 |
. . . . . . . 8
    ;  |
282 | 31, 3, 9, 3, 277, 279, 9, 32, 41, 216, 281 | decmac 11090 |
. . . . . . 7
 ;  ;   ;  |
283 | 218 | oveq1i 6300 |
. . . . . . . 8
       |
284 | | 6p4e10 10753 |
. . . . . . . . 9
   |
285 | 63, 217, 284 | addcomli 9825 |
. . . . . . . 8
   |
286 | 283, 285,
86 | 3eqtri 2477 |
. . . . . . 7
    ;  |
287 | 35, 32, 268, 2, 269, 276, 9, 41, 9, 282, 286 | decmac 11090 |
. . . . . 6
 ;;   ; ;   ;;   |
288 | 154, 147 | eqtri 2473 |
. . . . . . . 8
  ;  |
289 | | 3t3e9 10762 |
. . . . . . . . . 10
   |
290 | 289, 148 | oveq12i 6302 |
. . . . . . . . 9
         |
291 | 250 | addid1i 9820 |
. . . . . . . . 9
   |
292 | 290, 291 | eqtri 2473 |
. . . . . . . 8
       |
293 | 106 | oveq1i 6300 |
. . . . . . . . 9
       |
294 | 37 | dec0h 11067 |
. . . . . . . . 9
;  |
295 | 293, 226,
294 | 3eqtri 2477 |
. . . . . . . 8
    ;  |
296 | 31, 3, 41, 9, 277, 288, 31, 37, 41, 292, 295 | decmac 11090 |
. . . . . . 7
 ;     ;  |
297 | | 4t3e12 11123 |
. . . . . . . 8
  ;  |
298 | | 4p2e6 10744 |
. . . . . . . . 9
   |
299 | 217, 59, 298 | addcomli 9825 |
. . . . . . . 8
   |
300 | 9, 3, 32, 297, 299 | decaddi 11095 |
. . . . . . 7
    ;  |
301 | 35, 32, 41, 32, 269, 221, 31, 2, 9, 296, 300 | decmac 11090 |
. . . . . 6
 ;;    ;;   |
302 | 9, 31, 263, 32, 265, 266, 36, 2, 267, 287, 301 | decma2c 11091 |
. . . . 5
 ;;  ;  ;;   ;;;    |
303 | 154 | oveq2i 6301 |
. . . . . . . 8
           |
304 | | 6t3e18 11129 |
. . . . . . . . . 10
  ;  |
305 | 63, 104, 304 | mulcomli 9650 |
. . . . . . . . 9
  ;  |
306 | 9, 14, 15, 305 | decsuc 11074 |
. . . . . . . 8
    ;  |
307 | 303, 306 | eqtri 2473 |
. . . . . . 7
      ;  |
308 | 9, 3, 3, 65, 120 | decaddi 11095 |
. . . . . . 7
    ;  |
309 | 31, 3, 41, 3, 277, 224, 2, 32, 9, 307, 308 | decmac 11090 |
. . . . . 6
 ;   ;;   |
310 | | 6t4e24 11130 |
. . . . . . 7
  ;  |
311 | 63, 217, 310 | mulcomli 9650 |
. . . . . 6
  ;  |
312 | 2, 35, 32, 269, 32, 3, 309, 311 | decmul1c 11098 |
. . . . 5
;;   ;;;    |
313 | 36, 39, 2, 262, 32, 264, 302, 312 | decmul2c 11099 |
. . . 4
;;  ;;   ;;;;     |
314 | 261, 313 | eqtr4i 2476 |
. . 3
 ;     ;;  ;;    |
315 | 28, 1, 30, 34, 36, 25, 38, 40, 187, 188, 195, 314 | modxai 15040 |
. 2
   ;;         |
316 | | eqid 2451 |
. . . 4
;;  ;;   |
317 | | eqid 2451 |
. . . . 5
; ;  |
318 | 148 | oveq2i 6301 |
. . . . . 6
           |
319 | 65 | oveq1i 6300 |
. . . . . 6
    ;   |
320 | 11 | nn0cni 10881 |
. . . . . . 7
;  |
321 | 320 | addid1i 9820 |
. . . . . 6
;  ;  |
322 | 318, 319,
321 | 3eqtri 2477 |
. . . . 5
      ;  |
323 | 12 | dec0h 11067 |
. . . . . 6
;  |
324 | 83, 57, 323 | 3eqtri 2477 |
. . . . 5
    ;  |
325 | 2, 3, 41, 9, 317, 147, 3, 12, 41, 322, 324 | decma2c 11091 |
. . . 4
  ;   ;;   |
326 | | 9t2e18 11146 |
. . . . 5
  ;  |
327 | 250, 59, 326 | mulcomli 9650 |
. . . 4
  ;  |
328 | 3, 4, 5, 316, 14, 9, 325, 327 | decmul2c 11099 |
. . 3
 ;;   ;;;    |
329 | 328, 24 | eqtr4i 2476 |
. 2
 ;;      |
330 | | npcan 9884 |
. . 3
 
       |
331 | 69, 22, 330 | mp2an 678 |
. 2
     |
332 | 70 | oveq1i 6300 |
. . 3
       |
333 | 154, 332,
170 | 3eqtr4i 2483 |
. 2
       |
334 | 1, 6, 7, 8, 9, 25,
315, 329, 331, 333 | mod2xnegi 15043 |
1
           |