![]() |
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 25178 | . 2 class 0𝑝 | |
2 | cc 11105 | . . 3 class ℂ | |
3 | cc0 11107 | . . . 4 class 0 | |
4 | 3 | csn 4628 | . . 3 class {0} |
5 | 2, 4 | cxp 5674 | . 2 class (ℂ × {0}) |
6 | 1, 5 | wceq 1542 | 1 wff 0𝑝 = (ℂ × {0}) |
Colors of variables: wff setvar class |
This definition is referenced by: 0pval 25180 0plef 25181 0pledm 25182 itg1ge0 25195 mbfi1fseqlem5 25229 itg2addlem 25268 ply0 25714 coeeulem 25730 dgrnznn 25753 coe0 25762 dgr0 25768 dgreq0 25771 dgrmulc 25777 plymul0or 25786 plydiveu 25803 fta1lem 25812 fta1 25813 quotcan 25814 plyexmo 25818 elqaalem3 25826 aaliou2 25845 plymul02 33546 mpaaeu 41878 |
Copyright terms: Public domain | W3C validator |