Proof of Theorem plyrem
Step | Hyp | Ref
| Expression |
1 | | plyssc 23956 |
. . . . . . . 8
Poly Poly |
2 | | simpl 473 |
. . . . . . . 8
Poly Poly |
3 | 1, 2 | sseldi 3601 |
. . . . . . 7
Poly Poly |
4 | | plyrem.1 |
. . . . . . . . . 10
|
5 | 4 | plyremlem 24059 |
. . . . . . . . 9
Poly deg |
6 | 5 | adantl 482 |
. . . . . . . 8
Poly
Poly deg |
7 | 6 | simp1d 1073 |
. . . . . . 7
Poly Poly |
8 | 6 | simp2d 1074 |
. . . . . . . . 9
Poly deg |
9 | | ax-1ne0 10005 |
. . . . . . . . . 10
|
10 | 9 | a1i 11 |
. . . . . . . . 9
Poly |
11 | 8, 10 | eqnetrd 2861 |
. . . . . . . 8
Poly deg |
12 | | fveq2 6191 |
. . . . . . . . . 10
deg deg |
13 | | dgr0 24018 |
. . . . . . . . . 10
deg |
14 | 12, 13 | syl6eq 2672 |
. . . . . . . . 9
deg |
15 | 14 | necon3i 2826 |
. . . . . . . 8
deg
|
16 | 11, 15 | syl 17 |
. . . . . . 7
Poly |
17 | | plyrem.2 |
. . . . . . . 8
quot |
18 | 17 | quotdgr 24058 |
. . . . . . 7
Poly
Poly
deg deg |
19 | 3, 7, 16, 18 | syl3anc 1326 |
. . . . . 6
Poly
deg deg |
20 | | 0lt1 10550 |
. . . . . . . 8
|
21 | 20, 8 | syl5breqr 4691 |
. . . . . . 7
Poly deg |
22 | | fveq2 6191 |
. . . . . . . . 9
deg deg |
23 | 22, 13 | syl6eq 2672 |
. . . . . . . 8
deg |
24 | 23 | breq1d 4663 |
. . . . . . 7
deg
deg deg |
25 | 21, 24 | syl5ibrcom 237 |
. . . . . 6
Poly
deg deg |
26 | | pm2.62 425 |
. . . . . 6
deg
deg
deg
deg deg deg |
27 | 19, 25, 26 | sylc 65 |
. . . . 5
Poly deg deg |
28 | 27, 8 | breqtrd 4679 |
. . . 4
Poly deg |
29 | | quotcl2 24057 |
. . . . . . . . . 10
Poly
Poly
quot Poly |
30 | 3, 7, 16, 29 | syl3anc 1326 |
. . . . . . . . 9
Poly quot Poly |
31 | | plymulcl 23977 |
. . . . . . . . 9
Poly
quot Poly quot Poly |
32 | 7, 30, 31 | syl2anc 693 |
. . . . . . . 8
Poly quot Poly |
33 | | plysubcl 23978 |
. . . . . . . 8
Poly
quot Poly
quot Poly |
34 | 3, 32, 33 | syl2anc 693 |
. . . . . . 7
Poly quot Poly |
35 | 17, 34 | syl5eqel 2705 |
. . . . . 6
Poly Poly |
36 | | dgrcl 23989 |
. . . . . 6
Poly deg |
37 | 35, 36 | syl 17 |
. . . . 5
Poly deg |
38 | | nn0lt10b 11439 |
. . . . 5
deg deg deg |
39 | 37, 38 | syl 17 |
. . . 4
Poly deg deg |
40 | 28, 39 | mpbid 222 |
. . 3
Poly deg |
41 | | 0dgrb 24002 |
. . . 4
Poly deg |
42 | 35, 41 | syl 17 |
. . 3
Poly deg
|
43 | 40, 42 | mpbid 222 |
. 2
Poly |
44 | 43 | fveq1d 6193 |
. . . . 5
Poly |
45 | 17 | fveq1i 6192 |
. . . . . . 7
quot |
46 | | plyf 23954 |
. . . . . . . . . . 11
Poly
|
47 | 46 | adantr 481 |
. . . . . . . . . 10
Poly |
48 | | ffn 6045 |
. . . . . . . . . 10
|
49 | 47, 48 | syl 17 |
. . . . . . . . 9
Poly |
50 | | plyf 23954 |
. . . . . . . . . . . 12
Poly |
51 | 7, 50 | syl 17 |
. . . . . . . . . . 11
Poly |
52 | | ffn 6045 |
. . . . . . . . . . 11
|
53 | 51, 52 | syl 17 |
. . . . . . . . . 10
Poly |
54 | | plyf 23954 |
. . . . . . . . . . . 12
quot Poly quot |
55 | 30, 54 | syl 17 |
. . . . . . . . . . 11
Poly quot |
56 | | ffn 6045 |
. . . . . . . . . . 11
quot quot |
57 | 55, 56 | syl 17 |
. . . . . . . . . 10
Poly quot |
58 | | cnex 10017 |
. . . . . . . . . . 11
|
59 | 58 | a1i 11 |
. . . . . . . . . 10
Poly |
60 | | inidm 3822 |
. . . . . . . . . 10
|
61 | 53, 57, 59, 59, 60 | offn 6908 |
. . . . . . . . 9
Poly quot |
62 | | eqidd 2623 |
. . . . . . . . 9
Poly |
63 | 6 | simp3d 1075 |
. . . . . . . . . . . . . . 15
Poly |
64 | | ssun1 3776 |
. . . . . . . . . . . . . . 15
quot |
65 | 63, 64 | syl6eqssr 3656 |
. . . . . . . . . . . . . 14
Poly quot |
66 | | snssg 4327 |
. . . . . . . . . . . . . . 15
quot
quot |
67 | 66 | adantl 482 |
. . . . . . . . . . . . . 14
Poly
quot
quot |
68 | 65, 67 | mpbird 247 |
. . . . . . . . . . . . 13
Poly quot |
69 | | ofmulrt 24037 |
. . . . . . . . . . . . . 14
quot quot quot |
70 | 59, 51, 55, 69 | syl3anc 1326 |
. . . . . . . . . . . . 13
Poly
quot quot |
71 | 68, 70 | eleqtrrd 2704 |
. . . . . . . . . . . 12
Poly quot |
72 | | fniniseg 6338 |
. . . . . . . . . . . . 13
quot quot
quot |
73 | 61, 72 | syl 17 |
. . . . . . . . . . . 12
Poly
quot
quot |
74 | 71, 73 | mpbid 222 |
. . . . . . . . . . 11
Poly
quot |
75 | 74 | simprd 479 |
. . . . . . . . . 10
Poly quot |
76 | 75 | adantr 481 |
. . . . . . . . 9
Poly quot |
77 | 49, 61, 59, 59, 60, 62, 76 | ofval 6906 |
. . . . . . . 8
Poly
quot |
78 | 77 | anabss3 864 |
. . . . . . 7
Poly
quot |
79 | 45, 78 | syl5eq 2668 |
. . . . . 6
Poly |
80 | 46 | ffvelrnda 6359 |
. . . . . . 7
Poly |
81 | 80 | subid1d 10381 |
. . . . . 6
Poly |
82 | 79, 81 | eqtrd 2656 |
. . . . 5
Poly |
83 | | fvex 6201 |
. . . . . . 7
|
84 | 83 | fvconst2 6469 |
. . . . . 6
|
85 | 84 | adantl 482 |
. . . . 5
Poly |
86 | 44, 82, 85 | 3eqtr3d 2664 |
. . . 4
Poly |
87 | 86 | sneqd 4189 |
. . 3
Poly |
88 | 87 | xpeq2d 5139 |
. 2
Poly |
89 | 43, 88 | eqtr4d 2659 |
1
Poly |