| 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 25704 | . 2 class 0𝑝 | |
| 2 | cc 11153 | . . 3 class ℂ | |
| 3 | cc0 11155 | . . . 4 class 0 | |
| 4 | 3 | csn 4626 | . . 3 class {0} |
| 5 | 2, 4 | cxp 5683 | . 2 class (ℂ × {0}) |
| 6 | 1, 5 | wceq 1540 | 1 wff 0𝑝 = (ℂ × {0}) |
| Colors of variables: wff setvar class |
| This definition is referenced by: 0pval 25706 0plef 25707 0pledm 25708 itg1ge0 25721 mbfi1fseqlem5 25754 itg2addlem 25793 ply0 26247 coeeulem 26263 dgrnznn 26286 coe0 26295 dgr0 26302 dgreq0 26305 dgrmulc 26311 plymul0or 26322 plydiveu 26340 fta1lem 26349 fta1 26350 quotcan 26351 plyexmo 26355 elqaalem3 26363 aaliou2 26382 plymul02 34561 mpaaeu 43162 |
| Copyright terms: Public domain | W3C validator |