Step | Hyp | Ref
| Expression |
1 | | eldiophelnn0 35606 |
. 2
 Dioph 
  |
2 | | eldioph4b.a |
. . . . . 6
 |
3 | | ovex 6318 |
. . . . . 6
     |
4 | 2, 3 | unex 6589 |
. . . . 5
       |
5 | 4 | jctr 545 |
. . . 4



        |
6 | | eldioph4b.b |
. . . . . . 7
 |
7 | 6 | intnanr 926 |
. . . . . 6

      |
8 | | unfir 7839 |
. . . . . 6
       
       |
9 | 7, 8 | mto 180 |
. . . . 5

      |
10 | | ssun2 3598 |
. . . . 5
    
      |
11 | 9, 10 | pm3.2i 457 |
. . . 4
           
       |
12 | | eldioph2b 35605 |
. . . 4
          
         
         Dioph   mzPoly 
          
                       |
13 | 5, 11, 12 | sylancl 668 |
. . 3

 Dioph   mzPoly            
                       |
14 | | elmapssres 7496 |
. . . . . . . . . . . . . . 15
             
                     |
15 | 10, 14 | mpan2 677 |
. . . . . . . . . . . . . 14
  
     
              |
16 | 15 | adantr 467 |
. . . . . . . . . . . . 13
                             |
17 | | ssun1 3597 |
. . . . . . . . . . . . . . . 16

      |
18 | | elmapssres 7496 |
. . . . . . . . . . . . . . . 16
                       |
19 | 17, 18 | mpan2 677 |
. . . . . . . . . . . . . . 15
  
     
      |
20 | 19 | adantr 467 |
. . . . . . . . . . . . . 14
                     |
21 | | uncom 3578 |
. . . . . . . . . . . . . . . . . . 19
 
                   |
22 | | resundi 5118 |
. . . . . . . . . . . . . . . . . . 19
         
         |
23 | 21, 22 | eqtr4i 2476 |
. . . . . . . . . . . . . . . . . 18
 
         
       |
24 | | elmapi 7493 |
. . . . . . . . . . . . . . . . . . 19
  
     
            |
25 | | ffn 5728 |
. . . . . . . . . . . . . . . . . . 19
                   |
26 | | fnresdm 5685 |
. . . . . . . . . . . . . . . . . . 19
                 |
27 | 24, 25, 26 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
  
     
          |
28 | 23, 27 | syl5eq 2497 |
. . . . . . . . . . . . . . . . 17
  
     
            |
29 | 28 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
  
     
                    |
30 | 29 | eqeq1d 2453 |
. . . . . . . . . . . . . . 15
  
     
                      |
31 | 30 | biimpar 488 |
. . . . . . . . . . . . . 14
                               |
32 | | uneq2 3582 |
. . . . . . . . . . . . . . . . 17
                       |
33 | 32 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
                               |
34 | 33 | eqeq1d 2453 |
. . . . . . . . . . . . . . 15
               
                 |
35 | 34 | rspcev 3150 |
. . . . . . . . . . . . . 14
                    
                  |
36 | 20, 31, 35 | syl2anc 667 |
. . . . . . . . . . . . 13
                                 |
37 | 16, 36 | jca 535 |
. . . . . . . . . . . 12
                                               |
38 | | eleq1 2517 |
. . . . . . . . . . . . 13
             
               |
39 | | uneq1 3581 |
. . . . . . . . . . . . . . . 16
                   |
40 | 39 | fveq2d 5869 |
. . . . . . . . . . . . . . 15
                           |
41 | 40 | eqeq1d 2453 |
. . . . . . . . . . . . . 14
                             |
42 | 41 | rexbidv 2901 |
. . . . . . . . . . . . 13
        
        
                   |
43 | 38, 42 | anbi12d 717 |
. . . . . . . . . . . 12
                                                           |
44 | 37, 43 | syl5ibrcom 226 |
. . . . . . . . . . 11
                                           |
45 | 44 | expimpd 608 |
. . . . . . . . . 10
  
     
                                  |
46 | 45 | ancomsd 456 |
. . . . . . . . 9
  
     
                                  |
47 | 46 | rexlimiv 2873 |
. . . . . . . 8
                                           |
48 | | uncom 3578 |
. . . . . . . . . . . 12
     |
49 | | fz1ssnn 11830 |
. . . . . . . . . . . . . . . . . . . 20
     |
50 | | sslin 3658 |
. . . . . . . . . . . . . . . . . . . 20
    
      
   |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
      
  |
52 | | eldioph4b.c |
. . . . . . . . . . . . . . . . . . 19
   |
53 | 51, 52 | sseqtri 3464 |
. . . . . . . . . . . . . . . . . 18
       |
54 | | ss0 3765 |
. . . . . . . . . . . . . . . . . 18
      
        |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
       |
56 | 55 | reseq2i 5102 |
. . . . . . . . . . . . . . . 16
           |
57 | | res0 5109 |
. . . . . . . . . . . . . . . 16
   |
58 | 56, 57 | eqtri 2473 |
. . . . . . . . . . . . . . 15
         |
59 | 55 | reseq2i 5102 |
. . . . . . . . . . . . . . . 16
           |
60 | | res0 5109 |
. . . . . . . . . . . . . . . 16
   |
61 | 59, 60 | eqtri 2473 |
. . . . . . . . . . . . . . 15
         |
62 | 58, 61 | eqtr4i 2476 |
. . . . . . . . . . . . . 14
                 |
63 | | elmapresaun 35613 |
. . . . . . . . . . . . . 14
   
                      
            |
64 | 62, 63 | mp3an3 1353 |
. . . . . . . . . . . . 13
   
                   |
65 | 64 | ancoms 455 |
. . . . . . . . . . . 12
       
               |
66 | 48, 65 | syl5eqel 2533 |
. . . . . . . . . . 11
       
               |
67 | 66 | adantr 467 |
. . . . . . . . . 10
                      
        |
68 | 48 | reseq1i 5101 |
. . . . . . . . . . . 12
                 |
69 | | elmapresaunres2 35614 |
. . . . . . . . . . . . . 14
   
                      
          |
70 | 62, 69 | mp3an3 1353 |
. . . . . . . . . . . . 13
   
                 |
71 | 70 | ancoms 455 |
. . . . . . . . . . . 12
       
             |
72 | 68, 71 | syl5req 2498 |
. . . . . . . . . . 11
       
             |
73 | 72 | adantr 467 |
. . . . . . . . . 10
                             |
74 | | simpr 463 |
. . . . . . . . . 10
                           |
75 | | reseq1 5099 |
. . . . . . . . . . . . 13
                   |
76 | 75 | eqeq2d 2461 |
. . . . . . . . . . . 12
         
           |
77 | | fveq2 5865 |
. . . . . . . . . . . . 13
               |
78 | 77 | eqeq1d 2453 |
. . . . . . . . . . . 12
                 |
79 | 76, 78 | anbi12d 717 |
. . . . . . . . . . 11
     
                             |
80 | 79 | rspcev 3150 |
. . . . . . . . . 10
                            
  
                     |
81 | 67, 73, 74, 80 | syl12anc 1266 |
. . . . . . . . 9
                     
                     |
82 | 81 | r19.29an 2931 |
. . . . . . . 8
                   
                       |
83 | 47, 82 | impbii 191 |
. . . . . . 7
                      
                    |
84 | 83 | abbii 2567 |
. . . . . 6
   
                            
            |
85 | | df-rab 2746 |
. . . . . 6
       
                  
            |
86 | 84, 85 | eqtr4i 2476 |
. . . . 5
   
                                       |
87 | 86 | eqeq2i 2463 |
. . . 4
             
          
                    |
88 | 87 | rexbii 2889 |
. . 3
  mzPoly 
          
                   
 mzPoly                             |
89 | 13, 88 | syl6bb 265 |
. 2

 Dioph   mzPoly                              |
90 | 1, 89 | biadan2 648 |
1
 Dioph  
 mzPoly                              |