![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-0p | Structured version Visualization version Unicode version |
Description: Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.) |
Ref | Expression |
---|---|
df-0p |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c0p 22676 |
. 2
![]() ![]() ![]() | |
2 | cc 9563 |
. . 3
![]() ![]() | |
3 | cc0 9565 |
. . . 4
![]() ![]() | |
4 | 3 | csn 3980 |
. . 3
![]() ![]() ![]() ![]() |
5 | 2, 4 | cxp 4851 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | wceq 1455 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: 0pval 22678 0plef 22679 0pledm 22680 itg1ge0 22693 mbfi1fseqlem5 22726 itg2addlem 22765 ply0 23211 coeeulem 23227 dgrnznn 23250 coe0 23259 dgr0 23265 dgreq0 23268 dgrmulc 23274 plymul0or 23283 plydiveu 23300 fta1lem 23309 fta1 23310 quotcan 23311 plyexmo 23315 elqaalem3 23323 elqaalem3OLD 23326 aaliou2 23345 plymul02 29484 mpaaeu 36061 |
Copyright terms: Public domain | W3C validator |