Description: A polynomial is homogeneous iff the degree of every nonzero term is the same. (Contributed by SN, 22-Jul-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mhpfval.h | |
|
mhpfval.p | |
||
mhpfval.b | |
||
mhpfval.0 | |
||
mhpfval.d | |
||
mhpfval.i | |
||
mhpfval.r | |
||
mhpval.n | |
||
ismhp2.1 | |
||
Assertion | ismhp3 | |
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 | ismhp2.1 | |
|
10 | 1 2 3 4 5 6 7 8 | ismhp | |
11 | 9 | biantrurd | |
12 | eqid | |
|
13 | 2 12 3 5 9 | mplelf | |
14 | 13 | ffnd | |
15 | 4 | fvexi | |
16 | 15 | a1i | |
17 | elsuppfng | |
|
18 | 14 9 16 17 | syl3anc | |
19 | oveq2 | |
|
20 | 19 | eqeq1d | |
21 | 20 | elrab | |
22 | 21 | a1i | |
23 | 18 22 | imbi12d | |
24 | imdistan | |
|
25 | 23 24 | bitr4di | |
26 | 25 | albidv | |
27 | dfss2 | |
|
28 | df-ral | |
|
29 | 26 27 28 | 3bitr4g | |
30 | 10 11 29 | 3bitr2d | |