Proof of Theorem 2503lem2
Step | Hyp | Ref
| Expression |
1 | | 2503prm.1 |
. . 3
;;;    |
2 | | 2nn0 10886 |
. . . . . 6
 |
3 | | 5nn0 10889 |
. . . . . 6
 |
4 | 2, 3 | deccl 11065 |
. . . . 5
;  |
5 | | 0nn0 10884 |
. . . . 5
 |
6 | 4, 5 | deccl 11065 |
. . . 4
;;   |
7 | | 3nn 10768 |
. . . 4
 |
8 | 6, 7 | decnncl 11064 |
. . 3
;;;    |
9 | 1, 8 | eqeltri 2525 |
. 2
 |
10 | | 2nn 10767 |
. 2
 |
11 | | 1nn0 10885 |
. . . . 5
 |
12 | 11, 2 | deccl 11065 |
. . . 4
;  |
13 | 12, 3 | deccl 11065 |
. . 3
;;   |
14 | 13, 11 | deccl 11065 |
. 2
;;;    |
15 | | 0z 10948 |
. 2
 |
16 | | 4nn0 10888 |
. . . . 5
 |
17 | 12, 16 | deccl 11065 |
. . . 4
;;   |
18 | | 8nn0 10892 |
. . . 4
 |
19 | 17, 18 | deccl 11065 |
. . 3
;;;    |
20 | | 1z 10967 |
. . 3
 |
21 | | 3nn0 10887 |
. . . . 5
 |
22 | 21, 11 | deccl 11065 |
. . . 4
;  |
23 | 22, 21 | deccl 11065 |
. . 3
;;   |
24 | | 6nn0 10890 |
. . . . . 6
 |
25 | 24, 2 | deccl 11065 |
. . . . 5
;  |
26 | 25, 16 | deccl 11065 |
. . . 4
;;   |
27 | | 9nn0 10893 |
. . . . . 6
 |
28 | 2, 27 | deccl 11065 |
. . . . 5
;  |
29 | 28 | nn0zi 10962 |
. . . 4
;  |
30 | | 7nn0 10891 |
. . . . . 6
 |
31 | 2, 30 | deccl 11065 |
. . . . 5
;  |
32 | 31, 5 | deccl 11065 |
. . . 4
;;   |
33 | 22, 2 | deccl 11065 |
. . . . 5
;;   |
34 | 2, 21 | deccl 11065 |
. . . . . . 7
;  |
35 | 34, 18 | deccl 11065 |
. . . . . 6
;;   |
36 | 35 | nn0zi 10962 |
. . . . 5
;;   |
37 | 30, 30 | deccl 11065 |
. . . . . 6
;  |
38 | 37, 2 | deccl 11065 |
. . . . 5
;;   |
39 | 11, 3 | deccl 11065 |
. . . . . . 7
;  |
40 | 39, 24 | deccl 11065 |
. . . . . 6
;;   |
41 | 21 | nn0zi 10962 |
. . . . . 6
 |
42 | 27, 11 | deccl 11065 |
. . . . . 6
;  |
43 | 30, 18 | deccl 11065 |
. . . . . . 7
;  |
44 | 39 | nn0zi 10962 |
. . . . . . 7
;  |
45 | 11, 27 | deccl 11065 |
. . . . . . . 8
;  |
46 | | 4nn 10769 |
. . . . . . . 8
 |
47 | 45, 46 | decnncl 11064 |
. . . . . . 7
;;   |
48 | 34, 5 | deccl 11065 |
. . . . . . . 8
;;   |
49 | 48, 27 | deccl 11065 |
. . . . . . 7
;;;    |
50 | 21, 27 | deccl 11065 |
. . . . . . . 8
;  |
51 | 16 | nn0zi 10962 |
. . . . . . . 8
 |
52 | 11, 11 | deccl 11065 |
. . . . . . . . 9
;  |
53 | 52, 11 | deccl 11065 |
. . . . . . . 8
;;   |
54 | 21, 18 | deccl 11065 |
. . . . . . . . 9
;  |
55 | 11, 21 | deccl 11065 |
. . . . . . . . . . 11
;  |
56 | 55, 5 | deccl 11065 |
. . . . . . . . . 10
;;   |
57 | 56, 30 | deccl 11065 |
. . . . . . . . 9
;;;    |
58 | 3, 21 | deccl 11065 |
. . . . . . . . . . . 12
;  |
59 | 58, 18 | deccl 11065 |
. . . . . . . . . . 11
;;   |
60 | 59 | nn0zi 10962 |
. . . . . . . . . 10
;;   |
61 | 52, 24 | deccl 11065 |
. . . . . . . . . . 11
;;   |
62 | 61, 11 | deccl 11065 |
. . . . . . . . . 10
;;;    |
63 | 11, 18 | deccl 11065 |
. . . . . . . . . . 11
;  |
64 | 63, 21 | deccl 11065 |
. . . . . . . . . . . 12
;;   |
65 | 64, 2 | deccl 11065 |
. . . . . . . . . . 11
;;;    |
66 | 1 | 2503lem1 15108 |
. . . . . . . . . . 11
   ;   ;;;     |
67 | | 8p1e9 10740 |
. . . . . . . . . . . 12
   |
68 | | eqid 2451 |
. . . . . . . . . . . 12
; ;  |
69 | 11, 18, 67, 68 | decsuc 11074 |
. . . . . . . . . . 11
;  ;  |
70 | | eqid 2451 |
. . . . . . . . . . . . 13
;;;   ;;;    |
71 | | eqid 2451 |
. . . . . . . . . . . . . 14
;;  ;;   |
72 | 61 | nn0cni 10881 |
. . . . . . . . . . . . . . 15
;;   |
73 | 72 | addid1i 9820 |
. . . . . . . . . . . . . 14
;;   ;;   |
74 | | eqid 2451 |
. . . . . . . . . . . . . . 15
; ;  |
75 | 52 | nn0cni 10881 |
. . . . . . . . . . . . . . . 16
;  |
76 | 75 | addid1i 9820 |
. . . . . . . . . . . . . . 15
;  ;  |
77 | | 2cn 10680 |
. . . . . . . . . . . . . . . . . 18
 |
78 | 77 | mulid2i 9646 |
. . . . . . . . . . . . . . . . 17
   |
79 | | 1p0e1 10722 |
. . . . . . . . . . . . . . . . 17
   |
80 | 78, 79 | oveq12i 6302 |
. . . . . . . . . . . . . . . 16
         |
81 | | 2p1e3 10733 |
. . . . . . . . . . . . . . . 16
   |
82 | 80, 81 | eqtri 2473 |
. . . . . . . . . . . . . . 15
       |
83 | | 5cn 10689 |
. . . . . . . . . . . . . . . . . 18
 |
84 | 83 | mulid2i 9646 |
. . . . . . . . . . . . . . . . 17
   |
85 | 84 | oveq1i 6300 |
. . . . . . . . . . . . . . . 16
       |
86 | | 5p1e6 10737 |
. . . . . . . . . . . . . . . 16
   |
87 | 24 | dec0h 11067 |
. . . . . . . . . . . . . . . 16
;  |
88 | 85, 86, 87 | 3eqtri 2477 |
. . . . . . . . . . . . . . 15
    ;  |
89 | 2, 3, 11, 11, 74, 76, 11, 24, 5, 82, 88 | decma2c 11091 |
. . . . . . . . . . . . . 14
  ;  ;   ;  |
90 | | ax-1cn 9597 |
. . . . . . . . . . . . . . . . 17
 |
91 | 90 | mul01i 9823 |
. . . . . . . . . . . . . . . 16
   |
92 | 91 | oveq1i 6300 |
. . . . . . . . . . . . . . 15
       |
93 | | 6cn 10691 |
. . . . . . . . . . . . . . . 16
 |
94 | 93 | addid2i 9821 |
. . . . . . . . . . . . . . 15
   |
95 | 92, 94, 87 | 3eqtri 2477 |
. . . . . . . . . . . . . 14
    ;  |
96 | 4, 5, 52, 24, 71, 73, 11, 24, 5, 89, 95 | decma2c 11091 |
. . . . . . . . . . . . 13
  ;;   ;;    ;;   |
97 | | 3cn 10684 |
. . . . . . . . . . . . . . . 16
 |
98 | 97 | mulid2i 9646 |
. . . . . . . . . . . . . . 15
   |
99 | 98 | oveq1i 6300 |
. . . . . . . . . . . . . 14
       |
100 | | 3p1e4 10735 |
. . . . . . . . . . . . . 14
   |
101 | 16 | dec0h 11067 |
. . . . . . . . . . . . . 14
;  |
102 | 99, 100, 101 | 3eqtri 2477 |
. . . . . . . . . . . . 13
    ;  |
103 | 6, 21, 61, 11, 1, 70, 11, 16, 5, 96, 102 | decma2c 11091 |
. . . . . . . . . . . 12
   ;;;    ;;;    |
104 | | eqid 2451 |
. . . . . . . . . . . . 13
;;;   ;;;    |
105 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
;;  ;;   |
106 | 78 | oveq1i 6300 |
. . . . . . . . . . . . . . . . . . . 20
       |
107 | 106, 81 | eqtri 2473 |
. . . . . . . . . . . . . . . . . . 19
     |
108 | | 8t2e16 11139 |
. . . . . . . . . . . . . . . . . . 19
  ;  |
109 | 2, 11, 18, 68, 24, 11, 107, 108 | decmul1c 11098 |
. . . . . . . . . . . . . . . . . 18
;  ;  |
110 | 109 | oveq1i 6300 |
. . . . . . . . . . . . . . . . 17
 ;   ;   |
111 | 21, 24 | deccl 11065 |
. . . . . . . . . . . . . . . . . . 19
;  |
112 | 111 | nn0cni 10881 |
. . . . . . . . . . . . . . . . . 18
;  |
113 | 112 | addid1i 9820 |
. . . . . . . . . . . . . . . . 17
;  ;  |
114 | 110, 113 | eqtri 2473 |
. . . . . . . . . . . . . . . 16
 ;   ;  |
115 | | 3t2e6 10761 |
. . . . . . . . . . . . . . . . 17
   |
116 | 115, 87 | eqtri 2473 |
. . . . . . . . . . . . . . . 16
  ;  |
117 | 2, 63, 21, 105, 24, 5, 114, 116 | decmul1c 11098 |
. . . . . . . . . . . . . . 15
;;   ;;   |
118 | 117 | oveq1i 6300 |
. . . . . . . . . . . . . 14
 ;;    ;;    |
119 | 111, 24 | deccl 11065 |
. . . . . . . . . . . . . . . 16
;;   |
120 | 119 | nn0cni 10881 |
. . . . . . . . . . . . . . 15
;;   |
121 | 120 | addid1i 9820 |
. . . . . . . . . . . . . 14
;;   ;;   |
122 | 118, 121 | eqtri 2473 |
. . . . . . . . . . . . 13
 ;;    ;;   |
123 | | 2t2e4 10759 |
. . . . . . . . . . . . . 14
   |
124 | 123, 101 | eqtri 2473 |
. . . . . . . . . . . . 13
  ;  |
125 | 2, 64, 2, 104, 16, 5, 122, 124 | decmul1c 11098 |
. . . . . . . . . . . 12
;;;    ;;;    |
126 | 103, 125 | eqtr4i 2476 |
. . . . . . . . . . 11
   ;;;    ;;;     |
127 | 9, 10, 63, 20, 65, 62, 66, 69, 126 | modxp1i 15042 |
. . . . . . . . . 10
   ;   ;;;     |
128 | | eqid 2451 |
. . . . . . . . . . 11
; ;  |
129 | | 2t1e2 10758 |
. . . . . . . . . . . . 13
   |
130 | 129 | oveq1i 6300 |
. . . . . . . . . . . 12
       |
131 | 130, 81 | eqtri 2473 |
. . . . . . . . . . 11
     |
132 | | 9cn 10697 |
. . . . . . . . . . . 12
 |
133 | | 9t2e18 11146 |
. . . . . . . . . . . 12
  ;  |
134 | 132, 77, 133 | mulcomli 9650 |
. . . . . . . . . . 11
  ;  |
135 | 2, 11, 27, 128, 18, 11, 131, 134 | decmul2c 11099 |
. . . . . . . . . 10
 ;  ;  |
136 | | eqid 2451 |
. . . . . . . . . . . 12
;;;   ;;;    |
137 | 11, 24 | deccl 11065 |
. . . . . . . . . . . . 13
;  |
138 | 137, 2 | deccl 11065 |
. . . . . . . . . . . 12
;;   |
139 | | eqid 2451 |
. . . . . . . . . . . . . 14
;;  ;;   |
140 | | eqid 2451 |
. . . . . . . . . . . . . 14
;;  ;;   |
141 | | eqid 2451 |
. . . . . . . . . . . . . . 15
; ;  |
142 | | eqid 2451 |
. . . . . . . . . . . . . . 15
; ;  |
143 | | 1p1e2 10723 |
. . . . . . . . . . . . . . 15
   |
144 | | 6p3e9 10752 |
. . . . . . . . . . . . . . . 16
   |
145 | 93, 97, 144 | addcomli 9825 |
. . . . . . . . . . . . . . 15
   |
146 | 11, 21, 11, 24, 141, 142, 143, 145 | decadd 11092 |
. . . . . . . . . . . . . 14
; ;  ;  |
147 | 77 | addid2i 9821 |
. . . . . . . . . . . . . 14
   |
148 | 55, 5, 137, 2, 139, 140, 146, 147 | decadd 11092 |
. . . . . . . . . . . . 13
;;  ;;   ;;   |
149 | 28 | nn0cni 10881 |
. . . . . . . . . . . . . . 15
;  |
150 | 149 | addid1i 9820 |
. . . . . . . . . . . . . 14
;  ;  |
151 | 2, 24 | deccl 11065 |
. . . . . . . . . . . . . . 15
;  |
152 | 151, 27 | deccl 11065 |
. . . . . . . . . . . . . 14
;;   |
153 | | eqid 2451 |
. . . . . . . . . . . . . . 15
;;  ;;   |
154 | 2 | dec0h 11067 |
. . . . . . . . . . . . . . . 16
;  |
155 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
;;  ;;   |
156 | | 6p1e7 10738 |
. . . . . . . . . . . . . . . . 17
   |
157 | 151 | nn0cni 10881 |
. . . . . . . . . . . . . . . . . 18
;  |
158 | 157 | addid2i 9821 |
. . . . . . . . . . . . . . . . 17
 ;  ;  |
159 | 2, 24, 156, 158 | decsuc 11074 |
. . . . . . . . . . . . . . . 16
  ;   ;  |
160 | | 9p2e11 11113 |
. . . . . . . . . . . . . . . . 17
  ;  |
161 | 132, 77, 160 | addcomli 9825 |
. . . . . . . . . . . . . . . 16
  ;  |
162 | 5, 2, 151, 27, 154, 155, 159, 11, 161 | decaddc 11093 |
. . . . . . . . . . . . . . 15
 ;;   ;;   |
163 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
; ;  |
164 | | 7p1e8 10739 |
. . . . . . . . . . . . . . . . 17
   |
165 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
; ;  |
166 | 2, 30, 164, 165 | decsuc 11074 |
. . . . . . . . . . . . . . . 16
;  ;  |
167 | 81 | oveq2i 6301 |
. . . . . . . . . . . . . . . . 17
           |
168 | | 5t2e10 10764 |
. . . . . . . . . . . . . . . . . . 19
   |
169 | | dec10 11081 |
. . . . . . . . . . . . . . . . . . 19
;  |
170 | 168, 169 | eqtri 2473 |
. . . . . . . . . . . . . . . . . 18
  ;  |
171 | 97 | addid2i 9821 |
. . . . . . . . . . . . . . . . . 18
   |
172 | 11, 5, 21, 170, 171 | decaddi 11095 |
. . . . . . . . . . . . . . . . 17
    ;  |
173 | 167, 172 | eqtri 2473 |
. . . . . . . . . . . . . . . 16
      ;  |
174 | 115 | oveq1i 6300 |
. . . . . . . . . . . . . . . . 17
       |
175 | | 8cn 10695 |
. . . . . . . . . . . . . . . . . 18
 |
176 | | 8p6e14 11110 |
. . . . . . . . . . . . . . . . . 18
  ;  |
177 | 175, 93, 176 | addcomli 9825 |
. . . . . . . . . . . . . . . . 17
  ;  |
178 | 174, 177 | eqtri 2473 |
. . . . . . . . . . . . . . . 16
    ;  |
179 | 3, 21, 2, 18, 163, 166, 2, 16, 11, 173, 178 | decmac 11090 |
. . . . . . . . . . . . . . 15
 ;  ;   ;;   |
180 | 11, 24, 156, 108 | decsuc 11074 |
. . . . . . . . . . . . . . 15
    ;  |
181 | 58, 18, 31, 11, 153, 162, 2, 30, 11, 179, 180 | decmac 11090 |
. . . . . . . . . . . . . 14
 ;;    ;;    ;;;    |
182 | 27 | dec0h 11067 |
. . . . . . . . . . . . . . 15
;  |
183 | | 4cn 10687 |
. . . . . . . . . . . . . . . . . 18
 |
184 | 183 | addid2i 9821 |
. . . . . . . . . . . . . . . . 17
   |
185 | 184, 101 | eqtri 2473 |
. . . . . . . . . . . . . . . 16
  ;  |
186 | | 0p1e1 10721 |
. . . . . . . . . . . . . . . . . 18
   |
187 | 186 | oveq2i 6301 |
. . . . . . . . . . . . . . . . 17
           |
188 | | 5t5e25 11127 |
. . . . . . . . . . . . . . . . . 18
  ;  |
189 | 2, 3, 86, 188 | decsuc 11074 |
. . . . . . . . . . . . . . . . 17
    ;  |
190 | 187, 189 | eqtri 2473 |
. . . . . . . . . . . . . . . 16
      ;  |
191 | | 5t3e15 11125 |
. . . . . . . . . . . . . . . . . 18
  ;  |
192 | 83, 97, 191 | mulcomli 9650 |
. . . . . . . . . . . . . . . . 17
  ;  |
193 | | 5p4e9 10749 |
. . . . . . . . . . . . . . . . 17
   |
194 | 11, 3, 16, 192, 193 | decaddi 11095 |
. . . . . . . . . . . . . . . 16
    ;  |
195 | 3, 21, 5, 16, 163, 185, 3, 27, 11, 190, 194 | decmac 11090 |
. . . . . . . . . . . . . . 15
 ;     ;;   |
196 | | 8t5e40 11142 |
. . . . . . . . . . . . . . . 16
  ;  |
197 | 132 | addid2i 9821 |
. . . . . . . . . . . . . . . 16
   |
198 | 16, 5, 27, 196, 197 | decaddi 11095 |
. . . . . . . . . . . . . . 15
    ;  |
199 | 58, 18, 5, 27, 153, 182, 3, 27, 16, 195, 198 | decmac 11090 |
. . . . . . . . . . . . . 14
 ;;    ;;;    |
200 | 2, 3, 2, 27, 74, 150, 59, 27, 152, 181, 199 | decma2c 11091 |
. . . . . . . . . . . . 13
 ;;  ;  ;   ;;;;     |
201 | 59 | nn0cni 10881 |
. . . . . . . . . . . . . . . 16
;;   |
202 | 201 | mul01i 9823 |
. . . . . . . . . . . . . . 15
;;    |
203 | 202 | oveq1i 6300 |
. . . . . . . . . . . . . 14
 ;;       |
204 | 203, 147,
154 | 3eqtri 2477 |
. . . . . . . . . . . . 13
 ;;    ;  |
205 | 4, 5, 28, 2, 71, 148, 59, 2, 5, 200, 204 | decma2c 11091 |
. . . . . . . . . . . 12
 ;;  ;;   ;;  ;;    ;;;;;      |
206 | 30 | dec0h 11067 |
. . . . . . . . . . . . 13
;  |
207 | 21 | dec0h 11067 |
. . . . . . . . . . . . . . 15
;  |
208 | 171, 207 | eqtri 2473 |
. . . . . . . . . . . . . 14
  ;  |
209 | 186 | oveq2i 6301 |
. . . . . . . . . . . . . . 15
           |
210 | 11, 3, 86, 191 | decsuc 11074 |
. . . . . . . . . . . . . . 15
    ;  |
211 | 209, 210 | eqtri 2473 |
. . . . . . . . . . . . . 14
      ;  |
212 | | 3t3e9 10762 |
. . . . . . . . . . . . . . . 16
   |
213 | 212 | oveq1i 6300 |
. . . . . . . . . . . . . . 15
       |
214 | | 9p3e12 11114 |
. . . . . . . . . . . . . . 15
  ;  |
215 | 213, 214 | eqtri 2473 |
. . . . . . . . . . . . . 14
    ;  |
216 | 3, 21, 5, 21, 163, 208, 21, 2, 11, 211, 215 | decmac 11090 |
. . . . . . . . . . . . 13
 ;     ;;   |
217 | | 8t3e24 11140 |
. . . . . . . . . . . . . 14
  ;  |
218 | | 7cn 10693 |
. . . . . . . . . . . . . . 15
 |
219 | | 7p4e11 11103 |
. . . . . . . . . . . . . . 15
  ;  |
220 | 218, 183,
219 | addcomli 9825 |
. . . . . . . . . . . . . 14
  ;  |
221 | 2, 16, 30, 217, 81, 11, 220 | decaddci 11096 |
. . . . . . . . . . . . 13
    ;  |
222 | 58, 18, 5, 30, 153, 206, 21, 11, 21, 216, 221 | decmac 11090 |
. . . . . . . . . . . 12
 ;;    ;;;    |
223 | 6, 21, 56, 30, 1, 136, 59, 11, 138, 205, 222 | decma2c 11091 |
. . . . . . . . . . 11
 ;;   ;;;    ;;;;;;       |
224 | | eqid 2451 |
. . . . . . . . . . . . 13
;;  ;;   |
225 | 24, 27 | deccl 11065 |
. . . . . . . . . . . . . 14
;  |
226 | 225, 30 | deccl 11065 |
. . . . . . . . . . . . 13
;;   |
227 | 30, 5 | deccl 11065 |
. . . . . . . . . . . . . 14
;  |
228 | | eqid 2451 |
. . . . . . . . . . . . . 14
; ;  |
229 | | eqid 2451 |
. . . . . . . . . . . . . . 15
;;  ;;   |
230 | 11 | dec0h 11067 |
. . . . . . . . . . . . . . . 16
;  |
231 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
; ;  |
232 | 94 | oveq1i 6300 |
. . . . . . . . . . . . . . . . 17
       |
233 | 232, 156 | eqtri 2473 |
. . . . . . . . . . . . . . . 16
     |
234 | | 9p1e10 10741 |
. . . . . . . . . . . . . . . . 17
   |
235 | 132, 90, 234 | addcomli 9825 |
. . . . . . . . . . . . . . . 16
   |
236 | 5, 11, 24, 27, 230, 231, 233, 235 | decaddc2 11094 |
. . . . . . . . . . . . . . 15
 ;  ;  |
237 | 218, 90, 164 | addcomli 9825 |
. . . . . . . . . . . . . . 15
   |
238 | 11, 11, 225, 30, 228, 229, 236, 237 | decadd 11092 |
. . . . . . . . . . . . . 14
; ;;   ;;   |
239 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
; ;  |
240 | 5, 30, 11, 11, 206, 228, 186, 164 | decadd 11092 |
. . . . . . . . . . . . . . . 16
 ;  ;  |
241 | 30, 5, 52, 24, 239, 224, 240, 94 | decadd 11092 |
. . . . . . . . . . . . . . 15
; ;;   ;;   |
242 | 63 | nn0cni 10881 |
. . . . . . . . . . . . . . . . 17
;  |
243 | 242 | addid1i 9820 |
. . . . . . . . . . . . . . . 16
;  ;  |
244 | 143, 154 | eqtri 2473 |
. . . . . . . . . . . . . . . . 17
  ;  |
245 | | 1t1e1 10757 |
. . . . . . . . . . . . . . . . . . 19
   |
246 | | 00id 9808 |
. . . . . . . . . . . . . . . . . . 19
   |
247 | 245, 246 | oveq12i 6302 |
. . . . . . . . . . . . . . . . . 18
         |
248 | 247, 79 | eqtri 2473 |
. . . . . . . . . . . . . . . . 17
       |
249 | 245 | oveq1i 6300 |
. . . . . . . . . . . . . . . . . 18
       |
250 | | 1p2e3 10734 |
. . . . . . . . . . . . . . . . . 18
   |
251 | 249, 250,
207 | 3eqtri 2477 |
. . . . . . . . . . . . . . . . 17
    ;  |
252 | 11, 11, 5, 2, 228, 244, 11, 21, 5, 248, 251 | decmac 11090 |
. . . . . . . . . . . . . . . 16
 ;     ;  |
253 | 93 | mulid1i 9645 |
. . . . . . . . . . . . . . . . . 18
   |
254 | 253 | oveq1i 6300 |
. . . . . . . . . . . . . . . . 17
       |
255 | 254, 177 | eqtri 2473 |
. . . . . . . . . . . . . . . 16
    ;  |
256 | 52, 24, 11, 18, 224, 243, 11, 16, 11, 252, 255 | decmac 11090 |
. . . . . . . . . . . . . . 15
 ;;   ;   ;;   |
257 | 245 | oveq1i 6300 |
. . . . . . . . . . . . . . . 16
       |
258 | 93, 90, 156 | addcomli 9825 |
. . . . . . . . . . . . . . . 16
   |
259 | 257, 258,
206 | 3eqtri 2477 |
. . . . . . . . . . . . . . 15
    ;  |
260 | 61, 11, 63, 24, 70, 241, 11, 30, 5, 256, 259 | decmac 11090 |
. . . . . . . . . . . . . 14
 ;;;    ; ;;    ;;;    |
261 | 18 | dec0h 11067 |
. . . . . . . . . . . . . . 15
;  |
262 | 5 | dec0h 11067 |
. . . . . . . . . . . . . . . . 17
;  |
263 | 246, 262 | eqtri 2473 |
. . . . . . . . . . . . . . . 16
  ;  |
264 | 245 | oveq1i 6300 |
. . . . . . . . . . . . . . . . . 18
       |
265 | 264, 79 | eqtri 2473 |
. . . . . . . . . . . . . . . . 17
     |
266 | 11, 11, 5, 5, 228, 263, 11, 265, 265 | decma 11089 |
. . . . . . . . . . . . . . . 16
 ;     ;  |
267 | 253 | oveq1i 6300 |
. . . . . . . . . . . . . . . . 17
       |
268 | 93 | addid1i 9820 |
. . . . . . . . . . . . . . . . 17
   |
269 | 267, 268,
87 | 3eqtri 2477 |
. . . . . . . . . . . . . . . 16
    ;  |
270 | 52, 24, 5, 5, 224, 263, 11, 24, 5, 266, 269 | decmac 11090 |
. . . . . . . . . . . . . . 15
 ;;      ;;   |
271 | 245 | oveq1i 6300 |
. . . . . . . . . . . . . . . 16
       |
272 | 175, 90, 67 | addcomli 9825 |
. . . . . . . . . . . . . . . 16
   |
273 | 271, 272,
182 | 3eqtri 2477 |
. . . . . . . . . . . . . . 15
    ;  |
274 | 61, 11, 5, 18, 70, 261, 11, 27, 5, 270, 273 | decmac 11090 |
. . . . . . . . . . . . . 14
 ;;;     ;;;    |
275 | 11, 11, 227, 18, 228, 238, 62, 27, 61, 260, 274 | decma2c 11091 |
. . . . . . . . . . . . 13
 ;;;   ;  ; ;;    ;;;;     |
276 | 186, 230 | eqtri 2473 |
. . . . . . . . . . . . . . 15
  ;  |
277 | 93 | mulid2i 9646 |
. . . . . . . . . . . . . . . . . 18
   |
278 | 277, 246 | oveq12i 6302 |
. . . . . . . . . . . . . . . . 17
         |
279 | 278, 268 | eqtri 2473 |
. . . . . . . . . . . . . . . 16
       |
280 | 277 | oveq1i 6300 |
. . . . . . . . . . . . . . . . 17
       |
281 | 280, 144,
182 | 3eqtri 2477 |
. . . . . . . . . . . . . . . 16
    ;  |
282 | 11, 11, 5, 21, 228, 208, 24, 27, 5, 279, 281 | decmac 11090 |
. . . . . . . . . . . . . . 15
 ;     ;  |
283 | | 6t6e36 11132 |
. . . . . . . . . . . . . . . 16
  ;  |
284 | 21, 24, 156, 283 | decsuc 11074 |
. . . . . . . . . . . . . . 15
    ;  |
285 | 52, 24, 5, 11, 224, 276, 24, 30, 21, 282, 284 | decmac 11090 |
. . . . . . . . . . . . . 14
 ;;      ;;   |
286 | 277 | oveq1i 6300 |
. . . . . . . . . . . . . . 15
       |
287 | | 6p6e12 11102 |
. . . . . . . . . . . . . . 15
  ;  |
288 | 286, 287 | eqtri 2473 |
. . . . . . . . . . . . . 14
    ;  |
289 | 61, 11, 5, 24, 70, 87, 24, 2, 11, 285, 288 | decmac 11090 |
. . . . . . . . . . . . 13
 ;;;     ;;;    |
290 | 52, 24, 52, 24, 224, 224, 62, 2, 226, 275, 289 | decma2c 11091 |
. . . . . . . . . . . 12
 ;;;   ;;   ;;   ;;;;;      |
291 | 62 | nn0cni 10881 |
. . . . . . . . . . . . 13
;;;    |
292 | 291 | mulid1i 9645 |
. . . . . . . . . . . 12
;;;    ;;;    |
293 | 62, 61, 11, 70, 11, 61, 290, 292 | decmul2c 11099 |
. . . . . . . . . . 11
;;;   ;;;    ;;;;;;       |
294 | 223, 293 | eqtr4i 2476 |
. . . . . . . . . 10
 ;;   ;;;    ;;;   ;;;     |
295 | 9, 10, 45, 60, 62, 57, 127, 135, 294 | mod2xi 15041 |
. . . . . . . . 9
   ;   ;;;     |
296 | | eqid 2451 |
. . . . . . . . . 10
; ;  |
297 | 21, 18, 67, 296 | decsuc 11074 |
. . . . . . . . 9
;  ;  |
298 | | eqid 2451 |
. . . . . . . . . . 11
;;  ;;   |
299 | 79, 230 | eqtri 2473 |
. . . . . . . . . . . . 13
  ;  |
300 | 78, 246 | oveq12i 6302 |
. . . . . . . . . . . . . 14
         |
301 | 77 | addid1i 9820 |
. . . . . . . . . . . . . 14
   |
302 | 300, 301 | eqtri 2473 |
. . . . . . . . . . . . 13
       |
303 | 2, 3, 5, 11, 74, 299, 11, 24, 5, 302, 88 | decma2c 11091 |
. . . . . . . . . . . 12
  ;     ;  |
304 | 91 | oveq1i 6300 |
. . . . . . . . . . . . 13
       |
305 | 304, 186,
230 | 3eqtri 2477 |
. . . . . . . . . . . 12
    ;  |
306 | 4, 5, 11, 11, 71, 76, 11, 11, 5, 303, 305 | decma2c 11091 |
. . . . . . . . . . 11
  ;;   ;   ;;   |
307 | 6, 21, 52, 11, 1, 298, 11, 16, 5, 306, 102 | decma2c 11091 |
. . . . . . . . . 10
   ;;   ;;;    |
308 | 115 | oveq1i 6300 |
. . . . . . . . . . . . . 14
       |
309 | 308, 268,
87 | 3eqtri 2477 |
. . . . . . . . . . . . 13
    ;  |
310 | 11, 21, 5, 5, 141, 263, 2, 24, 5, 302, 309 | decmac 11090 |
. . . . . . . . . . . 12
 ;     ;  |
311 | 77 | mul02i 9822 |
. . . . . . . . . . . . . 14
   |
312 | 311 | oveq1i 6300 |
. . . . . . . . . . . . 13
       |
313 | 312, 186,
230 | 3eqtri 2477 |
. . . . . . . . . . . 12
    ;  |
314 | 55, 5, 5, 11, 139, 230, 2, 11, 5, 310, 313 | decmac 11090 |
. . . . . . . . . . 11
 ;;    ;;   |
315 | | 7t2e14 11133 |
. . . . . . . . . . 11
  ;  |
316 | 2, 56, 30, 136, 16, 11, 314, 315 | decmul1c 11098 |
. . . . . . . . . 10
;;;    ;;;    |
317 | 307, 316 | eqtr4i 2476 |
. . . . . . . . 9
   ;;   ;;;     |
318 | 9, 10, 54, 20, 57, 53, 295, 297, 317 | modxp1i 15042 |
. . . . . . . 8
   ;   ;;    |
319 | | eqid 2451 |
. . . . . . . . 9
; ;  |
320 | 97, 77, 115 | mulcomli 9650 |
. . . . . . . . . . 11
   |
321 | 320 | oveq1i 6300 |
. . . . . . . . . 10
       |
322 | 321, 156 | eqtri 2473 |
. . . . . . . . 9
     |
323 | 2, 21, 27, 319, 18, 11, 322, 134 | decmul2c 11099 |
. . . . . . . 8
 ;  ;  |
324 | | eqid 2451 |
. . . . . . . . . 10
;;;   ;;;    |
325 | | eqid 2451 |
. . . . . . . . . . . 12
;;  ;;   |
326 | 34, 5, 2, 325, 147 | decaddi 11095 |
. . . . . . . . . . 11
;;   ;;   |
327 | 34 | nn0cni 10881 |
. . . . . . . . . . . . 13
;  |
328 | 327 | addid1i 9820 |
. . . . . . . . . . . 12
;  ;  |
329 | | 4t2e8 10763 |
. . . . . . . . . . . . . 14
   |
330 | | 2p2e4 10727 |
. . . . . . . . . . . . . 14
   |
331 | 329, 330 | oveq12i 6302 |
. . . . . . . . . . . . 13
         |
332 | | 8p4e12 11108 |
. . . . . . . . . . . . 13
  ;  |
333 | 331, 332 | eqtri 2473 |
. . . . . . . . . . . 12
      ;  |
334 | | 5t4e20 11126 |
. . . . . . . . . . . . . 14
  ;  |
335 | 83, 183, 334 | mulcomli 9650 |
. . . . . . . . . . . . 13
  ;  |
336 | 2, 5, 21, 335, 171 | decaddi 11095 |
. . . . . . . . . . . 12
    ;  |
337 | 2, 3, 2, 21, 74, 328, 16, 21, 2, 333, 336 | decma2c 11091 |
. . . . . . . . . . 11
  ;  ;   ;;   |
338 | 183 | mul01i 9823 |
. . . . . . . . . . . . 13
   |
339 | 338 | oveq1i 6300 |
. . . . . . . . . . . 12
       |
340 | 339, 147,
154 | 3eqtri 2477 |
. . . . . . . . . . 11
    ;  |
341 | 4, 5, 34, 2, 71, 326, 16, 2, 5, 337, 340 | decma2c 11091 |
. . . . . . . . . 10
  ;;   ;;    ;;;    |
342 | | 4t3e12 11123 |
. . . . . . . . . . 11
  ;  |
343 | 11, 2, 27, 342, 143, 11, 161 | decaddci 11096 |
. . . . . . . . . 10
    ;  |
344 | 6, 21, 48, 27, 1, 324, 16, 11, 2, 341, 343 | decma2c 11091 |
. . . . . . . . 9
   ;;;    ;;;;     |
345 | 5, 11, 11, 11, 230, 228, 186, 143 | decadd 11092 |
. . . . . . . . . . . 12
 ;  ;  |
346 | 245 | oveq1i 6300 |
. . . . . . . . . . . . . 14
       |
347 | 346, 143,
154 | 3eqtri 2477 |
. . . . . . . . . . . . 13
    ;  |
348 | 11, 11, 5, 11, 228, 299, 11, 2, 5, 248, 347 | decmac 11090 |
. . . . . . . . . . . 12
 ;     ;  |
349 | 52, 11, 11, 2, 298, 345, 11, 21, 5, 348, 251 | decmac 11090 |
. . . . . . . . . . 11
 ;;    ;   ;;   |
350 | 52, 11, 5, 11, 298, 230, 11, 2, 5, 266, 347 | decmac 11090 |
. . . . . . . . . . 11
 ;;    ;;   |
351 | 11, 11, 11, 11, 228, 228, 53, 2, 52, 349, 350 | decma2c 11091 |
. . . . . . . . . 10
 ;;  ;  ;  ;;;    |
352 | 53 | nn0cni 10881 |
. . . . . . . . . . 11
;;   |
353 | 352 | mulid1i 9645 |
. . . . . . . . . 10
;;   ;;   |
354 | 53, 52, 11, 298, 11, 52, 351, 353 | decmul2c 11099 |
. . . . . . . . 9
;;  ;;   ;;;;     |
355 | 344, 354 | eqtr4i 2476 |
. . . . . . . 8
   ;;;    ;;  ;;    |
356 | 9, 10, 50, 51, 53, 49, 318, 323, 355 | mod2xi 15041 |
. . . . . . 7
   ;   ;;;     |
357 | | eqid 2451 |
. . . . . . . 8
; ;  |
358 | | 4p1e5 10736 |
. . . . . . . . 9
   |
359 | 218, 77, 315 | mulcomli 9650 |
. . . . . . . . 9
  ;  |
360 | 11, 16, 358, 359 | decsuc 11074 |
. . . . . . . 8
    ;  |
361 | 175, 77, 108 | mulcomli 9650 |
. . . . . . . 8
  ;  |
362 | 2, 30, 18, 357, 24, 11, 360, 361 | decmul2c 11099 |
. . . . . . 7
 ;  ;;   |
363 | | eqid 2451 |
. . . . . . . . 9
;;  ;;   |
364 | 2, 16 | deccl 11065 |
. . . . . . . . . 10
;  |
365 | | eqid 2451 |
. . . . . . . . . . 11
; ;  |
366 | 2, 16, 358, 365 | decsuc 11074 |
. . . . . . . . . 10
;  ;  |
367 | | eqid 2451 |
. . . . . . . . . . . 12
; ;  |
368 | 2, 21, 100, 367 | decsuc 11074 |
. . . . . . . . . . 11
;  ;  |
369 | 34, 5, 11, 27, 325, 128, 368, 197 | decadd 11092 |
. . . . . . . . . 10
;;  ;  ;;   |
370 | 364, 366,
369 | decsucc 11078 |
. . . . . . . . 9
 ;;  ;   ;;   |
371 | | 9p4e13 11115 |
. . . . . . . . 9
  ;  |
372 | 48, 27, 45, 16, 324, 363, 370, 21, 371 | decaddc 11093 |
. . . . . . . 8
;;;   ;;   ;;;    |
373 | 372, 1 | eqtr4i 2476 |
. . . . . . 7
;;;   ;;    |
374 | | eqid 2451 |
. . . . . . . . 9
; ;  |
375 | | eqid 2451 |
. . . . . . . . . . . 12
; ;  |
376 | 218 | addid2i 9821 |
. . . . . . . . . . . . 13
   |
377 | 376, 206 | eqtri 2473 |
. . . . . . . . . . . 12
  ;  |
378 | 78, 186 | oveq12i 6302 |
. . . . . . . . . . . . 13
         |
379 | 378, 81 | eqtri 2473 |
. . . . . . . . . . . 12
       |
380 | 11, 5, 30, 170, 376 | decaddi 11095 |
. . . . . . . . . . . 12
    ;  |
381 | 11, 3, 5, 30, 375, 377, 2, 30, 11, 379, 380 | decmac 11090 |
. . . . . . . . . . 11
 ;     ;  |
382 | 84, 147 | oveq12i 6302 |
. . . . . . . . . . . . 13
         |
383 | | 5p2e7 10747 |
. . . . . . . . . . . . 13
   |
384 | 382, 383 | eqtri 2473 |
. . . . . . . . . . . 12
       |
385 | 11, 3, 5, 11, 375, 230, 3, 24, 2, 384, 189 | decmac 11090 |
. . . . . . . . . . 11
 ;   ;  |
386 | 2, 3, 5, 11, 74, 299, 39, 24, 30, 381, 385 | decma2c 11091 |
. . . . . . . . . 10
 ; ;     ;;   |
387 | 39 | nn0cni 10881 |
. . . . . . . . . . . . 13
;  |
388 | 387 | mul01i 9823 |
. . . . . . . . . . . 12
;   |
389 | 388 | oveq1i 6300 |
. . . . . . . . . . 11
 ;      |
390 | 389, 171,
207 | 3eqtri 2477 |
. . . . . . . . . 10
 ;   ;  |
391 | 4, 5, 11, 21, 71, 371, 39, 21, 5, 386, 390 | decma2c 11091 |
. . . . . . . . 9
 ; ;;      ;;;    |
392 | 98, 186 | oveq12i 6302 |
. . . . . . . . . . 11
         |
393 | 392, 100 | eqtri 2473 |
. . . . . . . . . 10
       |
394 | 11, 3, 5, 11, 375, 230, 21, 24, 11, 393, 210 | decmac 11090 |
. . . . . . . . 9
 ;   ;  |
395 | 6, 21, 27, 11, 1, 374, 39, 24, 16, 391, 394 | decma2c 11091 |
. . . . . . . 8
 ;  ;  ;;;;     |
396 | 45, 16 | deccl 11065 |
. . . . . . . . 9
;;   |
397 | | eqid 2451 |
. . . . . . . . . 10
; ;  |
398 | 11, 30 | deccl 11065 |
. . . . . . . . . . 11
;  |
399 | 398, 3 | deccl 11065 |
. . . . . . . . . 10
;;   |
400 | | eqid 2451 |
. . . . . . . . . . . 12
;;  ;;   |
401 | 398 | nn0cni 10881 |
. . . . . . . . . . . . . 14
;  |
402 | 401 | addid2i 9821 |
. . . . . . . . . . . . 13
 ;  ;  |
403 | 11, 30, 164, 402 | decsuc 11074 |
. . . . . . . . . . . 12
  ;   ;  |
404 | | 7p5e12 11104 |
. . . . . . . . . . . 12
  ;  |
405 | 5, 30, 398, 3, 206, 400, 403, 2, 404 | decaddc 11093 |
. . . . . . . . . . 11
 ;;   ;;   |
406 | 245, 143 | oveq12i 6302 |
. . . . . . . . . . . . 13
         |
407 | 406, 250 | eqtri 2473 |
. . . . . . . . . . . 12
       |
408 | 132 | mulid1i 9645 |
. . . . . . . . . . . . . 14
   |
409 | 408 | oveq1i 6300 |
. . . . . . . . . . . . 13
       |
410 | | 9p8e17 11119 |
. . . . . . . . . . . . 13
  ;  |
411 | 409, 410 | eqtri 2473 |
. . . . . . . . . . . 12
    ;  |
412 | 11, 27, 11, 18, 128, 243, 11, 30, 11, 407, 411 | decmac 11090 |
. . . . . . . . . . 11
 ;  ;   ;  |
413 | 183 | mulid1i 9645 |
. . . . . . . . . . . . 13
   |
414 | 413 | oveq1i 6300 |
. . . . . . . . . . . 12
       |
415 | | 4p2e6 10744 |
. . . . . . . . . . . 12
   |
416 | 414, 415,
87 | 3eqtri 2477 |
. . . . . . . . . . 11
    ;  |
417 | 45, 16, 63, 2, 363, 405, 11, 24, 5, 412, 416 | decmac 11090 |
. . . . . . . . . 10
 ;;    ;;    ;;   |
418 | 132 | mulid2i 9646 |
. . . . . . . . . . . . . 14
   |
419 | 175 | addid2i 9821 |
. . . . . . . . . . . . . 14
   |
420 | 418, 419 | oveq12i 6302 |
. . . . . . . . . . . . 13
         |
421 | 420, 410 | eqtri 2473 |
. . . . . . . . . . . 12
      ;  |
422 | | 9t9e81 11153 |
. . . . . . . . . . . . 13
  ;  |
423 | 183, 90, 358 | addcomli 9825 |
. . . . . . . . . . . . 13
   |
424 | 18, 11, 16, 422, 423 | decaddi 11095 |
. . . . . . . . . . . 12
    ;  |
425 | 11, 27, 5, 16, 128, 185, 27, 3, 18, 421, 424 | decmac 11090 |
. . . . . . . . . . 11
 ;     ;;   |
426 | | 9t4e36 11148 |
. . . . . . . . . . . . 13
  ;  |
427 | 132, 183,
426 | mulcomli 9650 |
. . . . . . . . . . . 12
  ;  |
428 | | 7p6e13 11105 |
. . . . . . . . . . . . 13
  ;  |
429 | 218, 93, 428 | addcomli 9825 |
. . . . . . . . . . . 12
  ;  |
430 | 21, 24, 30, 427, 100, 21, 429 | decaddci 11096 |
. . . . . . . . . . 11
    ;  |
431 | 45, 16, 5, 30, 363, 206, 27, 21, 16, 425, 430 | decmac 11090 |
. . . . . . . . . 10
 ;;    ;;;    |
432 | 11, 27, 30, 30, 128, 397, 396, 21, 399, 417, 431 | decma2c 11091 |
. . . . . . . . 9
 ;;  ;  ;  ;;;    |
433 | 183 | mulid2i 9646 |
. . . . . . . . . . . . 13
   |
434 | 433, 171 | oveq12i 6302 |
. . . . . . . . . . . 12
         |
435 | | 4p3e7 10745 |
. . . . . . . . . . . 12
   |
436 | 434, 435 | eqtri 2473 |
. . . . . . . . . . 11
       |
437 | 21, 24, 156, 426 | decsuc 11074 |
. . . . . . . . . . 11
    ;  |
438 | 11, 27, 5, 11, 128, 230, 16, 30, 21, 436, 437 | decmac 11090 |
. . . . . . . . . 10
 ;   ;  |
439 | | 4t4e16 11124 |
. . . . . . . . . 10
  ;  |
440 | 16, 45, 16, 363, 24, 11, 438, 439 | decmul1c 11098 |
. . . . . . . . 9
;;   ;;   |
441 | 396, 45, 16, 363, 24, 37, 432, 440 | decmul2c 11099 |
. . . . . . . 8
;;  ;;   ;;;;     |
442 | 395, 441 | eqtr4i 2476 |
. . . . . . 7
 ;  ;  ;;  ;;    |
443 | 10, 43, 44, 47, 42, 49, 356, 362, 373, 442 | mod2xnegi 15043 |
. . . . . 6
   ;;    ;
  |
444 | | eqid 2451 |
. . . . . . 7
;;  ;;   |
445 | 129, 186 | oveq12i 6302 |
. . . . . . . . 9
         |
446 | 445, 81 | eqtri 2473 |
. . . . . . . 8
       |
447 | 83, 77, 168 | mulcomli 9650 |
. . . . . . . . . 10
   |
448 | 447, 169 | eqtri 2473 |
. . . . . . . . 9
  ;  |
449 | 11, 5, 186, 448 | decsuc 11074 |
. . . . . . . 8
    ;  |
450 | 11, 3, 5, 11, 375, 230, 2, 11, 11, 446, 449 | decma2c 11091 |
. . . . . . 7
  ;   ;  |
451 | | 6t2e12 11128 |
. . . . . . . 8
  ;  |
452 | 93, 77, 451 | mulcomli 9650 |
. . . . . . 7
  ;  |
453 | 2, 39, 24, 444, 2, 11, 450, 452 | decmul2c 11099 |
. . . . . 6
 ;;   ;;   |
454 | | eqid 2451 |
. . . . . . . 8
;;  ;;   |
455 | 30, 30, 164, 397 | decsuc 11074 |
. . . . . . . . 9
;  ;  |
456 | 218 | addid1i 9820 |
. . . . . . . . . . 11
   |
457 | 456, 206 | eqtri 2473 |
. . . . . . . . . 10
  ;  |
458 | 115, 147 | oveq12i 6302 |
. . . . . . . . . . 11
         |
459 | | 6p2e8 10751 |
. . . . . . . . . . 11
   |
460 | 458, 459 | eqtri 2473 |
. . . . . . . . . 10
       |
461 | 218, 83, 404 | addcomli 9825 |
. . . . . . . . . . 11
  ;  |
462 | 11, 3, 30, 192, 143, 2, 461 | decaddci 11096 |
. . . . . . . . . 10
    ;  |
463 | 2, 3, 5, 30, 74, 457, 21, 2, 2, 460, 462 | decma2c 11091 |
. . . . . . . . 9
  ;     ;  |
464 | 97 | mul01i 9823 |
. . . . . . . . . . 11
   |
465 | 464 | oveq1i 6300 |
. . . . . . . . . 10
       |
466 | 465, 419,
261 | 3eqtri 2477 |
. . . . . . . . 9
    ;  |
467 | 4, 5, 30, 18, 71, 455, 21, 18, 5, 463, 466 | decma2c 11091 |
. . . . . . . 8
  ;;   ;   ;;   |
468 | 212 | oveq1i 6300 |
. . . . . . . . 9
       |
469 | 468, 160 | eqtri 2473 |
. . . . . . . 8
    ;  |
470 | 6, 21, 37, 2, 1, 454, 21, 11, 11, 467, 469 | decma2c 11091 |
. . . . . . 7
   ;;   ;;;    |
471 | 186 | oveq2i 6301 |
. . . . . . . . . 10
           |
472 | 18, 11, 143, 422 | decsuc 11074 |
. . . . . . . . . 10
    ;  |
473 | 471, 472 | eqtri 2473 |
. . . . . . . . 9
      ;  |
474 | 418 | oveq1i 6300 |
. . . . . . . . . 10
       |
475 | | 9p9e18 11120 |
. . . . . . . . . 10
  ;  |
476 | 474, 475 | eqtri 2473 |
. . . . . . . . 9
    ;  |
477 | 27, 11, 5, 27, 374, 182, 27, 18, 11, 473, 476 | decmac 11090 |
. . . . . . . 8
 ;   ;;   |
478 | 42 | nn0cni 10881 |
. . . . . . . . 9
;  |
479 | 478 | mulid1i 9645 |
. . . . . . . 8
;  ;  |
480 | 42, 27, 11, 374, 11, 27, 477, 479 | decmul2c 11099 |
. . . . . . 7
; ;  ;;;    |
481 | 470, 480 | eqtr4i 2476 |
. . . . . 6
   ;;   ; ;   |
482 | 9, 10, 40, 41, 42, 38, 443, 453, 481 | mod2xi 15041 |
. . . . 5
   ;;    ;;    |
483 | | eqid 2451 |
. . . . . 6
;;  ;;   |
484 | | eqid 2451 |
. . . . . . . . 9
; ;  |
485 | 320 | oveq1i 6300 |
. . . . . . . . . 10
       |
486 | 485, 268 | eqtri 2473 |
. . . . . . . . 9
     |
487 | 129, 154 | eqtri 2473 |
. . . . . . . . 9
  ;  |
488 | 2, 21, 11, 484, 2, 5, 486, 487 | decmul2c 11099 |
. . . . . . . 8
 ;  ;  |
489 | 488 | oveq1i 6300 |
. . . . . . 7
  ;   ;   |
490 | 25 | nn0cni 10881 |
. . . . . . . 8
;  |
491 | 490 | addid1i 9820 |
. . . . . . 7
;  ;  |
492 | 489, 491 | eqtri 2473 |
. . . . . 6
  ;   ;  |
493 | 2, 22, 2, 483, 16, 5, 492, 124 | decmul2c 11099 |
. . . . 5
 ;;   ;;   |
494 | | eqid 2451 |
. . . . . . 7
;;  ;;   |
495 | 30, 11 | deccl 11065 |
. . . . . . 7
;  |
496 | | eqid 2451 |
. . . . . . . . 9
; ;  |
497 | | 7p2e9 10754 |
. . . . . . . . . 10
   |
498 | 218, 77, 497 | addcomli 9825 |
. . . . . . . . 9
   |
499 | 2, 30, 30, 11, 165, 496, 498, 164 | decadd 11092 |
. . . . . . . 8
; ;  ;  |
500 | 132 | addid1i 9820 |
. . . . . . . . . 10
   |
501 | 500, 182 | eqtri 2473 |
. . . . . . . . 9
  ;  |
502 | 52, 27 | deccl 11065 |
. . . . . . . . 9
;;   |
503 | | eqid 2451 |
. . . . . . . . . 10
;;  ;;   |
504 | 502 | nn0cni 10881 |
. . . . . . . . . . 11
;;   |
505 | 504 | addid2i 9821 |
. . . . . . . . . 10
 ;;   ;;   |
506 | 11, 11, 2, 228, 250 | decaddi 11095 |
. . . . . . . . . . 11
;  ;  |
507 | 123, 79 | oveq12i 6302 |
. . . . . . . . . . . 12
         |
508 | 507, 358 | eqtri 2473 |
. . . . . . . . . . 11
       |
509 | 115 | oveq1i 6300 |
. . . . . . . . . . . 12
       |
510 | 509, 144,
182 | 3eqtri 2477 |
. . . . . . . . . . 11
    ;  |
511 | 2, 21, 11, 21, 367, 506, 2, 27, 5, 508, 510 | decmac 11090 |
. . . . . . . . . 10
 ;  ;   ;  |
512 | | 9p6e15 11117 |
. . . . . . . . . . . 12
  ;  |
513 | 132, 93, 512 | addcomli 9825 |
. . . . . . . . . . 11
  ;  |
514 | 11, 24, 27, 108, 143, 3, 513 | decaddci 11096 |
. . . . . . . . . 10
    ;  |
515 | 34, 18, 52, 27, 503, 505, 2, 3, 2, 511, 514 | decmac 11090 |
. . . . . . . . 9
 ;;    ;;    ;;   |
516 | 186 | oveq2i 6301 |
. . . . . . . . . . . 12
           |
517 | 516, 449 | eqtri 2473 |
. . . . . . . . . . 11
      ;  |
518 | 2, 21, 5, 16, 367, 185, 3, 27, 11, 517, 194 | decmac 11090 |
. . . . . . . . . 10
 ;     ;;   |
519 | 34, 18, 5, 27, 503, 182, 3, 27, 16, 518, 198 | decmac 11090 |
. . . . . . . . 9
 ;;    ;;;    |
520 | 2, 3, 5, 27, 74, 501, 35, 27, 502, 515, 519 | decma2c 11091 |
. . . . . . . 8
 ;;  ;     ;;;    |
521 | 35 | nn0cni 10881 |
. . . . . . . . . . 11
;;   |
522 | 521 | mul01i 9823 |
. . . . . . . . . 10
;;    |
523 | 522 | oveq1i 6300 |
. . . . . . . . 9
 ;;       |
524 | 523, 419,
261 | 3eqtri 2477 |
. . . . . . . 8
 ;;    ;  |
525 | 4, 5, 27, 18, 71, 499, 35, 18, 5, 520, 524 | decma2c 11091 |
. . . . . . 7
 ;;  ;;   ; ;   ;;;;     |
526 | 320, 186 | oveq12i 6302 |
. . . . . . . . . . . 12
         |
527 | 526, 156 | eqtri 2473 |
. . . . . . . . . . 11
       |
528 | 2, 21, 5, 2, 367, 154, 21, 11, 11, 527, 469 | decmac 11090 |
. . . . . . . . . 10
 ;   ;  |
529 | 21, 34, 18, 503, 16, 2, 528, 217 | decmul1c 11098 |
. . . . . . . . 9
;;   ;;   |
530 | 529 | oveq1i 6300 |
. . . . . . . 8
 ;;    ;;    |
531 | 495, 16 | deccl 11065 |
. . . . . . . . . 10
;;   |
532 | 531 | nn0cni 10881 |
. . . . . . . . 9
;;   |
533 | 532 | addid1i 9820 |
. . . . . . . 8
;;   ;;   |
534 | 530, 533 | eqtri 2473 |
. . . . . . 7
 ;;    ;;   |
535 | 6, 21, 31, 5, 1, 494, 35, 16, 495, 525, 534 | decma2c 11091 |
. . . . . 6
 ;;   ;;   ;;;;;      |
536 | 39, 16 | deccl 11065 |
. . . . . . 7
;;   |
537 | | eqid 2451 |
. . . . . . . 8
;;  ;;   |
538 | 3, 16 | deccl 11065 |
. . . . . . . . 9
;  |
539 | 538, 5 | deccl 11065 |
. . . . . . . 8
;;   |
540 | 3, 3 | deccl 11065 |
. . . . . . . . 9
;  |
541 | | eqid 2451 |
. . . . . . . . . 10
;;  ;;   |
542 | | eqid 2451 |
. . . . . . . . . . 11
; ;  |
543 | 83 | addid2i 9821 |
. . . . . . . . . . 11
   |
544 | 5, 11, 3, 16, 230, 542, 543, 423 | decadd 11092 |
. . . . . . . . . 10
 ;  ;  |
545 | 83 | addid1i 9820 |
. . . . . . . . . 10
   |
546 | 11, 3, 538, 5, 375, 541, 544, 545 | decadd 11092 |
. . . . . . . . 9
; ;;   ;;   |
547 | | eqid 2451 |
. . . . . . . . . . 11
; ;  |
548 | 3, 3, 86, 547 | decsuc 11074 |
. . . . . . . . . 10
;  ;  |
549 | | 7t7e49 11138 |
. . . . . . . . . . 11
  ;  |
550 | | 5p5e10 10750 |
. . . . . . . . . . . 12
   |
551 | 550, 169 | eqtri 2473 |
. . . . . . . . . . 11
  ;  |
552 | 16, 27, 11, 5, 549, 551, 358, 500 | decadd 11092 |
. . . . . . . . . 10
      ;  |
553 | 16, 27, 24, 549, 358, 3, 512 | decaddci 11096 |
. . . . . . . . . 10
    ;  |
554 | 30, 30, 3, 24, 397, 548, 30, 3, 3, 552, 553 | decmac 11090 |
. . . . . . . . 9
 ;  ;   ;;   |
555 | 83, 183, 193 | addcomli 9825 |
. . . . . . . . . 10
   |
556 | 11, 16, 3, 359, 555 | decaddi 11095 |
. . . . . . . . 9
    ;  |
557 | 37, 2, 540, 3, 454, 546, 30, 27, 11, 554, 556 | decmac 11090 |
. . . . . . . 8
 ;;   ; ;;    ;;;    |
558 | 543 | oveq2i 6301 |
. . . . . . . . . . 11
           |
559 | | 9p5e14 11116 |
. . . . . . . . . . . 12
  ;  |
560 | 16, 27, 3, 549, 358, 16, 559 | decaddci 11096 |
. . . . . . . . . . 11
    ;  |
561 | 558, 560 | eqtri 2473 |
. . . . . . . . . 10
      ;  |
562 | 16, 358, 549 | decsucc 11078 |
. . . . . . . . . 10
    ;  |
563 | 30, 30, 5, 11, 397, 276, 30, 5, 3, 561, 562 | decmac 11090 |
. . . . . . . . 9
 ;     ;;   |
564 | | 4p4e8 10746 |
. . . . . . . . . 10
   |
565 | 11, 16, 16, 359, 564 | decaddi 11095 |
. . . . . . . . 9
    ;  |
566 | 37, 2, 5, 16, 454, 101, 30, 18, 11, 563, 565 | decmac 11090 |
. . . . . . . 8
 ;;    ;;;    |
567 | 30, 30, 39, 16, 397, 537, 38, 18, 539, 557, 566 | decma2c 11091 |
. . . . . . 7
 ;;  ;  ;;   ;;;;     |
568 | 11, 16, 358, 315 | decsuc 11074 |
. . . . . . . . . . 11
    ;  |
569 | 2, 30, 30, 397, 16, 11, 568, 315 | decmul1c 11098 |
. . . . . . . . . 10
;  ;;   |
570 | 569 | oveq1i 6300 |
. . . . . . . . 9
 ;   ;;    |
571 | 536 | nn0cni 10881 |
. . . . . . . . . 10
;;   |
572 | 571 | addid1i 9820 |
. . . . . . . . 9
;;   ;;   |
573 | 570, 572 | eqtri 2473 |
. . . . . . . 8
 ;   ;;   |
574 | 2, 37, 2, 454, 16, 5, 573, 124 | decmul1c 11098 |
. . . . . . 7
;;   ;;;    |
575 | 38, 37, 2, 454, 16, 536, 567, 574 | decmul2c 11099 |
. . . . . 6
;;  ;;   ;;;;;      |
576 | 535, 575 | eqtr4i 2476 |
. . . . 5
 ;;   ;;   ;;  ;;    |
577 | 9, 10, 33, 36, 38, 32, 482, 493, 576 | mod2xi 15041 |
. . . 4
   ;;    ;;    |
578 | | eqid 2451 |
. . . . 5
;;  ;;   |
579 | | eqid 2451 |
. . . . . . . 8
; ;  |
580 | 452 | oveq1i 6300 |
. . . . . . . . 9
    ;   |
581 | 12 | nn0cni 10881 |
. . . . . . . . . 10
;  |
582 | 581 | addid1i 9820 |
. . . . . . . . 9
;  ;  |
583 | 580, 582 | eqtri 2473 |
. . . . . . . 8
    ;  |
584 | 2, 24, 2, 579, 16, 5, 583, 124 | decmul2c 11099 |
. . . . . . 7
 ;  ;;   |
585 | 584 | oveq1i 6300 |
. . . . . 6
  ;   ;;    |
586 | 17 | nn0cni 10881 |
. . . . . . 7
;;   |
587 | 586 | addid1i 9820 |
. . . . . 6
;;   ;;   |
588 | 585, 587 | eqtri 2473 |
. . . . 5
  ;   ;;   |
589 | 183, 77, 329 | mulcomli 9650 |
. . . . . 6
   |
590 | 589, 261 | eqtri 2473 |
. . . . 5
  ;  |
591 | 2, 25, 16, 578, 18, 5, 588, 590 | decmul2c 11099 |
. . . 4
 ;;   ;;;    |
592 | | eqid 2451 |
. . . . . 6
;;  ;;   |
593 | 21, 11, 27, 484, 100, 235 | decaddci2 11097 |
. . . . . . 7
;  ;  |
594 | 183 | addid1i 9820 |
. . . . . . . . 9
   |
595 | 594, 101 | eqtri 2473 |
. . . . . . . 8
  ;  |
596 | 11, 16 | deccl 11065 |
. . . . . . . 8
;  |
597 | | eqid 2451 |
. . . . . . . . 9
; ;  |
598 | 596 | nn0cni 10881 |
. . . . . . . . . 10
;  |
599 | 598 | addid2i 9821 |
. . . . . . . . 9
 ;  ;  |
600 | 123, 250 | oveq12i 6302 |
. . . . . . . . . 10
         |
601 | 600, 435 | eqtri 2473 |
. . . . . . . . 9
       |
602 | 11, 18, 16, 133, 143, 2, 332 | decaddci 11096 |
. . . . . . . . 9
    ;  |
603 | 2, 27, 11, 16, 597, 599, 2, 2, 2, 601, 602 | decmac 11090 |
. . . . . . . 8
 ;   ;   ;  |
604 | 184 | oveq2i 6301 |
. . . . . . . . . 10
           |
605 | 11, 5, 16, 448, 184 | decaddi 11095 |
. . . . . . . . . 10
    ;  |
606 | 604, 605 | eqtri 2473 |
. . . . . . . . 9
      ;  |
607 | | 9t5e45 11149 |
. . . . . . . . . 10
  ;  |
608 | 16, 3, 16, 607, 193 | decaddi 11095 |
. . . . . . . . 9
    ;  |
609 | 2, 27, 5, 16, 597, 101, 3, 27, 16, 606, 608 | decmac 11090 |
. . . . . . . 8
 ;   ;;   |
610 | 2, 3, 5, 16, 74, 595, 28, 27, 596, 603, 609 | decma2c 11091 |
. . . . . . 7
 ; ;     ;;   |
611 | 149 | mul01i 9823 |
. . . . . . . . 9
;   |
612 | 611 | oveq1i 6300 |
. . . . . . . 8
 ;      |
613 | 612, 246,
262 | 3eqtri 2477 |
. . . . . . 7
 ;   ;  |
614 | 4, 5, 16, 5, 71, 593, 28, 5, 5, 610, 613 | decma2c 11091 |
. . . . . 6
 ; ;;   ;   ;;;    |
615 | 320, 171 | oveq12i 6302 |
. . . . . . . 8
         |
616 | 615, 144 | eqtri 2473 |
. . . . . . 7
       |
617 | | 9t3e27 11147 |
. . . . . . . 8
  ;  |
618 | | 7p3e10 10755 |
. . . . . . . 8
   |
619 | 2, 30, 21, 617, 81, 618 | decaddci2 11097 |
. . . . . . 7
    ;  |
620 | 2, 27, 5, 21, 597, 207, 21, 5, 21, 616, 619 | decmac 11090 |
. . . . . 6
 ;   ;  |
621 | 6, 21, 22, 21, 1, 592, 28, 5, 27, 614, 620 | decma2c 11091 |
. . . . 5
 ;  ;;   ;;;;     |
622 | 63, 27 | deccl 11065 |
. . . . . . . . 9
;;   |
623 | | eqid 2451 |
. . . . . . . . . 10
;;  ;;   |
624 | 175, 183,
332 | addcomli 9825 |
. . . . . . . . . . . 12
  ;  |
625 | 11, 16, 18, 315, 143, 2, 624 | decaddci 11096 |
. . . . . . . . . . 11
    ;  |
626 | 2, 30, 11, 18, 165, 243, 2, 2, 2, 601, 625 | decmac 11090 |
. . . . . . . . . 10
 ;  ;   ;  |
627 | 311 | oveq1i 6300 |
. . . . . . . . . . 11
       |
628 | 627, 197,
182 | 3eqtri 2477 |
. . . . . . . . . 10
    ;  |
629 | 31, 5, 63, 27, 494, 623, 2, 27, 5, 626, 628 | decmac 11090 |
. . . . . . . . 9
 ;;   ;;   ;;   |
630 | 30, 2, 30, 165, 27, 16, 565, 549 | decmul1c 11098 |
. . . . . . . . . . . 12
;  ;;   |
631 | 630 | oveq1i 6300 |
. . . . . . . . . . 11
 ;   ;;    |
632 | 622 | nn0cni 10881 |
. . . . . . . . . . . 12
;;   |
633 | 632 | addid1i 9820 |
. . . . . . . . . . 11
;;   ;;   |
634 | 631, 633 | eqtri 2473 |
. . . . . . . . . 10
 ;   ;;   |
635 | 218 | mul02i 9822 |
. . . . . . . . . . 11
   |
636 | 635, 262 | eqtri 2473 |
. . . . . . . . . 10
  ;  |
637 | 30, 31, 5, 494, 5, 5, 634, 636 | decmul1c 11098 |
. . . . . . . . 9
;;   ;;;    |
638 | 32, 2, 30, 165, 5, 622, 629, 637 | decmul2c 11099 |
. . . . . . . 8
;;  ;  ;;;    |
639 | 638 | oveq1i 6300 |
. . . . . . 7
 ;;  ;   ;;;     |
640 | 30, 2 | deccl 11065 |
. . . . . . . . . . 11
;  |
641 | 640, 27 | deccl 11065 |
. . . . . . . . . 10
;;   |
642 | 641, 5 | deccl 11065 |
. . . . . . . . 9
;;;    |
643 | 642 | nn0cni 10881 |
. . . . . . . 8
;;;    |
644 | 643 | addid1i 9820 |
. . . . . . 7
;;;    ;;;    |
645 | 639, 644 | eqtri 2473 |
. . . . . 6
 ;;  ;   ;;;    |
646 | 32 | nn0cni 10881 |
. . . . . . . 8
;;   |
647 | 646 | mul01i 9823 |
. . . . . . 7
;;    |
648 | 647, 262 | eqtri 2473 |
. . . . . 6
;;   ;  |
649 | 32, 31, 5, 494, 5, 5, 645, 648 | decmul2c 11099 |
. . . . 5
;;  ;;   ;;;;     |
650 | 621, 649 | eqtr4i 2476 |
. . . 4
 ;  ;;   ;;  ;;    |
651 | 9, 10, 26, 29, 32, 23, 577, 591, 650 | mod2xi 15041 |
. . 3
   ;;;     ;;    |
652 | | cu2 12373 |
. . . 4
     |
653 | 652 | oveq1i 6300 |
. . 3
         |
654 | | eqid 2451 |
. . . 4
;;;   ;;;    |
655 | | eqid 2451 |
. . . . 5
;;  ;;   |
656 | 12, 16, 358, 655 | decsuc 11074 |
. . . 4
;;   ;;   |
657 | | 8p3e11 11107 |
. . . 4
  ;  |
658 | 17, 18, 21, 654, 656, 11, 657 | decaddci 11096 |
. . 3
;;;    ;;;    |
659 | 9 | nncni 10619 |
. . . . . . 7
 |
660 | 659 | mulid2i 9646 |
. . . . . 6
   |
661 | 660, 1 | eqtri 2473 |
. . . . 5
  ;;;    |
662 | 6, 21, 100, 661 | decsuc 11074 |
. . . 4
    ;;;    |
663 | 186 | oveq2i 6301 |
. . . . . . 7
           |
664 | 175, 97, 217 | mulcomli 9650 |
. . . . . . . 8
  ;  |
665 | 2, 16, 358, 664 | decsuc 11074 |
. . . . . . 7
    ;  |
666 | 663, 665 | eqtri 2473 |
. . . . . 6
      ;  |
667 | 175 | mulid2i 9646 |
. . . . . . . 8
   |
668 | 667 | oveq1i 6300 |
. . . . . . 7
       |
669 | | 8p2e10 10756 |
. . . . . . 7
   |
670 | 668, 669,
169 | 3eqtri 2477 |
. . . . . 6
    ;  |
671 | 21, 11, 5, 2, 484, 154, 18, 5, 11, 666, 670 | decmac 11090 |
. . . . 5
 ;   ;;   |
672 | 18, 22, 21, 592, 16, 2, 671, 664 | decmul1c 11098 |
. . . 4
;;   ;;;    |
673 | 662, 672 | eqtr4i 2476 |
. . 3
    ;;    |
674 | 9, 10, 19, 20, 23, 11, 21, 18, 651, 653, 658, 673 | modxai 15040 |
. 2
   ;;;        |
675 | | eqid 2451 |
. . . 4
;;;   ;;;    |
676 | | eqid 2451 |
. . . . . 6
;;  ;;   |
677 | | eqid 2451 |
. . . . . . 7
; ;  |
678 | 129, 246 | oveq12i 6302 |
. . . . . . . 8
         |
679 | 678, 301 | eqtri 2473 |
. . . . . . 7
       |
680 | 123 | oveq1i 6300 |
. . . . . . . 8
       |
681 | 3 | dec0h 11067 |
. . . . . . . 8
;  |
682 | 680, 358,
681 | 3eqtri 2477 |
. . . . . . 7
    ;  |
683 | 11, 2, 5, 11, 677, 230, 2, 3, 5, 679, 682 | decma2c 11091 |
. . . . . 6
  ;   ;  |
684 | 2, 12, 3, 676, 5, 11, 683, 448 | decmul2c 11099 |
. . . . 5
 ;;   ;;   |
685 | 4, 5, 5, 684, 246 | decaddi 11095 |
. . . 4
  ;;    ;;   |
686 | 2, 13, 11, 675, 2, 5, 685, 487 | decmul2c 11099 |
. . 3
 ;;;    ;;;    |
687 | | eqid 2451 |
. . . . . . 7
;;;   ;;;    |
688 | 6, 2, 81, 687 | decsuc 11074 |
. . . . . 6
;;;    ;;;    |
689 | 1, 688 | eqtr4i 2476 |
. . . . 5
;;;     |
690 | 689 | oveq1i 6300 |
. . . 4
   ;;;      |
691 | 6, 2 | deccl 11065 |
. . . . . 6
;;;    |
692 | 691 | nn0cni 10881 |
. . . . 5
;;;    |
693 | 692, 90 | pncan3oi 9891 |
. . . 4
 ;;;     ;;;    |
694 | 690, 693 | eqtri 2473 |
. . 3
  ;;;    |
695 | 686, 694 | eqtr4i 2476 |
. 2
 ;;;       |
696 | 659 | mul02i 9822 |
. . . 4
   |
697 | 696 | oveq1i 6300 |
. . 3
       |
698 | 245, 186 | eqtr4i 2476 |
. . 3
     |
699 | 697, 698 | eqtr4i 2476 |
. 2
       |
700 | 9, 10, 14, 15, 11, 11, 674, 695, 699 | mod2xi 15041 |
1
           |