Step | Hyp | Ref
| Expression |
1 | | ssid 3624 |
. . . . 5
|
2 | | plyconst 23962 |
. . . . 5
Poly |
3 | 1, 2 | mpan 706 |
. . . 4
Poly |
4 | | plyssc 23956 |
. . . . 5
Poly Poly |
5 | 4 | sseli 3599 |
. . . 4
Poly
Poly |
6 | | plymulcl 23977 |
. . . 4
Poly Poly
Poly |
7 | 3, 5, 6 | syl2an 494 |
. . 3
Poly Poly |
8 | | eqid 2622 |
. . . 4
coeff coeff |
9 | 8 | coef3 23988 |
. . 3
Poly coeff |
10 | | ffn 6045 |
. . 3
coeff coeff |
11 | 7, 9, 10 | 3syl 18 |
. 2
Poly coeff |
12 | | fconstg 6092 |
. . . . 5
|
13 | 12 | adantr 481 |
. . . 4
Poly |
14 | | ffn 6045 |
. . . 4
|
15 | 13, 14 | syl 17 |
. . 3
Poly |
16 | | eqid 2622 |
. . . . . 6
coeff coeff |
17 | 16 | coef3 23988 |
. . . . 5
Poly
coeff |
18 | 17 | adantl 482 |
. . . 4
Poly coeff |
19 | | ffn 6045 |
. . . 4
coeff coeff |
20 | 18, 19 | syl 17 |
. . 3
Poly coeff |
21 | | nn0ex 11298 |
. . . 4
|
22 | 21 | a1i 11 |
. . 3
Poly |
23 | | inidm 3822 |
. . 3
|
24 | 15, 20, 22, 22, 23 | offn 6908 |
. 2
Poly
coeff |
25 | 3 | ad2antrr 762 |
. . . . . 6
Poly
Poly |
26 | | eqid 2622 |
. . . . . . 7
coeff
coeff |
27 | 26 | coefv0 24004 |
. . . . . 6
Poly coeff |
28 | 25, 27 | syl 17 |
. . . . 5
Poly
coeff |
29 | | simpll 790 |
. . . . . 6
Poly
|
30 | | 0cn 10032 |
. . . . . 6
|
31 | | fvconst2g 6467 |
. . . . . 6
|
32 | 29, 30, 31 | sylancl 694 |
. . . . 5
Poly
|
33 | 28, 32 | eqtr3d 2658 |
. . . 4
Poly
coeff |
34 | | simpr 477 |
. . . . . . 7
Poly
|
35 | 34 | nn0cnd 11353 |
. . . . . 6
Poly
|
36 | 35 | subid1d 10381 |
. . . . 5
Poly
|
37 | 36 | fveq2d 6195 |
. . . 4
Poly
coeff coeff |
38 | 33, 37 | oveq12d 6668 |
. . 3
Poly
coeff
coeff coeff |
39 | 5 | ad2antlr 763 |
. . . . 5
Poly
Poly |
40 | 26, 16 | coemul 24008 |
. . . . 5
Poly Poly
coeff coeff
coeff |
41 | 25, 39, 34, 40 | syl3anc 1326 |
. . . 4
Poly
coeff coeff
coeff |
42 | | nn0uz 11722 |
. . . . . . 7
|
43 | 34, 42 | syl6eleq 2711 |
. . . . . 6
Poly
|
44 | | fzss2 12381 |
. . . . . 6
|
45 | 43, 44 | syl 17 |
. . . . 5
Poly
|
46 | | elfz1eq 12352 |
. . . . . . . 8
|
47 | 46 | adantl 482 |
. . . . . . 7
Poly
|
48 | | fveq2 6191 |
. . . . . . . 8
coeff coeff
|
49 | | oveq2 6658 |
. . . . . . . . 9
|
50 | 49 | fveq2d 6195 |
. . . . . . . 8
coeff coeff |
51 | 48, 50 | oveq12d 6668 |
. . . . . . 7
coeff coeff coeff coeff |
52 | 47, 51 | syl 17 |
. . . . . 6
Poly
coeff coeff coeff coeff |
53 | 18 | ffvelrnda 6359 |
. . . . . . . . 9
Poly
coeff |
54 | 29, 53 | mulcld 10060 |
. . . . . . . 8
Poly
coeff |
55 | 38, 54 | eqeltrd 2701 |
. . . . . . 7
Poly
coeff
coeff |
56 | 55 | adantr 481 |
. . . . . 6
Poly
coeff coeff |
57 | 52, 56 | eqeltrd 2701 |
. . . . 5
Poly
coeff coeff |
58 | | eldifn 3733 |
. . . . . . . . 9
|
59 | 58 | adantl 482 |
. . . . . . . 8
Poly
|
60 | | eldifi 3732 |
. . . . . . . . . . . . 13
|
61 | | elfznn0 12433 |
. . . . . . . . . . . . 13
|
62 | 60, 61 | syl 17 |
. . . . . . . . . . . 12
|
63 | | eqid 2622 |
. . . . . . . . . . . . . 14
deg
deg |
64 | 26, 63 | dgrub 23990 |
. . . . . . . . . . . . 13
Poly coeff
deg |
65 | 64 | 3expia 1267 |
. . . . . . . . . . . 12
Poly coeff
deg |
66 | 25, 62, 65 | syl2an 494 |
. . . . . . . . . . 11
Poly
coeff deg |
67 | | 0dgr 24001 |
. . . . . . . . . . . . . 14
deg |
68 | 67 | ad3antrrr 766 |
. . . . . . . . . . . . 13
Poly
deg |
69 | 68 | breq2d 4665 |
. . . . . . . . . . . 12
Poly
deg |
70 | 62 | adantl 482 |
. . . . . . . . . . . . 13
Poly
|
71 | | nn0le0eq0 11321 |
. . . . . . . . . . . . 13
|
72 | 70, 71 | syl 17 |
. . . . . . . . . . . 12
Poly
|
73 | 69, 72 | bitrd 268 |
. . . . . . . . . . 11
Poly
deg |
74 | 66, 73 | sylibd 229 |
. . . . . . . . . 10
Poly
coeff |
75 | | id 22 |
. . . . . . . . . . 11
|
76 | | 0z 11388 |
. . . . . . . . . . . 12
|
77 | | elfz3 12351 |
. . . . . . . . . . . 12
|
78 | 76, 77 | ax-mp 5 |
. . . . . . . . . . 11
|
79 | 75, 78 | syl6eqel 2709 |
. . . . . . . . . 10
|
80 | 74, 79 | syl6 35 |
. . . . . . . . 9
Poly
coeff |
81 | 80 | necon1bd 2812 |
. . . . . . . 8
Poly
coeff |
82 | 59, 81 | mpd 15 |
. . . . . . 7
Poly
coeff |
83 | 82 | oveq1d 6665 |
. . . . . 6
Poly
coeff coeff coeff |
84 | 18 | adantr 481 |
. . . . . . . 8
Poly
coeff |
85 | | fznn0sub 12373 |
. . . . . . . . 9
|
86 | 60, 85 | syl 17 |
. . . . . . . 8
|
87 | | ffvelrn 6357 |
. . . . . . . 8
coeff coeff |
88 | 84, 86, 87 | syl2an 494 |
. . . . . . 7
Poly
coeff |
89 | 88 | mul02d 10234 |
. . . . . 6
Poly
coeff |
90 | 83, 89 | eqtrd 2656 |
. . . . 5
Poly
coeff coeff |
91 | | fzfid 12772 |
. . . . 5
Poly
|
92 | 45, 57, 90, 91 | fsumss 14456 |
. . . 4
Poly
coeff coeff
coeff coeff |
93 | 51 | fsum1 14476 |
. . . . 5
coeff
coeff coeff coeff coeff
coeff |
94 | 76, 55, 93 | sylancr 695 |
. . . 4
Poly
coeff coeff coeff coeff |
95 | 41, 92, 94 | 3eqtr2d 2662 |
. . 3
Poly
coeff coeff
coeff |
96 | | simpl 473 |
. . . 4
Poly |
97 | | eqidd 2623 |
. . . 4
Poly
coeff coeff |
98 | 22, 96, 20, 97 | ofc1 6920 |
. . 3
Poly
coeff coeff |
99 | 38, 95, 98 | 3eqtr4d 2666 |
. 2
Poly
coeff coeff |
100 | 11, 24, 99 | eqfnfvd 6314 |
1
Poly coeff coeff |