| Step | Hyp | Ref | Expression | 
						
							| 1 |  | psdmul.s |  | 
						
							| 2 |  | psdmul.b |  | 
						
							| 3 |  | psdmul.p |  | 
						
							| 4 |  | psdmul.m |  | 
						
							| 5 |  | psdmul.r |  | 
						
							| 6 |  | psdmul.x |  | 
						
							| 7 |  | psdmul.f |  | 
						
							| 8 |  | psdmul.g |  | 
						
							| 9 |  | eqid |  | 
						
							| 10 |  | eqid |  | 
						
							| 11 | 5 | crngringd |  | 
						
							| 12 | 11 | ringcmnd |  | 
						
							| 13 | 12 | adantr |  | 
						
							| 14 |  | simpr |  | 
						
							| 15 |  | reldmpsr |  | 
						
							| 16 | 1 2 15 | strov2rcl |  | 
						
							| 17 | 7 16 | syl |  | 
						
							| 18 |  | eqid |  | 
						
							| 19 | 18 | psrbagsn |  | 
						
							| 20 | 17 19 | syl |  | 
						
							| 21 | 20 | adantr |  | 
						
							| 22 | 18 | psrbagaddcl |  | 
						
							| 23 | 14 21 22 | syl2anc |  | 
						
							| 24 | 18 | psrbaglefi |  | 
						
							| 25 | 23 24 | syl |  | 
						
							| 26 |  | eqid |  | 
						
							| 27 | 5 | crnggrpd |  | 
						
							| 28 | 27 | grpmndd |  | 
						
							| 29 | 28 | ad2antrr |  | 
						
							| 30 | 18 | psrbagf |  | 
						
							| 31 | 30 | adantl |  | 
						
							| 32 | 6 | adantr |  | 
						
							| 33 | 31 32 | ffvelcdmd |  | 
						
							| 34 |  | peano2nn0 |  | 
						
							| 35 | 33 34 | syl |  | 
						
							| 36 | 35 | adantr |  | 
						
							| 37 |  | eqid |  | 
						
							| 38 | 11 | ad2antrr |  | 
						
							| 39 | 1 9 18 2 7 | psrelbas |  | 
						
							| 40 | 39 | ad2antrr |  | 
						
							| 41 |  | elrabi |  | 
						
							| 42 | 41 | adantl |  | 
						
							| 43 | 40 42 | ffvelcdmd |  | 
						
							| 44 | 1 9 18 2 8 | psrelbas |  | 
						
							| 45 | 44 | ad2antrr |  | 
						
							| 46 |  | eqid |  | 
						
							| 47 | 18 46 | psrbagconcl |  | 
						
							| 48 | 23 47 | sylan |  | 
						
							| 49 |  | elrabi |  | 
						
							| 50 | 48 49 | syl |  | 
						
							| 51 | 45 50 | ffvelcdmd |  | 
						
							| 52 | 9 37 38 43 51 | ringcld |  | 
						
							| 53 | 9 26 29 36 52 | mulgnn0cld |  | 
						
							| 54 |  | disjdifr |  | 
						
							| 55 | 54 | a1i |  | 
						
							| 56 |  | 1nn0 |  | 
						
							| 57 |  | 0nn0 |  | 
						
							| 58 | 56 57 | ifcli |  | 
						
							| 59 | 58 | nn0ge0i |  | 
						
							| 60 | 31 | ffvelcdmda |  | 
						
							| 61 | 60 | nn0red |  | 
						
							| 62 | 58 | nn0rei |  | 
						
							| 63 | 62 | a1i |  | 
						
							| 64 | 61 63 | addge01d |  | 
						
							| 65 | 59 64 | mpbii |  | 
						
							| 66 | 65 | ralrimiva |  | 
						
							| 67 | 31 | ffnd |  | 
						
							| 68 | 56 57 | ifcli |  | 
						
							| 69 | 68 | elexi |  | 
						
							| 70 |  | eqid |  | 
						
							| 71 | 69 70 | fnmpti |  | 
						
							| 72 | 71 | a1i |  | 
						
							| 73 | 17 | adantr |  | 
						
							| 74 |  | inidm |  | 
						
							| 75 | 67 72 73 73 74 | offn |  | 
						
							| 76 |  | eqidd |  | 
						
							| 77 |  | eqeq1 |  | 
						
							| 78 | 77 | ifbid |  | 
						
							| 79 | 58 | elexi |  | 
						
							| 80 | 78 70 79 | fvmpt |  | 
						
							| 81 | 80 | adantl |  | 
						
							| 82 | 67 72 73 73 74 76 81 | ofval |  | 
						
							| 83 | 67 75 73 73 74 76 82 | ofrfval |  | 
						
							| 84 | 66 83 | mpbird |  | 
						
							| 85 | 84 | adantr |  | 
						
							| 86 | 17 | ad2antrr |  | 
						
							| 87 | 18 | psrbagf |  | 
						
							| 88 | 87 | adantl |  | 
						
							| 89 | 31 | adantr |  | 
						
							| 90 | 18 | psrbagf |  | 
						
							| 91 | 23 90 | syl |  | 
						
							| 92 | 91 | adantr |  | 
						
							| 93 |  | nn0re |  | 
						
							| 94 |  | nn0re |  | 
						
							| 95 |  | nn0re |  | 
						
							| 96 |  | letr |  | 
						
							| 97 | 93 94 95 96 | syl3an |  | 
						
							| 98 | 97 | adantl |  | 
						
							| 99 | 86 88 89 92 98 | caoftrn |  | 
						
							| 100 | 85 99 | mpan2d |  | 
						
							| 101 | 100 | ss2rabdv |  | 
						
							| 102 |  | undifr |  | 
						
							| 103 | 101 102 | sylib |  | 
						
							| 104 | 103 | eqcomd |  | 
						
							| 105 | 9 10 13 25 53 55 104 | gsummptfidmsplit |  | 
						
							| 106 |  | eqid |  | 
						
							| 107 |  | ovex |  | 
						
							| 108 | 107 | rabex |  | 
						
							| 109 | 108 | rabex |  | 
						
							| 110 | 109 | a1i |  | 
						
							| 111 |  | ovex |  | 
						
							| 112 |  | eqid |  | 
						
							| 113 | 111 112 | fnmpti |  | 
						
							| 114 | 113 | a1i |  | 
						
							| 115 |  | fvexd |  | 
						
							| 116 | 114 25 115 | fndmfifsupp |  | 
						
							| 117 | 9 106 26 110 52 116 13 35 | gsummulg |  | 
						
							| 118 |  | difrab |  | 
						
							| 119 | 118 | eleq2i |  | 
						
							| 120 |  | breq1 |  | 
						
							| 121 |  | breq1 |  | 
						
							| 122 | 121 | notbid |  | 
						
							| 123 | 120 122 | anbi12d |  | 
						
							| 124 | 123 | elrab |  | 
						
							| 125 | 18 | psrbagf |  | 
						
							| 126 | 125 | ffnd |  | 
						
							| 127 | 126 | adantl |  | 
						
							| 128 | 75 | adantr |  | 
						
							| 129 | 17 | ad2antrr |  | 
						
							| 130 |  | eqidd |  | 
						
							| 131 | 67 | adantr |  | 
						
							| 132 | 68 | a1i |  | 
						
							| 133 | 70 132 | fmpti |  | 
						
							| 134 | 133 | a1i |  | 
						
							| 135 | 134 | ffnd |  | 
						
							| 136 | 135 | ad2antrr |  | 
						
							| 137 |  | eqidd |  | 
						
							| 138 | 80 | adantl |  | 
						
							| 139 | 131 136 129 129 74 137 138 | ofval |  | 
						
							| 140 | 127 128 129 129 74 130 139 | ofrfval |  | 
						
							| 141 | 127 131 129 129 74 130 137 | ofrfval |  | 
						
							| 142 | 141 | notbid |  | 
						
							| 143 |  | rexnal |  | 
						
							| 144 | 142 143 | bitr4di |  | 
						
							| 145 | 140 144 | anbi12d |  | 
						
							| 146 | 33 | ad2antrr |  | 
						
							| 147 | 125 | adantl |  | 
						
							| 148 | 6 | adantr |  | 
						
							| 149 | 147 148 | ffvelcdmd |  | 
						
							| 150 | 149 | adantlr |  | 
						
							| 151 | 150 | adantr |  | 
						
							| 152 |  | nn0nlt0 |  | 
						
							| 153 | 146 152 | syl |  | 
						
							| 154 | 31 | adantr |  | 
						
							| 155 | 154 | ffvelcdmda |  | 
						
							| 156 | 155 | nn0cnd |  | 
						
							| 157 | 156 | addridd |  | 
						
							| 158 | 157 | breq2d |  | 
						
							| 159 | 158 | biimpd |  | 
						
							| 160 |  | ifnefalse |  | 
						
							| 161 | 160 | oveq2d |  | 
						
							| 162 | 161 | breq2d |  | 
						
							| 163 | 162 | imbi1d |  | 
						
							| 164 | 159 163 | syl5ibrcom |  | 
						
							| 165 | 164 | imp |  | 
						
							| 166 | 165 | impancom |  | 
						
							| 167 | 166 | necon1bd |  | 
						
							| 168 | 167 | ancrd |  | 
						
							| 169 | 168 | ex |  | 
						
							| 170 | 169 | ralimdva |  | 
						
							| 171 | 170 | anim1d |  | 
						
							| 172 | 171 | imp |  | 
						
							| 173 |  | rexim |  | 
						
							| 174 | 173 | imp |  | 
						
							| 175 |  | fveq2 |  | 
						
							| 176 |  | fveq2 |  | 
						
							| 177 | 175 176 | breq12d |  | 
						
							| 178 | 177 | notbid |  | 
						
							| 179 | 178 | ceqsrexbv |  | 
						
							| 180 | 179 | simprbi |  | 
						
							| 181 | 174 180 | syl |  | 
						
							| 182 | 33 | adantr |  | 
						
							| 183 | 182 | nn0red |  | 
						
							| 184 | 150 | nn0red |  | 
						
							| 185 | 183 184 | ltnled |  | 
						
							| 186 | 185 | biimpar |  | 
						
							| 187 | 181 186 | sylan2 |  | 
						
							| 188 | 172 187 | syldan |  | 
						
							| 189 |  | breq2 |  | 
						
							| 190 | 188 189 | syl5ibcom |  | 
						
							| 191 | 153 190 | mtod |  | 
						
							| 192 | 191 | neqned |  | 
						
							| 193 |  | elnnne0 |  | 
						
							| 194 | 151 192 193 | sylanbrc |  | 
						
							| 195 |  | elfzo0 |  | 
						
							| 196 | 146 194 188 195 | syl3anbrc |  | 
						
							| 197 |  | fzostep1 |  | 
						
							| 198 | 196 197 | syl |  | 
						
							| 199 | 151 | nn0red |  | 
						
							| 200 | 35 | ad2antrr |  | 
						
							| 201 | 200 | nn0red |  | 
						
							| 202 | 6 | ad2antrr |  | 
						
							| 203 |  | iftrue |  | 
						
							| 204 | 176 203 | oveq12d |  | 
						
							| 205 | 175 204 | breq12d |  | 
						
							| 206 | 205 | rspcv |  | 
						
							| 207 | 202 206 | syl |  | 
						
							| 208 | 207 | imp |  | 
						
							| 209 | 208 | adantrr |  | 
						
							| 210 | 199 201 209 | lensymd |  | 
						
							| 211 | 210 | intn3an3d |  | 
						
							| 212 |  | elfzo0 |  | 
						
							| 213 | 211 212 | sylnibr |  | 
						
							| 214 | 198 213 | orcnd |  | 
						
							| 215 | 145 214 | sylbida |  | 
						
							| 216 | 215 | anasss |  | 
						
							| 217 | 124 216 | sylan2b |  | 
						
							| 218 | 119 217 | sylan2b |  | 
						
							| 219 | 218 | oveq1d |  | 
						
							| 220 | 219 | mpteq2dva |  | 
						
							| 221 | 220 | oveq2d |  | 
						
							| 222 | 18 | psrbaglefi |  | 
						
							| 223 | 222 | adantl |  | 
						
							| 224 | 28 | ad2antrr |  | 
						
							| 225 | 35 | adantr |  | 
						
							| 226 | 11 | ad2antrr |  | 
						
							| 227 |  | elrabi |  | 
						
							| 228 | 39 | adantr |  | 
						
							| 229 | 228 | ffvelcdmda |  | 
						
							| 230 | 227 229 | sylan2 |  | 
						
							| 231 | 44 | ad2antrr |  | 
						
							| 232 | 31 | adantr |  | 
						
							| 233 | 232 | ffvelcdmda |  | 
						
							| 234 | 233 | nn0cnd |  | 
						
							| 235 | 227 125 | syl |  | 
						
							| 236 | 235 | adantl |  | 
						
							| 237 | 236 | ffvelcdmda |  | 
						
							| 238 | 237 | nn0cnd |  | 
						
							| 239 | 58 | nn0cni |  | 
						
							| 240 | 239 | a1i |  | 
						
							| 241 | 234 238 240 | subadd23d |  | 
						
							| 242 | 234 240 238 | addsubassd |  | 
						
							| 243 | 241 242 | eqtr4d |  | 
						
							| 244 | 243 | mpteq2dva |  | 
						
							| 245 |  | eqid |  | 
						
							| 246 | 18 245 | psrbagconcl |  | 
						
							| 247 |  | elrabi |  | 
						
							| 248 | 246 247 | syl |  | 
						
							| 249 | 248 | adantll |  | 
						
							| 250 | 18 | psrbagf |  | 
						
							| 251 | 249 250 | syl |  | 
						
							| 252 | 251 | ffnd |  | 
						
							| 253 | 71 | a1i |  | 
						
							| 254 | 17 | ad2antrr |  | 
						
							| 255 | 232 | ffnd |  | 
						
							| 256 | 236 | ffnd |  | 
						
							| 257 |  | eqidd |  | 
						
							| 258 |  | eqidd |  | 
						
							| 259 | 255 256 254 254 74 257 258 | ofval |  | 
						
							| 260 | 80 | adantl |  | 
						
							| 261 | 252 253 254 254 74 259 260 | offval |  | 
						
							| 262 |  | simplr |  | 
						
							| 263 | 20 | ad2antrr |  | 
						
							| 264 | 262 263 22 | syl2anc |  | 
						
							| 265 | 264 90 | syl |  | 
						
							| 266 | 265 | ffnd |  | 
						
							| 267 | 255 253 254 254 74 257 260 | ofval |  | 
						
							| 268 | 266 256 254 254 74 267 258 | offval |  | 
						
							| 269 | 244 261 268 | 3eqtr4d |  | 
						
							| 270 | 18 | psrbagaddcl |  | 
						
							| 271 | 249 263 270 | syl2anc |  | 
						
							| 272 | 269 271 | eqeltrrd |  | 
						
							| 273 | 231 272 | ffvelcdmd |  | 
						
							| 274 | 9 37 226 230 273 | ringcld |  | 
						
							| 275 | 9 26 224 225 274 | mulgnn0cld |  | 
						
							| 276 |  | disjdifr |  | 
						
							| 277 | 276 | a1i |  | 
						
							| 278 |  | simpl |  | 
						
							| 279 | 278 | a1i |  | 
						
							| 280 | 279 | ss2rabi |  | 
						
							| 281 | 280 | a1i |  | 
						
							| 282 |  | undifr |  | 
						
							| 283 | 281 282 | sylib |  | 
						
							| 284 | 283 | eqcomd |  | 
						
							| 285 | 9 10 13 223 275 277 284 | gsummptfidmsplit |  | 
						
							| 286 |  | eldifi |  | 
						
							| 287 | 6 | ad2antrr |  | 
						
							| 288 |  | eqidd |  | 
						
							| 289 |  | eqidd |  | 
						
							| 290 | 255 256 254 254 74 288 289 | ofval |  | 
						
							| 291 | 287 290 | mpdan |  | 
						
							| 292 | 286 291 | sylan2 |  | 
						
							| 293 | 292 | oveq2d |  | 
						
							| 294 | 236 287 | ffvelcdmd |  | 
						
							| 295 | 286 294 | sylan2 |  | 
						
							| 296 | 295 | nn0cnd |  | 
						
							| 297 | 33 | nn0cnd |  | 
						
							| 298 | 297 | adantr |  | 
						
							| 299 | 296 298 | pncan3d |  | 
						
							| 300 | 293 299 | eqtrd |  | 
						
							| 301 | 300 | oveq1d |  | 
						
							| 302 | 251 287 | ffvelcdmd |  | 
						
							| 303 | 286 302 | sylan2 |  | 
						
							| 304 | 303 | nn0cnd |  | 
						
							| 305 |  | 1cnd |  | 
						
							| 306 | 296 304 305 | addassd |  | 
						
							| 307 | 301 306 | eqtr3d |  | 
						
							| 308 | 307 | oveq1d |  | 
						
							| 309 | 28 | ad2antrr |  | 
						
							| 310 |  | peano2nn0 |  | 
						
							| 311 | 302 310 | syl |  | 
						
							| 312 | 286 311 | sylan2 |  | 
						
							| 313 | 286 274 | sylan2 |  | 
						
							| 314 | 9 26 10 | mulgnn0dir |  | 
						
							| 315 | 309 295 312 313 314 | syl13anc |  | 
						
							| 316 | 308 315 | eqtrd |  | 
						
							| 317 | 316 | mpteq2dva |  | 
						
							| 318 | 317 | oveq2d |  | 
						
							| 319 |  | difssd |  | 
						
							| 320 | 223 319 | ssfid |  | 
						
							| 321 | 9 26 224 294 274 | mulgnn0cld |  | 
						
							| 322 | 286 321 | sylan2 |  | 
						
							| 323 | 9 26 224 311 274 | mulgnn0cld |  | 
						
							| 324 | 286 323 | sylan2 |  | 
						
							| 325 |  | eqid |  | 
						
							| 326 |  | eqid |  | 
						
							| 327 | 9 10 13 320 322 324 325 326 | gsummptfidmadd |  | 
						
							| 328 | 318 327 | eqtrd |  | 
						
							| 329 | 6 | ad2antrr |  | 
						
							| 330 | 67 | adantr |  | 
						
							| 331 |  | elrabi |  | 
						
							| 332 | 331 126 | syl |  | 
						
							| 333 | 332 | adantl |  | 
						
							| 334 | 17 | ad2antrr |  | 
						
							| 335 |  | eqidd |  | 
						
							| 336 |  | eqidd |  | 
						
							| 337 | 330 333 334 334 74 335 336 | ofval |  | 
						
							| 338 | 329 337 | mpdan |  | 
						
							| 339 |  | fveq1 |  | 
						
							| 340 | 339 | eqeq1d |  | 
						
							| 341 | 121 340 | anbi12d |  | 
						
							| 342 | 341 | elrab |  | 
						
							| 343 | 342 | simprbi |  | 
						
							| 344 | 343 | simprd |  | 
						
							| 345 | 344 | adantl |  | 
						
							| 346 | 345 | oveq2d |  | 
						
							| 347 | 33 | adantr |  | 
						
							| 348 | 347 | nn0cnd |  | 
						
							| 349 | 348 | subid1d |  | 
						
							| 350 | 338 346 349 | 3eqtrrd |  | 
						
							| 351 | 350 | oveq1d |  | 
						
							| 352 | 351 | oveq1d |  | 
						
							| 353 | 352 | mpteq2dva |  | 
						
							| 354 | 353 | oveq2d |  | 
						
							| 355 | 328 354 | oveq12d |  | 
						
							| 356 | 27 | adantr |  | 
						
							| 357 | 108 | rabex |  | 
						
							| 358 | 357 | difexi |  | 
						
							| 359 | 358 | a1i |  | 
						
							| 360 | 322 | fmpttd |  | 
						
							| 361 |  | ovex |  | 
						
							| 362 | 361 325 | fnmpti |  | 
						
							| 363 | 362 | a1i |  | 
						
							| 364 | 363 320 115 | fndmfifsupp |  | 
						
							| 365 | 9 106 13 359 360 364 | gsumcl |  | 
						
							| 366 | 324 | fmpttd |  | 
						
							| 367 |  | ovex |  | 
						
							| 368 | 367 326 | fnmpti |  | 
						
							| 369 | 368 | a1i |  | 
						
							| 370 | 369 320 115 | fndmfifsupp |  | 
						
							| 371 | 9 106 13 359 366 370 | gsumcl |  | 
						
							| 372 | 108 | rabex |  | 
						
							| 373 | 372 | a1i |  | 
						
							| 374 | 280 | sseli |  | 
						
							| 375 | 374 323 | sylan2 |  | 
						
							| 376 | 375 | fmpttd |  | 
						
							| 377 |  | eqid |  | 
						
							| 378 | 367 377 | fnmpti |  | 
						
							| 379 | 378 | a1i |  | 
						
							| 380 | 223 281 | ssfid |  | 
						
							| 381 | 379 380 115 | fndmfifsupp |  | 
						
							| 382 | 9 106 13 373 376 381 | gsumcl |  | 
						
							| 383 | 9 10 356 365 371 382 | grpassd |  | 
						
							| 384 | 285 355 383 | 3eqtrd |  | 
						
							| 385 | 221 384 | oveq12d |  | 
						
							| 386 | 105 117 385 | 3eqtr3d |  | 
						
							| 387 | 7 | adantr |  | 
						
							| 388 | 8 | adantr |  | 
						
							| 389 | 1 2 37 4 18 387 388 23 | psrmulval |  | 
						
							| 390 | 389 | oveq2d |  | 
						
							| 391 | 109 | difexi |  | 
						
							| 392 | 391 | a1i |  | 
						
							| 393 |  | eldifi |  | 
						
							| 394 | 41 125 | syl |  | 
						
							| 395 | 394 | adantl |  | 
						
							| 396 | 6 | ad2antrr |  | 
						
							| 397 | 395 396 | ffvelcdmd |  | 
						
							| 398 | 9 26 29 397 52 | mulgnn0cld |  | 
						
							| 399 | 393 398 | sylan2 |  | 
						
							| 400 | 399 | fmpttd |  | 
						
							| 401 |  | eqid |  | 
						
							| 402 | 361 401 | fnmpti |  | 
						
							| 403 | 402 | a1i |  | 
						
							| 404 |  | difssd |  | 
						
							| 405 | 25 404 | ssfid |  | 
						
							| 406 | 403 405 115 | fndmfifsupp |  | 
						
							| 407 | 9 106 13 392 400 406 | gsumcl |  | 
						
							| 408 | 9 10 356 371 382 | grpcld |  | 
						
							| 409 | 9 10 356 407 365 408 | grpassd |  | 
						
							| 410 | 386 390 409 | 3eqtr4d |  | 
						
							| 411 | 410 | mpteq2dva |  | 
						
							| 412 | 1 2 4 11 7 8 | psrmulcl |  | 
						
							| 413 | 1 2 18 6 412 | psdval |  | 
						
							| 414 | 27 | grpmgmd |  | 
						
							| 415 | 1 2 414 6 7 | psdcl |  | 
						
							| 416 | 1 2 4 11 415 8 | psrmulcl |  | 
						
							| 417 | 1 2 414 6 8 | psdcl |  | 
						
							| 418 | 1 2 4 11 7 417 | psrmulcl |  | 
						
							| 419 | 1 2 10 3 416 418 | psradd |  | 
						
							| 420 | 1 9 18 2 416 | psrelbas |  | 
						
							| 421 | 420 | ffnd |  | 
						
							| 422 | 1 9 18 2 418 | psrelbas |  | 
						
							| 423 | 422 | ffnd |  | 
						
							| 424 | 108 | a1i |  | 
						
							| 425 |  | inidm |  | 
						
							| 426 | 415 | adantr |  | 
						
							| 427 | 1 2 37 4 18 426 388 14 | psrmulval |  | 
						
							| 428 | 357 | a1i |  | 
						
							| 429 | 11 | ad2antrr |  | 
						
							| 430 |  | elrabi |  | 
						
							| 431 | 1 9 18 2 415 | psrelbas |  | 
						
							| 432 | 431 | adantr |  | 
						
							| 433 | 432 | ffvelcdmda |  | 
						
							| 434 | 430 433 | sylan2 |  | 
						
							| 435 | 44 | ad2antrr |  | 
						
							| 436 | 18 245 | psrbagconcl |  | 
						
							| 437 | 436 | adantll |  | 
						
							| 438 |  | elrabi |  | 
						
							| 439 | 437 438 | syl |  | 
						
							| 440 | 435 439 | ffvelcdmd |  | 
						
							| 441 | 9 37 429 434 440 | ringcld |  | 
						
							| 442 | 441 | fmpttd |  | 
						
							| 443 |  | ovex |  | 
						
							| 444 |  | eqid |  | 
						
							| 445 | 443 444 | fnmpti |  | 
						
							| 446 | 445 | a1i |  | 
						
							| 447 | 446 223 115 | fndmfifsupp |  | 
						
							| 448 |  | eqid |  | 
						
							| 449 |  | df-of |  | 
						
							| 450 |  | vex |  | 
						
							| 451 | 450 | a1i |  | 
						
							| 452 |  | ssv |  | 
						
							| 453 | 452 | a1i |  | 
						
							| 454 |  | ssv |  | 
						
							| 455 | 454 | a1i |  | 
						
							| 456 | 449 451 453 455 | elimampo |  | 
						
							| 457 | 456 | biimpa |  | 
						
							| 458 |  | elrabi |  | 
						
							| 459 | 18 | psrbagf |  | 
						
							| 460 | 459 | ffund |  | 
						
							| 461 | 458 460 | syl |  | 
						
							| 462 | 461 | funfnd |  | 
						
							| 463 | 462 | ad2antrl |  | 
						
							| 464 |  | velsn |  | 
						
							| 465 |  | funmpt |  | 
						
							| 466 |  | funeq |  | 
						
							| 467 | 465 466 | mpbiri |  | 
						
							| 468 | 467 | funfnd |  | 
						
							| 469 | 464 468 | sylbi |  | 
						
							| 470 | 469 | ad2antll |  | 
						
							| 471 |  | vex |  | 
						
							| 472 | 471 | dmex |  | 
						
							| 473 | 472 | a1i |  | 
						
							| 474 |  | vex |  | 
						
							| 475 | 474 | dmex |  | 
						
							| 476 | 475 | a1i |  | 
						
							| 477 |  | eqid |  | 
						
							| 478 |  | eqidd |  | 
						
							| 479 |  | eqidd |  | 
						
							| 480 | 463 470 473 476 477 478 479 | offval |  | 
						
							| 481 | 480 | eqeq2d |  | 
						
							| 482 |  | elsni |  | 
						
							| 483 | 482 | oveq2d |  | 
						
							| 484 | 483 | eqeq2d |  | 
						
							| 485 | 484 | ad2antll |  | 
						
							| 486 | 17 | ad3antrrr |  | 
						
							| 487 | 458 459 | syl |  | 
						
							| 488 | 487 | adantl |  | 
						
							| 489 | 133 | a1i |  | 
						
							| 490 |  | nn0cn |  | 
						
							| 491 |  | nn0cn |  | 
						
							| 492 |  | nn0cn |  | 
						
							| 493 |  | addsubass |  | 
						
							| 494 | 490 491 492 493 | syl3an |  | 
						
							| 495 | 494 | adantl |  | 
						
							| 496 | 486 488 489 489 495 | caofass |  | 
						
							| 497 |  | simpr |  | 
						
							| 498 | 58 | a1i |  | 
						
							| 499 | 70 78 497 498 | fvmptd3 |  | 
						
							| 500 | 135 135 17 17 74 499 499 | offval |  | 
						
							| 501 | 500 | oveq2d |  | 
						
							| 502 | 501 | ad3antrrr |  | 
						
							| 503 | 239 | subidi |  | 
						
							| 504 | 503 | mpteq2i |  | 
						
							| 505 |  | fconstmpt |  | 
						
							| 506 | 504 505 | eqtr4i |  | 
						
							| 507 | 506 | oveq2i |  | 
						
							| 508 |  | 0zd |  | 
						
							| 509 | 490 | addridd |  | 
						
							| 510 | 509 | adantl |  | 
						
							| 511 | 486 488 508 510 | caofid0r |  | 
						
							| 512 | 507 511 | eqtrid |  | 
						
							| 513 | 496 502 512 | 3eqtrd |  | 
						
							| 514 |  | simpr |  | 
						
							| 515 | 513 514 | eqeltrd |  | 
						
							| 516 |  | oveq1 |  | 
						
							| 517 | 516 | eleq1d |  | 
						
							| 518 | 515 517 | syl5ibrcom |  | 
						
							| 519 | 518 | adantrr |  | 
						
							| 520 | 485 519 | sylbid |  | 
						
							| 521 | 481 520 | sylbird |  | 
						
							| 522 | 521 | rexlimdvva |  | 
						
							| 523 | 457 522 | mpd |  | 
						
							| 524 |  | simpr |  | 
						
							| 525 | 17 | mptexd |  | 
						
							| 526 |  | elsng |  | 
						
							| 527 | 525 526 | syl |  | 
						
							| 528 | 70 527 | mpbiri |  | 
						
							| 529 | 528 | ad2antrr |  | 
						
							| 530 | 449 | mpofun |  | 
						
							| 531 | 530 | a1i |  | 
						
							| 532 |  | xpss |  | 
						
							| 533 | 472 | inex1 |  | 
						
							| 534 | 533 | mptex |  | 
						
							| 535 | 534 | rgen2w |  | 
						
							| 536 | 449 | dmmpoga |  | 
						
							| 537 | 535 536 | mp1i |  | 
						
							| 538 | 532 537 | sseqtrrid |  | 
						
							| 539 | 524 529 531 538 | elovimad |  | 
						
							| 540 | 17 | ad2antrr |  | 
						
							| 541 |  | elrabi |  | 
						
							| 542 | 18 | psrbagf |  | 
						
							| 543 | 541 542 | syl |  | 
						
							| 544 | 543 | ad2antll |  | 
						
							| 545 | 133 | a1i |  | 
						
							| 546 | 494 | adantl |  | 
						
							| 547 | 540 544 545 545 546 | caofass |  | 
						
							| 548 | 135 | ad2antrr |  | 
						
							| 549 | 80 | adantl |  | 
						
							| 550 | 548 548 540 540 74 549 549 | offval |  | 
						
							| 551 | 550 | oveq2d |  | 
						
							| 552 | 506 | oveq2i |  | 
						
							| 553 |  | 0zd |  | 
						
							| 554 |  | nn0cn |  | 
						
							| 555 | 554 | addridd |  | 
						
							| 556 | 555 | adantl |  | 
						
							| 557 | 540 544 553 556 | caofid0r |  | 
						
							| 558 | 552 557 | eqtrid |  | 
						
							| 559 | 547 551 558 | 3eqtrrd |  | 
						
							| 560 |  | oveq1 |  | 
						
							| 561 | 560 | eqeq2d |  | 
						
							| 562 | 559 561 | syl5ibrcom |  | 
						
							| 563 | 20 | ad3antrrr |  | 
						
							| 564 | 18 | psrbagaddcl |  | 
						
							| 565 | 458 563 564 | syl2an2 |  | 
						
							| 566 | 18 | psrbagf |  | 
						
							| 567 | 565 566 | syl |  | 
						
							| 568 | 567 | adantrr |  | 
						
							| 569 |  | feq1 |  | 
						
							| 570 | 568 569 | syl5ibrcom |  | 
						
							| 571 | 485 570 | sylbid |  | 
						
							| 572 | 481 571 | sylbird |  | 
						
							| 573 | 572 | rexlimdvva |  | 
						
							| 574 | 457 573 | mpd |  | 
						
							| 575 | 574 | adantrr |  | 
						
							| 576 | 575 | ffvelcdmda |  | 
						
							| 577 | 576 | nn0cnd |  | 
						
							| 578 | 239 | a1i |  | 
						
							| 579 | 577 578 | npcand |  | 
						
							| 580 | 579 | mpteq2dva |  | 
						
							| 581 | 575 | ffnd |  | 
						
							| 582 | 581 548 540 540 74 | offn |  | 
						
							| 583 |  | eqidd |  | 
						
							| 584 | 581 548 540 540 74 583 549 | ofval |  | 
						
							| 585 | 582 548 540 540 74 584 549 | offval |  | 
						
							| 586 | 575 | feqmptd |  | 
						
							| 587 | 580 585 586 | 3eqtr4rd |  | 
						
							| 588 |  | oveq1 |  | 
						
							| 589 | 588 | eqeq2d |  | 
						
							| 590 | 587 589 | syl5ibrcom |  | 
						
							| 591 | 562 590 | impbid |  | 
						
							| 592 | 448 523 539 591 | f1o2d |  | 
						
							| 593 | 9 106 13 428 442 447 592 | gsumf1o |  | 
						
							| 594 | 555 | adantl |  | 
						
							| 595 | 486 488 508 594 | caofid0r |  | 
						
							| 596 | 507 595 | eqtrid |  | 
						
							| 597 | 496 502 596 | 3eqtrd |  | 
						
							| 598 | 597 514 | eqeltrd |  | 
						
							| 599 | 598 517 | syl5ibrcom |  | 
						
							| 600 | 599 | adantrr |  | 
						
							| 601 | 485 600 | sylbid |  | 
						
							| 602 | 481 601 | sylbird |  | 
						
							| 603 | 602 | rexlimdvva |  | 
						
							| 604 | 457 603 | mpd |  | 
						
							| 605 |  | eqidd |  | 
						
							| 606 |  | eqidd |  | 
						
							| 607 |  | fveq2 |  | 
						
							| 608 |  | oveq2 |  | 
						
							| 609 | 608 | fveq2d |  | 
						
							| 610 | 607 609 | oveq12d |  | 
						
							| 611 | 604 605 606 610 | fmptco |  | 
						
							| 612 | 6 | ad2antrr |  | 
						
							| 613 | 7 | ad2antrr |  | 
						
							| 614 |  | elrabi |  | 
						
							| 615 | 604 614 | syl |  | 
						
							| 616 | 1 2 18 612 613 615 | psdcoef |  | 
						
							| 617 | 574 | ffnd |  | 
						
							| 618 | 133 | a1i |  | 
						
							| 619 | 618 | ffnd |  | 
						
							| 620 | 17 | ad2antrr |  | 
						
							| 621 |  | eqidd |  | 
						
							| 622 |  | iftrue |  | 
						
							| 623 |  | 1ex |  | 
						
							| 624 | 622 70 623 | fvmpt |  | 
						
							| 625 | 624 | adantl |  | 
						
							| 626 | 617 619 620 620 74 621 625 | ofval |  | 
						
							| 627 | 612 626 | mpdan |  | 
						
							| 628 | 627 | oveq1d |  | 
						
							| 629 |  | nn0sscn |  | 
						
							| 630 | 629 | a1i |  | 
						
							| 631 | 574 630 | fssd |  | 
						
							| 632 | 631 612 | ffvelcdmd |  | 
						
							| 633 |  | 1cnd |  | 
						
							| 634 | 632 633 | npcand |  | 
						
							| 635 | 628 634 | eqtrd |  | 
						
							| 636 | 617 619 620 620 74 | offn |  | 
						
							| 637 |  | eqidd |  | 
						
							| 638 | 80 | adantl |  | 
						
							| 639 | 617 619 620 620 74 637 638 | ofval |  | 
						
							| 640 | 574 | ffvelcdmda |  | 
						
							| 641 | 640 | nn0cnd |  | 
						
							| 642 | 239 | a1i |  | 
						
							| 643 | 641 642 | npcand |  | 
						
							| 644 | 620 636 619 617 639 638 643 | offveq |  | 
						
							| 645 | 644 | fveq2d |  | 
						
							| 646 | 635 645 | oveq12d |  | 
						
							| 647 | 616 646 | eqtrd |  | 
						
							| 648 | 30 | ad2antlr |  | 
						
							| 649 | 648 | ffvelcdmda |  | 
						
							| 650 | 649 | nn0cnd |  | 
						
							| 651 | 650 641 642 | subsub3d |  | 
						
							| 652 | 651 | mpteq2dva |  | 
						
							| 653 | 67 | adantr |  | 
						
							| 654 |  | eqidd |  | 
						
							| 655 | 653 636 620 620 74 654 639 | offval |  | 
						
							| 656 | 653 619 620 620 74 | offn |  | 
						
							| 657 | 653 619 620 620 74 654 638 | ofval |  | 
						
							| 658 | 656 617 620 620 74 657 637 | offval |  | 
						
							| 659 | 652 655 658 | 3eqtr4d |  | 
						
							| 660 | 659 | fveq2d |  | 
						
							| 661 | 647 660 | oveq12d |  | 
						
							| 662 | 11 | ad2antrr |  | 
						
							| 663 | 574 612 | ffvelcdmd |  | 
						
							| 664 | 663 | nn0zd |  | 
						
							| 665 | 39 | ad2antrr |  | 
						
							| 666 |  | simpllr |  | 
						
							| 667 | 20 | ad3antrrr |  | 
						
							| 668 |  | simprl |  | 
						
							| 669 |  | eqid |  | 
						
							| 670 | 18 245 669 | psrbagleadd1 |  | 
						
							| 671 | 666 667 668 670 | syl3anc |  | 
						
							| 672 |  | eleq1 |  | 
						
							| 673 | 671 672 | syl5ibrcom |  | 
						
							| 674 | 485 673 | sylbid |  | 
						
							| 675 | 481 674 | sylbird |  | 
						
							| 676 | 675 | rexlimdvva |  | 
						
							| 677 | 457 676 | mpd |  | 
						
							| 678 |  | elrabi |  | 
						
							| 679 | 677 678 | syl |  | 
						
							| 680 | 665 679 | ffvelcdmd |  | 
						
							| 681 | 44 | ad2antrr |  | 
						
							| 682 | 23 | adantr |  | 
						
							| 683 | 18 669 | psrbagconcl |  | 
						
							| 684 | 682 677 683 | syl2anc |  | 
						
							| 685 |  | elrabi |  | 
						
							| 686 | 684 685 | syl |  | 
						
							| 687 | 681 686 | ffvelcdmd |  | 
						
							| 688 | 9 26 37 | mulgass2 |  | 
						
							| 689 | 662 664 680 687 688 | syl13anc |  | 
						
							| 690 | 661 689 | eqtrd |  | 
						
							| 691 | 690 | mpteq2dva |  | 
						
							| 692 | 611 691 | eqtrd |  | 
						
							| 693 | 692 | oveq2d |  | 
						
							| 694 |  | snex |  | 
						
							| 695 | 357 694 | xpex |  | 
						
							| 696 | 695 | funimaex |  | 
						
							| 697 | 530 696 | mp1i |  | 
						
							| 698 | 28 | ad2antrr |  | 
						
							| 699 | 9 37 662 680 687 | ringcld |  | 
						
							| 700 | 9 26 698 663 699 | mulgnn0cld |  | 
						
							| 701 |  | eqid |  | 
						
							| 702 | 361 701 | fnmpti |  | 
						
							| 703 | 702 | a1i |  | 
						
							| 704 | 703 25 115 | fndmfifsupp |  | 
						
							| 705 | 462 | ad2antlr |  | 
						
							| 706 | 469 | adantl |  | 
						
							| 707 | 472 | a1i |  | 
						
							| 708 | 475 | a1i |  | 
						
							| 709 |  | eqidd |  | 
						
							| 710 |  | eqidd |  | 
						
							| 711 | 705 706 707 708 477 709 710 | offval |  | 
						
							| 712 | 711 | eqeq2d |  | 
						
							| 713 | 712 | rexbidva |  | 
						
							| 714 | 20 | ad2antrr |  | 
						
							| 715 |  | oveq2 |  | 
						
							| 716 | 715 | eqeq2d |  | 
						
							| 717 | 716 | rexsng |  | 
						
							| 718 | 714 717 | syl |  | 
						
							| 719 | 713 718 | bitr3d |  | 
						
							| 720 | 719 | rexbidva |  | 
						
							| 721 |  | breq1 |  | 
						
							| 722 |  | breq1 |  | 
						
							| 723 |  | fveq1 |  | 
						
							| 724 | 723 | eqeq1d |  | 
						
							| 725 | 722 724 | anbi12d |  | 
						
							| 726 | 725 | notbid |  | 
						
							| 727 | 721 726 | anbi12d |  | 
						
							| 728 | 458 714 564 | syl2an2 |  | 
						
							| 729 |  | simplr |  | 
						
							| 730 |  | simpr |  | 
						
							| 731 | 18 245 46 | psrbagleadd1 |  | 
						
							| 732 | 729 714 730 731 | syl3anc |  | 
						
							| 733 | 721 | elrab |  | 
						
							| 734 | 733 | simprbi |  | 
						
							| 735 | 732 734 | syl |  | 
						
							| 736 | 6 | ad2antrr |  | 
						
							| 737 | 487 | adantl |  | 
						
							| 738 | 737 | ffnd |  | 
						
							| 739 | 135 | ad2antrr |  | 
						
							| 740 | 17 | ad2antrr |  | 
						
							| 741 |  | eqidd |  | 
						
							| 742 | 624 | adantl |  | 
						
							| 743 | 738 739 740 740 74 741 742 | ofval |  | 
						
							| 744 | 736 743 | mpdan |  | 
						
							| 745 | 737 736 | ffvelcdmd |  | 
						
							| 746 |  | nn0p1nn |  | 
						
							| 747 | 745 746 | syl |  | 
						
							| 748 | 744 747 | eqeltrd |  | 
						
							| 749 | 748 | nnne0d |  | 
						
							| 750 | 749 | neneqd |  | 
						
							| 751 | 750 | intnand |  | 
						
							| 752 | 735 751 | jca |  | 
						
							| 753 | 727 728 752 | elrabd |  | 
						
							| 754 |  | eleq1 |  | 
						
							| 755 | 753 754 | syl5ibrcom |  | 
						
							| 756 |  | breq1 |  | 
						
							| 757 |  | elrabi |  | 
						
							| 758 | 757 | adantl |  | 
						
							| 759 | 133 | a1i |  | 
						
							| 760 | 757 125 | syl |  | 
						
							| 761 | 760 | adantl |  | 
						
							| 762 | 6 | ad2antrr |  | 
						
							| 763 | 761 762 | ffvelcdmd |  | 
						
							| 764 | 341 | notbid |  | 
						
							| 765 | 120 764 | anbi12d |  | 
						
							| 766 | 765 | elrab |  | 
						
							| 767 | 766 | simprbi |  | 
						
							| 768 | 767 | simpld |  | 
						
							| 769 | 768 | adantl |  | 
						
							| 770 | 769 | adantr |  | 
						
							| 771 | 757 126 | syl |  | 
						
							| 772 | 771 | adantl |  | 
						
							| 773 | 772 | adantr |  | 
						
							| 774 | 23 | adantr |  | 
						
							| 775 | 90 | ffnd |  | 
						
							| 776 | 774 775 | syl |  | 
						
							| 777 | 776 | adantr |  | 
						
							| 778 | 17 | ad3antrrr |  | 
						
							| 779 |  | eqidd |  | 
						
							| 780 |  | eqidd |  | 
						
							| 781 | 773 777 778 778 74 779 780 | ofrfval |  | 
						
							| 782 | 770 781 | mpbid |  | 
						
							| 783 | 782 | r19.21bi |  | 
						
							| 784 | 783 | adantr |  | 
						
							| 785 | 67 | ad3antrrr |  | 
						
							| 786 | 71 | a1i |  | 
						
							| 787 | 17 | ad4antr |  | 
						
							| 788 |  | eqidd |  | 
						
							| 789 | 80 | adantl |  | 
						
							| 790 | 785 786 787 787 74 788 789 | ofval |  | 
						
							| 791 | 790 | an32s |  | 
						
							| 792 | 160 | adantl |  | 
						
							| 793 | 792 | oveq2d |  | 
						
							| 794 | 31 | ad2antrr |  | 
						
							| 795 | 794 | ffvelcdmda |  | 
						
							| 796 | 795 | adantr |  | 
						
							| 797 | 796 | nn0cnd |  | 
						
							| 798 | 797 | addridd |  | 
						
							| 799 | 791 793 798 | 3eqtrd |  | 
						
							| 800 | 784 799 | breqtrd |  | 
						
							| 801 |  | simpr |  | 
						
							| 802 | 31 | adantr |  | 
						
							| 803 | 802 762 | ffvelcdmd |  | 
						
							| 804 | 803 | nn0ge0d |  | 
						
							| 805 | 804 | adantr |  | 
						
							| 806 | 801 805 | eqbrtrd |  | 
						
							| 807 | 806 | adantr |  | 
						
							| 808 | 177 800 807 | pm2.61ne |  | 
						
							| 809 | 808 | ralrimiva |  | 
						
							| 810 | 67 | adantr |  | 
						
							| 811 | 810 | adantr |  | 
						
							| 812 |  | eqidd |  | 
						
							| 813 | 773 811 778 778 74 779 812 | ofrfval |  | 
						
							| 814 | 809 813 | mpbird |  | 
						
							| 815 | 814 | ex |  | 
						
							| 816 | 767 | simprd |  | 
						
							| 817 | 816 | adantl |  | 
						
							| 818 |  | imnan |  | 
						
							| 819 | 817 818 | sylibr |  | 
						
							| 820 | 819 | con2d |  | 
						
							| 821 | 815 820 | pm2.65d |  | 
						
							| 822 | 821 | neqned |  | 
						
							| 823 | 763 822 193 | sylanbrc |  | 
						
							| 824 | 823 | nnge1d |  | 
						
							| 825 | 824 | adantr |  | 
						
							| 826 | 175 | breq2d |  | 
						
							| 827 | 825 826 | syl5ibrcom |  | 
						
							| 828 | 827 | imp |  | 
						
							| 829 | 761 | ffvelcdmda |  | 
						
							| 830 | 829 | nn0ge0d |  | 
						
							| 831 | 830 | adantr |  | 
						
							| 832 | 828 831 | ifpimpda |  | 
						
							| 833 |  | brif1 |  | 
						
							| 834 | 832 833 | sylibr |  | 
						
							| 835 | 834 | ralrimiva |  | 
						
							| 836 | 71 | a1i |  | 
						
							| 837 | 17 | ad2antrr |  | 
						
							| 838 | 80 | adantl |  | 
						
							| 839 |  | eqidd |  | 
						
							| 840 | 836 772 837 837 74 838 839 | ofrfval |  | 
						
							| 841 | 835 840 | mpbird |  | 
						
							| 842 | 18 | psrbagcon |  | 
						
							| 843 | 758 759 841 842 | syl3anc |  | 
						
							| 844 | 843 | simpld |  | 
						
							| 845 |  | eqidd |  | 
						
							| 846 | 810 836 837 837 74 845 838 | ofval |  | 
						
							| 847 | 772 776 837 837 74 839 846 | ofrfval |  | 
						
							| 848 | 769 847 | mpbid |  | 
						
							| 849 | 848 | r19.21bi |  | 
						
							| 850 | 829 | nn0red |  | 
						
							| 851 | 62 | a1i |  | 
						
							| 852 | 802 | ffvelcdmda |  | 
						
							| 853 | 852 | nn0red |  | 
						
							| 854 | 850 851 853 | lesubaddd |  | 
						
							| 855 | 849 854 | mpbird |  | 
						
							| 856 | 855 | ralrimiva |  | 
						
							| 857 | 772 836 837 837 74 | offn |  | 
						
							| 858 | 772 836 837 837 74 839 838 | ofval |  | 
						
							| 859 | 857 810 837 837 74 858 845 | ofrfval |  | 
						
							| 860 | 856 859 | mpbird |  | 
						
							| 861 | 756 844 860 | elrabd |  | 
						
							| 862 | 829 | nn0cnd |  | 
						
							| 863 | 239 | a1i |  | 
						
							| 864 | 862 863 | npcand |  | 
						
							| 865 | 864 | mpteq2dva |  | 
						
							| 866 | 857 836 837 837 74 858 838 | offval |  | 
						
							| 867 | 761 | feqmptd |  | 
						
							| 868 | 865 866 867 | 3eqtr4rd |  | 
						
							| 869 |  | oveq1 |  | 
						
							| 870 | 869 | eqeq2d |  | 
						
							| 871 | 755 861 868 870 | rspceb2dv |  | 
						
							| 872 | 456 720 871 | 3bitrd |  | 
						
							| 873 | 872 | eqrdv |  | 
						
							| 874 |  | difrab |  | 
						
							| 875 | 873 874 | eqtr4di |  | 
						
							| 876 |  | difssd |  | 
						
							| 877 | 875 876 | eqsstrd |  | 
						
							| 878 | 704 877 115 | fmptssfisupp |  | 
						
							| 879 |  | difss |  | 
						
							| 880 |  | disjdif |  | 
						
							| 881 |  | ssdisj |  | 
						
							| 882 | 879 880 881 | mp2an |  | 
						
							| 883 | 882 | ineqcomi |  | 
						
							| 884 | 883 | a1i |  | 
						
							| 885 | 281 101 | psdmullem |  | 
						
							| 886 | 875 885 | eqtr4d |  | 
						
							| 887 | 9 106 10 13 697 700 878 884 886 | gsumsplit2 |  | 
						
							| 888 | 693 887 | eqtrd |  | 
						
							| 889 | 427 593 888 | 3eqtrd |  | 
						
							| 890 | 417 | adantr |  | 
						
							| 891 | 1 2 37 4 18 387 890 14 | psrmulval |  | 
						
							| 892 | 8 | ad2antrr |  | 
						
							| 893 | 1 2 18 287 892 249 | psdcoef |  | 
						
							| 894 | 269 | fveq2d |  | 
						
							| 895 | 894 | oveq2d |  | 
						
							| 896 | 893 895 | eqtrd |  | 
						
							| 897 | 896 | oveq2d |  | 
						
							| 898 | 311 | nn0zd |  | 
						
							| 899 | 9 26 37 | mulgass3 |  | 
						
							| 900 | 226 898 230 273 899 | syl13anc |  | 
						
							| 901 | 897 900 | eqtrd |  | 
						
							| 902 | 901 | mpteq2dva |  | 
						
							| 903 | 902 | oveq2d |  | 
						
							| 904 | 9 10 13 223 323 277 284 | gsummptfidmsplit |  | 
						
							| 905 | 891 903 904 | 3eqtrd |  | 
						
							| 906 | 421 423 424 424 425 889 905 | offval |  | 
						
							| 907 | 419 906 | eqtrd |  | 
						
							| 908 | 411 413 907 | 3eqtr4d |  |