Proof of Theorem 4001lem1
Step | Hyp | Ref
| Expression |
1 | | 4001prm.1 |
. . 3
;;;    |
2 | | 4nn0 10888 |
. . . . . 6
 |
3 | | 0nn0 10884 |
. . . . . 6
 |
4 | 2, 3 | deccl 11065 |
. . . . 5
;  |
5 | 4, 3 | deccl 11065 |
. . . 4
;;   |
6 | | 1nn 10620 |
. . . 4
 |
7 | 5, 6 | decnncl 11064 |
. . 3
;;;    |
8 | 1, 7 | eqeltri 2525 |
. 2
 |
9 | | 2nn 10767 |
. 2
 |
10 | | 10nn0 10894 |
. . 3
 |
11 | 10, 3 | deccl 11065 |
. 2
;  |
12 | | 9nn0 10893 |
. . . 4
 |
13 | 12, 2 | deccl 11065 |
. . 3
;  |
14 | 13 | nn0zi 10962 |
. 2
;  |
15 | | 6nn0 10890 |
. . . 4
 |
16 | | 1nn0 10885 |
. . . 4
 |
17 | 15, 16 | deccl 11065 |
. . 3
;  |
18 | 17, 2 | deccl 11065 |
. 2
;;   |
19 | 12, 3 | deccl 11065 |
. . 3
;  |
20 | | 2nn0 10886 |
. . 3
 |
21 | 19, 20 | deccl 11065 |
. 2
;;   |
22 | | 5nn0 10889 |
. . . 4
 |
23 | 22, 3 | deccl 11065 |
. . 3
;  |
24 | | 8nn0 10892 |
. . . . . 6
 |
25 | 20, 24 | deccl 11065 |
. . . . 5
;  |
26 | 25, 15 | deccl 11065 |
. . . 4
;;   |
27 | 26 | nn0zi 10962 |
. . 3
;;   |
28 | | 7nn0 10891 |
. . . . 5
 |
29 | 10, 28 | deccl 11065 |
. . . 4
;  |
30 | 29, 3 | deccl 11065 |
. . 3
;;   |
31 | 20, 22 | deccl 11065 |
. . . 4
;  |
32 | 10, 2 | deccl 11065 |
. . . . . 6
;  |
33 | 32, 15 | deccl 11065 |
. . . . 5
;;   |
34 | 33 | nn0zi 10962 |
. . . 4
;;   |
35 | 20, 3 | deccl 11065 |
. . . . . 6
;  |
36 | 35, 2 | deccl 11065 |
. . . . 5
;;   |
37 | 36, 15 | deccl 11065 |
. . . 4
;;;    |
38 | 20, 2 | deccl 11065 |
. . . . 5
;  |
39 | | 0z 10948 |
. . . . 5
 |
40 | 10, 20 | deccl 11065 |
. . . . . 6
;  |
41 | | 3nn0 10887 |
. . . . . 6
 |
42 | 40, 41 | deccl 11065 |
. . . . 5
;;   |
43 | 16, 20 | deccl 11065 |
. . . . . 6
;  |
44 | | 2z 10969 |
. . . . . 6
 |
45 | 12, 22 | deccl 11065 |
. . . . . 6
;  |
46 | | 1z 10967 |
. . . . . . 7
 |
47 | 15, 2 | deccl 11065 |
. . . . . . 7
;  |
48 | | 2exp6 15058 |
. . . . . . . 8
    ;  |
49 | 48 | oveq1i 6300 |
. . . . . . 7
      ;   |
50 | | 6cn 10691 |
. . . . . . . 8
 |
51 | | 2cn 10680 |
. . . . . . . 8
 |
52 | | 6t2e12 11128 |
. . . . . . . 8
  ;  |
53 | 50, 51, 52 | mulcomli 9650 |
. . . . . . 7
  ;  |
54 | | eqid 2451 |
. . . . . . . . 9
; ;  |
55 | | eqid 2451 |
. . . . . . . . . 10
;;  ;;   |
56 | | 9cn 10697 |
. . . . . . . . . . . 12
 |
57 | 56 | addid1i 9820 |
. . . . . . . . . . 11
   |
58 | 12 | dec0h 11067 |
. . . . . . . . . . 11
;  |
59 | 57, 58 | eqtri 2473 |
. . . . . . . . . 10
  ;  |
60 | | eqid 2451 |
. . . . . . . . . . 11
; ;  |
61 | | 00id 9808 |
. . . . . . . . . . . 12
   |
62 | 3 | dec0h 11067 |
. . . . . . . . . . . 12
;  |
63 | 61, 62 | eqtri 2473 |
. . . . . . . . . . 11
  ;  |
64 | | 4cn 10687 |
. . . . . . . . . . . . . 14
 |
65 | 64 | mulid2i 9646 |
. . . . . . . . . . . . 13
   |
66 | 65, 61 | oveq12i 6302 |
. . . . . . . . . . . 12
         |
67 | 64 | addid1i 9820 |
. . . . . . . . . . . 12
   |
68 | 66, 67 | eqtri 2473 |
. . . . . . . . . . 11
       |
69 | | ax-1cn 9597 |
. . . . . . . . . . . . . 14
 |
70 | 69 | mul01i 9823 |
. . . . . . . . . . . . 13
   |
71 | 70 | oveq1i 6300 |
. . . . . . . . . . . 12
       |
72 | 71, 63 | eqtri 2473 |
. . . . . . . . . . 11
    ;  |
73 | 2, 3, 3, 3, 60, 63, 16, 3, 3, 68, 72 | decma2c 11091 |
. . . . . . . . . 10
  ;     ;  |
74 | 70 | oveq1i 6300 |
. . . . . . . . . . 11
       |
75 | 56 | addid2i 9821 |
. . . . . . . . . . . 12
   |
76 | 75, 58 | eqtri 2473 |
. . . . . . . . . . 11
  ;  |
77 | 74, 76 | eqtri 2473 |
. . . . . . . . . 10
    ;  |
78 | 4, 3, 3, 12, 55, 59, 16, 12, 3, 73, 77 | decma2c 11091 |
. . . . . . . . 9
  ;;      ;;   |
79 | 69 | mulid1i 9645 |
. . . . . . . . . . 11
   |
80 | 79 | oveq1i 6300 |
. . . . . . . . . 10
       |
81 | | 5cn 10689 |
. . . . . . . . . . . 12
 |
82 | | 5p1e6 10737 |
. . . . . . . . . . . 12
   |
83 | 81, 69, 82 | addcomli 9825 |
. . . . . . . . . . 11
   |
84 | 15 | dec0h 11067 |
. . . . . . . . . . 11
;  |
85 | 83, 84 | eqtri 2473 |
. . . . . . . . . 10
  ;  |
86 | 80, 85 | eqtri 2473 |
. . . . . . . . 9
    ;  |
87 | 5, 16, 12, 22, 1, 54, 16, 15, 3, 78, 86 | decma2c 11091 |
. . . . . . . 8
   ;  ;;;    |
88 | | eqid 2451 |
. . . . . . . . 9
; ;  |
89 | | eqid 2451 |
. . . . . . . . . 10
; ;  |
90 | | 2p2e4 10727 |
. . . . . . . . . . . 12
   |
91 | 90 | oveq2i 6301 |
. . . . . . . . . . 11
           |
92 | | 6t6e36 11132 |
. . . . . . . . . . . 12
  ;  |
93 | | 3p1e4 10735 |
. . . . . . . . . . . 12
   |
94 | | 6p4e10 10753 |
. . . . . . . . . . . 12
   |
95 | 41, 15, 2, 92, 93, 94 | decaddci2 11097 |
. . . . . . . . . . 11
    ;  |
96 | 91, 95 | eqtri 2473 |
. . . . . . . . . 10
      ;  |
97 | | 6t4e24 11130 |
. . . . . . . . . . . 12
  ;  |
98 | 50, 64, 97 | mulcomli 9650 |
. . . . . . . . . . 11
  ;  |
99 | | 5p4e9 10749 |
. . . . . . . . . . . 12
   |
100 | 81, 64, 99 | addcomli 9825 |
. . . . . . . . . . 11
   |
101 | 20, 2, 22, 98, 100 | decaddi 11095 |
. . . . . . . . . 10
    ;  |
102 | 15, 2, 20, 22, 88, 89, 15, 12, 20, 96, 101 | decmac 11090 |
. . . . . . . . 9
 ;  ;  ;;   |
103 | | 4p1e5 10736 |
. . . . . . . . . . 11
   |
104 | 20, 2, 103, 97 | decsuc 11074 |
. . . . . . . . . 10
    ;  |
105 | | 4t4e16 11124 |
. . . . . . . . . 10
  ;  |
106 | 2, 15, 2, 88, 15, 16, 104, 105 | decmul1c 11098 |
. . . . . . . . 9
;  ;;   |
107 | 47, 15, 2, 88, 15, 31, 102, 106 | decmul2c 11099 |
. . . . . . . 8
; ;  ;;;    |
108 | 87, 107 | eqtr4i 2476 |
. . . . . . 7
   ;  ; ;   |
109 | 8, 9, 15, 46, 47, 45, 49, 53, 108 | mod2xi 15041 |
. . . . . 6
   ;   ;
  |
110 | | eqid 2451 |
. . . . . . 7
; ;  |
111 | 51 | mulid1i 9645 |
. . . . . . . . 9
   |
112 | 111 | oveq1i 6300 |
. . . . . . . 8
       |
113 | 51 | addid1i 9820 |
. . . . . . . 8
   |
114 | 112, 113 | eqtri 2473 |
. . . . . . 7
     |
115 | | 2t2e4 10759 |
. . . . . . . 8
   |
116 | 2 | dec0h 11067 |
. . . . . . . 8
;  |
117 | 115, 116 | eqtri 2473 |
. . . . . . 7
  ;  |
118 | 20, 16, 20, 110, 2, 3, 114, 117 | decmul2c 11099 |
. . . . . 6
 ;  ;  |
119 | | eqid 2451 |
. . . . . . . 8
;;  ;;   |
120 | 40 | nn0cni 10881 |
. . . . . . . . . 10
;  |
121 | 120 | addid1i 9820 |
. . . . . . . . 9
;  ;  |
122 | | dec10p 11080 |
. . . . . . . . . 10
  ;  |
123 | | 4t2e8 10763 |
. . . . . . . . . . . . 13
   |
124 | 64, 51, 123 | mulcomli 9650 |
. . . . . . . . . . . 12
   |
125 | 69 | addid1i 9820 |
. . . . . . . . . . . 12
   |
126 | 124, 125 | oveq12i 6302 |
. . . . . . . . . . 11
         |
127 | | 8p1e9 10740 |
. . . . . . . . . . 11
   |
128 | 126, 127 | eqtri 2473 |
. . . . . . . . . 10
       |
129 | 51 | mul01i 9823 |
. . . . . . . . . . . 12
   |
130 | 129 | oveq1i 6300 |
. . . . . . . . . . 11
       |
131 | 130, 63 | eqtri 2473 |
. . . . . . . . . 10
    ;  |
132 | 2, 3, 16, 3, 60, 122, 20, 3, 3, 128, 131 | decma2c 11091 |
. . . . . . . . 9
  ;     ;  |
133 | 129 | oveq1i 6300 |
. . . . . . . . . 10
       |
134 | 51 | addid2i 9821 |
. . . . . . . . . . 11
   |
135 | 20 | dec0h 11067 |
. . . . . . . . . . 11
;  |
136 | 134, 135 | eqtri 2473 |
. . . . . . . . . 10
  ;  |
137 | 133, 136 | eqtri 2473 |
. . . . . . . . 9
    ;  |
138 | 4, 3, 10, 20, 55, 121, 20, 20, 3, 132, 137 | decma2c 11091 |
. . . . . . . 8
  ;;   ;
  ;;   |
139 | 111 | oveq1i 6300 |
. . . . . . . . 9
       |
140 | | 3cn 10684 |
. . . . . . . . . . 11
 |
141 | | 3p2e5 10742 |
. . . . . . . . . . 11
   |
142 | 140, 51, 141 | addcomli 9825 |
. . . . . . . . . 10
   |
143 | 22 | dec0h 11067 |
. . . . . . . . . 10
;  |
144 | 142, 143 | eqtri 2473 |
. . . . . . . . 9
  ;  |
145 | 139, 144 | eqtri 2473 |
. . . . . . . 8
    ;  |
146 | 5, 16, 40, 41, 1, 119, 20, 22, 3, 138, 145 | decma2c 11091 |
. . . . . . 7
   ;;   ;;;    |
147 | 2, 28 | deccl 11065 |
. . . . . . . 8
;  |
148 | | eqid 2451 |
. . . . . . . . 9
; ;  |
149 | 100 | oveq2i 6301 |
. . . . . . . . . 10
           |
150 | | 9t9e81 11153 |
. . . . . . . . . . 11
  ;  |
151 | | 9p1e10 10741 |
. . . . . . . . . . . 12
   |
152 | 56, 69, 151 | addcomli 9825 |
. . . . . . . . . . 11
   |
153 | 24, 16, 12, 150, 127, 152 | decaddci2 11097 |
. . . . . . . . . 10
    ;  |
154 | 149, 153 | eqtri 2473 |
. . . . . . . . 9
      ;  |
155 | | 9t5e45 11149 |
. . . . . . . . . . 11
  ;  |
156 | 56, 81, 155 | mulcomli 9650 |
. . . . . . . . . 10
  ;  |
157 | | 7cn 10693 |
. . . . . . . . . . 11
 |
158 | | 7p5e12 11104 |
. . . . . . . . . . 11
  ;  |
159 | 157, 81, 158 | addcomli 9825 |
. . . . . . . . . 10
  ;  |
160 | 2, 22, 28, 156, 103, 20, 159 | decaddci 11096 |
. . . . . . . . 9
    ;  |
161 | 12, 22, 2, 28, 54, 148, 12, 20, 22, 154, 160 | decmac 11090 |
. . . . . . . 8
 ;  ;  ;;   |
162 | | 5p2e7 10747 |
. . . . . . . . . 10
   |
163 | 2, 22, 20, 155, 162 | decaddi 11095 |
. . . . . . . . 9
    ;  |
164 | | 5t5e25 11127 |
. . . . . . . . 9
  ;  |
165 | 22, 12, 22, 54, 22, 20, 163, 164 | decmul1c 11098 |
. . . . . . . 8
;  ;;   |
166 | 45, 12, 22, 54, 22, 147, 161, 165 | decmul2c 11099 |
. . . . . . 7
; ;  ;;;    |
167 | 146, 166 | eqtr4i 2476 |
. . . . . 6
   ;;   ; ;   |
168 | 8, 9, 43, 44, 45, 42, 109, 118, 167 | mod2xi 15041 |
. . . . 5
   ;   ;;    |
169 | | eqid 2451 |
. . . . . 6
; ;  |
170 | 20, 2, 103, 169 | decsuc 11074 |
. . . . 5
;  ;  |
171 | 37 | nn0cni 10881 |
. . . . . . 7
;;;    |
172 | 171 | addid2i 9821 |
. . . . . 6
 ;;;    ;;;    |
173 | 8 | nncni 10619 |
. . . . . . . 8
 |
174 | 173 | mul02i 9822 |
. . . . . . 7
   |
175 | 174 | oveq1i 6300 |
. . . . . 6
   ;;;     ;;;     |
176 | | eqid 2451 |
. . . . . . . . . 10
; ;  |
177 | 20 | dec0u 11066 |
. . . . . . . . . . . 12
  ;  |
178 | 177 | oveq1i 6300 |
. . . . . . . . . . 11
    ;   |
179 | 35 | nn0cni 10881 |
. . . . . . . . . . . 12
;  |
180 | 179 | addid1i 9820 |
. . . . . . . . . . 11
;  ;  |
181 | 178, 180 | eqtri 2473 |
. . . . . . . . . 10
    ;  |
182 | 20, 10, 20, 176, 2, 3, 181, 117 | decmul1c 11098 |
. . . . . . . . 9
;  ;;   |
183 | 182 | oveq1i 6300 |
. . . . . . . 8
 ;
  ;;    |
184 | 36 | nn0cni 10881 |
. . . . . . . . 9
;;   |
185 | 184 | addid1i 9820 |
. . . . . . . 8
;;   ;;   |
186 | 183, 185 | eqtri 2473 |
. . . . . . 7
 ;
  ;;   |
187 | | 3t2e6 10761 |
. . . . . . . 8
   |
188 | 187, 84 | eqtri 2473 |
. . . . . . 7
  ;  |
189 | 20, 40, 41, 119, 15, 3, 186, 188 | decmul1c 11098 |
. . . . . 6
;;   ;;;    |
190 | 172, 175,
189 | 3eqtr4i 2483 |
. . . . 5
   ;;;    ;;    |
191 | 8, 9, 38, 39, 42, 37, 168, 170, 190 | modxp1i 15042 |
. . . 4
   ;   ;;;     |
192 | 115 | oveq1i 6300 |
. . . . . 6
       |
193 | 192, 103 | eqtri 2473 |
. . . . 5
     |
194 | | 5t2e10 10764 |
. . . . . . 7
   |
195 | 81, 51, 194 | mulcomli 9650 |
. . . . . 6
   |
196 | | dec10 11081 |
. . . . . 6
;  |
197 | 195, 196 | eqtri 2473 |
. . . . 5
  ;  |
198 | 20, 20, 22, 89, 3, 16, 193, 197 | decmul2c 11099 |
. . . 4
 ;  ;  |
199 | | eqid 2451 |
. . . . . 6
;;  ;;   |
200 | 20, 16 | deccl 11065 |
. . . . . . 7
;  |
201 | | eqid 2451 |
. . . . . . . 8
; ;  |
202 | | eqid 2451 |
. . . . . . . 8
; ;  |
203 | | 0p1e1 10721 |
. . . . . . . . 9
   |
204 | | 10p10e20 11121 |
. . . . . . . . 9
  ;  |
205 | 20, 3, 203, 204 | decsuc 11074 |
. . . . . . . 8
    ;  |
206 | | 7p4e11 11103 |
. . . . . . . 8
  ;  |
207 | 10, 28, 10, 2, 201, 202, 205, 16, 206 | decaddc 11093 |
. . . . . . 7
; ;  ;;   |
208 | 200 | nn0cni 10881 |
. . . . . . . . 9
;  |
209 | 208 | addid1i 9820 |
. . . . . . . 8
;  ;  |
210 | | eqid 2451 |
. . . . . . . . 9
;;  ;;   |
211 | 113, 135 | eqtri 2473 |
. . . . . . . . 9
  ;  |
212 | 16 | dec0h 11067 |
. . . . . . . . . . . 12
;  |
213 | 203, 212 | eqtri 2473 |
. . . . . . . . . . 11
  ;  |
214 | 64 | mul02i 9822 |
. . . . . . . . . . . . 13
   |
215 | 214 | oveq1i 6300 |
. . . . . . . . . . . 12
       |
216 | 215, 213 | eqtri 2473 |
. . . . . . . . . . 11
    ;  |
217 | 16, 3, 3, 16, 196, 213, 2, 16, 3, 68, 216 | decmac 11090 |
. . . . . . . . . 10
      ;  |
218 | | 6p2e8 10751 |
. . . . . . . . . . 11
   |
219 | 16, 15, 20, 105, 218 | decaddi 11095 |
. . . . . . . . . 10
    ;  |
220 | 10, 2, 3, 20, 202, 136, 2, 24, 16, 217, 219 | decmac 11090 |
. . . . . . . . 9
 ;
    ;;   |
221 | | 4p2e6 10744 |
. . . . . . . . . 10
   |
222 | 20, 2, 20, 97, 221 | decaddi 11095 |
. . . . . . . . 9
    ;  |
223 | 32, 15, 3, 20, 210, 211, 2, 15, 20, 220, 222 | decmac 11090 |
. . . . . . . 8
 ;;      ;;;    |
224 | 33 | nn0cni 10881 |
. . . . . . . . . . 11
;;   |
225 | 224 | mul01i 9823 |
. . . . . . . . . 10
;;    |
226 | 225 | oveq1i 6300 |
. . . . . . . . 9
 ;;       |
227 | 226, 213 | eqtri 2473 |
. . . . . . . 8
 ;;    ;  |
228 | 2, 3, 20, 16, 60, 209, 33, 16, 3, 223, 227 | decma2c 11091 |
. . . . . . 7
 ;;  ;  ;   ;;;;     |
229 | 4, 3, 200, 16, 55, 207, 33, 16, 3, 228, 227 | decma2c 11091 |
. . . . . 6
 ;;  ;;   ; ;   ;;;;;      |
230 | 224 | mulid1i 9645 |
. . . . . . . 8
;;   ;;   |
231 | 230 | oveq1i 6300 |
. . . . . . 7
 ;;    ;;    |
232 | 224 | addid1i 9820 |
. . . . . . 7
;;   ;;   |
233 | 231, 232 | eqtri 2473 |
. . . . . 6
 ;;    ;;   |
234 | 5, 16, 29, 3, 1, 199, 33, 15, 32, 229, 233 | decma2c 11091 |
. . . . 5
 ;;   ;;   ;;;;;;       |
235 | | eqid 2451 |
. . . . . 6
;;;   ;;;    |
236 | 43, 20 | deccl 11065 |
. . . . . . 7
;;   |
237 | 236, 28 | deccl 11065 |
. . . . . 6
;;;    |
238 | | eqid 2451 |
. . . . . . 7
;;  ;;   |
239 | | eqid 2451 |
. . . . . . 7
;;;   ;;;    |
240 | 24, 16 | deccl 11065 |
. . . . . . . 8
;  |
241 | 240, 12 | deccl 11065 |
. . . . . . 7
;;   |
242 | | eqid 2451 |
. . . . . . . 8
; ;  |
243 | | eqid 2451 |
. . . . . . . . 9
;;  ;;   |
244 | | eqid 2451 |
. . . . . . . . 9
;;  ;;   |
245 | | eqid 2451 |
. . . . . . . . . . 11
; ;  |
246 | | 8cn 10695 |
. . . . . . . . . . . 12
 |
247 | 246, 69, 127 | addcomli 9825 |
. . . . . . . . . . 11
   |
248 | | 2p1e3 10733 |
. . . . . . . . . . 11
   |
249 | 16, 20, 24, 16, 110, 245, 247, 248 | decadd 11092 |
. . . . . . . . . 10
; ;  ;  |
250 | 12, 41, 93, 249 | decsuc 11074 |
. . . . . . . . 9
 ; ;   ;  |
251 | | 9p2e11 11113 |
. . . . . . . . . 10
  ;  |
252 | 56, 51, 251 | addcomli 9825 |
. . . . . . . . 9
  ;  |
253 | 43, 20, 240, 12, 243, 244, 250, 16, 252 | decaddc 11093 |
. . . . . . . 8
;;  ;;   ;;   |
254 | 13 | nn0cni 10881 |
. . . . . . . . . 10
;  |
255 | 254 | addid1i 9820 |
. . . . . . . . 9
;  ;  |
256 | 151, 196 | eqtri 2473 |
. . . . . . . . . 10
  ;  |
257 | 125, 212 | eqtri 2473 |
. . . . . . . . . . 11
  ;  |
258 | 115, 61 | oveq12i 6302 |
. . . . . . . . . . . 12
         |
259 | 258, 67 | eqtri 2473 |
. . . . . . . . . . 11
       |
260 | 51 | mul02i 9822 |
. . . . . . . . . . . . 13
   |
261 | 260 | oveq1i 6300 |
. . . . . . . . . . . 12
       |
262 | 261, 213 | eqtri 2473 |
. . . . . . . . . . 11
    ;  |
263 | 20, 3, 3, 16, 242, 257, 20, 16, 3, 259, 262 | decmac 11090 |
. . . . . . . . . 10
 ;     ;  |
264 | 123 | oveq1i 6300 |
. . . . . . . . . . 11
       |
265 | 246 | addid1i 9820 |
. . . . . . . . . . . 12
   |
266 | 24 | dec0h 11067 |
. . . . . . . . . . . 12
;  |
267 | 265, 266 | eqtri 2473 |
. . . . . . . . . . 11
  ;  |
268 | 264, 267 | eqtri 2473 |
. . . . . . . . . 10
    ;  |
269 | 35, 2, 16, 3, 238, 256, 20, 24, 3, 263, 268 | decmac 11090 |
. . . . . . . . 9
 ;;      ;;   |
270 | 64, 51, 221 | addcomli 9825 |
. . . . . . . . . 10
   |
271 | 16, 20, 2, 52, 270 | decaddi 11095 |
. . . . . . . . 9
    ;  |
272 | 36, 15, 12, 2, 235, 255, 20, 15, 16, 269, 271 | decmac 11090 |
. . . . . . . 8
 ;;;    ;   ;;;    |
273 | 171 | mul01i 9823 |
. . . . . . . . . 10
;;;     |
274 | 273 | oveq1i 6300 |
. . . . . . . . 9
 ;;;        |
275 | 274, 213 | eqtri 2473 |
. . . . . . . 8
 ;;;     ;  |
276 | 20, 3, 13, 16, 242, 253, 37, 16, 3, 272, 275 | decma2c 11091 |
. . . . . . 7
 ;;;   ;  ;;  ;;    ;;;;     |
277 | 28 | dec0h 11067 |
. . . . . . . 8
;  |
278 | 140 | addid2i 9821 |
. . . . . . . . . 10
   |
279 | 41 | dec0h 11067 |
. . . . . . . . . 10
;  |
280 | 278, 279 | eqtri 2473 |
. . . . . . . . 9
  ;  |
281 | 124, 61 | oveq12i 6302 |
. . . . . . . . . . 11
         |
282 | 281, 265 | eqtri 2473 |
. . . . . . . . . 10
       |
283 | 20, 3, 3, 16, 242, 213, 2, 16, 3, 282, 216 | decmac 11090 |
. . . . . . . . 9
 ;     ;  |
284 | | 6p3e9 10752 |
. . . . . . . . . 10
   |
285 | 16, 15, 41, 105, 284 | decaddi 11095 |
. . . . . . . . 9
    ;  |
286 | 35, 2, 3, 41, 238, 280, 2, 12, 16, 283, 285 | decmac 11090 |
. . . . . . . 8
 ;;      ;;   |
287 | 157, 64, 206 | addcomli 9825 |
. . . . . . . . 9
  ;  |
288 | 20, 2, 28, 97, 248, 16, 287 | decaddci 11096 |
. . . . . . . 8
    ;  |
289 | 36, 15, 3, 28, 235, 277, 2, 16, 41, 286, 288 | decmac 11090 |
. . . . . . 7
 ;;;     ;;;    |
290 | 35, 2, 236, 28, 238, 239, 37, 16, 241, 276, 289 | decma2c 11091 |
. . . . . 6
 ;;;   ;;   ;;;    ;;;;;      |
291 | 53 | oveq1i 6300 |
. . . . . . . . . 10
    ;   |
292 | 43 | nn0cni 10881 |
. . . . . . . . . . 11
;  |
293 | 292 | addid1i 9820 |
. . . . . . . . . 10
;  ;  |
294 | 291, 293 | eqtri 2473 |
. . . . . . . . 9
    ;  |
295 | 50 | mul02i 9822 |
. . . . . . . . . . 11
   |
296 | 295 | oveq1i 6300 |
. . . . . . . . . 10
       |
297 | 296, 134 | eqtri 2473 |
. . . . . . . . 9
     |
298 | 20, 3, 3, 20, 242, 136, 15, 294, 297 | decma 11089 |
. . . . . . . 8
 ;     ;;   |
299 | | 4p3e7 10745 |
. . . . . . . . 9
   |
300 | 20, 2, 41, 98, 299 | decaddi 11095 |
. . . . . . . 8
    ;  |
301 | 35, 2, 3, 41, 238, 279, 15, 28, 20, 298, 300 | decmac 11090 |
. . . . . . 7
 ;;    ;;;    |
302 | 15, 36, 15, 235, 15, 41, 301, 92 | decmul1c 11098 |
. . . . . 6
;;;    ;;;;     |
303 | 37, 36, 15, 235, 15, 237, 290, 302 | decmul2c 11099 |
. . . . 5
;;;   ;;;    ;;;;;;       |
304 | 234, 303 | eqtr4i 2476 |
. . . 4
 ;;   ;;   ;;;   ;;;     |
305 | 8, 9, 31, 34, 37, 30, 191, 198, 304 | mod2xi 15041 |
. . 3
   ;   ;;    |
306 | | eqid 2451 |
. . . 4
; ;  |
307 | 195 | oveq1i 6300 |
. . . . 5
       |
308 | | 10nn 10775 |
. . . . . . 7
 |
309 | 308 | nncni 10619 |
. . . . . 6
 |
310 | 309 | addid1i 9820 |
. . . . 5
   |
311 | 307, 310 | eqtri 2473 |
. . . 4
     |
312 | 129, 62 | eqtri 2473 |
. . . 4
  ;  |
313 | 20, 22, 3, 306, 3, 3, 311, 312 | decmul2c 11099 |
. . 3
 ;  ;  |
314 | | eqid 2451 |
. . . . 5
;;  ;;   |
315 | 20, 12 | deccl 11065 |
. . . . 5
;  |
316 | | eqid 2451 |
. . . . . . 7
; ;  |
317 | | eqid 2451 |
. . . . . . 7
; ;  |
318 | 218 | oveq1i 6300 |
. . . . . . . 8
       |
319 | 318, 127 | eqtri 2473 |
. . . . . . 7
     |
320 | 15, 16, 20, 12, 316, 317, 319, 152 | decaddc2 11094 |
. . . . . 6
; ;  ;  |
321 | | eqid 2451 |
. . . . . . . 8
;;  ;;   |
322 | | eqid 2451 |
. . . . . . . . 9
; ;  |
323 | 124, 278 | oveq12i 6302 |
. . . . . . . . . 10
         |
324 | | 8p3e11 11107 |
. . . . . . . . . 10
  ;  |
325 | 323, 324 | eqtri 2473 |
. . . . . . . . 9
      ;  |
326 | | 8t4e32 11141 |
. . . . . . . . . 10
  ;  |
327 | 41, 20, 20, 326, 90 | decaddi 11095 |
. . . . . . . . 9
    ;  |
328 | 20, 24, 3, 20, 322, 136, 2, 2, 41, 325, 327 | decmac 11090 |
. . . . . . . 8
 ;     ;;   |
329 | 97 | oveq1i 6300 |
. . . . . . . . 9
    ;   |
330 | 38 | nn0cni 10881 |
. . . . . . . . . 10
;  |
331 | 330 | addid1i 9820 |
. . . . . . . . 9
;  ;  |
332 | 329, 331 | eqtri 2473 |
. . . . . . . 8
    ;  |
333 | 25, 15, 3, 3, 321, 63, 2, 2, 20, 328, 332 | decmac 11090 |
. . . . . . 7
 ;;      ;;;    |
334 | 26 | nn0cni 10881 |
. . . . . . . . . 10
;;   |
335 | 334 | mul01i 9823 |
. . . . . . . . 9
;;    |
336 | 335 | oveq1i 6300 |
. . . . . . . 8
 ;;       |
337 | 336, 76 | eqtri 2473 |
. . . . . . 7
 ;;    ;  |
338 | 2, 3, 3, 12, 60, 59, 26, 12, 3, 333, 337 | decma2c 11091 |
. . . . . 6
 ;;  ;     ;;;;     |
339 | 335 | oveq1i 6300 |
. . . . . . 7
 ;;       |
340 | 339, 63 | eqtri 2473 |
. . . . . 6
 ;;    ;  |
341 | 4, 3, 12, 3, 55, 320, 26, 3, 3, 338, 340 | decma2c 11091 |
. . . . 5
 ;;  ;;   ; ;   ;;;;;      |
342 | 111, 61 | oveq12i 6302 |
. . . . . . . 8
         |
343 | 342, 113 | eqtri 2473 |
. . . . . . 7
       |
344 | 246 | mulid1i 9645 |
. . . . . . . . 9
   |
345 | 344 | oveq1i 6300 |
. . . . . . . 8
       |
346 | 127, 58 | eqtri 2473 |
. . . . . . . 8
  ;  |
347 | 345, 346 | eqtri 2473 |
. . . . . . 7
    ;  |
348 | 20, 24, 3, 16, 322, 213, 16, 12, 3, 343, 347 | decmac 11090 |
. . . . . 6
 ;     ;  |
349 | 50 | mulid1i 9645 |
. . . . . . . 8
   |
350 | 349 | oveq1i 6300 |
. . . . . . 7
       |
351 | 94, 196 | eqtri 2473 |
. . . . . . 7
  ;  |
352 | 350, 351 | eqtri 2473 |
. . . . . 6
    ;  |
353 | 25, 15, 3, 2, 321, 116, 16, 3, 16, 348, 352 | decmac 11090 |
. . . . 5
 ;;    ;;   |
354 | 5, 16, 17, 2, 1, 314, 26, 3, 315, 341, 353 | decma2c 11091 |
. . . 4
 ;;   ;;   ;;;;;;       |
355 | 16, 16 | deccl 11065 |
. . . . . . . . 9
;  |
356 | 355, 2 | deccl 11065 |
. . . . . . . 8
;;   |
357 | 356, 2 | deccl 11065 |
. . . . . . 7
;;;    |
358 | 357, 12 | deccl 11065 |
. . . . . 6
;;;;     |
359 | 28, 2 | deccl 11065 |
. . . . . . . 8
;  |
360 | 359, 12 | deccl 11065 |
. . . . . . 7
;;   |
361 | | eqid 2451 |
. . . . . . . 8
;;  ;;   |
362 | 359 | nn0cni 10881 |
. . . . . . . . . 10
;  |
363 | 362 | addid1i 9820 |
. . . . . . . . 9
;  ;  |
364 | 157 | addid1i 9820 |
. . . . . . . . . . 11
   |
365 | 364, 277 | eqtri 2473 |
. . . . . . . . . 10
  ;  |
366 | 79, 61 | oveq12i 6302 |
. . . . . . . . . . . 12
         |
367 | 366, 125 | eqtri 2473 |
. . . . . . . . . . 11
       |
368 | 69 | mul02i 9822 |
. . . . . . . . . . . . 13
   |
369 | 368 | oveq1i 6300 |
. . . . . . . . . . . 12
       |
370 | 369, 213 | eqtri 2473 |
. . . . . . . . . . 11
    ;  |
371 | 16, 3, 3, 16, 196, 213, 16, 16, 3, 367, 370 | decmac 11090 |
. . . . . . . . . 10
      ;  |
372 | 157 | mulid1i 9645 |
. . . . . . . . . . . 12
   |
373 | 372 | oveq1i 6300 |
. . . . . . . . . . 11
       |
374 | | 7p7e14 11106 |
. . . . . . . . . . 11
  ;  |
375 | 373, 374 | eqtri 2473 |
. . . . . . . . . 10
    ;  |
376 | 10, 28, 3, 28, 201, 365, 16, 2, 16, 371, 375 | decmac 11090 |
. . . . . . . . 9
 ;
    ;;   |
377 | 368 | oveq1i 6300 |
. . . . . . . . . 10
       |
378 | 64 | addid2i 9821 |
. . . . . . . . . . 11
   |
379 | 378, 116 | eqtri 2473 |
. . . . . . . . . 10
  ;  |
380 | 377, 379 | eqtri 2473 |
. . . . . . . . 9
    ;  |
381 | 29, 3, 28, 2, 199, 363, 16, 2, 3, 376, 380 | decmac 11090 |
. . . . . . . 8
 ;;   ;   ;;;    |
382 | 30 | nn0cni 10881 |
. . . . . . . . . . 11
;;   |
383 | 382 | mul01i 9823 |
. . . . . . . . . 10
;;    |
384 | 383 | oveq1i 6300 |
. . . . . . . . 9
 ;;       |
385 | 384, 76 | eqtri 2473 |
. . . . . . . 8
 ;;    ;  |
386 | 16, 3, 359, 12, 196, 361, 30, 12, 3, 381, 385 | decma2c 11091 |
. . . . . . 7
 ;;   ;;   ;;;;     |
387 | 157 | mulid2i 9646 |
. . . . . . . . . . . . . 14
   |
388 | 387, 61 | oveq12i 6302 |
. . . . . . . . . . . . 13
         |
389 | 388, 364 | eqtri 2473 |
. . . . . . . . . . . 12
       |
390 | 157 | mul02i 9822 |
. . . . . . . . . . . . . 14
   |
391 | 390 | oveq1i 6300 |
. . . . . . . . . . . . 13
       |
392 | 391, 379 | eqtri 2473 |
. . . . . . . . . . . 12
    ;  |
393 | 16, 3, 3, 2, 196, 116, 28, 2, 3, 389, 392 | decmac 11090 |
. . . . . . . . . . 11
    ;  |
394 | | 7t7e49 11138 |
. . . . . . . . . . 11
  ;  |
395 | 28, 10, 28, 201, 12, 2, 393, 394 | decmul1c 11098 |
. . . . . . . . . 10
;  ;;   |
396 | 395 | oveq1i 6300 |
. . . . . . . . 9
 ;
  ;;    |
397 | 360 | nn0cni 10881 |
. . . . . . . . . 10
;;   |
398 | 397 | addid1i 9820 |
. . . . . . . . 9
;;   ;;   |
399 | 396, 398 | eqtri 2473 |
. . . . . . . 8
 ;
  ;;   |
400 | 390, 62 | eqtri 2473 |
. . . . . . . 8
  ;  |
401 | 28, 29, 3, 199, 3, 3, 399, 400 | decmul1c 11098 |
. . . . . . 7
;;   ;;;    |
402 | 30, 10, 28, 201, 3, 360, 386, 401 | decmul2c 11099 |
. . . . . 6
;;  ;  ;;;;;      |
403 | 358, 3, 3, 402, 61 | decaddi 11095 |
. . . . 5
 ;;  ;   ;;;;;      |
404 | 383, 62 | eqtri 2473 |
. . . . 5
;;   ;  |
405 | 30, 29, 3, 199, 3, 3, 403, 404 | decmul2c 11099 |
. . . 4
;;  ;;   ;;;;;;       |
406 | 354, 405 | eqtr4i 2476 |
. . 3
 ;;   ;;   ;;  ;;    |
407 | 8, 9, 23, 27, 30, 18, 305, 313, 406 | mod2xi 15041 |
. 2
   ;   ;;    |
408 | | eqid 2451 |
. . 3
; ;  |
409 | 20, 16, 3, 196, 3, 3, 114, 312 | decmul2c 11099 |
. . . . 5
  ;  |
410 | 409 | oveq1i 6300 |
. . . 4
    ;   |
411 | 410, 180 | eqtri 2473 |
. . 3
    ;  |
412 | 20, 10, 3, 408, 3, 3, 411, 312 | decmul2c 11099 |
. 2
 ;  ;;   |
413 | | eqid 2451 |
. . . 4
;;  ;;   |
414 | | eqid 2451 |
. . . . . 6
; ;  |
415 | 12, 3, 12, 414, 75 | decaddi 11095 |
. . . . 5
;  ;  |
416 | | eqid 2451 |
. . . . . . 7
; ;  |
417 | 203 | oveq2i 6301 |
. . . . . . . 8
           |
418 | | 6p1e7 10738 |
. . . . . . . . 9
   |
419 | | 9t4e36 11148 |
. . . . . . . . 9
  ;  |
420 | 41, 15, 418, 419 | decsuc 11074 |
. . . . . . . 8
    ;  |
421 | 417, 420 | eqtri 2473 |
. . . . . . 7
      ;  |
422 | 105 | oveq1i 6300 |
. . . . . . . 8
    ;   |
423 | 16, 15 | deccl 11065 |
. . . . . . . . . 10
;  |
424 | 423 | nn0cni 10881 |
. . . . . . . . 9
;  |
425 | 424 | addid1i 9820 |
. . . . . . . 8
;  ;  |
426 | 422, 425 | eqtri 2473 |
. . . . . . 7
    ;  |
427 | 12, 2, 3, 3, 416, 63, 2, 15, 16, 421, 426 | decmac 11090 |
. . . . . 6
 ;     ;;   |
428 | 254 | mul01i 9823 |
. . . . . . . 8
;   |
429 | 428 | oveq1i 6300 |
. . . . . . 7
 ;      |
430 | 429, 76 | eqtri 2473 |
. . . . . 6
 ;   ;  |
431 | 2, 3, 3, 12, 60, 59, 13, 12, 3, 427, 430 | decma2c 11091 |
. . . . 5
 ; ;     ;;;    |
432 | 4, 3, 12, 12, 55, 415, 13, 12, 3, 431, 430 | decma2c 11091 |
. . . 4
 ; ;;   ;   ;;;;     |
433 | 56 | mulid1i 9645 |
. . . . . . 7
   |
434 | 433, 61 | oveq12i 6302 |
. . . . . 6
         |
435 | 434, 57 | eqtri 2473 |
. . . . 5
       |
436 | 64 | mulid1i 9645 |
. . . . . . 7
   |
437 | 436 | oveq1i 6300 |
. . . . . 6
       |
438 | 221, 84 | eqtri 2473 |
. . . . . 6
  ;  |
439 | 437, 438 | eqtri 2473 |
. . . . 5
    ;  |
440 | 12, 2, 3, 20, 416, 135, 16, 15, 3, 435, 439 | decmac 11090 |
. . . 4
 ;   ;  |
441 | 5, 16, 19, 20, 1, 413, 13, 15, 12, 432, 440 | decma2c 11091 |
. . 3
 ;  ;;   ;;;;;      |
442 | 38, 22 | deccl 11065 |
. . . 4
;;   |
443 | | eqid 2451 |
. . . . 5
;;  ;;   |
444 | 50, 51, 218 | addcomli 9825 |
. . . . . . 7
   |
445 | 20, 2, 15, 16, 169, 316, 444, 103 | decadd 11092 |
. . . . . 6
; ;  ;  |
446 | | 8p2e10 10756 |
. . . . . . . 8
   |
447 | 446, 196 | eqtri 2473 |
. . . . . . 7
  ;  |
448 | 41, 15, 418, 92 | decsuc 11074 |
. . . . . . 7
    ;  |
449 | 50 | mulid2i 9646 |
. . . . . . . . 9
   |
450 | 449 | oveq1i 6300 |
. . . . . . . 8
       |
451 | 50 | addid1i 9820 |
. . . . . . . 8
   |
452 | 450, 451 | eqtri 2473 |
. . . . . . 7
     |
453 | 15, 16, 16, 3, 316, 447, 15, 448, 452 | decma 11089 |
. . . . . 6
 ;     ;;   |
454 | 17, 2, 24, 22, 314, 445, 15, 12, 20, 453, 101 | decmac 11090 |
. . . . 5
 ;;   ; ;   ;;;    |
455 | 349, 61 | oveq12i 6302 |
. . . . . . . 8
         |
456 | 455, 451 | eqtri 2473 |
. . . . . . 7
       |
457 | 79 | oveq1i 6300 |
. . . . . . . 8
       |
458 | 457, 257 | eqtri 2473 |
. . . . . . 7
    ;  |
459 | 15, 16, 3, 3, 316, 63, 16, 16, 3, 456, 458 | decmac 11090 |
. . . . . 6
 ;     ;  |
460 | 436 | oveq1i 6300 |
. . . . . . 7
       |
461 | 100, 58 | eqtri 2473 |
. . . . . . 7
  ;  |
462 | 460, 461 | eqtri 2473 |
. . . . . 6
    ;  |
463 | 17, 2, 3, 22, 314, 143, 16, 12, 3, 459, 462 | decmac 11090 |
. . . . 5
 ;;    ;;   |
464 | 15, 16, 38, 22, 316, 443, 18, 12, 17, 454, 463 | decma2c 11091 |
. . . 4
 ;;  ;  ;;   ;;;;     |
465 | 65 | oveq1i 6300 |
. . . . . . 7
       |
466 | 465, 103 | eqtri 2473 |
. . . . . 6
     |
467 | 15, 16, 3, 16, 316, 212, 2, 332, 466 | decma 11089 |
. . . . 5
 ;   ;;   |
468 | 2, 17, 2, 314, 15, 16, 467, 105 | decmul1c 11098 |
. . . 4
;;   ;;;    |
469 | 18, 17, 2, 314, 15, 442, 464, 468 | decmul2c 11099 |
. . 3
;;  ;;   ;;;;;      |
470 | 441, 469 | eqtr4i 2476 |
. 2
 ;  ;;   ;;  ;;    |
471 | 8, 9, 11, 14, 18, 21, 407, 412, 470 | mod2xi 15041 |
1
   ;;    ;;    |