Step | Hyp | Ref
| Expression |
1 | | rabid 2966 |
. . 3
   Poly         coeff    deg    
  Poly         coeff    deg       |
2 | | qsscn 11272 |
. . . . 5
 |
3 | | itgoval 36021 |
. . . . 5

IntgOver 
  Poly         coeff    deg       |
4 | 2, 3 | ax-mp 5 |
. . . 4
IntgOver 
  Poly         coeff    deg      |
5 | 4 | eleq2i 2520 |
. . 3
 IntgOver   
Poly         coeff    deg       |
6 | | aacn 23263 |
. . . . 5
   |
7 | | mpaacl 36013 |
. . . . . 6
 minPolyAA  Poly    |
8 | | mpaaroot 36015 |
. . . . . 6
  minPolyAA       |
9 | | mpaadgr 36014 |
. . . . . . . 8
 deg minPolyAA   degAA    |
10 | 9 | fveq2d 5867 |
. . . . . . 7
  coeff minPolyAA     deg minPolyAA     coeff minPolyAA     degAA     |
11 | | mpaamn 36016 |
. . . . . . 7
  coeff minPolyAA     degAA     |
12 | 10, 11 | eqtrd 2484 |
. . . . . 6
  coeff minPolyAA     deg minPolyAA      |
13 | | fveq1 5862 |
. . . . . . . . 9
 minPolyAA 
     minPolyAA       |
14 | 13 | eqeq1d 2452 |
. . . . . . . 8
 minPolyAA 
    
 minPolyAA        |
15 | | fveq2 5863 |
. . . . . . . . . 10
 minPolyAA 
coeff  coeff minPolyAA     |
16 | | fveq2 5863 |
. . . . . . . . . 10
 minPolyAA 
deg  deg minPolyAA     |
17 | 15, 16 | fveq12d 5869 |
. . . . . . . . 9
 minPolyAA 
 coeff    deg    coeff minPolyAA     deg minPolyAA      |
18 | 17 | eqeq1d 2452 |
. . . . . . . 8
 minPolyAA 
  coeff    deg    coeff minPolyAA     deg minPolyAA       |
19 | 14, 18 | anbi12d 716 |
. . . . . . 7
 minPolyAA 
       coeff    deg      minPolyAA      coeff minPolyAA     deg minPolyAA        |
20 | 19 | rspcev 3149 |
. . . . . 6
  minPolyAA  Poly    minPolyAA      coeff minPolyAA     deg minPolyAA       Poly         coeff    deg      |
21 | 7, 8, 12, 20 | syl12anc 1265 |
. . . . 5
  Poly         coeff    deg      |
22 | 6, 21 | jca 535 |
. . . 4
   Poly         coeff    deg       |
23 | | simpl 459 |
. . . . . . . . 9
  Poly 
      coeff    deg     Poly    |
24 | | coe0 23203 |
. . . . . . . . . . . . . . 15
coeff        |
25 | 24 | fveq1i 5864 |
. . . . . . . . . . . . . 14
 coeff     deg           deg     |
26 | | dgr0 23209 |
. . . . . . . . . . . . . . . 16
deg    |
27 | | 0nn0 10881 |
. . . . . . . . . . . . . . . 16
 |
28 | 26, 27 | eqeltri 2524 |
. . . . . . . . . . . . . . 15
deg    |
29 | | c0ex 9634 |
. . . . . . . . . . . . . . . 16
 |
30 | 29 | fvconst2 6118 |
. . . . . . . . . . . . . . 15
 deg  
       deg      |
31 | 28, 30 | ax-mp 5 |
. . . . . . . . . . . . . 14
       deg     |
32 | 25, 31 | eqtri 2472 |
. . . . . . . . . . . . 13
 coeff     deg     |
33 | | 0ne1 10674 |
. . . . . . . . . . . . 13
 |
34 | 32, 33 | eqnetri 2693 |
. . . . . . . . . . . 12
 coeff     deg     |
35 | | fveq2 5863 |
. . . . . . . . . . . . . 14
  coeff  coeff     |
36 | | fveq2 5863 |
. . . . . . . . . . . . . 14
  deg  deg     |
37 | 35, 36 | fveq12d 5869 |
. . . . . . . . . . . . 13
   coeff    deg    coeff     deg      |
38 | 37 | neeq1d 2682 |
. . . . . . . . . . . 12
    coeff    deg    coeff     deg       |
39 | 34, 38 | mpbiri 237 |
. . . . . . . . . . 11
   coeff    deg     |
40 | 39 | necon2i 2657 |
. . . . . . . . . 10
  coeff    deg      |
41 | 40 | ad2antll 734 |
. . . . . . . . 9
  Poly 
      coeff    deg        |
42 | | eldifsn 4096 |
. . . . . . . . 9
  Poly 
   
 Poly 
    |
43 | 23, 41, 42 | sylanbrc 669 |
. . . . . . . 8
  Poly 
      coeff    deg      Poly        |
44 | | simprl 763 |
. . . . . . . 8
  Poly 
      coeff    deg           |
45 | 43, 44 | jca 535 |
. . . . . . 7
  Poly 
      coeff    deg       Poly             |
46 | 45 | reximi2 2853 |
. . . . . 6
  Poly         coeff    deg      Poly             |
47 | 46 | anim2i 572 |
. . . . 5
   Poly         coeff    deg        Poly              |
48 | | elqaa 23271 |
. . . . 5

   Poly              |
49 | 47, 48 | sylibr 216 |
. . . 4
   Poly         coeff    deg       |
50 | 22, 49 | impbii 191 |
. . 3

  Poly         coeff    deg       |
51 | 1, 5, 50 | 3bitr4ri 282 |
. 2

IntgOver    |
52 | 51 | eqriv 2447 |
1
IntgOver   |