Description: Degree image of a set of polynomials which does not include zero. (Contributed by Stefan O'Rear, 28-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | deg1z.d | |
|
deg1z.p | |
||
deg1z.z | |
||
deg1nn0cl.b | |
||
Assertion | deg1n0ima | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | deg1z.d | |
|
2 | deg1z.p | |
|
3 | deg1z.z | |
|
4 | deg1nn0cl.b | |
|
5 | simpl | |
|
6 | eldifi | |
|
7 | 6 | adantl | |
8 | eldifsni | |
|
9 | 8 | adantl | |
10 | 1 2 3 4 | deg1nn0cl | |
11 | 5 7 9 10 | syl3anc | |
12 | 11 | ralrimiva | |
13 | 1 2 4 | deg1xrf | |
14 | ffun | |
|
15 | 13 14 | ax-mp | |
16 | difss | |
|
17 | 13 | fdmi | |
18 | 16 17 | sseqtrri | |
19 | funimass4 | |
|
20 | 15 18 19 | mp2an | |
21 | 12 20 | sylibr | |