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 24843
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 24842 . 2 class 0𝑝
2 cc 10878 . . 3 class
3 cc0 10880 . . . 4 class 0
43csn 4562 . . 3 class {0}
52, 4cxp 5588 . 2 class (ℂ × {0})
61, 5wceq 1539 1 wff 0𝑝 = (ℂ × {0})
Colors of variables: wff setvar class
This definition is referenced by:  0pval  24844  0plef  24845  0pledm  24846  itg1ge0  24859  mbfi1fseqlem5  24893  itg2addlem  24932  ply0  25378  coeeulem  25394  dgrnznn  25417  coe0  25426  dgr0  25432  dgreq0  25435  dgrmulc  25441  plymul0or  25450  plydiveu  25467  fta1lem  25476  fta1  25477  quotcan  25478  plyexmo  25482  elqaalem3  25490  aaliou2  25509  plymul02  32534  mpaaeu  40982
  Copyright terms: Public domain W3C validator