Step | Hyp | Ref
| Expression |
1 | | plyssc 23956 |
. . . . . . . . 9
Poly Poly |
2 | | simp2 1062 |
. . . . . . . . 9
Poly Poly
Poly |
3 | 1, 2 | sseldi 3601 |
. . . . . . . 8
Poly Poly
Poly |
4 | | simp1 1061 |
. . . . . . . . . 10
Poly Poly
Poly |
5 | 1, 4 | sseldi 3601 |
. . . . . . . . 9
Poly Poly
Poly |
6 | | quotcan.1 |
. . . . . . . . . . . 12
|
7 | | plymulcl 23977 |
. . . . . . . . . . . 12
Poly Poly
Poly |
8 | 6, 7 | syl5eqel 2705 |
. . . . . . . . . . 11
Poly Poly
Poly |
9 | 8 | 3adant3 1081 |
. . . . . . . . . 10
Poly Poly
Poly |
10 | | simp3 1063 |
. . . . . . . . . 10
Poly Poly
|
11 | | quotcl2 24057 |
. . . . . . . . . 10
Poly
Poly
quot Poly |
12 | 9, 3, 10, 11 | syl3anc 1326 |
. . . . . . . . 9
Poly Poly
quot Poly |
13 | | plysubcl 23978 |
. . . . . . . . 9
Poly
quot Poly quot Poly |
14 | 5, 12, 13 | syl2anc 693 |
. . . . . . . 8
Poly Poly
quot Poly |
15 | | plymul0or 24036 |
. . . . . . . 8
Poly
quot Poly
quot
quot |
16 | 3, 14, 15 | syl2anc 693 |
. . . . . . 7
Poly Poly
quot
quot |
17 | | cnex 10017 |
. . . . . . . . . . . . 13
|
18 | 17 | a1i 11 |
. . . . . . . . . . . 12
Poly Poly
|
19 | | plyf 23954 |
. . . . . . . . . . . . 13
Poly
|
20 | 4, 19 | syl 17 |
. . . . . . . . . . . 12
Poly Poly
|
21 | | plyf 23954 |
. . . . . . . . . . . . 13
Poly
|
22 | 2, 21 | syl 17 |
. . . . . . . . . . . 12
Poly Poly
|
23 | | mulcom 10022 |
. . . . . . . . . . . . 13
|
24 | 23 | adantl 482 |
. . . . . . . . . . . 12
Poly Poly
|
25 | 18, 20, 22, 24 | caofcom 6929 |
. . . . . . . . . . 11
Poly Poly
|
26 | 6, 25 | syl5eq 2668 |
. . . . . . . . . 10
Poly Poly
|
27 | 26 | oveq1d 6665 |
. . . . . . . . 9
Poly Poly
quot
quot |
28 | | plyf 23954 |
. . . . . . . . . . 11
quot Poly quot |
29 | 12, 28 | syl 17 |
. . . . . . . . . 10
Poly Poly
quot |
30 | | subdi 10463 |
. . . . . . . . . . 11
|
31 | 30 | adantl 482 |
. . . . . . . . . 10
Poly Poly
|
32 | 18, 22, 20, 29, 31 | caofdi 6933 |
. . . . . . . . 9
Poly Poly
quot
quot |
33 | 27, 32 | eqtr4d 2659 |
. . . . . . . 8
Poly Poly
quot
quot |
34 | 33 | eqeq1d 2624 |
. . . . . . 7
Poly Poly
quot
quot |
35 | 10 | neneqd 2799 |
. . . . . . . 8
Poly Poly
|
36 | | biorf 420 |
. . . . . . . 8
quot
quot |
37 | 35, 36 | syl 17 |
. . . . . . 7
Poly Poly
quot quot |
38 | 16, 34, 37 | 3bitr4d 300 |
. . . . . 6
Poly Poly
quot
quot |
39 | 38 | biimpd 219 |
. . . . 5
Poly Poly
quot quot |
40 | | eqid 2622 |
. . . . . . . . . . 11
deg deg |
41 | | eqid 2622 |
. . . . . . . . . . 11
deg
quot deg
quot |
42 | 40, 41 | dgrmul 24026 |
. . . . . . . . . 10
Poly
quot Poly quot deg quot deg deg
quot |
43 | 42 | expr 643 |
. . . . . . . . 9
Poly
quot Poly
quot deg quot deg deg
quot |
44 | 3, 10, 14, 43 | syl21anc 1325 |
. . . . . . . 8
Poly Poly
quot deg quot deg deg
quot |
45 | | dgrcl 23989 |
. . . . . . . . . . . 12
Poly
deg |
46 | 2, 45 | syl 17 |
. . . . . . . . . . 11
Poly Poly
deg |
47 | 46 | nn0red 11352 |
. . . . . . . . . 10
Poly Poly
deg |
48 | | dgrcl 23989 |
. . . . . . . . . . 11
quot Poly
deg
quot |
49 | 14, 48 | syl 17 |
. . . . . . . . . 10
Poly Poly
deg quot |
50 | | nn0addge1 11339 |
. . . . . . . . . 10
deg deg
quot deg deg deg
quot |
51 | 47, 49, 50 | syl2anc 693 |
. . . . . . . . 9
Poly Poly
deg deg deg
quot |
52 | | breq2 4657 |
. . . . . . . . 9
deg
quot deg deg
quot
deg deg
quot deg deg deg
quot |
53 | 51, 52 | syl5ibrcom 237 |
. . . . . . . 8
Poly Poly
deg
quot deg deg
quot
deg
deg quot |
54 | 44, 53 | syld 47 |
. . . . . . 7
Poly Poly
quot deg
deg quot |
55 | 33 | fveq2d 6195 |
. . . . . . . . 9
Poly Poly
deg
quot deg quot |
56 | 55 | breq2d 4665 |
. . . . . . . 8
Poly Poly
deg deg
quot deg deg
quot |
57 | | plymulcl 23977 |
. . . . . . . . . . . . 13
Poly
quot Poly quot Poly |
58 | 3, 12, 57 | syl2anc 693 |
. . . . . . . . . . . 12
Poly Poly
quot Poly |
59 | | plysubcl 23978 |
. . . . . . . . . . . 12
Poly
quot Poly
quot Poly |
60 | 9, 58, 59 | syl2anc 693 |
. . . . . . . . . . 11
Poly Poly
quot Poly |
61 | | dgrcl 23989 |
. . . . . . . . . . 11
quot Poly deg
quot |
62 | 60, 61 | syl 17 |
. . . . . . . . . 10
Poly Poly
deg
quot |
63 | 62 | nn0red 11352 |
. . . . . . . . 9
Poly Poly
deg
quot |
64 | 47, 63 | lenltd 10183 |
. . . . . . . 8
Poly Poly
deg deg
quot
deg quot deg |
65 | 56, 64 | bitr3d 270 |
. . . . . . 7
Poly Poly
deg deg
quot
deg quot deg |
66 | 54, 65 | sylibd 229 |
. . . . . 6
Poly Poly
quot
deg quot deg |
67 | 66 | necon4ad 2813 |
. . . . 5
Poly Poly
deg
quot deg quot |
68 | | eqid 2622 |
. . . . . . 7
quot
quot |
69 | 68 | quotdgr 24058 |
. . . . . 6
Poly
Poly
quot deg
quot deg |
70 | 9, 3, 10, 69 | syl3anc 1326 |
. . . . 5
Poly Poly
quot deg
quot deg |
71 | 39, 67, 70 | mpjaod 396 |
. . . 4
Poly Poly
quot |
72 | | df-0p 23437 |
. . . 4
|
73 | 71, 72 | syl6eq 2672 |
. . 3
Poly Poly
quot |
74 | | ofsubeq0 11017 |
. . . 4
quot
quot
quot |
75 | 18, 20, 29, 74 | syl3anc 1326 |
. . 3
Poly Poly
quot
quot |
76 | 73, 75 | mpbid 222 |
. 2
Poly Poly
quot |
77 | 76 | eqcomd 2628 |
1
Poly Poly
quot |