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 23187
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 23186 . 2 class 0𝑝
2 cc 9790 . . 3 class
3 cc0 9792 . . . 4 class 0
43csn 4124 . . 3 class {0}
52, 4cxp 5025 . 2 class (ℂ × {0})
61, 5wceq 1474 1 wff 0𝑝 = (ℂ × {0})
Colors of variables: wff setvar class
This definition is referenced by:  0pval  23188  0plef  23189  0pledm  23190  itg1ge0  23203  mbfi1fseqlem5  23236  itg2addlem  23275  ply0  23712  coeeulem  23728  dgrnznn  23751  coe0  23760  dgr0  23766  dgreq0  23769  dgrmulc  23775  plymul0or  23784  plydiveu  23801  fta1lem  23810  fta1  23811  quotcan  23812  plyexmo  23816  elqaalem3  23824  aaliou2  23843  plymul02  29742  mpaaeu  36522
  Copyright terms: Public domain W3C validator