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 24198
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 24197 . 2 class 0𝑝
2 cc 10523 . . 3 class
3 cc0 10525 . . . 4 class 0
43csn 4557 . . 3 class {0}
52, 4cxp 5546 . 2 class (ℂ × {0})
61, 5wceq 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