Proof of Theorem log2ub
Step | Hyp | Ref
| Expression |
1 | | 4m1e3 11138 |
. . . . . . . . 9
|
2 | 1 | oveq2i 6661 |
. . . . . . . 8
|
3 | 2 | sumeq1i 14428 |
. . . . . . 7
|
4 | 3 | oveq2i 6661 |
. . . . . 6
|
5 | | 4nn0 11311 |
. . . . . . 7
|
6 | | log2tlbnd 24672 |
. . . . . . 7
|
7 | 5, 6 | ax-mp 5 |
. . . . . 6
|
8 | 4, 7 | eqeltrri 2698 |
. . . . 5
|
9 | | 0re 10040 |
. . . . . 6
|
10 | | 3re 11094 |
. . . . . . 7
|
11 | | 4nn 11187 |
. . . . . . . . 9
|
12 | | 2nn0 11309 |
. . . . . . . . . 10
|
13 | | 1nn 11031 |
. . . . . . . . . 10
|
14 | 12, 5, 13 | numnncl 11507 |
. . . . . . . . 9
|
15 | 11, 14 | nnmulcli 11044 |
. . . . . . . 8
|
16 | | 9nn 11192 |
. . . . . . . . 9
|
17 | | nnexpcl 12873 |
. . . . . . . . 9
|
18 | 16, 5, 17 | mp2an 708 |
. . . . . . . 8
|
19 | 15, 18 | nnmulcli 11044 |
. . . . . . 7
|
20 | | nndivre 11056 |
. . . . . . 7
|
21 | 10, 19, 20 | mp2an 708 |
. . . . . 6
|
22 | 9, 21 | elicc2i 12239 |
. . . . 5
|
23 | 8, 22 | mpbi 220 |
. . . 4
|
24 | 23 | simp3i 1072 |
. . 3
|
25 | | 2rp 11837 |
. . . . 5
|
26 | | relogcl 24322 |
. . . . 5
|
27 | 25, 26 | ax-mp 5 |
. . . 4
|
28 | | fzfid 12772 |
. . . . . 6
|
29 | | 2re 11090 |
. . . . . . 7
|
30 | | 3nn 11186 |
. . . . . . . . 9
|
31 | | elfznn0 12433 |
. . . . . . . . . . . 12
|
32 | 31 | adantl 482 |
. . . . . . . . . . 11
|
33 | | nn0mulcl 11329 |
. . . . . . . . . . 11
|
34 | 12, 32, 33 | sylancr 695 |
. . . . . . . . . 10
|
35 | | nn0p1nn 11332 |
. . . . . . . . . 10
|
36 | 34, 35 | syl 17 |
. . . . . . . . 9
|
37 | | nnmulcl 11043 |
. . . . . . . . 9
|
38 | 30, 36, 37 | sylancr 695 |
. . . . . . . 8
|
39 | | nnexpcl 12873 |
. . . . . . . . 9
|
40 | 16, 32, 39 | sylancr 695 |
. . . . . . . 8
|
41 | 38, 40 | nnmulcld 11068 |
. . . . . . 7
|
42 | | nndivre 11056 |
. . . . . . 7
|
43 | 29, 41, 42 | sylancr 695 |
. . . . . 6
|
44 | 28, 43 | fsumrecl 14465 |
. . . . 5
|
45 | 44 | trud 1493 |
. . . 4
|
46 | 27, 45, 21 | lesubadd2i 10588 |
. . 3
|
47 | 24, 46 | mpbi 220 |
. 2
|
48 | | log2ublem3 24675 |
. . . . 5
;;;; |
49 | | 3nn0 11310 |
. . . . 5
|
50 | | 5nn0 11312 |
. . . . . . . . 9
|
51 | 50, 49 | deccl 11512 |
. . . . . . . 8
; |
52 | | 0nn0 11307 |
. . . . . . . 8
|
53 | 51, 52 | deccl 11512 |
. . . . . . 7
;; |
54 | 53, 50 | deccl 11512 |
. . . . . 6
;;; |
55 | | 6nn0 11313 |
. . . . . 6
|
56 | 54, 55 | deccl 11512 |
. . . . 5
;;;; |
57 | | 1nn0 11308 |
. . . . 5
|
58 | | eqid 2622 |
. . . . 5
|
59 | | 6p1e7 11156 |
. . . . . 6
|
60 | | eqid 2622 |
. . . . . 6
;;;; ;;;; |
61 | 54, 55, 59, 60 | decsuc 11535 |
. . . . 5
;;;; ;;;; |
62 | | 5nn 11188 |
. . . . . . . . . 10
|
63 | | 7nn 11190 |
. . . . . . . . . 10
|
64 | 62, 63 | nnmulcli 11044 |
. . . . . . . . 9
|
65 | 64 | nnrei 11029 |
. . . . . . . 8
|
66 | 15 | nnrei 11029 |
. . . . . . . 8
|
67 | | 6nn 11189 |
. . . . . . . . . 10
|
68 | | 5lt6 11204 |
. . . . . . . . . 10
|
69 | 49, 50, 67, 68 | declt 11530 |
. . . . . . . . 9
; ; |
70 | | 7cn 11104 |
. . . . . . . . . 10
|
71 | | 5cn 11100 |
. . . . . . . . . 10
|
72 | | 7t5e35 11651 |
. . . . . . . . . 10
; |
73 | 70, 71, 72 | mulcomli 10047 |
. . . . . . . . 9
; |
74 | | 4cn 11098 |
. . . . . . . . . . . . . 14
|
75 | | 2cn 11091 |
. . . . . . . . . . . . . 14
|
76 | | 4t2e8 11181 |
. . . . . . . . . . . . . 14
|
77 | 74, 75, 76 | mulcomli 10047 |
. . . . . . . . . . . . 13
|
78 | 77 | oveq1i 6660 |
. . . . . . . . . . . 12
|
79 | | 8p1e9 11158 |
. . . . . . . . . . . 12
|
80 | 78, 79 | eqtri 2644 |
. . . . . . . . . . 11
|
81 | 80 | oveq2i 6661 |
. . . . . . . . . 10
|
82 | | 9cn 11108 |
. . . . . . . . . . 11
|
83 | | 9t4e36 11665 |
. . . . . . . . . . 11
; |
84 | 82, 74, 83 | mulcomli 10047 |
. . . . . . . . . 10
; |
85 | 81, 84 | eqtri 2644 |
. . . . . . . . 9
; |
86 | 69, 73, 85 | 3brtr4i 4683 |
. . . . . . . 8
|
87 | 65, 66, 86 | ltleii 10160 |
. . . . . . 7
|
88 | 18 | nngt0i 11054 |
. . . . . . . 8
|
89 | 18 | nnrei 11029 |
. . . . . . . . 9
|
90 | 65, 66, 89 | lemul2i 10947 |
. . . . . . . 8
|
91 | 88, 90 | ax-mp 5 |
. . . . . . 7
|
92 | 87, 91 | mpbi 220 |
. . . . . 6
|
93 | | 7nn0 11314 |
. . . . . . . . . 10
|
94 | | nnexpcl 12873 |
. . . . . . . . . 10
|
95 | 30, 93, 94 | mp2an 708 |
. . . . . . . . 9
|
96 | 95 | nncni 11030 |
. . . . . . . 8
|
97 | 64 | nncni 11030 |
. . . . . . . 8
|
98 | | 3cn 11095 |
. . . . . . . 8
|
99 | 96, 97, 98 | mul32i 10232 |
. . . . . . 7
|
100 | 74, 75 | mulcomi 10046 |
. . . . . . . . . . . 12
|
101 | | df-8 11085 |
. . . . . . . . . . . 12
|
102 | 76, 100, 101 | 3eqtr3i 2652 |
. . . . . . . . . . 11
|
103 | 102 | oveq2i 6661 |
. . . . . . . . . 10
|
104 | | expmul 12905 |
. . . . . . . . . . 11
|
105 | 98, 12, 5, 104 | mp3an 1424 |
. . . . . . . . . 10
|
106 | 103, 105 | eqtr3i 2646 |
. . . . . . . . 9
|
107 | | expp1 12867 |
. . . . . . . . . 10
|
108 | 98, 93, 107 | mp2an 708 |
. . . . . . . . 9
|
109 | | sq3 12961 |
. . . . . . . . . 10
|
110 | 109 | oveq1i 6660 |
. . . . . . . . 9
|
111 | 106, 108,
110 | 3eqtr3i 2652 |
. . . . . . . 8
|
112 | 111 | oveq1i 6660 |
. . . . . . 7
|
113 | 99, 112 | eqtri 2644 |
. . . . . 6
|
114 | 15 | nncni 11030 |
. . . . . . . . 9
|
115 | 18 | nncni 11030 |
. . . . . . . . 9
|
116 | 114, 115 | mulcomi 10046 |
. . . . . . . 8
|
117 | 116 | oveq1i 6660 |
. . . . . . 7
|
118 | 115, 114 | mulcli 10045 |
. . . . . . . 8
|
119 | 118 | mulid1i 10042 |
. . . . . . 7
|
120 | 117, 119 | eqtri 2644 |
. . . . . 6
|
121 | 92, 113, 120 | 3brtr4i 4683 |
. . . . 5
|
122 | 48, 45, 49, 19, 56, 57, 58, 61, 121 | log2ublem1 24673 |
. . . 4
;;;; |
123 | 45, 21 | readdcli 10053 |
. . . . 5
|
124 | 54, 93 | deccl 11512 |
. . . . . 6
;;;; |
125 | 124 | nn0rei 11303 |
. . . . 5
;;;; |
126 | 95, 64 | nnmulcli 11044 |
. . . . . . 7
|
127 | 126 | nnrei 11029 |
. . . . . 6
|
128 | 126 | nngt0i 11054 |
. . . . . 6
|
129 | 127, 128 | pm3.2i 471 |
. . . . 5
|
130 | | lemuldiv2 10904 |
. . . . 5
;;;; ;;;; ;;;; |
131 | 123, 125,
129, 130 | mp3an 1424 |
. . . 4
;;;;
;;;; |
132 | 122, 131 | mpbi 220 |
. . 3
;;;; |
133 | | 8nn0 11315 |
. . . . . . . . . . . . 13
|
134 | 49, 133 | deccl 11512 |
. . . . . . . . . . . 12
; |
135 | 134, 93 | deccl 11512 |
. . . . . . . . . . 11
;; |
136 | 135, 49 | deccl 11512 |
. . . . . . . . . 10
;;; |
137 | 136, 57 | deccl 11512 |
. . . . . . . . 9
;;;; |
138 | 137, 55 | deccl 11512 |
. . . . . . . 8
;;;;; |
139 | 137, 93 | deccl 11512 |
. . . . . . . 8
;;;;; |
140 | | 1lt10 11681 |
. . . . . . . 8
; |
141 | | 6lt7 11209 |
. . . . . . . . 9
|
142 | 137, 55, 63, 141 | declt 11530 |
. . . . . . . 8
;;;;; ;;;;; |
143 | 138, 139,
57, 93, 140, 142 | decltc 11532 |
. . . . . . 7
;;;;;; ;;;;;; |
144 | | eqid 2622 |
. . . . . . . 8
; ; |
145 | 57, 50 | deccl 11512 |
. . . . . . . . . . 11
; |
146 | | 9nn0 11316 |
. . . . . . . . . . 11
|
147 | 145, 146 | deccl 11512 |
. . . . . . . . . 10
;; |
148 | 147, 57 | deccl 11512 |
. . . . . . . . 9
;;; |
149 | 148, 93 | deccl 11512 |
. . . . . . . 8
;;;; |
150 | | eqid 2622 |
. . . . . . . . 9
;;;; ;;;; |
151 | | eqid 2622 |
. . . . . . . . 9
;;;; ;;;; |
152 | | eqid 2622 |
. . . . . . . . . 10
;;; ;;; |
153 | | eqid 2622 |
. . . . . . . . . . 11
;;; ;;; |
154 | | ax-1cn 9994 |
. . . . . . . . . . . 12
|
155 | | 5p1e6 11155 |
. . . . . . . . . . . 12
|
156 | 71, 154, 155 | addcomli 10228 |
. . . . . . . . . . 11
|
157 | 147, 57, 50, 153, 156 | decaddi 11579 |
. . . . . . . . . 10
;;; ;;; |
158 | 57, 55 | deccl 11512 |
. . . . . . . . . . 11
; |
159 | | eqid 2622 |
. . . . . . . . . . 11
;; ;; |
160 | | eqid 2622 |
. . . . . . . . . . . 12
;; ;; |
161 | | eqid 2622 |
. . . . . . . . . . . . 13
; ; |
162 | 57, 50, 155, 161 | decsuc 11535 |
. . . . . . . . . . . 12
; ; |
163 | | 9p4e13 11622 |
. . . . . . . . . . . 12
; |
164 | 145, 146,
5, 160, 162, 49, 163 | decaddci 11580 |
. . . . . . . . . . 11
;; ;; |
165 | | eqid 2622 |
. . . . . . . . . . . 12
; ; |
166 | 158 | nn0cni 11304 |
. . . . . . . . . . . . 13
; |
167 | 166 | addid1i 10223 |
. . . . . . . . . . . 12
; ; |
168 | | 1p2e3 11152 |
. . . . . . . . . . . . . 14
|
169 | 168 | oveq2i 6661 |
. . . . . . . . . . . . 13
|
170 | | 5p3e8 11166 |
. . . . . . . . . . . . . 14
|
171 | 49, 50, 49, 73, 170 | decaddi 11579 |
. . . . . . . . . . . . 13
; |
172 | 169, 171 | eqtri 2644 |
. . . . . . . . . . . 12
; |
173 | | 7t3e21 11649 |
. . . . . . . . . . . . . 14
; |
174 | 70, 98, 173 | mulcomli 10047 |
. . . . . . . . . . . . 13
; |
175 | | 6cn 11102 |
. . . . . . . . . . . . . 14
|
176 | 175, 154,
59 | addcomli 10228 |
. . . . . . . . . . . . 13
|
177 | 12, 57, 55, 174, 176 | decaddi 11579 |
. . . . . . . . . . . 12
; |
178 | 50, 49, 57, 55, 165, 167, 93, 93, 12, 172, 177 | decmac 11566 |
. . . . . . . . . . 11
; ; ;; |
179 | 70 | mul02i 10225 |
. . . . . . . . . . . . 13
|
180 | 179 | oveq1i 6660 |
. . . . . . . . . . . 12
|
181 | 98 | addid2i 10224 |
. . . . . . . . . . . . 13
|
182 | 49 | dec0h 11522 |
. . . . . . . . . . . . 13
; |
183 | 181, 182 | eqtri 2644 |
. . . . . . . . . . . 12
; |
184 | 180, 183 | eqtri 2644 |
. . . . . . . . . . 11
; |
185 | 51, 52, 158, 49, 159, 164, 93, 49, 52, 178, 184 | decmac 11566 |
. . . . . . . . . 10
;; ;; ;;; |
186 | | 3p1e4 11153 |
. . . . . . . . . . 11
|
187 | | 6p5e11 11600 |
. . . . . . . . . . . 12
; |
188 | 175, 71, 187 | addcomli 10228 |
. . . . . . . . . . 11
; |
189 | 49, 50, 55, 73, 186, 57, 188 | decaddci 11580 |
. . . . . . . . . 10
; |
190 | 53, 50, 147, 55, 152, 157, 93, 57, 5, 185, 189 | decmac 11566 |
. . . . . . . . 9
;;; ;;; ;;;; |
191 | | 7t7e49 11653 |
. . . . . . . . . 10
; |
192 | | 4p1e5 11154 |
. . . . . . . . . 10
|
193 | | 9p7e16 11625 |
. . . . . . . . . 10
; |
194 | 5, 146, 93, 191, 192, 55, 193 | decaddci 11580 |
. . . . . . . . 9
; |
195 | 54, 93, 148, 93, 150, 151, 93, 55, 50, 190, 194 | decmac 11566 |
. . . . . . . 8
;;;; ;;;; ;;;;; |
196 | 12 | dec0h 11522 |
. . . . . . . . . 10
; |
197 | 154 | addid2i 10224 |
. . . . . . . . . . . 12
|
198 | 57 | dec0h 11522 |
. . . . . . . . . . . 12
; |
199 | 197, 198 | eqtri 2644 |
. . . . . . . . . . 11
; |
200 | | 00id 10211 |
. . . . . . . . . . . . 13
|
201 | 52 | dec0h 11522 |
. . . . . . . . . . . . 13
; |
202 | 200, 201 | eqtri 2644 |
. . . . . . . . . . . 12
; |
203 | | 5t3e15 11635 |
. . . . . . . . . . . . . 14
; |
204 | 203 | oveq1i 6660 |
. . . . . . . . . . . . 13
; |
205 | 145 | nn0cni 11304 |
. . . . . . . . . . . . . 14
; |
206 | 205 | addid1i 10223 |
. . . . . . . . . . . . 13
; ; |
207 | 204, 206 | eqtri 2644 |
. . . . . . . . . . . 12
; |
208 | | 3t3e9 11180 |
. . . . . . . . . . . . . 14
|
209 | 208 | oveq1i 6660 |
. . . . . . . . . . . . 13
|
210 | 82 | addid1i 10223 |
. . . . . . . . . . . . 13
|
211 | 209, 210 | eqtri 2644 |
. . . . . . . . . . . 12
|
212 | 50, 49, 52, 52, 165, 202, 49, 207, 211 | decma 11564 |
. . . . . . . . . . 11
; ;; |
213 | 98 | mul02i 10225 |
. . . . . . . . . . . . 13
|
214 | 213 | oveq1i 6660 |
. . . . . . . . . . . 12
|
215 | 214, 199 | eqtri 2644 |
. . . . . . . . . . 11
; |
216 | 51, 52, 52, 57, 159, 199, 49, 57, 52, 212, 215 | decmac 11566 |
. . . . . . . . . 10
;; ;;; |
217 | | 5p2e7 11165 |
. . . . . . . . . . 11
|
218 | 57, 50, 12, 203, 217 | decaddi 11579 |
. . . . . . . . . 10
; |
219 | 53, 50, 52, 12, 152, 196, 49, 93, 57, 216, 218 | decmac 11566 |
. . . . . . . . 9
;;; ;;;; |
220 | 49, 54, 93, 150, 57, 12, 219, 173 | decmul1c 11587 |
. . . . . . . 8
;;;; ;;;;; |
221 | 124, 93, 49, 144, 57, 149, 195, 220 | decmul2c 11589 |
. . . . . . 7
;;;; ; ;;;;;; |
222 | 50, 50 | deccl 11512 |
. . . . . . . . . . 11
; |
223 | 222, 49 | deccl 11512 |
. . . . . . . . . 10
;; |
224 | 223, 49 | deccl 11512 |
. . . . . . . . 9
;;; |
225 | 224, 57 | deccl 11512 |
. . . . . . . 8
;;;; |
226 | 12, 50 | deccl 11512 |
. . . . . . . . . 10
; |
227 | 226, 49 | deccl 11512 |
. . . . . . . . 9
;; |
228 | 12, 57 | deccl 11512 |
. . . . . . . . . 10
; |
229 | 228, 133 | deccl 11512 |
. . . . . . . . 9
;; |
230 | 93, 12 | deccl 11512 |
. . . . . . . . . . 11
; |
231 | | 3t2e6 11179 |
. . . . . . . . . . . . 13
|
232 | 98, 75, 231 | mulcomli 10047 |
. . . . . . . . . . . 12
|
233 | | 3exp3 15798 |
. . . . . . . . . . . 12
; |
234 | 12, 93 | deccl 11512 |
. . . . . . . . . . . . 13
; |
235 | | eqid 2622 |
. . . . . . . . . . . . 13
; ; |
236 | 57, 133 | deccl 11512 |
. . . . . . . . . . . . 13
; |
237 | | eqid 2622 |
. . . . . . . . . . . . . 14
; ; |
238 | | 2t2e4 11177 |
. . . . . . . . . . . . . . . 16
|
239 | 238, 168 | oveq12i 6662 |
. . . . . . . . . . . . . . 15
|
240 | | 4p3e7 11163 |
. . . . . . . . . . . . . . 15
|
241 | 239, 240 | eqtri 2644 |
. . . . . . . . . . . . . 14
|
242 | | 7t2e14 11648 |
. . . . . . . . . . . . . . 15
; |
243 | | 1p1e2 11134 |
. . . . . . . . . . . . . . 15
|
244 | | 8cn 11106 |
. . . . . . . . . . . . . . . 16
|
245 | | 8p4e12 11614 |
. . . . . . . . . . . . . . . 16
; |
246 | 244, 74, 245 | addcomli 10228 |
. . . . . . . . . . . . . . 15
; |
247 | 57, 5, 133, 242, 243, 12, 246 | decaddci 11580 |
. . . . . . . . . . . . . 14
; |
248 | 12, 93, 57, 133, 235, 237, 12, 12, 12, 241, 247 | decmac 11566 |
. . . . . . . . . . . . 13
; ; ; |
249 | 70, 75, 242 | mulcomli 10047 |
. . . . . . . . . . . . . . 15
; |
250 | | 4p4e8 11164 |
. . . . . . . . . . . . . . 15
|
251 | 57, 5, 5, 249, 250 | decaddi 11579 |
. . . . . . . . . . . . . 14
; |
252 | 93, 12, 93, 235, 146, 5, 251, 191 | decmul1c 11587 |
. . . . . . . . . . . . 13
; ;; |
253 | 234, 12, 93, 235, 146, 236, 248, 252 | decmul2c 11589 |
. . . . . . . . . . . 12
; ; ;; |
254 | 49, 49, 232, 233, 253 | numexp2x 15783 |
. . . . . . . . . . 11
;; |
255 | | eqid 2622 |
. . . . . . . . . . . 12
; ; |
256 | 232 | oveq1i 6660 |
. . . . . . . . . . . . 13
|
257 | | 6p2e8 11169 |
. . . . . . . . . . . . 13
|
258 | 256, 257 | eqtri 2644 |
. . . . . . . . . . . 12
|
259 | 93, 12, 12, 255, 49, 173, 258 | decrmanc 11576 |
. . . . . . . . . . 11
; ;; |
260 | | 9t3e27 11664 |
. . . . . . . . . . 11
; |
261 | 49, 230, 146, 254, 93, 12, 259, 260 | decmul1c 11587 |
. . . . . . . . . 10
;;; |
262 | 49, 55, 59, 261 | numexpp1 15782 |
. . . . . . . . 9
;;; |
263 | 57, 93 | deccl 11512 |
. . . . . . . . . 10
; |
264 | 263, 93 | deccl 11512 |
. . . . . . . . 9
;; |
265 | | eqid 2622 |
. . . . . . . . . 10
;; ;; |
266 | | eqid 2622 |
. . . . . . . . . 10
;; ;; |
267 | 12, 52 | deccl 11512 |
. . . . . . . . . . 11
; |
268 | 267, 49 | deccl 11512 |
. . . . . . . . . 10
;; |
269 | 12, 12 | deccl 11512 |
. . . . . . . . . . 11
; |
270 | | eqid 2622 |
. . . . . . . . . . 11
; ; |
271 | | eqid 2622 |
. . . . . . . . . . . 12
; ; |
272 | | eqid 2622 |
. . . . . . . . . . . 12
;; ;; |
273 | | eqid 2622 |
. . . . . . . . . . . . . 14
; ; |
274 | 75 | addid2i 10224 |
. . . . . . . . . . . . . 14
|
275 | 154 | addid1i 10223 |
. . . . . . . . . . . . . 14
|
276 | 52, 57, 12, 52, 198, 273, 274, 275 | decadd 11570 |
. . . . . . . . . . . . 13
; ; |
277 | 12, 57, 243, 276 | decsuc 11535 |
. . . . . . . . . . . 12
; ; |
278 | | 7p3e10 11603 |
. . . . . . . . . . . 12
; |
279 | 57, 93, 267, 49, 271, 272, 277, 278 | decaddc2 11575 |
. . . . . . . . . . 11
; ;; ;; |
280 | | eqid 2622 |
. . . . . . . . . . . 12
;; ;; |
281 | | eqid 2622 |
. . . . . . . . . . . . 13
; ; |
282 | | eqid 2622 |
. . . . . . . . . . . . 13
; ; |
283 | | 2p2e4 11144 |
. . . . . . . . . . . . 13
|
284 | 71, 75, 217 | addcomli 10228 |
. . . . . . . . . . . . 13
|
285 | 12, 12, 12, 50, 281, 282, 283, 284 | decadd 11570 |
. . . . . . . . . . . 12
; ; ; |
286 | 50 | dec0h 11522 |
. . . . . . . . . . . . . 14
; |
287 | 192, 286 | eqtri 2644 |
. . . . . . . . . . . . 13
; |
288 | 238, 197 | oveq12i 6662 |
. . . . . . . . . . . . . 14
|
289 | 288, 192 | eqtri 2644 |
. . . . . . . . . . . . 13
|
290 | | 5t2e10 11634 |
. . . . . . . . . . . . . 14
; |
291 | 71 | addid2i 10224 |
. . . . . . . . . . . . . 14
|
292 | 57, 52, 50, 290, 291 | decaddi 11579 |
. . . . . . . . . . . . 13
; |
293 | 12, 50, 52, 50, 282, 287, 12, 50, 57, 289, 292 | decmac 11566 |
. . . . . . . . . . . 12
; ; |
294 | 231 | oveq1i 6660 |
. . . . . . . . . . . . 13
|
295 | | 7p6e13 11608 |
. . . . . . . . . . . . . 14
; |
296 | 70, 175, 295 | addcomli 10228 |
. . . . . . . . . . . . 13
; |
297 | 294, 296 | eqtri 2644 |
. . . . . . . . . . . 12
; |
298 | 226, 49, 5, 93, 280, 285, 12, 49, 57, 293, 297 | decmac 11566 |
. . . . . . . . . . 11
;; ; ; ;; |
299 | 227 | nn0cni 11304 |
. . . . . . . . . . . . . 14
;; |
300 | 299 | mulid1i 10042 |
. . . . . . . . . . . . 13
;; ;; |
301 | 300 | oveq1i 6660 |
. . . . . . . . . . . 12
;; ;; |
302 | 299 | addid1i 10223 |
. . . . . . . . . . . 12
;; ;; |
303 | 301, 302 | eqtri 2644 |
. . . . . . . . . . 11
;; ;; |
304 | 12, 57, 269, 52, 270, 279, 227, 49, 226, 298, 303 | decma2c 11568 |
. . . . . . . . . 10
;; ; ; ;; ;;; |
305 | 93 | dec0h 11522 |
. . . . . . . . . . 11
; |
306 | 74 | addid2i 10224 |
. . . . . . . . . . . . . 14
|
307 | 306 | oveq2i 6661 |
. . . . . . . . . . . . 13
|
308 | | 8t2e16 11654 |
. . . . . . . . . . . . . . 15
; |
309 | 244, 75, 308 | mulcomli 10047 |
. . . . . . . . . . . . . 14
; |
310 | | 6p4e10 11598 |
. . . . . . . . . . . . . 14
; |
311 | 57, 55, 5, 309, 243, 310 | decaddci2 11581 |
. . . . . . . . . . . . 13
; |
312 | 307, 311 | eqtri 2644 |
. . . . . . . . . . . 12
; |
313 | | 8t5e40 11657 |
. . . . . . . . . . . . . 14
; |
314 | 244, 71, 313 | mulcomli 10047 |
. . . . . . . . . . . . 13
; |
315 | 5, 52, 49, 314, 181 | decaddi 11579 |
. . . . . . . . . . . 12
; |
316 | 12, 50, 52, 49, 282, 183, 133, 49, 5, 312, 315 | decmac 11566 |
. . . . . . . . . . 11
; ;; |
317 | | 8t3e24 11655 |
. . . . . . . . . . . . 13
; |
318 | 244, 98, 317 | mulcomli 10047 |
. . . . . . . . . . . 12
; |
319 | | 2p1e3 11151 |
. . . . . . . . . . . 12
|
320 | | 7p4e11 11605 |
. . . . . . . . . . . . 13
; |
321 | 70, 74, 320 | addcomli 10228 |
. . . . . . . . . . . 12
; |
322 | 12, 5, 93, 318, 319, 57, 321 | decaddci 11580 |
. . . . . . . . . . 11
; |
323 | 226, 49, 52, 93, 280, 305, 133, 57, 49, 316, 322 | decmac 11566 |
. . . . . . . . . 10
;; ;;; |
324 | 228, 133,
263, 93, 265, 266, 227, 57, 268, 304, 323 | decma2c 11568 |
. . . . . . . . 9
;; ;; ;; ;;;; |
325 | 57, 5, 49, 249, 240 | decaddi 11579 |
. . . . . . . . . . 11
; |
326 | 49, 50, 12, 73, 217 | decaddi 11579 |
. . . . . . . . . . 11
; |
327 | 12, 50, 12, 282, 93, 93, 49, 325, 326 | decrmac 11577 |
. . . . . . . . . 10
; ;; |
328 | 93, 226, 49, 280, 57, 12, 327, 174 | decmul1c 11587 |
. . . . . . . . 9
;; ;;; |
329 | 227, 229,
93, 262, 57, 264, 324, 328 | decmul2c 11589 |
. . . . . . . 8
;; ;;;;; |
330 | | eqid 2622 |
. . . . . . . . 9
;;;; ;;;; |
331 | | eqid 2622 |
. . . . . . . . . 10
;;; ;;; |
332 | | eqid 2622 |
. . . . . . . . . . 11
;; ;; |
333 | | eqid 2622 |
. . . . . . . . . . . 12
; ; |
334 | 274, 196 | eqtri 2644 |
. . . . . . . . . . . 12
; |
335 | 181 | oveq2i 6661 |
. . . . . . . . . . . . 13
|
336 | 335, 171 | eqtri 2644 |
. . . . . . . . . . . 12
; |
337 | 50, 50, 52, 12, 333, 334, 93, 93, 49, 336, 326 | decmac 11566 |
. . . . . . . . . . 11
; ;; |
338 | 12, 57, 12, 174, 168 | decaddi 11579 |
. . . . . . . . . . 11
; |
339 | 222, 49, 52, 12, 332, 196, 93, 49, 12, 337, 338 | decmac 11566 |
. . . . . . . . . 10
;; ;;; |
340 | 93, 223, 49, 331, 57, 12, 339, 174 | decmul1c 11587 |
. . . . . . . . 9
;;; ;;;; |
341 | 70 | mulid2i 10043 |
. . . . . . . . 9
|
342 | 93, 224, 57, 330, 93, 340, 341 | decmul1 11585 |
. . . . . . . 8
;;;; ;;;;; |
343 | 93, 225, 57, 329, 93, 342, 341 | decmul1 11585 |
. . . . . . 7
;; ;;;;;; |
344 | 143, 221,
343 | 3brtr4i 4683 |
. . . . . 6
;;;; ; ;; |
345 | 93, 49 | deccl 11512 |
. . . . . . . . 9
; |
346 | 124, 345 | nn0mulcli 11331 |
. . . . . . . 8
;;;; ; |
347 | 346 | nn0rei 11303 |
. . . . . . 7
;;;; ; |
348 | 49, 93 | nn0expcli 12886 |
. . . . . . . . . 10
|
349 | 227, 348 | nn0mulcli 11331 |
. . . . . . . . 9
;; |
350 | 349, 93 | nn0mulcli 11331 |
. . . . . . . 8
;; |
351 | 350 | nn0rei 11303 |
. . . . . . 7
;; |
352 | 62 | nnrei 11029 |
. . . . . . 7
|
353 | 62 | nngt0i 11054 |
. . . . . . 7
|
354 | 347, 351,
352, 353 | ltmul1ii 10952 |
. . . . . 6
;;;; ; ;; ;;;; ; ;; |
355 | 344, 354 | mpbi 220 |
. . . . 5
;;;; ; ;; |
356 | 124 | nn0cni 11304 |
. . . . . . 7
;;;; |
357 | 345 | nn0cni 11304 |
. . . . . . 7
; |
358 | 356, 357,
71 | mulassi 10049 |
. . . . . 6
;;;; ; ;;;; ; |
359 | 49, 50, 155, 72 | decsuc 11535 |
. . . . . . . 8
; |
360 | 71, 98, 203 | mulcomli 10047 |
. . . . . . . 8
; |
361 | 50, 93, 49, 144, 50, 57, 359, 360 | decmul1c 11587 |
. . . . . . 7
; ;; |
362 | 361 | oveq2i 6661 |
. . . . . 6
;;;; ; ;;;; ;; |
363 | 358, 362 | eqtri 2644 |
. . . . 5
;;;; ; ;;;; ;; |
364 | 299, 96 | mulcli 10045 |
. . . . . . 7
;; |
365 | 364, 70, 71 | mulassi 10049 |
. . . . . 6
;; ;; |
366 | 70, 71 | mulcomi 10046 |
. . . . . . . 8
|
367 | 366 | oveq2i 6661 |
. . . . . . 7
;; ;; |
368 | 299, 96, 97 | mulassi 10049 |
. . . . . . 7
;; ;; |
369 | 367, 368 | eqtri 2644 |
. . . . . 6
;; ;; |
370 | 365, 369 | eqtri 2644 |
. . . . 5
;; ;; |
371 | 355, 363,
370 | 3brtr3i 4682 |
. . . 4
;;;; ;; ;; |
372 | 49, 55 | deccl 11512 |
. . . . . . . 8
; |
373 | 372, 62 | decnncl 11518 |
. . . . . . 7
;; |
374 | 373 | nnrei 11029 |
. . . . . 6
;; |
375 | 373 | nngt0i 11054 |
. . . . . 6
;; |
376 | 374, 375 | pm3.2i 471 |
. . . . 5
;; ;; |
377 | 227 | nn0rei 11303 |
. . . . 5
;; |
378 | | lt2mul2div 10901 |
. . . . 5
;;;; ;; ;; ;; ;;;; ;; ;;
;;;; ;; ;; |
379 | 125, 376,
377, 129, 378 | mp4an 709 |
. . . 4
;;;; ;; ;; ;;;; ;; ;; |
380 | 371, 379 | mpbi 220 |
. . 3
;;;; ;; ;; |
381 | | nndivre 11056 |
. . . . 5
;;;; ;;;; |
382 | 125, 126,
381 | mp2an 708 |
. . . 4
;;;; |
383 | | nndivre 11056 |
. . . . 5
;; ;; ;; ;; |
384 | 377, 373,
383 | mp2an 708 |
. . . 4
;; ;; |
385 | 123, 382,
384 | lelttri 10164 |
. . 3
;;;; ;;;; ;; ;; ;; ;; |
386 | 132, 380,
385 | mp2an 708 |
. 2
;; ;; |
387 | 27, 123, 384 | lelttri 10164 |
. 2
;; ;;
;; ;; |
388 | 47, 386, 387 | mp2an 708 |
1
;; ;; |