![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-0p | Structured version Visualization version GIF version |
Description: Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.) |
Ref | Expression |
---|---|
df-0p | ⊢ 0𝑝 = (ℂ × {0}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c0p 23481 | . 2 class 0𝑝 | |
2 | cc 9972 | . . 3 class ℂ | |
3 | cc0 9974 | . . . 4 class 0 | |
4 | 3 | csn 4210 | . . 3 class {0} |
5 | 2, 4 | cxp 5141 | . 2 class (ℂ × {0}) |
6 | 1, 5 | wceq 1523 | 1 wff 0𝑝 = (ℂ × {0}) |
Colors of variables: wff setvar class |
This definition is referenced by: 0pval 23483 0plef 23484 0pledm 23485 itg1ge0 23498 mbfi1fseqlem5 23531 itg2addlem 23570 ply0 24009 coeeulem 24025 dgrnznn 24048 coe0 24057 dgr0 24063 dgreq0 24066 dgrmulc 24072 plymul0or 24081 plydiveu 24098 fta1lem 24107 fta1 24108 quotcan 24109 plyexmo 24113 elqaalem3 24121 aaliou2 24140 plymul02 30751 mpaaeu 38037 |
Copyright terms: Public domain | W3C validator |