| Step |
Hyp |
Ref |
Expression |
| 1 |
|
3cubeslem1.a |
|
| 2 |
|
3cn |
|
| 3 |
2
|
a1i |
|
| 4 |
|
3nn0 |
|
| 5 |
4
|
a1i |
|
| 6 |
3 5
|
expcld |
|
| 7 |
|
qcn |
|
| 8 |
1 7
|
syl |
|
| 9 |
8
|
sqcld |
|
| 10 |
6 9
|
mulcld |
|
| 11 |
3
|
sqcld |
|
| 12 |
11 8
|
mulcld |
|
| 13 |
10 12 3
|
cu3addd |
|
| 14 |
13
|
oveq2d |
|
| 15 |
10 5
|
expcld |
|
| 16 |
10
|
sqcld |
|
| 17 |
16 12
|
mulcld |
|
| 18 |
3 17
|
mulcld |
|
| 19 |
15 18
|
addcld |
|
| 20 |
12
|
sqcld |
|
| 21 |
10 20
|
mulcld |
|
| 22 |
3 21
|
mulcld |
|
| 23 |
12 5
|
expcld |
|
| 24 |
22 23
|
addcld |
|
| 25 |
19 24
|
addcld |
|
| 26 |
16 3
|
mulcld |
|
| 27 |
3 26
|
mulcld |
|
| 28 |
|
2nn0 |
|
| 29 |
28
|
a1i |
|
| 30 |
5 29
|
nn0mulcld |
|
| 31 |
30
|
nn0cnd |
|
| 32 |
10 12
|
mulcld |
|
| 33 |
31 32
|
mulcld |
|
| 34 |
33 3
|
mulcld |
|
| 35 |
27 34
|
addcld |
|
| 36 |
20 3
|
mulcld |
|
| 37 |
3 36
|
mulcld |
|
| 38 |
35 37
|
addcld |
|
| 39 |
25 38
|
addcld |
|
| 40 |
10 11
|
mulcld |
|
| 41 |
3 40
|
mulcld |
|
| 42 |
12 11
|
mulcld |
|
| 43 |
3 42
|
mulcld |
|
| 44 |
41 43
|
addcld |
|
| 45 |
44 6
|
addcld |
|
| 46 |
8 39 45
|
adddid |
|
| 47 |
8 25 38
|
adddid |
|
| 48 |
47
|
oveq1d |
|
| 49 |
46 48
|
eqtrd |
|
| 50 |
8 19 24
|
adddid |
|
| 51 |
50
|
oveq1d |
|
| 52 |
51
|
oveq1d |
|
| 53 |
49 52
|
eqtrd |
|
| 54 |
8 15 18
|
adddid |
|
| 55 |
54
|
oveq1d |
|
| 56 |
55
|
oveq1d |
|
| 57 |
56
|
oveq1d |
|
| 58 |
53 57
|
eqtrd |
|
| 59 |
8 22 23
|
adddid |
|
| 60 |
59
|
oveq2d |
|
| 61 |
60
|
oveq1d |
|
| 62 |
61
|
oveq1d |
|
| 63 |
58 62
|
eqtrd |
|
| 64 |
8 35 37
|
adddid |
|
| 65 |
64
|
oveq2d |
|
| 66 |
65
|
oveq1d |
|
| 67 |
63 66
|
eqtrd |
|
| 68 |
8 27 34
|
adddid |
|
| 69 |
68
|
oveq1d |
|
| 70 |
69
|
oveq2d |
|
| 71 |
70
|
oveq1d |
|
| 72 |
67 71
|
eqtrd |
|
| 73 |
8 44 6
|
adddid |
|
| 74 |
73
|
oveq2d |
|
| 75 |
72 74
|
eqtrd |
|
| 76 |
8 41 43
|
adddid |
|
| 77 |
76
|
oveq1d |
|
| 78 |
77
|
oveq2d |
|
| 79 |
75 78
|
eqtrd |
|
| 80 |
14 79
|
eqtrd |
|
| 81 |
8 15
|
mulcld |
|
| 82 |
8 18
|
mulcld |
|
| 83 |
81 82
|
addcld |
|
| 84 |
8 22
|
mulcld |
|
| 85 |
8 23
|
mulcld |
|
| 86 |
84 85
|
addcld |
|
| 87 |
83 86
|
addcld |
|
| 88 |
8 27
|
mulcld |
|
| 89 |
8 34
|
mulcld |
|
| 90 |
88 89
|
addcld |
|
| 91 |
8 37
|
mulcld |
|
| 92 |
90 91
|
addcld |
|
| 93 |
8 41
|
mulcld |
|
| 94 |
8 43
|
mulcld |
|
| 95 |
93 94
|
addcld |
|
| 96 |
8 6
|
mulcld |
|
| 97 |
95 96
|
addcld |
|
| 98 |
87 92 97
|
addassd |
|
| 99 |
92 97
|
addcld |
|
| 100 |
83 86 99
|
addassd |
|
| 101 |
98 100
|
eqtrd |
|
| 102 |
86 99
|
addcld |
|
| 103 |
81 82 102
|
addassd |
|
| 104 |
101 103
|
eqtrd |
|
| 105 |
84 85 99
|
addassd |
|
| 106 |
105
|
oveq2d |
|
| 107 |
106
|
oveq2d |
|
| 108 |
104 107
|
eqtrd |
|
| 109 |
85 99
|
addcomd |
|
| 110 |
109
|
oveq2d |
|
| 111 |
110
|
oveq2d |
|
| 112 |
111
|
oveq2d |
|
| 113 |
108 112
|
eqtrd |
|
| 114 |
92 97 85
|
addassd |
|
| 115 |
114
|
oveq2d |
|
| 116 |
115
|
oveq2d |
|
| 117 |
116
|
oveq2d |
|
| 118 |
113 117
|
eqtrd |
|
| 119 |
97 85
|
addcld |
|
| 120 |
90 91 119
|
addassd |
|
| 121 |
120
|
oveq2d |
|
| 122 |
121
|
oveq2d |
|
| 123 |
122
|
oveq2d |
|
| 124 |
118 123
|
eqtrd |
|
| 125 |
91 119
|
addcld |
|
| 126 |
88 89 125
|
addassd |
|
| 127 |
126
|
oveq2d |
|
| 128 |
127
|
oveq2d |
|
| 129 |
128
|
oveq2d |
|
| 130 |
124 129
|
eqtrd |
|
| 131 |
91 119
|
addcomd |
|
| 132 |
131
|
oveq2d |
|
| 133 |
132
|
oveq2d |
|
| 134 |
133
|
oveq2d |
|
| 135 |
134
|
oveq2d |
|
| 136 |
135
|
oveq2d |
|
| 137 |
130 136
|
eqtrd |
|
| 138 |
97 85
|
addcomd |
|
| 139 |
138
|
oveq1d |
|
| 140 |
139
|
oveq2d |
|
| 141 |
140
|
oveq2d |
|
| 142 |
141
|
oveq2d |
|
| 143 |
142
|
oveq2d |
|
| 144 |
143
|
oveq2d |
|
| 145 |
137 144
|
eqtrd |
|
| 146 |
85 97 91
|
addassd |
|
| 147 |
146
|
oveq2d |
|
| 148 |
147
|
oveq2d |
|
| 149 |
148
|
oveq2d |
|
| 150 |
149
|
oveq2d |
|
| 151 |
150
|
oveq2d |
|
| 152 |
145 151
|
eqtrd |
|
| 153 |
95 96 91
|
addassd |
|
| 154 |
153
|
oveq2d |
|
| 155 |
154
|
oveq2d |
|
| 156 |
155
|
oveq2d |
|
| 157 |
156
|
oveq2d |
|
| 158 |
157
|
oveq2d |
|
| 159 |
158
|
oveq2d |
|
| 160 |
152 159
|
eqtrd |
|
| 161 |
96 91
|
addcld |
|
| 162 |
93 94 161
|
addassd |
|
| 163 |
162
|
oveq2d |
|
| 164 |
163
|
oveq2d |
|
| 165 |
164
|
oveq2d |
|
| 166 |
165
|
oveq2d |
|
| 167 |
166
|
oveq2d |
|
| 168 |
167
|
oveq2d |
|
| 169 |
160 168
|
eqtrd |
|
| 170 |
94 161
|
addcomd |
|
| 171 |
170
|
oveq2d |
|
| 172 |
171
|
oveq2d |
|
| 173 |
172
|
oveq2d |
|
| 174 |
173
|
oveq2d |
|
| 175 |
174
|
oveq2d |
|
| 176 |
175
|
oveq2d |
|
| 177 |
176
|
oveq2d |
|
| 178 |
169 177
|
eqtrd |
|
| 179 |
96 91
|
addcomd |
|
| 180 |
179
|
oveq1d |
|
| 181 |
180
|
oveq2d |
|
| 182 |
181
|
oveq2d |
|
| 183 |
182
|
oveq2d |
|
| 184 |
183
|
oveq2d |
|
| 185 |
184
|
oveq2d |
|
| 186 |
185
|
oveq2d |
|
| 187 |
186
|
oveq2d |
|
| 188 |
178 187
|
eqtrd |
|
| 189 |
91 96 94
|
addassd |
|
| 190 |
189
|
oveq2d |
|
| 191 |
190
|
oveq2d |
|
| 192 |
191
|
oveq2d |
|
| 193 |
192
|
oveq2d |
|
| 194 |
193
|
oveq2d |
|
| 195 |
194
|
oveq2d |
|
| 196 |
195
|
oveq2d |
|
| 197 |
188 196
|
eqtrd |
|
| 198 |
96 94
|
addcomd |
|
| 199 |
198
|
oveq2d |
|
| 200 |
199
|
oveq2d |
|
| 201 |
200
|
oveq2d |
|
| 202 |
201
|
oveq2d |
|
| 203 |
202
|
oveq2d |
|
| 204 |
203
|
oveq2d |
|
| 205 |
204
|
oveq2d |
|
| 206 |
205
|
oveq2d |
|
| 207 |
197 206
|
eqtrd |
|
| 208 |
80 207
|
eqtrd |
|
| 209 |
94 96
|
addcld |
|
| 210 |
91 209
|
addcld |
|
| 211 |
93 210
|
addcld |
|
| 212 |
85 211
|
addcld |
|
| 213 |
89 212
|
addcld |
|
| 214 |
84 88 213
|
addassd |
|
| 215 |
214
|
oveq2d |
|
| 216 |
215
|
oveq2d |
|
| 217 |
216
|
eqcomd |
|
| 218 |
89 85 211
|
addassd |
|
| 219 |
218
|
oveq2d |
|
| 220 |
219
|
oveq2d |
|
| 221 |
220
|
oveq2d |
|
| 222 |
217 221
|
eqtr4d |
|
| 223 |
93 91 209
|
addassd |
|
| 224 |
223
|
oveq2d |
|
| 225 |
224
|
oveq2d |
|
| 226 |
225
|
oveq2d |
|
| 227 |
226
|
oveq2d |
|
| 228 |
222 227
|
eqtr4d |
|
| 229 |
208 228
|
eqtrd |
|
| 230 |
3 42
|
mulcomd |
|
| 231 |
230
|
oveq2d |
|
| 232 |
11 8
|
mulcomd |
|
| 233 |
232
|
oveq1d |
|
| 234 |
233
|
oveq1d |
|
| 235 |
234
|
oveq2d |
|
| 236 |
231 235
|
eqtrd |
|
| 237 |
8 11
|
mulcld |
|
| 238 |
237 11 3
|
mulassd |
|
| 239 |
238
|
oveq2d |
|
| 240 |
236 239
|
eqtrd |
|
| 241 |
11 3
|
mulcld |
|
| 242 |
8 11 241
|
mulassd |
|
| 243 |
242
|
oveq2d |
|
| 244 |
240 243
|
eqtrd |
|
| 245 |
11 241
|
mulcld |
|
| 246 |
8 8 245
|
mulassd |
|
| 247 |
246
|
eqcomd |
|
| 248 |
11 11 3
|
mulassd |
|
| 249 |
248
|
oveq2d |
|
| 250 |
247 249
|
eqtr4d |
|
| 251 |
244 250
|
eqtrd |
|
| 252 |
8
|
sqvald |
|
| 253 |
252
|
eqcomd |
|
| 254 |
253
|
oveq1d |
|
| 255 |
251 254
|
eqtrd |
|
| 256 |
3 29 29
|
expaddd |
|
| 257 |
256
|
oveq1d |
|
| 258 |
257
|
eqcomd |
|
| 259 |
29 29
|
nn0addcld |
|
| 260 |
3 259
|
expp1d |
|
| 261 |
258 260
|
eqtr4d |
|
| 262 |
261
|
oveq2d |
|
| 263 |
255 262
|
eqtrd |
|
| 264 |
|
2p2e4 |
|
| 265 |
264
|
a1i |
|
| 266 |
265
|
oveq1d |
|
| 267 |
266
|
oveq2d |
|
| 268 |
267
|
oveq2d |
|
| 269 |
263 268
|
eqtrd |
|
| 270 |
|
4p1e5 |
|
| 271 |
270
|
a1i |
|
| 272 |
271
|
oveq2d |
|
| 273 |
272
|
oveq2d |
|
| 274 |
269 273
|
eqtrd |
|
| 275 |
274
|
oveq1d |
|
| 276 |
275
|
oveq2d |
|
| 277 |
276
|
oveq2d |
|
| 278 |
277
|
oveq2d |
|
| 279 |
278
|
oveq2d |
|
| 280 |
279
|
oveq2d |
|
| 281 |
229 280
|
eqtrd |
|
| 282 |
8 41
|
mulcomd |
|
| 283 |
3 40
|
mulcomd |
|
| 284 |
283
|
oveq1d |
|
| 285 |
282 284
|
eqtrd |
|
| 286 |
6 9
|
mulcomd |
|
| 287 |
286
|
oveq1d |
|
| 288 |
287
|
oveq1d |
|
| 289 |
288
|
oveq1d |
|
| 290 |
285 289
|
eqtrd |
|
| 291 |
9 6
|
mulcld |
|
| 292 |
291 11
|
mulcld |
|
| 293 |
292 3 8
|
mulassd |
|
| 294 |
290 293
|
eqtrd |
|
| 295 |
3 8
|
mulcld |
|
| 296 |
291 11 295
|
mulassd |
|
| 297 |
294 296
|
eqtrd |
|
| 298 |
11 295
|
mulcld |
|
| 299 |
9 6 298
|
mulassd |
|
| 300 |
297 299
|
eqtrd |
|
| 301 |
6 298
|
mulcomd |
|
| 302 |
301
|
oveq2d |
|
| 303 |
300 302
|
eqtrd |
|
| 304 |
11 295
|
mulcomd |
|
| 305 |
304
|
oveq1d |
|
| 306 |
305
|
oveq2d |
|
| 307 |
303 306
|
eqtrd |
|
| 308 |
3 8
|
mulcomd |
|
| 309 |
308
|
oveq1d |
|
| 310 |
309
|
oveq1d |
|
| 311 |
310
|
oveq2d |
|
| 312 |
307 311
|
eqtrd |
|
| 313 |
8 3
|
mulcld |
|
| 314 |
313 11 6
|
mulassd |
|
| 315 |
314
|
oveq2d |
|
| 316 |
312 315
|
eqtrd |
|
| 317 |
11 6
|
mulcld |
|
| 318 |
8 3 317
|
mulassd |
|
| 319 |
318
|
oveq2d |
|
| 320 |
316 319
|
eqtrd |
|
| 321 |
320
|
oveq1d |
|
| 322 |
3 317
|
mulcld |
|
| 323 |
9 8 322
|
mulassd |
|
| 324 |
323
|
oveq1d |
|
| 325 |
321 324
|
eqtr4d |
|
| 326 |
8 29
|
expp1d |
|
| 327 |
326
|
eqcomd |
|
| 328 |
327
|
oveq1d |
|
| 329 |
328
|
oveq1d |
|
| 330 |
325 329
|
eqtrd |
|
| 331 |
|
2p1e3 |
|
| 332 |
331
|
a1i |
|
| 333 |
332
|
oveq2d |
|
| 334 |
333
|
oveq1d |
|
| 335 |
334
|
oveq1d |
|
| 336 |
330 335
|
eqtrd |
|
| 337 |
3 5 29
|
expaddd |
|
| 338 |
337
|
oveq2d |
|
| 339 |
338
|
eqcomd |
|
| 340 |
29 5
|
nn0addcld |
|
| 341 |
3 340
|
expcld |
|
| 342 |
3 341
|
mulcomd |
|
| 343 |
339 342
|
eqtrd |
|
| 344 |
3 340
|
expp1d |
|
| 345 |
343 344
|
eqtr4d |
|
| 346 |
345
|
oveq2d |
|
| 347 |
346
|
oveq1d |
|
| 348 |
336 347
|
eqtrd |
|
| 349 |
332
|
oveq2d |
|
| 350 |
349
|
oveq1d |
|
| 351 |
350
|
oveq2d |
|
| 352 |
351
|
oveq2d |
|
| 353 |
352
|
oveq1d |
|
| 354 |
348 353
|
eqtr4d |
|
| 355 |
29
|
nn0cnd |
|
| 356 |
|
ax-1cn |
|
| 357 |
356
|
a1i |
|
| 358 |
355 355 357
|
addassd |
|
| 359 |
358
|
oveq1d |
|
| 360 |
359
|
oveq2d |
|
| 361 |
360
|
oveq2d |
|
| 362 |
361
|
oveq1d |
|
| 363 |
354 362
|
eqtr4d |
|
| 364 |
266
|
oveq1d |
|
| 365 |
364
|
oveq2d |
|
| 366 |
365
|
oveq2d |
|
| 367 |
366
|
oveq1d |
|
| 368 |
363 367
|
eqtrd |
|
| 369 |
271
|
oveq1d |
|
| 370 |
369
|
oveq2d |
|
| 371 |
370
|
oveq2d |
|
| 372 |
371
|
oveq1d |
|
| 373 |
368 372
|
eqtrd |
|
| 374 |
|
5p1e6 |
|
| 375 |
374
|
a1i |
|
| 376 |
375
|
oveq2d |
|
| 377 |
376
|
oveq2d |
|
| 378 |
377
|
oveq1d |
|
| 379 |
373 378
|
eqtrd |
|
| 380 |
11 8 29
|
mulexpd |
|
| 381 |
380
|
oveq1d |
|
| 382 |
381
|
oveq2d |
|
| 383 |
382
|
oveq2d |
|
| 384 |
383
|
oveq2d |
|
| 385 |
379 384
|
eqtrd |
|
| 386 |
11
|
sqcld |
|
| 387 |
386 9
|
mulcld |
|
| 388 |
387 3
|
mulcld |
|
| 389 |
3 388
|
mulcld |
|
| 390 |
8 389
|
mulcomd |
|
| 391 |
3 388
|
mulcomd |
|
| 392 |
391
|
oveq1d |
|
| 393 |
390 392
|
eqtrd |
|
| 394 |
386 9
|
mulcomd |
|
| 395 |
394
|
oveq1d |
|
| 396 |
395
|
oveq1d |
|
| 397 |
396
|
oveq1d |
|
| 398 |
393 397
|
eqtrd |
|
| 399 |
9 386
|
mulcld |
|
| 400 |
399 3
|
mulcld |
|
| 401 |
400 3 8
|
mulassd |
|
| 402 |
398 401
|
eqtrd |
|
| 403 |
399 3 295
|
mulassd |
|
| 404 |
402 403
|
eqtrd |
|
| 405 |
3 295
|
mulcld |
|
| 406 |
9 386 405
|
mulassd |
|
| 407 |
404 406
|
eqtrd |
|
| 408 |
386 405
|
mulcomd |
|
| 409 |
408
|
oveq2d |
|
| 410 |
407 409
|
eqtrd |
|
| 411 |
3 295
|
mulcomd |
|
| 412 |
411
|
oveq1d |
|
| 413 |
412
|
oveq2d |
|
| 414 |
410 413
|
eqtrd |
|
| 415 |
308
|
oveq1d |
|
| 416 |
415
|
oveq1d |
|
| 417 |
416
|
oveq2d |
|
| 418 |
414 417
|
eqtrd |
|
| 419 |
313 3 386
|
mulassd |
|
| 420 |
419
|
oveq2d |
|
| 421 |
418 420
|
eqtrd |
|
| 422 |
3 386
|
mulcld |
|
| 423 |
8 3 422
|
mulassd |
|
| 424 |
423
|
oveq2d |
|
| 425 |
421 424
|
eqtrd |
|
| 426 |
425
|
oveq2d |
|
| 427 |
385 426
|
eqtrd |
|
| 428 |
3 422
|
mulcld |
|
| 429 |
9 8 428
|
mulassd |
|
| 430 |
429
|
oveq2d |
|
| 431 |
427 430
|
eqtr4d |
|
| 432 |
327
|
oveq1d |
|
| 433 |
432
|
oveq2d |
|
| 434 |
431 433
|
eqtrd |
|
| 435 |
333
|
oveq1d |
|
| 436 |
435
|
oveq2d |
|
| 437 |
434 436
|
eqtrd |
|
| 438 |
8 5
|
expcld |
|
| 439 |
|
6nn0 |
|
| 440 |
439
|
a1i |
|
| 441 |
3 440
|
expcld |
|
| 442 |
438 441 428
|
adddid |
|
| 443 |
442
|
eqcomd |
|
| 444 |
437 443
|
eqtrd |
|
| 445 |
3 29 29
|
expmuld |
|
| 446 |
445
|
oveq2d |
|
| 447 |
446
|
oveq2d |
|
| 448 |
447
|
eqcomd |
|
| 449 |
29 29
|
nn0mulcld |
|
| 450 |
3 449
|
expcld |
|
| 451 |
3 450
|
mulcomd |
|
| 452 |
451
|
oveq2d |
|
| 453 |
448 452
|
eqtrd |
|
| 454 |
3 449
|
expp1d |
|
| 455 |
454
|
oveq2d |
|
| 456 |
453 455
|
eqtr4d |
|
| 457 |
|
1nn0 |
|
| 458 |
457
|
a1i |
|
| 459 |
449 458
|
nn0addcld |
|
| 460 |
3 459
|
expcld |
|
| 461 |
3 460
|
mulcomd |
|
| 462 |
456 461
|
eqtrd |
|
| 463 |
3 459
|
expp1d |
|
| 464 |
462 463
|
eqtr4d |
|
| 465 |
464
|
oveq2d |
|
| 466 |
465
|
oveq2d |
|
| 467 |
444 466
|
eqtrd |
|
| 468 |
|
2t2e4 |
|
| 469 |
468
|
a1i |
|
| 470 |
469
|
oveq1d |
|
| 471 |
470
|
oveq1d |
|
| 472 |
471
|
oveq2d |
|
| 473 |
472
|
oveq2d |
|
| 474 |
473
|
oveq2d |
|
| 475 |
467 474
|
eqtrd |
|
| 476 |
370
|
oveq2d |
|
| 477 |
476
|
oveq2d |
|
| 478 |
475 477
|
eqtrd |
|
| 479 |
376
|
oveq2d |
|
| 480 |
479
|
oveq2d |
|
| 481 |
478 480
|
eqtrd |
|
| 482 |
481
|
oveq1d |
|
| 483 |
482
|
oveq2d |
|
| 484 |
483
|
oveq2d |
|
| 485 |
484
|
oveq2d |
|
| 486 |
485
|
oveq2d |
|
| 487 |
281 486
|
eqtrd |
|
| 488 |
8 34
|
mulcomd |
|
| 489 |
31 32
|
mulcomd |
|
| 490 |
489
|
oveq1d |
|
| 491 |
490
|
oveq1d |
|
| 492 |
488 491
|
eqtrd |
|
| 493 |
286
|
oveq1d |
|
| 494 |
493
|
oveq1d |
|
| 495 |
494
|
oveq1d |
|
| 496 |
495
|
oveq1d |
|
| 497 |
492 496
|
eqtrd |
|
| 498 |
291 12
|
mulcld |
|
| 499 |
498 31
|
mulcld |
|
| 500 |
499 3 8
|
mulassd |
|
| 501 |
497 500
|
eqtrd |
|
| 502 |
498 31 295
|
mulassd |
|
| 503 |
501 502
|
eqtrd |
|
| 504 |
31 295
|
mulcld |
|
| 505 |
291 12 504
|
mulassd |
|
| 506 |
503 505
|
eqtrd |
|
| 507 |
12 504
|
mulcld |
|
| 508 |
9 6 507
|
mulassd |
|
| 509 |
506 508
|
eqtrd |
|
| 510 |
6 507
|
mulcomd |
|
| 511 |
510
|
oveq2d |
|
| 512 |
509 511
|
eqtrd |
|
| 513 |
232
|
oveq1d |
|
| 514 |
513
|
oveq1d |
|
| 515 |
514
|
oveq2d |
|
| 516 |
512 515
|
eqtrd |
|
| 517 |
237 504 6
|
mulassd |
|
| 518 |
517
|
oveq2d |
|
| 519 |
516 518
|
eqtrd |
|
| 520 |
504 6
|
mulcld |
|
| 521 |
8 11 520
|
mulassd |
|
| 522 |
521
|
oveq2d |
|
| 523 |
519 522
|
eqtrd |
|
| 524 |
11 520
|
mulcomd |
|
| 525 |
524
|
oveq2d |
|
| 526 |
525
|
oveq2d |
|
| 527 |
523 526
|
eqtrd |
|
| 528 |
31 295
|
mulcomd |
|
| 529 |
528
|
oveq1d |
|
| 530 |
529
|
oveq1d |
|
| 531 |
530
|
oveq2d |
|
| 532 |
531
|
oveq2d |
|
| 533 |
527 532
|
eqtrd |
|
| 534 |
308
|
oveq1d |
|
| 535 |
534
|
oveq1d |
|
| 536 |
535
|
oveq1d |
|
| 537 |
536
|
oveq2d |
|
| 538 |
537
|
oveq2d |
|
| 539 |
533 538
|
eqtrd |
|
| 540 |
313 31
|
mulcld |
|
| 541 |
540 6 11
|
mulassd |
|
| 542 |
541
|
oveq2d |
|
| 543 |
542
|
oveq2d |
|
| 544 |
539 543
|
eqtrd |
|
| 545 |
6 11
|
mulcld |
|
| 546 |
313 31 545
|
mulassd |
|
| 547 |
546
|
oveq2d |
|
| 548 |
547
|
oveq2d |
|
| 549 |
544 548
|
eqtrd |
|
| 550 |
31 545
|
mulcld |
|
| 551 |
8 3 550
|
mulassd |
|
| 552 |
551
|
oveq2d |
|
| 553 |
552
|
oveq2d |
|
| 554 |
549 553
|
eqtrd |
|
| 555 |
3 355 545
|
mulassd |
|
| 556 |
555
|
oveq2d |
|
| 557 |
556
|
oveq2d |
|
| 558 |
557
|
oveq2d |
|
| 559 |
558
|
oveq2d |
|
| 560 |
554 559
|
eqtrd |
|
| 561 |
560
|
oveq1d |
|
| 562 |
355 545
|
mulcld |
|
| 563 |
3 562
|
mulcld |
|
| 564 |
3 563
|
mulcld |
|
| 565 |
8 564
|
mulcld |
|
| 566 |
9 8 565
|
mulassd |
|
| 567 |
566
|
oveq1d |
|
| 568 |
561 567
|
eqtr4d |
|
| 569 |
9 8
|
mulcld |
|
| 570 |
569 8 564
|
mulassd |
|
| 571 |
570
|
oveq1d |
|
| 572 |
568 571
|
eqtr4d |
|
| 573 |
327
|
oveq1d |
|
| 574 |
29 458
|
nn0addcld |
|
| 575 |
8 574
|
expp1d |
|
| 576 |
573 575
|
eqtr4d |
|
| 577 |
576
|
oveq1d |
|
| 578 |
577
|
oveq1d |
|
| 579 |
572 578
|
eqtrd |
|
| 580 |
332
|
oveq1d |
|
| 581 |
580
|
oveq2d |
|
| 582 |
581
|
oveq1d |
|
| 583 |
582
|
oveq1d |
|
| 584 |
579 583
|
eqtrd |
|
| 585 |
|
3p1e4 |
|
| 586 |
585
|
a1i |
|
| 587 |
586
|
oveq2d |
|
| 588 |
587
|
oveq1d |
|
| 589 |
588
|
oveq1d |
|
| 590 |
584 589
|
eqtrd |
|
| 591 |
3 29 5
|
expaddd |
|
| 592 |
591
|
oveq2d |
|
| 593 |
592
|
oveq2d |
|
| 594 |
593
|
oveq2d |
|
| 595 |
594
|
eqcomd |
|
| 596 |
595
|
oveq2d |
|
| 597 |
596
|
oveq1d |
|
| 598 |
590 597
|
eqtrd |
|
| 599 |
|
3p2e5 |
|
| 600 |
599
|
a1i |
|
| 601 |
600
|
oveq2d |
|
| 602 |
601
|
oveq2d |
|
| 603 |
602
|
oveq2d |
|
| 604 |
603
|
oveq2d |
|
| 605 |
604
|
oveq2d |
|
| 606 |
605
|
oveq1d |
|
| 607 |
598 606
|
eqtrd |
|
| 608 |
|
5nn0 |
|
| 609 |
608
|
a1i |
|
| 610 |
3 609
|
expcld |
|
| 611 |
355 610
|
mulcomd |
|
| 612 |
611
|
oveq2d |
|
| 613 |
612
|
oveq2d |
|
| 614 |
613
|
oveq2d |
|
| 615 |
614
|
oveq1d |
|
| 616 |
607 615
|
eqtrd |
|
| 617 |
3 610 355
|
mulassd |
|
| 618 |
617
|
oveq2d |
|
| 619 |
618
|
oveq2d |
|
| 620 |
619
|
oveq1d |
|
| 621 |
616 620
|
eqtr4d |
|
| 622 |
3 610
|
mulcld |
|
| 623 |
3 622 355
|
mulassd |
|
| 624 |
623
|
oveq2d |
|
| 625 |
624
|
oveq1d |
|
| 626 |
621 625
|
eqtr4d |
|
| 627 |
3 610
|
mulcomd |
|
| 628 |
627
|
oveq2d |
|
| 629 |
3 609
|
expp1d |
|
| 630 |
629
|
oveq2d |
|
| 631 |
628 630
|
eqtr4d |
|
| 632 |
609 458
|
nn0addcld |
|
| 633 |
3 632
|
expcld |
|
| 634 |
3 633
|
mulcomd |
|
| 635 |
631 634
|
eqtrd |
|
| 636 |
3 632
|
expp1d |
|
| 637 |
635 636
|
eqtr4d |
|
| 638 |
637
|
oveq1d |
|
| 639 |
638
|
oveq2d |
|
| 640 |
639
|
oveq1d |
|
| 641 |
626 640
|
eqtrd |
|
| 642 |
375
|
oveq1d |
|
| 643 |
642
|
oveq2d |
|
| 644 |
643
|
oveq1d |
|
| 645 |
644
|
oveq2d |
|
| 646 |
645
|
oveq1d |
|
| 647 |
641 646
|
eqtrd |
|
| 648 |
|
6p1e7 |
|
| 649 |
648
|
a1i |
|
| 650 |
649
|
oveq2d |
|
| 651 |
650
|
oveq1d |
|
| 652 |
651
|
oveq2d |
|
| 653 |
652
|
oveq1d |
|
| 654 |
647 653
|
eqtrd |
|
| 655 |
11 8 5
|
mulexpd |
|
| 656 |
655
|
oveq2d |
|
| 657 |
656
|
oveq2d |
|
| 658 |
654 657
|
eqtrd |
|
| 659 |
11 5
|
expcld |
|
| 660 |
659 438
|
mulcld |
|
| 661 |
8 660
|
mulcomd |
|
| 662 |
659 438
|
mulcomd |
|
| 663 |
662
|
oveq1d |
|
| 664 |
661 663
|
eqtrd |
|
| 665 |
438 659 8
|
mulassd |
|
| 666 |
664 665
|
eqtrd |
|
| 667 |
659 8
|
mulcomd |
|
| 668 |
667
|
oveq2d |
|
| 669 |
666 668
|
eqtrd |
|
| 670 |
669
|
oveq2d |
|
| 671 |
658 670
|
eqtrd |
|
| 672 |
438 8 659
|
mulassd |
|
| 673 |
672
|
oveq2d |
|
| 674 |
671 673
|
eqtr4d |
|
| 675 |
8 5
|
expp1d |
|
| 676 |
675
|
eqcomd |
|
| 677 |
676
|
oveq1d |
|
| 678 |
677
|
oveq2d |
|
| 679 |
674 678
|
eqtrd |
|
| 680 |
587
|
oveq1d |
|
| 681 |
680
|
oveq2d |
|
| 682 |
679 681
|
eqtrd |
|
| 683 |
3 5 29
|
expmuld |
|
| 684 |
683
|
eqcomd |
|
| 685 |
684
|
oveq2d |
|
| 686 |
685
|
oveq2d |
|
| 687 |
682 686
|
eqtrd |
|
| 688 |
|
2cn |
|
| 689 |
|
3t2e6 |
|
| 690 |
2 688 689
|
mulcomli |
|
| 691 |
690
|
a1i |
|
| 692 |
691
|
oveq2d |
|
| 693 |
692
|
oveq2d |
|
| 694 |
693
|
oveq2d |
|
| 695 |
687 694
|
eqtrd |
|
| 696 |
|
4nn0 |
|
| 697 |
696
|
a1i |
|
| 698 |
8 697
|
expcld |
|
| 699 |
|
7nn0 |
|
| 700 |
699
|
a1i |
|
| 701 |
3 700
|
expcld |
|
| 702 |
701 355
|
mulcld |
|
| 703 |
698 702 441
|
adddid |
|
| 704 |
703
|
eqcomd |
|
| 705 |
695 704
|
eqtrd |
|
| 706 |
705
|
oveq1d |
|
| 707 |
706
|
oveq2d |
|
| 708 |
707
|
oveq2d |
|
| 709 |
708
|
oveq2d |
|
| 710 |
487 709
|
eqtrd |
|
| 711 |
380
|
oveq2d |
|
| 712 |
711
|
oveq2d |
|
| 713 |
712
|
oveq2d |
|
| 714 |
713
|
oveq1d |
|
| 715 |
10 387
|
mulcld |
|
| 716 |
3 715
|
mulcld |
|
| 717 |
8 716
|
mulcomd |
|
| 718 |
3 715
|
mulcomd |
|
| 719 |
718
|
oveq1d |
|
| 720 |
717 719
|
eqtrd |
|
| 721 |
286
|
oveq1d |
|
| 722 |
721
|
oveq1d |
|
| 723 |
722
|
oveq1d |
|
| 724 |
720 723
|
eqtrd |
|
| 725 |
291 387
|
mulcld |
|
| 726 |
725 3 8
|
mulassd |
|
| 727 |
724 726
|
eqtrd |
|
| 728 |
291 387 295
|
mulassd |
|
| 729 |
727 728
|
eqtrd |
|
| 730 |
387 295
|
mulcld |
|
| 731 |
9 6 730
|
mulassd |
|
| 732 |
729 731
|
eqtrd |
|
| 733 |
6 730
|
mulcomd |
|
| 734 |
733
|
oveq2d |
|
| 735 |
732 734
|
eqtrd |
|
| 736 |
394
|
oveq1d |
|
| 737 |
736
|
oveq1d |
|
| 738 |
737
|
oveq2d |
|
| 739 |
735 738
|
eqtrd |
|
| 740 |
399 295 6
|
mulassd |
|
| 741 |
740
|
oveq2d |
|
| 742 |
739 741
|
eqtrd |
|
| 743 |
295 6
|
mulcld |
|
| 744 |
9 386 743
|
mulassd |
|
| 745 |
744
|
oveq2d |
|
| 746 |
742 745
|
eqtrd |
|
| 747 |
386 743
|
mulcomd |
|
| 748 |
747
|
oveq2d |
|
| 749 |
748
|
oveq2d |
|
| 750 |
746 749
|
eqtrd |
|
| 751 |
308
|
oveq1d |
|
| 752 |
751
|
oveq1d |
|
| 753 |
752
|
oveq2d |
|
| 754 |
753
|
oveq2d |
|
| 755 |
750 754
|
eqtrd |
|
| 756 |
313 6 386
|
mulassd |
|
| 757 |
756
|
oveq2d |
|
| 758 |
757
|
oveq2d |
|
| 759 |
755 758
|
eqtrd |
|
| 760 |
6 386
|
mulcld |
|
| 761 |
8 3 760
|
mulassd |
|
| 762 |
761
|
oveq2d |
|
| 763 |
762
|
oveq2d |
|
| 764 |
759 763
|
eqtrd |
|
| 765 |
764
|
oveq1d |
|
| 766 |
714 765
|
eqtrd |
|
| 767 |
3 760
|
mulcld |
|
| 768 |
8 767
|
mulcld |
|
| 769 |
9 9 768
|
mulassd |
|
| 770 |
769
|
oveq1d |
|
| 771 |
766 770
|
eqtr4d |
|
| 772 |
9 9
|
mulcld |
|
| 773 |
772 8 767
|
mulassd |
|
| 774 |
773
|
oveq1d |
|
| 775 |
771 774
|
eqtr4d |
|
| 776 |
8 29 29
|
expaddd |
|
| 777 |
776
|
oveq1d |
|
| 778 |
777
|
eqcomd |
|
| 779 |
8 259
|
expp1d |
|
| 780 |
778 779
|
eqtr4d |
|
| 781 |
780
|
oveq1d |
|
| 782 |
781
|
oveq1d |
|
| 783 |
775 782
|
eqtrd |
|
| 784 |
266
|
oveq2d |
|
| 785 |
784
|
oveq1d |
|
| 786 |
785
|
oveq1d |
|
| 787 |
783 786
|
eqtrd |
|
| 788 |
271
|
oveq2d |
|
| 789 |
788
|
oveq1d |
|
| 790 |
789
|
oveq1d |
|
| 791 |
787 790
|
eqtrd |
|
| 792 |
445
|
oveq2d |
|
| 793 |
792
|
oveq2d |
|
| 794 |
793
|
eqcomd |
|
| 795 |
3 449 5
|
expaddd |
|
| 796 |
795
|
oveq2d |
|
| 797 |
794 796
|
eqtr4d |
|
| 798 |
5 449
|
nn0addcld |
|
| 799 |
3 798
|
expcld |
|
| 800 |
3 799
|
mulcomd |
|
| 801 |
797 800
|
eqtrd |
|
| 802 |
3 798
|
expp1d |
|
| 803 |
801 802
|
eqtr4d |
|
| 804 |
803
|
oveq2d |
|
| 805 |
804
|
oveq1d |
|
| 806 |
791 805
|
eqtrd |
|
| 807 |
469
|
oveq2d |
|
| 808 |
807
|
oveq1d |
|
| 809 |
808
|
oveq2d |
|
| 810 |
809
|
oveq2d |
|
| 811 |
810
|
oveq1d |
|
| 812 |
806 811
|
eqtrd |
|
| 813 |
586
|
oveq2d |
|
| 814 |
813
|
oveq1d |
|
| 815 |
814
|
oveq2d |
|
| 816 |
815
|
oveq2d |
|
| 817 |
816
|
oveq1d |
|
| 818 |
812 817
|
eqtr4d |
|
| 819 |
3 3 357
|
addassd |
|
| 820 |
819
|
oveq1d |
|
| 821 |
820
|
oveq2d |
|
| 822 |
821
|
oveq2d |
|
| 823 |
822
|
oveq1d |
|
| 824 |
818 823
|
eqtr4d |
|
| 825 |
|
3p3e6 |
|
| 826 |
825
|
a1i |
|
| 827 |
826
|
oveq1d |
|
| 828 |
827
|
oveq1d |
|
| 829 |
828
|
oveq2d |
|
| 830 |
829
|
oveq2d |
|
| 831 |
830
|
oveq1d |
|
| 832 |
824 831
|
eqtrd |
|
| 833 |
649
|
oveq1d |
|
| 834 |
833
|
oveq2d |
|
| 835 |
834
|
oveq2d |
|
| 836 |
835
|
oveq1d |
|
| 837 |
832 836
|
eqtrd |
|
| 838 |
|
7p1e8 |
|
| 839 |
838
|
a1i |
|
| 840 |
839
|
oveq2d |
|
| 841 |
840
|
oveq2d |
|
| 842 |
841
|
oveq1d |
|
| 843 |
837 842
|
eqtrd |
|
| 844 |
6 9 29
|
mulexpd |
|
| 845 |
844
|
oveq1d |
|
| 846 |
845
|
oveq2d |
|
| 847 |
846
|
oveq2d |
|
| 848 |
847
|
oveq2d |
|
| 849 |
843 848
|
eqtrd |
|
| 850 |
3 29 5
|
expmuld |
|
| 851 |
850
|
oveq1d |
|
| 852 |
851
|
oveq1d |
|
| 853 |
852
|
oveq2d |
|
| 854 |
853
|
oveq2d |
|
| 855 |
854
|
eqcomd |
|
| 856 |
8 29 29
|
expmuld |
|
| 857 |
856
|
oveq2d |
|
| 858 |
857
|
oveq1d |
|
| 859 |
858
|
oveq2d |
|
| 860 |
859
|
oveq2d |
|
| 861 |
855 860
|
eqtr4d |
|
| 862 |
861
|
oveq2d |
|
| 863 |
849 862
|
eqtrd |
|
| 864 |
689
|
a1i |
|
| 865 |
864
|
oveq2d |
|
| 866 |
865
|
oveq1d |
|
| 867 |
866
|
oveq1d |
|
| 868 |
867
|
oveq2d |
|
| 869 |
868
|
oveq2d |
|
| 870 |
869
|
oveq2d |
|
| 871 |
863 870
|
eqtrd |
|
| 872 |
469
|
oveq2d |
|
| 873 |
872
|
oveq2d |
|
| 874 |
873
|
oveq1d |
|
| 875 |
874
|
oveq2d |
|
| 876 |
875
|
oveq2d |
|
| 877 |
876
|
oveq2d |
|
| 878 |
871 877
|
eqtrd |
|
| 879 |
441 698
|
mulcld |
|
| 880 |
879 3
|
mulcld |
|
| 881 |
3 880
|
mulcld |
|
| 882 |
8 881
|
mulcomd |
|
| 883 |
3 880
|
mulcomd |
|
| 884 |
883
|
oveq1d |
|
| 885 |
882 884
|
eqtrd |
|
| 886 |
441 698
|
mulcomd |
|
| 887 |
886
|
oveq1d |
|
| 888 |
887
|
oveq1d |
|
| 889 |
888
|
oveq1d |
|
| 890 |
885 889
|
eqtrd |
|
| 891 |
698 441
|
mulcld |
|
| 892 |
891 3
|
mulcld |
|
| 893 |
892 3 8
|
mulassd |
|
| 894 |
890 893
|
eqtrd |
|
| 895 |
891 3 295
|
mulassd |
|
| 896 |
894 895
|
eqtrd |
|
| 897 |
698 441 405
|
mulassd |
|
| 898 |
896 897
|
eqtrd |
|
| 899 |
441 405
|
mulcomd |
|
| 900 |
899
|
oveq2d |
|
| 901 |
898 900
|
eqtrd |
|
| 902 |
411
|
oveq1d |
|
| 903 |
902
|
oveq2d |
|
| 904 |
901 903
|
eqtrd |
|
| 905 |
415
|
oveq1d |
|
| 906 |
905
|
oveq2d |
|
| 907 |
904 906
|
eqtrd |
|
| 908 |
313 3 441
|
mulassd |
|
| 909 |
908
|
oveq2d |
|
| 910 |
907 909
|
eqtrd |
|
| 911 |
3 441
|
mulcld |
|
| 912 |
8 3 911
|
mulassd |
|
| 913 |
912
|
oveq2d |
|
| 914 |
910 913
|
eqtrd |
|
| 915 |
914
|
oveq2d |
|
| 916 |
878 915
|
eqtrd |
|
| 917 |
3 911
|
mulcld |
|
| 918 |
698 8 917
|
mulassd |
|
| 919 |
918
|
oveq2d |
|
| 920 |
916 919
|
eqtr4d |
|
| 921 |
8 697
|
expp1d |
|
| 922 |
921
|
eqcomd |
|
| 923 |
922
|
oveq1d |
|
| 924 |
923
|
oveq2d |
|
| 925 |
920 924
|
eqtrd |
|
| 926 |
788
|
oveq1d |
|
| 927 |
926
|
oveq2d |
|
| 928 |
925 927
|
eqtrd |
|
| 929 |
3 441
|
mulcomd |
|
| 930 |
929
|
oveq2d |
|
| 931 |
3 440
|
expp1d |
|
| 932 |
931
|
oveq2d |
|
| 933 |
930 932
|
eqtr4d |
|
| 934 |
440 458
|
nn0addcld |
|
| 935 |
3 934
|
expcld |
|
| 936 |
3 935
|
mulcomd |
|
| 937 |
933 936
|
eqtrd |
|
| 938 |
3 934
|
expp1d |
|
| 939 |
937 938
|
eqtr4d |
|
| 940 |
939
|
oveq2d |
|
| 941 |
940
|
oveq2d |
|
| 942 |
928 941
|
eqtrd |
|
| 943 |
835
|
oveq2d |
|
| 944 |
942 943
|
eqtrd |
|
| 945 |
841
|
oveq2d |
|
| 946 |
944 945
|
eqtrd |
|
| 947 |
8 609
|
expcld |
|
| 948 |
|
8nn0 |
|
| 949 |
948
|
a1i |
|
| 950 |
3 949
|
expcld |
|
| 951 |
947 950 950
|
adddid |
|
| 952 |
951
|
eqcomd |
|
| 953 |
946 952
|
eqtrd |
|
| 954 |
953
|
oveq1d |
|
| 955 |
954
|
oveq2d |
|
| 956 |
955
|
oveq2d |
|
| 957 |
710 956
|
eqtrd |
|
| 958 |
844
|
oveq1d |
|
| 959 |
958
|
oveq2d |
|
| 960 |
959
|
oveq2d |
|
| 961 |
6
|
sqcld |
|
| 962 |
9
|
sqcld |
|
| 963 |
961 962
|
mulcld |
|
| 964 |
963 12
|
mulcld |
|
| 965 |
3 964
|
mulcld |
|
| 966 |
8 965
|
mulcomd |
|
| 967 |
3 964
|
mulcomd |
|
| 968 |
967
|
oveq1d |
|
| 969 |
966 968
|
eqtrd |
|
| 970 |
961 962
|
mulcomd |
|
| 971 |
970
|
oveq1d |
|
| 972 |
971
|
oveq1d |
|
| 973 |
972
|
oveq1d |
|
| 974 |
969 973
|
eqtrd |
|
| 975 |
962 961
|
mulcld |
|
| 976 |
975 12
|
mulcld |
|
| 977 |
976 3 8
|
mulassd |
|
| 978 |
974 977
|
eqtrd |
|
| 979 |
975 12 295
|
mulassd |
|
| 980 |
978 979
|
eqtrd |
|
| 981 |
12 295
|
mulcld |
|
| 982 |
962 961 981
|
mulassd |
|
| 983 |
980 982
|
eqtrd |
|
| 984 |
961 981
|
mulcomd |
|
| 985 |
984
|
oveq2d |
|
| 986 |
983 985
|
eqtrd |
|
| 987 |
232
|
oveq1d |
|
| 988 |
987
|
oveq1d |
|
| 989 |
988
|
oveq2d |
|
| 990 |
986 989
|
eqtrd |
|
| 991 |
237 295 961
|
mulassd |
|
| 992 |
991
|
oveq2d |
|
| 993 |
990 992
|
eqtrd |
|
| 994 |
295 961
|
mulcld |
|
| 995 |
8 11 994
|
mulassd |
|
| 996 |
995
|
oveq2d |
|
| 997 |
993 996
|
eqtrd |
|
| 998 |
11 994
|
mulcomd |
|
| 999 |
998
|
oveq2d |
|
| 1000 |
999
|
oveq2d |
|
| 1001 |
997 1000
|
eqtrd |
|
| 1002 |
308
|
oveq1d |
|
| 1003 |
1002
|
oveq1d |
|
| 1004 |
1003
|
oveq2d |
|
| 1005 |
1004
|
oveq2d |
|
| 1006 |
1001 1005
|
eqtrd |
|
| 1007 |
313 961 11
|
mulassd |
|
| 1008 |
1007
|
oveq2d |
|
| 1009 |
1008
|
oveq2d |
|
| 1010 |
1006 1009
|
eqtrd |
|
| 1011 |
961 11
|
mulcld |
|
| 1012 |
8 3 1011
|
mulassd |
|
| 1013 |
1012
|
oveq2d |
|
| 1014 |
1013
|
oveq2d |
|
| 1015 |
1010 1014
|
eqtrd |
|
| 1016 |
960 1015
|
eqtrd |
|
| 1017 |
3 1011
|
mulcld |
|
| 1018 |
8 1017
|
mulcld |
|
| 1019 |
962 8 1018
|
mulassd |
|
| 1020 |
1016 1019
|
eqtr4d |
|
| 1021 |
962 8
|
mulcld |
|
| 1022 |
1021 8 1017
|
mulassd |
|
| 1023 |
1020 1022
|
eqtr4d |
|
| 1024 |
856
|
oveq1d |
|
| 1025 |
1024
|
oveq1d |
|
| 1026 |
1025
|
eqcomd |
|
| 1027 |
8 449
|
expp1d |
|
| 1028 |
1027
|
oveq1d |
|
| 1029 |
1026 1028
|
eqtr4d |
|
| 1030 |
8 459
|
expp1d |
|
| 1031 |
1029 1030
|
eqtr4d |
|
| 1032 |
1031
|
oveq1d |
|
| 1033 |
1023 1032
|
eqtrd |
|
| 1034 |
471
|
oveq2d |
|
| 1035 |
1034
|
oveq1d |
|
| 1036 |
1033 1035
|
eqtrd |
|
| 1037 |
369
|
oveq2d |
|
| 1038 |
1037
|
oveq1d |
|
| 1039 |
1036 1038
|
eqtrd |
|
| 1040 |
375
|
oveq2d |
|
| 1041 |
1040
|
oveq1d |
|
| 1042 |
1039 1041
|
eqtrd |
|
| 1043 |
850
|
oveq1d |
|
| 1044 |
1043
|
oveq2d |
|
| 1045 |
1044
|
eqcomd |
|
| 1046 |
3 29 30
|
expaddd |
|
| 1047 |
1046
|
oveq2d |
|
| 1048 |
1045 1047
|
eqtr4d |
|
| 1049 |
30 29
|
nn0addcld |
|
| 1050 |
3 1049
|
expcld |
|
| 1051 |
3 1050
|
mulcomd |
|
| 1052 |
1048 1051
|
eqtrd |
|
| 1053 |
3 1049
|
expp1d |
|
| 1054 |
1052 1053
|
eqtr4d |
|
| 1055 |
1054
|
oveq2d |
|
| 1056 |
1042 1055
|
eqtrd |
|
| 1057 |
864
|
oveq1d |
|
| 1058 |
1057
|
oveq1d |
|
| 1059 |
1058
|
oveq2d |
|
| 1060 |
1059
|
oveq2d |
|
| 1061 |
1056 1060
|
eqtrd |
|
| 1062 |
|
6p2e8 |
|
| 1063 |
1062
|
a1i |
|
| 1064 |
1063
|
oveq1d |
|
| 1065 |
1064
|
oveq2d |
|
| 1066 |
1065
|
oveq2d |
|
| 1067 |
1061 1066
|
eqtrd |
|
| 1068 |
|
8p1e9 |
|
| 1069 |
1068
|
a1i |
|
| 1070 |
1069
|
oveq2d |
|
| 1071 |
1070
|
oveq2d |
|
| 1072 |
1067 1071
|
eqtrd |
|
| 1073 |
1072
|
oveq1d |
|
| 1074 |
1073
|
oveq2d |
|
| 1075 |
957 1074
|
eqtrd |
|
| 1076 |
6 9 5
|
mulexpd |
|
| 1077 |
1076
|
oveq2d |
|
| 1078 |
6 5
|
expcld |
|
| 1079 |
9 5
|
expcld |
|
| 1080 |
1078 1079
|
mulcomd |
|
| 1081 |
1080
|
oveq2d |
|
| 1082 |
1077 1081
|
eqtrd |
|
| 1083 |
8 1079 1078
|
mulassd |
|
| 1084 |
1082 1083
|
eqtr4d |
|
| 1085 |
8 5 29
|
expmuld |
|
| 1086 |
1085
|
oveq2d |
|
| 1087 |
1086
|
eqcomd |
|
| 1088 |
29 5
|
nn0mulcld |
|
| 1089 |
8 1088
|
expcld |
|
| 1090 |
8 1089
|
mulcomd |
|
| 1091 |
1087 1090
|
eqtrd |
|
| 1092 |
8 1088
|
expp1d |
|
| 1093 |
1091 1092
|
eqtr4d |
|
| 1094 |
1093
|
oveq1d |
|
| 1095 |
1084 1094
|
eqtrd |
|
| 1096 |
691
|
oveq1d |
|
| 1097 |
1096
|
oveq2d |
|
| 1098 |
1097
|
oveq1d |
|
| 1099 |
1095 1098
|
eqtrd |
|
| 1100 |
649
|
oveq2d |
|
| 1101 |
1100
|
oveq1d |
|
| 1102 |
1099 1101
|
eqtrd |
|
| 1103 |
1102
|
oveq1d |
|
| 1104 |
1075 1103
|
eqtrd |
|
| 1105 |
3 5 5
|
expmuld |
|
| 1106 |
1105
|
eqcomd |
|
| 1107 |
1106
|
oveq2d |
|
| 1108 |
1107
|
oveq1d |
|
| 1109 |
1104 1108
|
eqtrd |
|
| 1110 |
|
3t3e9 |
|
| 1111 |
1110
|
a1i |
|
| 1112 |
1111
|
oveq2d |
|
| 1113 |
1112
|
oveq2d |
|
| 1114 |
1113
|
oveq1d |
|
| 1115 |
1109 1114
|
eqtrd |
|