Step | Hyp | Ref
| Expression |
1 | | simplr 792 |
. . . . . . . . 9
Poly Poly
|
2 | | simpll 790 |
. . . . . . . . . . . . . 14
Poly Poly |
3 | 2 | sseld 3602 |
. . . . . . . . . . . . 13
Poly Poly |
4 | | simprll 802 |
. . . . . . . . . . . . . . . . . . 19
Poly Poly
Poly |
5 | | plyf 23954 |
. . . . . . . . . . . . . . . . . . 19
Poly |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Poly Poly |
7 | | ffn 6045 |
. . . . . . . . . . . . . . . . . 18
|
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . . . . 17
Poly Poly
|
9 | 8 | adantr 481 |
. . . . . . . . . . . . . . . 16
Poly Poly
|
10 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . 19
Poly Poly Poly |
11 | | plyf 23954 |
. . . . . . . . . . . . . . . . . . 19
Poly |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Poly Poly |
13 | | ffn 6045 |
. . . . . . . . . . . . . . . . . 18
|
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . . . . . 17
Poly Poly |
15 | 14 | adantr 481 |
. . . . . . . . . . . . . . . 16
Poly Poly
|
16 | | cnex 10017 |
. . . . . . . . . . . . . . . . 17
|
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . . 16
Poly Poly
|
18 | 2 | sselda 3603 |
. . . . . . . . . . . . . . . 16
Poly Poly
|
19 | | fnfvof 6911 |
. . . . . . . . . . . . . . . 16
|
20 | 9, 15, 17, 18, 19 | syl22anc 1327 |
. . . . . . . . . . . . . . 15
Poly Poly
|
21 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Poly Poly
|
22 | 21, 18 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
Poly Poly
|
23 | | simprlr 803 |
. . . . . . . . . . . . . . . . . . . 20
Poly Poly |
24 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . 20
Poly Poly |
25 | 23, 24 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . 19
Poly Poly |
26 | 25 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
Poly Poly
|
27 | 26 | fveq1d 6193 |
. . . . . . . . . . . . . . . . 17
Poly Poly
|
28 | | fvres 6207 |
. . . . . . . . . . . . . . . . . 18
|
29 | 28 | adantl 482 |
. . . . . . . . . . . . . . . . 17
Poly Poly
|
30 | | fvres 6207 |
. . . . . . . . . . . . . . . . . 18
|
31 | 30 | adantl 482 |
. . . . . . . . . . . . . . . . 17
Poly Poly
|
32 | 27, 29, 31 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . 16
Poly Poly
|
33 | 22, 32 | subeq0bd 10456 |
. . . . . . . . . . . . . . 15
Poly Poly
|
34 | 20, 33 | eqtrd 2656 |
. . . . . . . . . . . . . 14
Poly Poly
|
35 | 34 | ex 450 |
. . . . . . . . . . . . 13
Poly Poly |
36 | 3, 35 | jcad 555 |
. . . . . . . . . . . 12
Poly Poly |
37 | | plysubcl 23978 |
. . . . . . . . . . . . . 14
Poly
Poly
Poly |
38 | 4, 10, 37 | syl2anc 693 |
. . . . . . . . . . . . 13
Poly Poly Poly |
39 | | plyf 23954 |
. . . . . . . . . . . . 13
Poly |
40 | | ffn 6045 |
. . . . . . . . . . . . 13
|
41 | | fniniseg 6338 |
. . . . . . . . . . . . 13
|
42 | 38, 39, 40, 41 | 4syl 19 |
. . . . . . . . . . . 12
Poly Poly |
43 | 36, 42 | sylibrd 249 |
. . . . . . . . . . 11
Poly Poly |
44 | 43 | ssrdv 3609 |
. . . . . . . . . 10
Poly Poly |
45 | | ssfi 8180 |
. . . . . . . . . . 11
|
46 | 45 | expcom 451 |
. . . . . . . . . 10
|
47 | 44, 46 | syl 17 |
. . . . . . . . 9
Poly Poly |
48 | 1, 47 | mtod 189 |
. . . . . . . 8
Poly Poly |
49 | | df-ne 2795 |
. . . . . . . . . . . 12
|
50 | 49 | biimpri 218 |
. . . . . . . . . . 11
|
51 | | eqid 2622 |
. . . . . . . . . . . 12
|
52 | 51 | fta1 24063 |
. . . . . . . . . . 11
Poly
deg |
53 | 38, 50, 52 | syl2an 494 |
. . . . . . . . . 10
Poly Poly
deg |
54 | 53 | simpld 475 |
. . . . . . . . 9
Poly Poly
|
55 | 54 | ex 450 |
. . . . . . . 8
Poly Poly |
56 | 48, 55 | mt3d 140 |
. . . . . . 7
Poly Poly |
57 | | df-0p 23437 |
. . . . . . 7
|
58 | 56, 57 | syl6eq 2672 |
. . . . . 6
Poly Poly |
59 | 16 | a1i 11 |
. . . . . . 7
Poly Poly |
60 | | ofsubeq0 11017 |
. . . . . . 7
|
61 | 59, 6, 12, 60 | syl3anc 1326 |
. . . . . 6
Poly Poly |
62 | 58, 61 | mpbid 222 |
. . . . 5
Poly Poly
|
63 | 62 | ex 450 |
. . . 4
Poly Poly |
64 | 63 | alrimivv 1856 |
. . 3
Poly Poly |
65 | | eleq1 2689 |
. . . . 5
Poly
Poly |
66 | | reseq1 5390 |
. . . . . 6
|
67 | 66 | eqeq1d 2624 |
. . . . 5
|
68 | 65, 67 | anbi12d 747 |
. . . 4
Poly
Poly |
69 | 68 | mo4 2517 |
. . 3
Poly
Poly
Poly
|
70 | 64, 69 | sylibr 224 |
. 2
Poly |
71 | | plyssc 23956 |
. . . . 5
Poly Poly |
72 | 71 | sseli 3599 |
. . . 4
Poly
Poly |
73 | 72 | anim1i 592 |
. . 3
Poly Poly
|
74 | 73 | moimi 2520 |
. 2
Poly Poly |
75 | 70, 74 | syl 17 |
1
Poly
|