| Step | Hyp | Ref | Expression | 
						
							| 1 |  | 1arithidom.u |  | 
						
							| 2 |  | 1arithidom.i |  | 
						
							| 3 |  | 1arithidom.m |  | 
						
							| 4 |  | 1arithidom.t |  | 
						
							| 5 |  | 1arithidom.j |  | 
						
							| 6 |  | 1arithidom.r |  | 
						
							| 7 |  | 1arithidom.f |  | 
						
							| 8 |  | 1arithidom.g |  | 
						
							| 9 |  | 1arithidom.1 |  | 
						
							| 10 | 6 | idomringd |  | 
						
							| 11 |  | eqid |  | 
						
							| 12 | 1 11 | 1unit |  | 
						
							| 13 | 10 12 | syl |  | 
						
							| 14 |  | oveq1 |  | 
						
							| 15 | 14 | adantl |  | 
						
							| 16 |  | eqid |  | 
						
							| 17 | 10 | adantr |  | 
						
							| 18 | 3 16 | mgpbas |  | 
						
							| 19 | 3 11 | ringidval |  | 
						
							| 20 |  | id |  | 
						
							| 21 | 20 | idomcringd |  | 
						
							| 22 | 3 | crngmgp |  | 
						
							| 23 | 21 22 | syl |  | 
						
							| 24 | 6 23 | syl |  | 
						
							| 25 |  | ovexd |  | 
						
							| 26 |  | eqidd |  | 
						
							| 27 | 26 8 | wrdfd |  | 
						
							| 28 | 6 | adantr |  | 
						
							| 29 |  | simpr |  | 
						
							| 30 | 16 2 28 29 | rprmcl |  | 
						
							| 31 | 30 | ex |  | 
						
							| 32 | 31 | ssrdv |  | 
						
							| 33 | 27 32 | fssd |  | 
						
							| 34 | 13 8 | wrdfsupp |  | 
						
							| 35 | 18 19 24 25 33 34 | gsumcl |  | 
						
							| 36 | 35 | adantr |  | 
						
							| 37 | 16 4 11 17 36 | ringlidmd |  | 
						
							| 38 | 15 37 | eqtrd |  | 
						
							| 39 | 38 | eqeq2d |  | 
						
							| 40 | 13 39 9 | rspcedvd |  | 
						
							| 41 |  | oveq2 |  | 
						
							| 42 | 41 | oveq2d |  | 
						
							| 43 | 42 | eqeq2d |  | 
						
							| 44 | 43 | rexbidv |  | 
						
							| 45 |  | eqeq1 |  | 
						
							| 46 | 45 | anbi2d |  | 
						
							| 47 | 46 | rexbidv |  | 
						
							| 48 | 47 | exbidv |  | 
						
							| 49 | 44 48 | imbi12d |  | 
						
							| 50 |  | oveq2 |  | 
						
							| 51 | 50 | eqeq1d |  | 
						
							| 52 | 51 | rexbidv |  | 
						
							| 53 |  | fveq2 |  | 
						
							| 54 | 53 | oveq2d |  | 
						
							| 55 | 54 | oveq2d |  | 
						
							| 56 |  | eqidd |  | 
						
							| 57 | 56 54 54 | f1oeq123d |  | 
						
							| 58 |  | coeq1 |  | 
						
							| 59 | 58 | oveq2d |  | 
						
							| 60 | 59 | eqeq2d |  | 
						
							| 61 | 57 60 | anbi12d |  | 
						
							| 62 | 55 61 | rexeqbidv |  | 
						
							| 63 | 62 | exbidv |  | 
						
							| 64 | 52 63 | imbi12d |  | 
						
							| 65 | 64 | ralbidv |  | 
						
							| 66 | 65 | imbi2d |  | 
						
							| 67 |  | oveq2 |  | 
						
							| 68 | 67 | eqeq1d |  | 
						
							| 69 | 68 | rexbidv |  | 
						
							| 70 |  | fveq2 |  | 
						
							| 71 | 70 | oveq2d |  | 
						
							| 72 | 71 | oveq2d |  | 
						
							| 73 |  | eqidd |  | 
						
							| 74 | 73 71 71 | f1oeq123d |  | 
						
							| 75 |  | coeq1 |  | 
						
							| 76 | 75 | oveq2d |  | 
						
							| 77 | 76 | eqeq2d |  | 
						
							| 78 | 74 77 | anbi12d |  | 
						
							| 79 | 72 78 | rexeqbidv |  | 
						
							| 80 | 79 | exbidv |  | 
						
							| 81 | 69 80 | imbi12d |  | 
						
							| 82 | 81 | ralbidv |  | 
						
							| 83 | 82 | imbi2d |  | 
						
							| 84 |  | oveq2 |  | 
						
							| 85 | 84 | eqeq1d |  | 
						
							| 86 | 85 | rexbidv |  | 
						
							| 87 |  | fveq2 |  | 
						
							| 88 | 87 | oveq2d |  | 
						
							| 89 | 88 | oveq2d |  | 
						
							| 90 |  | eqidd |  | 
						
							| 91 | 90 88 88 | f1oeq123d |  | 
						
							| 92 |  | coeq1 |  | 
						
							| 93 | 92 | oveq2d |  | 
						
							| 94 | 93 | eqeq2d |  | 
						
							| 95 | 91 94 | anbi12d |  | 
						
							| 96 | 89 95 | rexeqbidv |  | 
						
							| 97 | 96 | exbidv |  | 
						
							| 98 | 86 97 | imbi12d |  | 
						
							| 99 | 98 | ralbidv |  | 
						
							| 100 | 99 | imbi2d |  | 
						
							| 101 |  | oveq2 |  | 
						
							| 102 | 101 | eqeq1d |  | 
						
							| 103 | 102 | rexbidv |  | 
						
							| 104 |  | fveq2 |  | 
						
							| 105 | 104 | oveq2d |  | 
						
							| 106 | 105 | oveq2d |  | 
						
							| 107 |  | eqidd |  | 
						
							| 108 | 107 105 105 | f1oeq123d |  | 
						
							| 109 |  | coeq1 |  | 
						
							| 110 | 109 | oveq2d |  | 
						
							| 111 | 110 | eqeq2d |  | 
						
							| 112 | 108 111 | anbi12d |  | 
						
							| 113 | 106 112 | rexeqbidv |  | 
						
							| 114 | 113 | exbidv |  | 
						
							| 115 | 103 114 | imbi12d |  | 
						
							| 116 | 115 | ralbidv |  | 
						
							| 117 | 116 | imbi2d |  | 
						
							| 118 |  | 0ex |  | 
						
							| 119 | 118 | a1i |  | 
						
							| 120 | 118 | snid |  | 
						
							| 121 | 1 | fvexi |  | 
						
							| 122 |  | mapdm0 |  | 
						
							| 123 | 121 122 | ax-mp |  | 
						
							| 124 | 120 123 | eleqtrri |  | 
						
							| 125 | 124 | a1i |  | 
						
							| 126 |  | f1o0 |  | 
						
							| 127 | 126 | biantrur |  | 
						
							| 128 |  | co02 |  | 
						
							| 129 | 128 | oveq2i |  | 
						
							| 130 |  | of0r |  | 
						
							| 131 | 129 130 | eqtri |  | 
						
							| 132 | 131 | eqeq2i |  | 
						
							| 133 | 127 132 | bitr3i |  | 
						
							| 134 | 133 | a1i |  | 
						
							| 135 |  | simpl |  | 
						
							| 136 | 135 | idomcringd |  | 
						
							| 137 | 136 | ad2antrr |  | 
						
							| 138 |  | simplr |  | 
						
							| 139 | 16 1 | unitcl |  | 
						
							| 140 | 138 139 | syl |  | 
						
							| 141 | 137 22 | syl |  | 
						
							| 142 |  | ovexd |  | 
						
							| 143 |  | eqidd |  | 
						
							| 144 |  | simpl |  | 
						
							| 145 |  | simpr |  | 
						
							| 146 | 16 2 144 145 | rprmcl |  | 
						
							| 147 | 146 | ex |  | 
						
							| 148 | 147 | ssrdv |  | 
						
							| 149 |  | sswrd |  | 
						
							| 150 | 148 149 | syl |  | 
						
							| 151 | 150 | sselda |  | 
						
							| 152 | 151 | ad2antrr |  | 
						
							| 153 | 143 152 | wrdfd |  | 
						
							| 154 | 135 | idomringd |  | 
						
							| 155 | 154 12 | syl |  | 
						
							| 156 | 155 | ad2antrr |  | 
						
							| 157 | 156 152 | wrdfsupp |  | 
						
							| 158 | 18 19 141 142 153 157 | gsumcl |  | 
						
							| 159 |  | simpr |  | 
						
							| 160 | 19 | gsum0 |  | 
						
							| 161 | 160 156 | eqeltrid |  | 
						
							| 162 | 159 161 | eqeltrrd |  | 
						
							| 163 | 1 4 16 | unitmulclb |  | 
						
							| 164 | 163 | biimpa |  | 
						
							| 165 | 137 140 158 162 164 | syl31anc |  | 
						
							| 166 | 165 | simprd |  | 
						
							| 167 | 166 | r19.29an |  | 
						
							| 168 | 16 1 3 136 151 | unitprodclb |  | 
						
							| 169 | 168 | adantr |  | 
						
							| 170 | 167 169 | mpbid |  | 
						
							| 171 | 170 | adantr |  | 
						
							| 172 |  | eqidd |  | 
						
							| 173 |  | simpr |  | 
						
							| 174 | 172 173 | wrdfd |  | 
						
							| 175 | 174 | freld |  | 
						
							| 176 | 175 | ad2antrr |  | 
						
							| 177 |  | simpr |  | 
						
							| 178 |  | relrn0 |  | 
						
							| 179 | 178 | necon3bid |  | 
						
							| 180 | 179 | biimpa |  | 
						
							| 181 | 176 177 180 | syl2anc |  | 
						
							| 182 |  | n0 |  | 
						
							| 183 | 181 182 | sylib |  | 
						
							| 184 |  | simpr |  | 
						
							| 185 | 135 | ad3antrrr |  | 
						
							| 186 | 174 | frnd |  | 
						
							| 187 | 186 | ad2antrr |  | 
						
							| 188 | 187 | sselda |  | 
						
							| 189 | 2 1 185 188 | rprmnunit |  | 
						
							| 190 |  | nelss |  | 
						
							| 191 | 184 189 190 | syl2anc |  | 
						
							| 192 | 183 191 | exlimddv |  | 
						
							| 193 | 171 192 | pm2.65da |  | 
						
							| 194 |  | nne |  | 
						
							| 195 | 193 194 | sylib |  | 
						
							| 196 | 125 134 195 | rspcedvd |  | 
						
							| 197 |  | hash0 |  | 
						
							| 198 | 197 | oveq2i |  | 
						
							| 199 |  | fzo0 |  | 
						
							| 200 | 198 199 | eqtri |  | 
						
							| 201 | 200 | oveq2i |  | 
						
							| 202 | 201 | a1i |  | 
						
							| 203 |  | id |  | 
						
							| 204 | 200 | a1i |  | 
						
							| 205 | 203 204 204 | f1oeq123d |  | 
						
							| 206 |  | coeq2 |  | 
						
							| 207 | 206 | oveq2d |  | 
						
							| 208 | 207 | eqeq2d |  | 
						
							| 209 | 205 208 | anbi12d |  | 
						
							| 210 | 202 209 | rexeqbidv |  | 
						
							| 211 | 119 196 210 | spcedv |  | 
						
							| 212 | 211 | ex |  | 
						
							| 213 | 212 | ralrimiva |  | 
						
							| 214 |  | eqid |  | 
						
							| 215 |  | simp-4r |  | 
						
							| 216 |  | simp-4r |  | 
						
							| 217 | 216 | ad2antrr |  | 
						
							| 218 |  | eqid |  | 
						
							| 219 | 214 215 217 218 | wrdpmtrlast |  | 
						
							| 220 |  | eqid |  | 
						
							| 221 |  | simp-5r |  | 
						
							| 222 | 221 | ad6antr |  | 
						
							| 223 |  | simp-5l |  | 
						
							| 224 | 223 | ad8antr |  | 
						
							| 225 |  | eqidd |  | 
						
							| 226 |  | simp-7r |  | 
						
							| 227 | 226 | ad6antr |  | 
						
							| 228 |  | simplr |  | 
						
							| 229 | 228 | ad10antr |  | 
						
							| 230 | 222 229 | mpd |  | 
						
							| 231 | 217 | ad4antr |  | 
						
							| 232 |  | simp-9r |  | 
						
							| 233 | 215 | ad4antr |  | 
						
							| 234 |  | simpr |  | 
						
							| 235 | 234 | ad6antr |  | 
						
							| 236 |  | simp-6r |  | 
						
							| 237 |  | simp-5r |  | 
						
							| 238 |  | simp-4r |  | 
						
							| 239 |  | simpllr |  | 
						
							| 240 |  | simplr |  | 
						
							| 241 |  | simpr |  | 
						
							| 242 | 1 2 3 4 220 222 224 224 225 227 230 231 232 233 235 236 237 238 239 240 241 | 1arithidomlem1 |  | 
						
							| 243 |  | ovexd |  | 
						
							| 244 |  | vex |  | 
						
							| 245 | 244 | cnvex |  | 
						
							| 246 | 245 | a1i |  | 
						
							| 247 | 243 246 | coexd |  | 
						
							| 248 |  | oveq1 |  | 
						
							| 249 | 248 | eqeq2d |  | 
						
							| 250 | 249 | anbi2d |  | 
						
							| 251 | 121 | a1i |  | 
						
							| 252 |  | ovexd |  | 
						
							| 253 |  | simplr |  | 
						
							| 254 |  | elmapi |  | 
						
							| 255 | 253 254 | syl |  | 
						
							| 256 |  | iswrdi |  | 
						
							| 257 | 255 256 | syl |  | 
						
							| 258 |  | ccatws1len |  | 
						
							| 259 | 257 258 | syl |  | 
						
							| 260 |  | elmapfn |  | 
						
							| 261 |  | hashfn |  | 
						
							| 262 | 253 260 261 | 3syl |  | 
						
							| 263 | 223 | ad10antr |  | 
						
							| 264 |  | lencl |  | 
						
							| 265 | 263 264 | syl |  | 
						
							| 266 |  | hashfzo0 |  | 
						
							| 267 | 265 266 | syl |  | 
						
							| 268 | 262 267 | eqtrd |  | 
						
							| 269 | 268 | oveq1d |  | 
						
							| 270 |  | simprr |  | 
						
							| 271 | 270 | dmeqd |  | 
						
							| 272 |  | f1of |  | 
						
							| 273 |  | iswrdi |  | 
						
							| 274 | 238 272 273 | 3syl |  | 
						
							| 275 |  | eqidd |  | 
						
							| 276 | 275 216 | wrdfd |  | 
						
							| 277 | 276 | ad6antr |  | 
						
							| 278 |  | wrdco |  | 
						
							| 279 | 274 277 278 | syl2anc |  | 
						
							| 280 | 279 | ad2antrr |  | 
						
							| 281 |  | elfzo0 |  | 
						
							| 282 | 281 | simp2bi |  | 
						
							| 283 |  | nnm1nn0 |  | 
						
							| 284 | 233 282 283 | 3syl |  | 
						
							| 285 |  | lenco |  | 
						
							| 286 | 274 277 285 | syl2anc |  | 
						
							| 287 |  | lencl |  | 
						
							| 288 | 274 287 | syl |  | 
						
							| 289 | 286 288 | eqeltrd |  | 
						
							| 290 |  | lencl |  | 
						
							| 291 | 231 290 | syl |  | 
						
							| 292 | 291 | nn0red |  | 
						
							| 293 | 292 | lem1d |  | 
						
							| 294 | 238 272 | syl |  | 
						
							| 295 |  | ffn |  | 
						
							| 296 |  | hashfn |  | 
						
							| 297 | 294 295 296 | 3syl |  | 
						
							| 298 |  | hashfzo0 |  | 
						
							| 299 | 231 290 298 | 3syl |  | 
						
							| 300 | 286 297 299 | 3eqtrrd |  | 
						
							| 301 | 293 300 | breqtrd |  | 
						
							| 302 |  | elfz2nn0 |  | 
						
							| 303 | 284 289 301 302 | syl3anbrc |  | 
						
							| 304 | 303 | ad2antrr |  | 
						
							| 305 |  | pfxfn |  | 
						
							| 306 | 280 304 305 | syl2anc |  | 
						
							| 307 | 306 | fndmd |  | 
						
							| 308 | 222 | idomringd |  | 
						
							| 309 | 308 | ad3antrrr |  | 
						
							| 310 |  | simprl |  | 
						
							| 311 | 16 1 | unitcl |  | 
						
							| 312 | 310 311 | syl |  | 
						
							| 313 | 222 | ad3antrrr |  | 
						
							| 314 |  | simprr |  | 
						
							| 315 | 16 2 313 314 | rprmcl |  | 
						
							| 316 | 16 4 309 312 315 | ringcld |  | 
						
							| 317 |  | eqidd |  | 
						
							| 318 | 317 263 | wrdfd |  | 
						
							| 319 |  | simprl |  | 
						
							| 320 |  | f1of |  | 
						
							| 321 | 319 320 | syl |  | 
						
							| 322 | 318 321 | fcod |  | 
						
							| 323 |  | ovexd |  | 
						
							| 324 |  | inidm |  | 
						
							| 325 | 316 255 322 323 323 324 | off |  | 
						
							| 326 | 325 | fdmd |  | 
						
							| 327 | 271 307 326 | 3eqtr3d |  | 
						
							| 328 | 284 | ad2antrr |  | 
						
							| 329 | 328 265 | fzo0opth |  | 
						
							| 330 | 327 329 | mpbid |  | 
						
							| 331 | 330 | oveq1d |  | 
						
							| 332 | 282 | ad10antlr |  | 
						
							| 333 | 332 | nncnd |  | 
						
							| 334 |  | npcan1 |  | 
						
							| 335 | 333 334 | syl |  | 
						
							| 336 | 331 335 | eqtr3d |  | 
						
							| 337 | 259 269 336 | 3eqtrd |  | 
						
							| 338 | 337 | oveq2d |  | 
						
							| 339 |  | eqidd |  | 
						
							| 340 | 236 | ad2antrr |  | 
						
							| 341 |  | ccatws1cl |  | 
						
							| 342 | 257 340 341 | syl2anc |  | 
						
							| 343 | 339 342 | wrdfd |  | 
						
							| 344 | 338 343 | feq2dd |  | 
						
							| 345 |  | ccatws1len |  | 
						
							| 346 | 263 345 | syl |  | 
						
							| 347 | 346 336 | eqtrd |  | 
						
							| 348 | 347 | oveq2d |  | 
						
							| 349 | 348 | eqcomd |  | 
						
							| 350 | 238 | ad2antrr |  | 
						
							| 351 |  | f1ocnv |  | 
						
							| 352 |  | f1of |  | 
						
							| 353 | 350 351 352 | 3syl |  | 
						
							| 354 | 349 353 | feq2dd |  | 
						
							| 355 | 344 354 | fcod |  | 
						
							| 356 | 251 252 355 | elmapdd |  | 
						
							| 357 | 222 | ad2antrr |  | 
						
							| 358 |  | eqidd |  | 
						
							| 359 | 227 | ad2antrr |  | 
						
							| 360 | 230 | ad2antrr |  | 
						
							| 361 | 231 | ad2antrr |  | 
						
							| 362 | 232 | ad2antrr |  | 
						
							| 363 | 233 | ad2antrr |  | 
						
							| 364 | 235 | ad2antrr |  | 
						
							| 365 | 237 | ad2antrr |  | 
						
							| 366 |  | simp-5r |  | 
						
							| 367 |  | simp-4r |  | 
						
							| 368 |  | simpllr |  | 
						
							| 369 | 1 2 3 4 220 357 263 263 358 359 360 361 362 363 364 340 365 350 366 367 368 253 319 270 | 1arithidomlem2 |  | 
						
							| 370 | 250 356 369 | rspcedvdw |  | 
						
							| 371 |  | f1oeq1 |  | 
						
							| 372 |  | coeq2 |  | 
						
							| 373 | 372 | oveq2d |  | 
						
							| 374 | 373 | eqeq2d |  | 
						
							| 375 | 371 374 | anbi12d |  | 
						
							| 376 | 375 | rexbidv |  | 
						
							| 377 | 247 370 376 | spcedv |  | 
						
							| 378 | 377 | r19.29an |  | 
						
							| 379 | 242 378 | exlimddv |  | 
						
							| 380 |  | simp-7r |  | 
						
							| 381 |  | oveq1 |  | 
						
							| 382 | 381 | eqeq2d |  | 
						
							| 383 | 382 | cbvrexvw |  | 
						
							| 384 | 380 383 | sylib |  | 
						
							| 385 | 379 384 | r19.29a |  | 
						
							| 386 | 385 | anasss |  | 
						
							| 387 | 219 386 | exlimddv |  | 
						
							| 388 |  | eqid |  | 
						
							| 389 |  | simplr |  | 
						
							| 390 | 276 389 | ffvelcdmd |  | 
						
							| 391 | 16 2 388 221 226 234 390 4 1 | rprmasso3 |  | 
						
							| 392 | 387 391 | r19.29a |  | 
						
							| 393 |  | suppssdm |  | 
						
							| 394 |  | eqidd |  | 
						
							| 395 |  | simpllr |  | 
						
							| 396 | 395 150 | syl |  | 
						
							| 397 | 396 | ad2antrr |  | 
						
							| 398 |  | simp-4r |  | 
						
							| 399 | 397 398 | sseldd |  | 
						
							| 400 | 394 399 | wrdfd |  | 
						
							| 401 | 393 400 | fssdm |  | 
						
							| 402 | 21 | ad5antlr |  | 
						
							| 403 |  | simp-5r |  | 
						
							| 404 | 403 | ad2antrr |  | 
						
							| 405 |  | ovexd |  | 
						
							| 406 |  | fvexd |  | 
						
							| 407 | 406 398 | wrdfsupp |  | 
						
							| 408 |  | simp-5r |  | 
						
							| 409 |  | simplr |  | 
						
							| 410 | 16 1 | unitcl |  | 
						
							| 411 | 409 410 | syl |  | 
						
							| 412 | 23 | ad5antlr |  | 
						
							| 413 | 18 19 412 405 400 407 | gsumcl |  | 
						
							| 414 | 16 2 395 403 | rprmcl |  | 
						
							| 415 | 414 | ad2antrr |  | 
						
							| 416 |  | ovexd |  | 
						
							| 417 |  | eqidd |  | 
						
							| 418 | 396 223 | sseldd |  | 
						
							| 419 | 418 | ad2antrr |  | 
						
							| 420 | 417 419 | wrdfd |  | 
						
							| 421 | 406 419 | wrdfsupp |  | 
						
							| 422 | 18 19 412 416 420 421 | gsumcl |  | 
						
							| 423 | 16 388 4 | dvdsrmul |  | 
						
							| 424 | 415 422 423 | syl2anc |  | 
						
							| 425 | 20 | idomringd |  | 
						
							| 426 | 3 | ringmgp |  | 
						
							| 427 | 425 426 | syl |  | 
						
							| 428 | 427 | ad3antlr |  | 
						
							| 429 | 3 4 | mgpplusg |  | 
						
							| 430 | 18 429 | gsumccatsn |  | 
						
							| 431 | 428 418 414 430 | syl3anc |  | 
						
							| 432 | 431 | ad2antrr |  | 
						
							| 433 |  | simpr |  | 
						
							| 434 | 432 433 | eqtr3d |  | 
						
							| 435 | 424 434 | breqtrd |  | 
						
							| 436 | 16 2 388 4 408 404 411 413 435 | rprmdvds |  | 
						
							| 437 | 1 2 388 402 404 409 | rprmndvdsru |  | 
						
							| 438 | 436 437 | orcnd |  | 
						
							| 439 | 16 2 388 11 3 402 404 405 407 400 438 | rprmdvdsprod |  | 
						
							| 440 |  | ssrexv |  | 
						
							| 441 | 401 439 440 | sylc |  | 
						
							| 442 | 383 | biimpi |  | 
						
							| 443 | 442 | adantl |  | 
						
							| 444 | 441 443 | r19.29a |  | 
						
							| 445 | 392 444 | r19.29a |  | 
						
							| 446 | 445 | ex |  | 
						
							| 447 | 446 | ralrimiva |  | 
						
							| 448 |  | f1oeq1 |  | 
						
							| 449 |  | coeq2 |  | 
						
							| 450 | 449 | oveq2d |  | 
						
							| 451 | 450 | eqeq2d |  | 
						
							| 452 | 448 451 | anbi12d |  | 
						
							| 453 | 452 | rexbidv |  | 
						
							| 454 | 453 | cbvexvw |  | 
						
							| 455 |  | oveq1 |  | 
						
							| 456 | 455 | eqeq2d |  | 
						
							| 457 | 456 | anbi2d |  | 
						
							| 458 | 457 | cbvrexvw |  | 
						
							| 459 | 458 | exbii |  | 
						
							| 460 | 454 459 | bitri |  | 
						
							| 461 | 460 | imbi2i |  | 
						
							| 462 | 461 | ralbii |  | 
						
							| 463 |  | oveq2 |  | 
						
							| 464 | 463 | oveq2d |  | 
						
							| 465 | 464 | eqeq2d |  | 
						
							| 466 | 465 | rexbidv |  | 
						
							| 467 |  | eqeq1 |  | 
						
							| 468 | 467 | anbi2d |  | 
						
							| 469 | 468 | rexbidv |  | 
						
							| 470 | 469 | exbidv |  | 
						
							| 471 | 466 470 | imbi12d |  | 
						
							| 472 | 471 | cbvralvw |  | 
						
							| 473 | 462 472 | bitri |  | 
						
							| 474 | 447 473 | sylibr |  | 
						
							| 475 | 474 | exp31 |  | 
						
							| 476 | 66 83 100 117 213 475 | wrdind |  | 
						
							| 477 | 7 6 476 | sylc |  | 
						
							| 478 | 49 477 8 | rspcdva |  | 
						
							| 479 | 40 478 | mpd |  | 
						
							| 480 | 5 | oveq2i |  | 
						
							| 481 |  | f1oeq23 |  | 
						
							| 482 | 5 5 481 | mp2an |  | 
						
							| 483 | 482 | anbi1i |  | 
						
							| 484 | 480 483 | rexeqbii |  | 
						
							| 485 | 484 | exbii |  | 
						
							| 486 | 479 485 | sylibr |  |