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 24842 | . 2 class 0𝑝 | |
2 | cc 10878 | . . 3 class ℂ | |
3 | cc0 10880 | . . . 4 class 0 | |
4 | 3 | csn 4562 | . . 3 class {0} |
5 | 2, 4 | cxp 5588 | . 2 class (ℂ × {0}) |
6 | 1, 5 | wceq 1539 | 1 wff 0𝑝 = (ℂ × {0}) |
Colors of variables: wff setvar class |
This definition is referenced by: 0pval 24844 0plef 24845 0pledm 24846 itg1ge0 24859 mbfi1fseqlem5 24893 itg2addlem 24932 ply0 25378 coeeulem 25394 dgrnznn 25417 coe0 25426 dgr0 25432 dgreq0 25435 dgrmulc 25441 plymul0or 25450 plydiveu 25467 fta1lem 25476 fta1 25477 quotcan 25478 plyexmo 25482 elqaalem3 25490 aaliou2 25509 plymul02 32534 mpaaeu 40982 |
Copyright terms: Public domain | W3C validator |