MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-0p Structured version   Visualization version   GIF version

Definition df-0p 25705
Description: Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.)
Assertion
Ref Expression
df-0p 0𝑝 = (ℂ × {0})

Detailed syntax breakdown of Definition df-0p
StepHypRef Expression
1 c0p 25704 . 2 class 0𝑝
2 cc 11153 . . 3 class
3 cc0 11155 . . . 4 class 0
43csn 4626 . . 3 class {0}
52, 4cxp 5683 . 2 class (ℂ × {0})
61, 5wceq 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