Description: Functionality of polynomial degree in the extended reals. (Contributed by Stefan O'Rear, 19-Mar-2015) (Proof shortened by AV, 27-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mdegxrcl.d | |
|
mdegxrcl.p | |
||
mdegxrcl.b | |
||
Assertion | mdegxrf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mdegxrcl.d | |
|
2 | mdegxrcl.p | |
|
3 | mdegxrcl.b | |
|
4 | xrltso | |
|
5 | 4 | supex | |
6 | eqid | |
|
7 | eqid | |
|
8 | eqid | |
|
9 | 1 2 3 6 7 8 | mdegfval | |
10 | 5 9 | fnmpti | |
11 | 1 2 3 | mdegxrcl | |
12 | 11 | rgen | |
13 | ffnfv | |
|
14 | 10 12 13 | mpbir2an | |