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 25179
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 25178 . 2 class 0𝑝
2 cc 11105 . . 3 class
3 cc0 11107 . . . 4 class 0
43csn 4628 . . 3 class {0}
52, 4cxp 5674 . 2 class (ℂ × {0})
61, 5wceq 1542 1 wff 0𝑝 = (ℂ × {0})
Colors of variables: wff setvar class
This definition is referenced by:  0pval  25180  0plef  25181  0pledm  25182  itg1ge0  25195  mbfi1fseqlem5  25229  itg2addlem  25268  ply0  25714  coeeulem  25730  dgrnznn  25753  coe0  25762  dgr0  25768  dgreq0  25771  dgrmulc  25777  plymul0or  25786  plydiveu  25803  fta1lem  25812  fta1  25813  quotcan  25814  plyexmo  25818  elqaalem3  25826  aaliou2  25845  plymul02  33546  mpaaeu  41878
  Copyright terms: Public domain W3C validator