Description: Property of being a homogeneous polynomial. (Contributed by Steven Nguyen, 25-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mhpfval.h | |
|
mhpfval.p | |
||
mhpfval.b | |
||
mhpfval.0 | |
||
mhpfval.d | |
||
mhpfval.i | |
||
mhpfval.r | |
||
mhpval.n | |
||
Assertion | ismhp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mhpfval.h | |
|
2 | mhpfval.p | |
|
3 | mhpfval.b | |
|
4 | mhpfval.0 | |
|
5 | mhpfval.d | |
|
6 | mhpfval.i | |
|
7 | mhpfval.r | |
|
8 | mhpval.n | |
|
9 | 1 2 3 4 5 6 7 8 | mhpval | |
10 | 9 | eleq2d | |
11 | oveq1 | |
|
12 | 11 | sseq1d | |
13 | 12 | elrab | |
14 | 10 13 | bitrdi | |