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 24197 | . 2 class 0𝑝 | |
2 | cc 10523 | . . 3 class ℂ | |
3 | cc0 10525 | . . . 4 class 0 | |
4 | 3 | csn 4557 | . . 3 class {0} |
5 | 2, 4 | cxp 5546 | . 2 class (ℂ × {0}) |
6 | 1, 5 | wceq 1528 | 1 wff 0𝑝 = (ℂ × {0}) |
Colors of variables: wff setvar class |
This definition is referenced by: 0pval 24199 0plef 24200 0pledm 24201 itg1ge0 24214 mbfi1fseqlem5 24247 itg2addlem 24286 ply0 24725 coeeulem 24741 dgrnznn 24764 coe0 24773 dgr0 24779 dgreq0 24782 dgrmulc 24788 plymul0or 24797 plydiveu 24814 fta1lem 24823 fta1 24824 quotcan 24825 plyexmo 24829 elqaalem3 24837 aaliou2 24856 plymul02 31715 mpaaeu 39628 |
Copyright terms: Public domain | W3C validator |