Step | Hyp | Ref
| Expression |
1 | | dgraalem 29640 |
. . . 4
  degAA    Poly        deg  degAA          |
2 | 1 | simprd 463 |
. . 3
   Poly        deg  degAA         |
3 | | qsscn 11065 |
. . . . . . . 8
 |
4 | | eldifi 3576 |
. . . . . . . . . . . 12
  Poly 
    Poly    |
5 | 4 | ad2antlr 726 |
. . . . . . . . . . 11
    Poly        deg  degAA       
Poly    |
6 | | zssq 11061 |
. . . . . . . . . . . 12
 |
7 | | 0z 10758 |
. . . . . . . . . . . 12
 |
8 | 6, 7 | sselii 3451 |
. . . . . . . . . . 11
 |
9 | | eqid 2451 |
. . . . . . . . . . . 12
coeff  coeff   |
10 | 9 | coef2 21815 |
. . . . . . . . . . 11
  Poly 
 coeff        |
11 | 5, 8, 10 | sylancl 662 |
. . . . . . . . . 10
    Poly        deg  degAA       
coeff        |
12 | | dgrcl 21817 |
. . . . . . . . . . 11
 Poly  deg    |
13 | 5, 12 | syl 16 |
. . . . . . . . . 10
    Poly        deg  degAA       
deg    |
14 | 11, 13 | ffvelrnd 5943 |
. . . . . . . . 9
    Poly        deg  degAA       
 coeff    deg     |
15 | | eldifsni 4099 |
. . . . . . . . . . 11
  Poly 
       |
16 | 15 | ad2antlr 726 |
. . . . . . . . . 10
    Poly        deg  degAA       
   |
17 | | eqid 2451 |
. . . . . . . . . . . . 13
deg  deg   |
18 | 17, 9 | dgreq0 21848 |
. . . . . . . . . . . 12
 Poly   
 coeff    deg      |
19 | 18 | necon3bid 2706 |
. . . . . . . . . . 11
 Poly   
 coeff    deg      |
20 | 5, 19 | syl 16 |
. . . . . . . . . 10
    Poly        deg  degAA       
 
 coeff    deg      |
21 | 16, 20 | mpbid 210 |
. . . . . . . . 9
    Poly        deg  degAA       
 coeff    deg     |
22 | | qreccl 11074 |
. . . . . . . . 9
   coeff    deg    coeff    deg   
  coeff    deg      |
23 | 14, 21, 22 | syl2anc 661 |
. . . . . . . 8
    Poly        deg  degAA       
  coeff    deg      |
24 | | plyconst 21790 |
. . . . . . . 8
 
  coeff    deg         coeff    deg      Poly    |
25 | 3, 23, 24 | sylancr 663 |
. . . . . . 7
    Poly        deg  degAA       
    coeff    deg      Poly    |
26 | | simpl 457 |
. . . . . . . 8
      coeff    deg      Poly  Poly       coeff    deg      Poly    |
27 | | simpr 461 |
. . . . . . . 8
      coeff    deg      Poly  Poly   Poly    |
28 | | qaddcl 11070 |
. . . . . . . . 9
 
     |
29 | 28 | adantl 466 |
. . . . . . . 8
       coeff    deg      Poly 
Poly  
       |
30 | | qmulcl 11072 |
. . . . . . . . 9
 
     |
31 | 30 | adantl 466 |
. . . . . . . 8
       coeff    deg      Poly 
Poly  
       |
32 | 26, 27, 29, 31 | plymul 21802 |
. . . . . . 7
      coeff    deg      Poly  Poly        coeff    deg        Poly    |
33 | 25, 5, 32 | syl2anc 661 |
. . . . . 6
    Poly        deg  degAA       
     coeff    deg        Poly    |
34 | 9 | coef3 21816 |
. . . . . . . . . . 11
 Poly  coeff        |
35 | 5, 34 | syl 16 |
. . . . . . . . . 10
    Poly        deg  degAA       
coeff        |
36 | 35, 13 | ffvelrnd 5943 |
. . . . . . . . 9
    Poly        deg  degAA       
 coeff    deg     |
37 | 36, 21 | reccld 10201 |
. . . . . . . 8
    Poly        deg  degAA       
  coeff    deg      |
38 | 36, 21 | recne0d 10202 |
. . . . . . . 8
    Poly        deg  degAA       
  coeff    deg      |
39 | | dgrmulc 21854 |
. . . . . . . 8
    coeff    deg      coeff    deg   
Poly   deg      coeff    deg         deg    |
40 | 37, 38, 5, 39 | syl3anc 1219 |
. . . . . . 7
    Poly        deg  degAA       
deg      coeff    deg         deg    |
41 | | simprl 755 |
. . . . . . 7
    Poly        deg  degAA       
deg  degAA    |
42 | 40, 41 | eqtrd 2492 |
. . . . . 6
    Poly        deg  degAA       
deg      coeff    deg         degAA    |
43 | | aacn 21899 |
. . . . . . . . 9
   |
44 | 43 | ad2antrr 725 |
. . . . . . . 8
    Poly        deg  degAA       
  |
45 | | ovex 6215 |
. . . . . . . . . 10
  coeff    deg     |
46 | | fnconstg 5696 |
. . . . . . . . . 10
   coeff    deg        coeff    deg        |
47 | 45, 46 | mp1i 12 |
. . . . . . . . 9
    Poly        deg  degAA       
    coeff    deg        |
48 | | plyf 21782 |
. . . . . . . . . 10
 Poly        |
49 | | ffn 5657 |
. . . . . . . . . 10
       |
50 | 5, 48, 49 | 3syl 20 |
. . . . . . . . 9
    Poly        deg  degAA       
  |
51 | | cnex 9464 |
. . . . . . . . . 10
 |
52 | 51 | a1i 11 |
. . . . . . . . 9
    Poly        deg  degAA       
  |
53 | | inidm 3657 |
. . . . . . . . 9
   |
54 | 45 | fvconst2 6032 |
. . . . . . . . . 10
      coeff    deg           coeff    deg      |
55 | 54 | adantl 466 |
. . . . . . . . 9
     Poly        deg  degAA              coeff    deg           coeff    deg      |
56 | | simplrr 760 |
. . . . . . . . 9
     Poly        deg  degAA               |
57 | 47, 50, 52, 52, 53, 55, 56 | ofval 6429 |
. . . . . . . 8
     Poly        deg  degAA               coeff    deg              coeff    deg       |
58 | 44, 57 | mpdan 668 |
. . . . . . 7
    Poly        deg  degAA       
      coeff    deg              coeff    deg       |
59 | 37 | mul01d 9669 |
. . . . . . 7
    Poly        deg  degAA       
   coeff    deg       |
60 | 58, 59 | eqtrd 2492 |
. . . . . 6
    Poly        deg  degAA       
      coeff    deg             |
61 | | coemulc 21838 |
. . . . . . . . 9
    coeff    deg    Poly   coeff      coeff    deg              coeff    deg       coeff     |
62 | 37, 5, 61 | syl2anc 661 |
. . . . . . . 8
    Poly        deg  degAA       
coeff      coeff    deg              coeff    deg       coeff     |
63 | 62 | fveq1d 5791 |
. . . . . . 7
    Poly        deg  degAA       
 coeff      coeff    deg           degAA         coeff    deg       coeff     degAA     |
64 | | dgraacl 29641 |
. . . . . . . . . 10
 degAA    |
65 | 64 | ad2antrr 725 |
. . . . . . . . 9
    Poly        deg  degAA       
degAA    |
66 | 65 | nnnn0d 10737 |
. . . . . . . 8
    Poly        deg  degAA       
degAA    |
67 | | fnconstg 5696 |
. . . . . . . . . 10
   coeff    deg        coeff    deg        |
68 | 45, 67 | mp1i 12 |
. . . . . . . . 9
    Poly        deg  degAA       
    coeff    deg        |
69 | | ffn 5657 |
. . . . . . . . . 10
 coeff      coeff    |
70 | 35, 69 | syl 16 |
. . . . . . . . 9
    Poly        deg  degAA       
coeff    |
71 | | nn0ex 10686 |
. . . . . . . . . 10
 |
72 | 71 | a1i 11 |
. . . . . . . . 9
    Poly        deg  degAA       
  |
73 | | inidm 3657 |
. . . . . . . . 9
   |
74 | 45 | fvconst2 6032 |
. . . . . . . . . 10
 degAA       coeff    deg        degAA     coeff    deg      |
75 | 74 | adantl 466 |
. . . . . . . . 9
     Poly        deg  degAA        degAA        coeff    deg        degAA     coeff    deg      |
76 | | simplrl 759 |
. . . . . . . . . . 11
     Poly        deg  degAA        degAA   deg  degAA    |
77 | 76 | eqcomd 2459 |
. . . . . . . . . 10
     Poly        deg  degAA        degAA   degAA  deg    |
78 | 77 | fveq2d 5793 |
. . . . . . . . 9
     Poly        deg  degAA        degAA    coeff    degAA    coeff    deg     |
79 | 68, 70, 72, 72, 73, 75, 78 | ofval 6429 |
. . . . . . . 8
     Poly        deg  degAA        degAA         coeff    deg       coeff     degAA      coeff    deg     coeff    deg      |
80 | 66, 79 | mpdan 668 |
. . . . . . 7
    Poly        deg  degAA       
  
   coeff    deg       coeff     degAA      coeff    deg     coeff    deg      |
81 | 36, 21 | recid2d 10204 |
. . . . . . 7
    Poly        deg  degAA       
   coeff    deg     coeff    deg      |
82 | 63, 80, 81 | 3eqtrd 2496 |
. . . . . 6
    Poly        deg  degAA       
 coeff      coeff    deg           degAA     |
83 | | fveq2 5789 |
. . . . . . . . 9
      coeff    deg        deg  deg      coeff    deg           |
84 | 83 | eqeq1d 2453 |
. . . . . . . 8
      coeff    deg         deg  degAA  deg      coeff    deg         degAA     |
85 | | fveq1 5788 |
. . . . . . . . 9
      coeff    deg                  coeff    deg             |
86 | 85 | eqeq1d 2453 |
. . . . . . . 8
      coeff    deg                   coeff    deg              |
87 | | fveq2 5789 |
. . . . . . . . . 10
      coeff    deg        coeff  coeff      coeff    deg           |
88 | 87 | fveq1d 5791 |
. . . . . . . . 9
      coeff    deg         coeff    degAA    coeff      coeff    deg           degAA     |
89 | 88 | eqeq1d 2453 |
. . . . . . . 8
      coeff    deg          coeff    degAA    coeff      coeff    deg           degAA      |
90 | 84, 86, 89 | 3anbi123d 1290 |
. . . . . . 7
      coeff    deg          deg  degAA       coeff    degAA   
 deg      coeff    deg         degAA        coeff    deg            coeff      coeff    deg           degAA       |
91 | 90 | rspcev 3169 |
. . . . . 6
       coeff    deg        Poly   deg      coeff    deg         degAA        coeff    deg            coeff      coeff    deg           degAA     
Poly    deg  degAA       coeff    degAA      |
92 | 33, 42, 60, 82, 91 | syl13anc 1221 |
. . . . 5
    Poly        deg  degAA       
 Poly    deg  degAA 
     coeff    degAA      |
93 | 92 | ex 434 |
. . . 4
 
 Poly      
  deg  degAA        Poly    deg  degAA       coeff    degAA       |
94 | 93 | rexlimdva 2937 |
. . 3
  
 Poly        deg  degAA       
Poly    deg  degAA       coeff    degAA       |
95 | 2, 94 | mpd 15 |
. 2
  Poly    deg  degAA 
     coeff    degAA      |
96 | | simp2 989 |
. . . . . . . . . . 11
  deg  degAA       coeff    degAA   
      |
97 | | simp2 989 |
. . . . . . . . . . 11
  deg  degAA       coeff    degAA   
      |
98 | 96, 97 | anim12i 566 |
. . . . . . . . . 10
   deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA                 |
99 | | plyf 21782 |
. . . . . . . . . . . . . . . 16
 Poly        |
100 | | ffn 5657 |
. . . . . . . . . . . . . . . 16
       |
101 | 99, 100 | syl 16 |
. . . . . . . . . . . . . . 15
 Poly    |
102 | 101 | ad2antrr 725 |
. . . . . . . . . . . . . 14
   Poly  Poly  
             |
103 | 48, 49 | syl 16 |
. . . . . . . . . . . . . . 15
 Poly    |
104 | 103 | ad2antlr 726 |
. . . . . . . . . . . . . 14
   Poly  Poly  
             |
105 | 51 | a1i 11 |
. . . . . . . . . . . . . 14
   Poly  Poly  
             |
106 | | simplrl 759 |
. . . . . . . . . . . . . 14
    Poly 
Poly                     |
107 | | simplrr 760 |
. . . . . . . . . . . . . 14
    Poly 
Poly                     |
108 | 102, 104,
105, 105, 53, 106, 107 | ofval 6429 |
. . . . . . . . . . . . 13
    Poly 
Poly                          |
109 | 43, 108 | sylan2 474 |
. . . . . . . . . . . 12
    Poly 
Poly                          |
110 | | 0m0e0 10532 |
. . . . . . . . . . . 12
   |
111 | 109, 110 | syl6eq 2508 |
. . . . . . . . . . 11
    Poly 
Poly                        |
112 | 111 | ex 434 |
. . . . . . . . . 10
   Poly  Poly  
           
          |
113 | 98, 112 | sylan2 474 |
. . . . . . . . 9
   Poly  Poly  
  deg  degAA       coeff    degAA     deg  degAA       coeff    degAA                 |
114 | 113 | com12 31 |
. . . . . . . 8
    Poly 
Poly     deg  degAA       coeff    degAA     deg  degAA       coeff    degAA                |
115 | 114 | impl 620 |
. . . . . . 7
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA               |
116 | | simpll 753 |
. . . . . . . 8
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA     
  |
117 | | simpl 457 |
. . . . . . . . . 10
  Poly 
Poly  
Poly    |
118 | | simpr 461 |
. . . . . . . . . 10
  Poly 
Poly  
Poly    |
119 | 28 | adantl 466 |
. . . . . . . . . 10
   Poly  Poly  
       |
120 | 30 | adantl 466 |
. . . . . . . . . 10
   Poly  Poly  
       |
121 | | 1z 10777 |
. . . . . . . . . . . 12
 |
122 | | zq 11060 |
. . . . . . . . . . . 12
   |
123 | | qnegcl 11071 |
. . . . . . . . . . . 12
    |
124 | 121, 122,
123 | mp2b 10 |
. . . . . . . . . . 11
  |
125 | 124 | a1i 11 |
. . . . . . . . . 10
  Poly 
Poly  
   |
126 | 117, 118,
119, 120, 125 | plysub 21803 |
. . . . . . . . 9
  Poly 
Poly  
 
 Poly    |
127 | 126 | ad2antlr 726 |
. . . . . . . 8
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA         Poly    |
128 | | simplrl 759 |
. . . . . . . . . 10
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA     
Poly    |
129 | | simplrr 760 |
. . . . . . . . . 10
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA      Poly    |
130 | | simprr1 1036 |
. . . . . . . . . . 11
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA      deg  degAA    |
131 | | simprl1 1033 |
. . . . . . . . . . 11
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA      deg  degAA    |
132 | 130, 131 | eqtr4d 2495 |
. . . . . . . . . 10
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA      deg  deg    |
133 | 64 | ad2antrr 725 |
. . . . . . . . . . 11
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA      degAA    |
134 | 131, 133 | eqeltrd 2539 |
. . . . . . . . . 10
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA      deg    |
135 | | simprl3 1035 |
. . . . . . . . . . 11
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA       coeff    degAA     |
136 | 131 | fveq2d 5793 |
. . . . . . . . . . 11
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA       coeff    deg    coeff    degAA     |
137 | 131 | fveq2d 5793 |
. . . . . . . . . . . 12
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA       coeff    deg    coeff    degAA     |
138 | | simprr3 1038 |
. . . . . . . . . . . 12
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA       coeff    degAA     |
139 | 137, 138 | eqtrd 2492 |
. . . . . . . . . . 11
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA       coeff    deg     |
140 | 135, 136,
139 | 3eqtr4d 2502 |
. . . . . . . . . 10
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA       coeff    deg    coeff    deg     |
141 | | eqid 2451 |
. . . . . . . . . . 11
deg  deg   |
142 | 141 | dgrsub2 29629 |
. . . . . . . . . 10
   Poly  Poly  
 deg  deg  deg   coeff    deg    coeff    deg     deg     deg    |
143 | 128, 129,
132, 134, 140, 142 | syl23anc 1226 |
. . . . . . . . 9
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA      deg  
  deg    |
144 | 143, 131 | breqtrd 4414 |
. . . . . . . 8
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA      deg  
  degAA    |
145 | | dgraa0p 29644 |
. . . . . . . 8
  
  Poly  deg  
  degAA          
 
     |
146 | 116, 127,
144, 145 | syl3anc 1219 |
. . . . . . 7
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA             
 
     |
147 | 115, 146 | mpbid 210 |
. . . . . 6
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA            |
148 | | df-0p 21264 |
. . . . . 6

     |
149 | 147, 148 | syl6eq 2508 |
. . . . 5
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA               |
150 | | ofsubeq0 10420 |
. . . . . . . 8
                  
   |
151 | 51, 150 | mp3an1 1302 |
. . . . . . 7
                  
   |
152 | 99, 48, 151 | syl2an 477 |
. . . . . 6
  Poly 
Poly  
       
   |
153 | 152 | ad2antlr 726 |
. . . . 5
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA                 |
154 | 149, 153 | mpbid 210 |
. . . 4
    Poly  Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA     
  |
155 | 154 | ex 434 |
. . 3
  
Poly  Poly       deg  degAA       coeff    degAA     deg  degAA       coeff    degAA        |
156 | 155 | ralrimivva 2904 |
. 2
  Poly   
Poly      deg  degAA 
     coeff    degAA     deg  degAA       coeff    degAA        |
157 | | fveq2 5789 |
. . . . 5
 deg  deg    |
158 | 157 | eqeq1d 2453 |
. . . 4
  deg  degAA 
deg  degAA     |
159 | | fveq1 5788 |
. . . . 5
           |
160 | 159 | eqeq1d 2453 |
. . . 4
             |
161 | | fveq2 5789 |
. . . . . 6
 coeff  coeff    |
162 | 161 | fveq1d 5791 |
. . . . 5
  coeff    degAA    coeff    degAA     |
163 | 162 | eqeq1d 2453 |
. . . 4
   coeff    degAA    coeff    degAA      |
164 | 158, 160,
163 | 3anbi123d 1290 |
. . 3
   deg  degAA 
     coeff    degAA   
 deg  degAA       coeff    degAA       |
165 | 164 | reu4 3250 |
. 2
  Poly    deg  degAA       coeff    degAA   
 
Poly    deg  degAA       coeff    degAA     Poly    Poly      deg  degAA       coeff    degAA     deg  degAA       coeff    degAA         |
166 | 95, 156, 165 | sylanbrc 664 |
1
 
Poly    deg  degAA       coeff    degAA      |