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 23482
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 23481 . 2 class 0𝑝
2 cc 9972 . . 3 class
3 cc0 9974 . . . 4 class 0
43csn 4210 . . 3 class {0}
52, 4cxp 5141 . 2 class (ℂ × {0})
61, 5wceq 1523 1 wff 0𝑝 = (ℂ × {0})
Colors of variables: wff setvar class
This definition is referenced by:  0pval  23483  0plef  23484  0pledm  23485  itg1ge0  23498  mbfi1fseqlem5  23531  itg2addlem  23570  ply0  24009  coeeulem  24025  dgrnznn  24048  coe0  24057  dgr0  24063  dgreq0  24066  dgrmulc  24072  plymul0or  24081  plydiveu  24098  fta1lem  24107  fta1  24108  quotcan  24109  plyexmo  24113  elqaalem3  24121  aaliou2  24140  plymul02  30751  mpaaeu  38037
  Copyright terms: Public domain W3C validator