Step | Hyp | Ref
| Expression |
1 | | plyaddcl 23976 |
. . 3
Poly Poly
Poly |
2 | | coeadd.4 |
. . . . . 6
deg |
3 | | dgrcl 23989 |
. . . . . 6
Poly
deg |
4 | 2, 3 | syl5eqel 2705 |
. . . . 5
Poly
|
5 | 4 | adantl 482 |
. . . 4
Poly Poly
|
6 | | coeadd.3 |
. . . . . 6
deg |
7 | | dgrcl 23989 |
. . . . . 6
Poly
deg |
8 | 6, 7 | syl5eqel 2705 |
. . . . 5
Poly
|
9 | 8 | adantr 481 |
. . . 4
Poly Poly
|
10 | 5, 9 | ifcld 4131 |
. . 3
Poly Poly
|
11 | | addcl 10018 |
. . . . 5
|
12 | 11 | adantl 482 |
. . . 4
Poly Poly
|
13 | | coefv0.1 |
. . . . . 6
coeff |
14 | 13 | coef3 23988 |
. . . . 5
Poly
|
15 | 14 | adantr 481 |
. . . 4
Poly Poly
|
16 | | coeadd.2 |
. . . . . 6
coeff |
17 | 16 | coef3 23988 |
. . . . 5
Poly
|
18 | 17 | adantl 482 |
. . . 4
Poly Poly
|
19 | | nn0ex 11298 |
. . . . 5
|
20 | 19 | a1i 11 |
. . . 4
Poly Poly
|
21 | | inidm 3822 |
. . . 4
|
22 | 12, 15, 18, 20, 20, 21 | off 6912 |
. . 3
Poly Poly
|
23 | | oveq12 6659 |
. . . . . . . . . 10
|
24 | | 00id 10211 |
. . . . . . . . . 10
|
25 | 23, 24 | syl6eq 2672 |
. . . . . . . . 9
|
26 | | ffn 6045 |
. . . . . . . . . . . 12
|
27 | 15, 26 | syl 17 |
. . . . . . . . . . 11
Poly Poly
|
28 | | ffn 6045 |
. . . . . . . . . . . 12
|
29 | 18, 28 | syl 17 |
. . . . . . . . . . 11
Poly Poly
|
30 | | eqidd 2623 |
. . . . . . . . . . 11
Poly Poly
|
31 | | eqidd 2623 |
. . . . . . . . . . 11
Poly Poly
|
32 | 27, 29, 20, 20, 21, 30, 31 | ofval 6906 |
. . . . . . . . . 10
Poly Poly
|
33 | 32 | eqeq1d 2624 |
. . . . . . . . 9
Poly Poly
|
34 | 25, 33 | syl5ibr 236 |
. . . . . . . 8
Poly Poly
|
35 | 34 | necon3ad 2807 |
. . . . . . 7
Poly Poly
|
36 | | neorian 2888 |
. . . . . . 7
|
37 | 35, 36 | syl6ibr 242 |
. . . . . 6
Poly Poly
|
38 | 13, 6 | dgrub2 23991 |
. . . . . . . . . . 11
Poly
|
39 | 38 | adantr 481 |
. . . . . . . . . 10
Poly Poly
|
40 | | plyco0 23948 |
. . . . . . . . . . 11
|
41 | 9, 15, 40 | syl2anc 693 |
. . . . . . . . . 10
Poly Poly
|
42 | 39, 41 | mpbid 222 |
. . . . . . . . 9
Poly Poly
|
43 | 42 | r19.21bi 2932 |
. . . . . . . 8
Poly Poly
|
44 | 9 | adantr 481 |
. . . . . . . . . . 11
Poly Poly
|
45 | 44 | nn0red 11352 |
. . . . . . . . . 10
Poly Poly
|
46 | 5 | adantr 481 |
. . . . . . . . . . 11
Poly Poly
|
47 | 46 | nn0red 11352 |
. . . . . . . . . 10
Poly Poly
|
48 | | max1 12016 |
. . . . . . . . . 10
|
49 | 45, 47, 48 | syl2anc 693 |
. . . . . . . . 9
Poly Poly
|
50 | | nn0re 11301 |
. . . . . . . . . . 11
|
51 | 50 | adantl 482 |
. . . . . . . . . 10
Poly Poly
|
52 | 10 | adantr 481 |
. . . . . . . . . . 11
Poly Poly
|
53 | 52 | nn0red 11352 |
. . . . . . . . . 10
Poly Poly
|
54 | | letr 10131 |
. . . . . . . . . 10
|
55 | 51, 45, 53, 54 | syl3anc 1326 |
. . . . . . . . 9
Poly Poly
|
56 | 49, 55 | mpan2d 710 |
. . . . . . . 8
Poly Poly
|
57 | 43, 56 | syld 47 |
. . . . . . 7
Poly Poly
|
58 | 16, 2 | dgrub2 23991 |
. . . . . . . . . . 11
Poly
|
59 | 58 | adantl 482 |
. . . . . . . . . 10
Poly Poly
|
60 | | plyco0 23948 |
. . . . . . . . . . 11
|
61 | 5, 18, 60 | syl2anc 693 |
. . . . . . . . . 10
Poly Poly
|
62 | 59, 61 | mpbid 222 |
. . . . . . . . 9
Poly Poly
|
63 | 62 | r19.21bi 2932 |
. . . . . . . 8
Poly Poly
|
64 | | max2 12018 |
. . . . . . . . . 10
|
65 | 45, 47, 64 | syl2anc 693 |
. . . . . . . . 9
Poly Poly
|
66 | | letr 10131 |
. . . . . . . . . 10
|
67 | 51, 47, 53, 66 | syl3anc 1326 |
. . . . . . . . 9
Poly Poly
|
68 | 65, 67 | mpan2d 710 |
. . . . . . . 8
Poly Poly
|
69 | 63, 68 | syld 47 |
. . . . . . 7
Poly Poly
|
70 | 57, 69 | jaod 395 |
. . . . . 6
Poly Poly
|
71 | 37, 70 | syld 47 |
. . . . 5
Poly Poly
|
72 | 71 | ralrimiva 2966 |
. . . 4
Poly Poly
|
73 | | plyco0 23948 |
. . . . 5
|
74 | 10, 22, 73 | syl2anc 693 |
. . . 4
Poly Poly
|
75 | 72, 74 | mpbird 247 |
. . 3
Poly Poly
|
76 | | simpl 473 |
. . . 4
Poly Poly
Poly |
77 | | simpr 477 |
. . . 4
Poly Poly
Poly |
78 | 13, 6 | coeid 23994 |
. . . . 5
Poly
|
79 | 78 | adantr 481 |
. . . 4
Poly Poly
|
80 | 16, 2 | coeid 23994 |
. . . . 5
Poly
|
81 | 80 | adantl 482 |
. . . 4
Poly Poly
|
82 | 76, 77, 9, 5, 15, 18, 39, 59, 79, 81 | plyaddlem1 23969 |
. . 3
Poly Poly
|
83 | 1, 10, 22, 75, 82 | coeeq 23983 |
. 2
Poly Poly
coeff |
84 | | elfznn0 12433 |
. . . 4
|
85 | | ffvelrn 6357 |
. . . 4
|
86 | 22, 84, 85 | syl2an 494 |
. . 3
Poly Poly
|
87 | 1, 10, 86, 82 | dgrle 23999 |
. 2
Poly Poly
deg
|
88 | 83, 87 | jca 554 |
1
Poly Poly
coeff
deg
|