Step | Hyp | Ref
| Expression |
1 | | aasscn 23350 |
. . . 4
 |
2 | | eldifi 3544 |
. . . 4
       |
3 | 1, 2 | sseldi 3416 |
. . 3
       |
4 | | elaa 23348 |
. . . . . 6

   Poly              |
5 | 2, 4 | sylib 201 |
. . . . 5
        Poly              |
6 | 5 | simprd 470 |
. . . 4
       Poly             |
7 | 2 | 3ad2ant1 1051 |
. . . . . 6
       Poly          
  |
8 | | eldifsni 4089 |
. . . . . . 7
       |
9 | 8 | 3ad2ant1 1051 |
. . . . . 6
       Poly             |
10 | | eldifi 3544 |
. . . . . . 7
  Poly 
    Poly    |
11 | 10 | 3ad2ant2 1052 |
. . . . . 6
       Poly           Poly    |
12 | | eldifsni 4089 |
. . . . . . 7
  Poly 
       |
13 | 12 | 3ad2ant2 1052 |
. . . . . 6
       Poly              |
14 | | simp3 1032 |
. . . . . 6
       Poly                 |
15 | | fveq2 5879 |
. . . . . . . . 9
  coeff      coeff       |
16 | 15 | neeq1d 2702 |
. . . . . . . 8
   coeff    
 coeff        |
17 | 16 | cbvrabv 3030 |
. . . . . . 7
  coeff      
 coeff       |
18 | 17 | infeq1i 8012 |
. . . . . 6
inf   coeff        inf 
 coeff         |
19 | | oveq1 6315 |
. . . . . . . 8
 
inf   coeff          inf 
 coeff           |
20 | 19 | fveq2d 5883 |
. . . . . . 7
  coeff     inf 
 coeff           coeff    
inf   coeff            |
21 | 20 | cbvmptv 4488 |
. . . . . 6

 coeff    
inf   coeff           
 coeff    
inf   coeff            |
22 | | eqid 2471 |
. . . . . 6
      deg  inf 
 coeff               coeff     inf 
 coeff                          deg  inf   coeff             
 coeff    
inf   coeff                     |
23 | 7, 9, 11, 13, 14, 18, 21, 22 | elaa2lem 38209 |
. . . . 5
       Poly           
Poly     coeff            |
24 | 23 | rexlimdv3a 2873 |
. . . 4
        Poly          
 Poly     coeff             |
25 | 6, 24 | mpd 15 |
. . 3
      Poly     coeff            |
26 | 3, 25 | jca 541 |
. 2
       Poly     coeff             |
27 | | simpl 464 |
. . . . . . . . 9
  Poly 
 coeff      Poly    |
28 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
  coeff  coeff     |
29 | | coe0 23289 |
. . . . . . . . . . . . . . 15
coeff        |
30 | 28, 29 | syl6eq 2521 |
. . . . . . . . . . . . . 14
  coeff        |
31 | 30 | fveq1d 5881 |
. . . . . . . . . . . . 13
   coeff               |
32 | | 0nn0 10908 |
. . . . . . . . . . . . . 14
 |
33 | | fvconst2g 6134 |
. . . . . . . . . . . . . 14
 
           |
34 | 32, 32, 33 | mp2an 686 |
. . . . . . . . . . . . 13
         |
35 | 31, 34 | syl6eq 2521 |
. . . . . . . . . . . 12
   coeff       |
36 | 35 | adantl 473 |
. . . . . . . . . . 11
   Poly   coeff         coeff       |
37 | | neneq 2649 |
. . . . . . . . . . . 12
  coeff    
 coeff       |
38 | 37 | ad2antlr 741 |
. . . . . . . . . . 11
   Poly   coeff       
 coeff       |
39 | 36, 38 | pm2.65da 586 |
. . . . . . . . . 10
  Poly 
 coeff     
   |
40 | | elsn 3973 |
. . . . . . . . . 10
       |
41 | 39, 40 | sylnibr 312 |
. . . . . . . . 9
  Poly 
 coeff     
     |
42 | 27, 41 | eldifd 3401 |
. . . . . . . 8
  Poly 
 coeff       Poly        |
43 | 42 | adantrr 731 |
. . . . . . 7
  Poly 
  coeff    
       Poly        |
44 | | simprr 774 |
. . . . . . 7
  Poly 
  coeff    
            |
45 | 43, 44 | jca 541 |
. . . . . 6
  Poly 
  coeff    
        Poly             |
46 | 45 | reximi2 2851 |
. . . . 5
  Poly     coeff            Poly             |
47 | 46 | anim2i 579 |
. . . 4
   Poly     coeff          
   Poly              |
48 | | elaa 23348 |
. . . 4

   Poly              |
49 | 47, 48 | sylibr 217 |
. . 3
   Poly     coeff          
  |
50 | | simpr 468 |
. . . 4
   Poly     coeff          
 Poly     coeff            |
51 | | nfv 1769 |
. . . . . 6
  |
52 | | nfre1 2846 |
. . . . . 6
   Poly     coeff           |
53 | 51, 52 | nfan 2031 |
. . . . 5
    Poly     coeff            |
54 | | nfv 1769 |
. . . . 5
    |
55 | | simpl3r 1086 |
. . . . . . . . 9
   Poly 
  coeff    
      
      |
56 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
57 | | eqid 2471 |
. . . . . . . . . . . . . . . 16
coeff  coeff   |
58 | 57 | coefv0 23281 |
. . . . . . . . . . . . . . 15
 Poly       coeff       |
59 | 56, 58 | sylan9eqr 2527 |
. . . . . . . . . . . . . 14
  Poly 
      coeff       |
60 | 59 | adantlr 729 |
. . . . . . . . . . . . 13
   Poly   coeff            coeff       |
61 | | simplr 770 |
. . . . . . . . . . . . 13
   Poly   coeff        coeff       |
62 | 60, 61 | eqnetrd 2710 |
. . . . . . . . . . . 12
   Poly   coeff             |
63 | 62 | neneqd 2648 |
. . . . . . . . . . 11
   Poly   coeff             |
64 | 63 | adantlrr 735 |
. . . . . . . . . 10
   Poly    coeff    
      
      |
65 | 64 | 3adantl1 1186 |
. . . . . . . . 9
   Poly 
  coeff    
      
      |
66 | 55, 65 | pm2.65da 586 |
. . . . . . . 8
 
Poly    coeff          
  |
67 | | elsncg 3983 |
. . . . . . . . . 10
 
     |
68 | 67 | biimpa 492 |
. . . . . . . . 9
 
     |
69 | 68 | 3ad2antl1 1192 |
. . . . . . . 8
   Poly 
  coeff    
        
  |
70 | 66, 69 | mtand 671 |
. . . . . . 7
 
Poly    coeff          
    |
71 | 70 | 3exp 1230 |
. . . . . 6
  Poly 
   coeff    
    
      |
72 | 71 | adantr 472 |
. . . . 5
   Poly     coeff          
 Poly     coeff         
      |
73 | 53, 54, 72 | rexlimd 2866 |
. . . 4
   Poly     coeff          
 
Poly     coeff         
     |
74 | 50, 73 | mpd 15 |
. . 3
   Poly     coeff          
    |
75 | 49, 74 | eldifd 3401 |
. 2
   Poly     coeff          

     |
76 | 26, 75 | impbii 192 |
1
       Poly     coeff             |