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 23651
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 23650 . 2 class 0𝑝
2 cc 10219 . . 3 class
3 cc0 10221 . . . 4 class 0
43csn 4370 . . 3 class {0}
52, 4cxp 5309 . 2 class (ℂ × {0})
61, 5wceq 1637 1 wff 0𝑝 = (ℂ × {0})
Colors of variables: wff setvar class
This definition is referenced by:  0pval  23652  0plef  23653  0pledm  23654  itg1ge0  23667  mbfi1fseqlem5  23700  itg2addlem  23739  ply0  24178  coeeulem  24194  dgrnznn  24217  coe0  24226  dgr0  24232  dgreq0  24235  dgrmulc  24241  plymul0or  24250  plydiveu  24267  fta1lem  24276  fta1  24277  quotcan  24278  plyexmo  24282  elqaalem3  24290  aaliou2  24309  plymul02  30948  mpaaeu  38221
  Copyright terms: Public domain W3C validator