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 23243
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 23242 . 2 class 0𝑝
2 cc 9813 . . 3 class
3 cc0 9815 . . . 4 class 0
43csn 4125 . . 3 class {0}
52, 4cxp 5036 . 2 class (ℂ × {0})
61, 5wceq 1475 1 wff 0𝑝 = (ℂ × {0})
Colors of variables: wff setvar class
This definition is referenced by:  0pval  23244  0plef  23245  0pledm  23246  itg1ge0  23259  mbfi1fseqlem5  23292  itg2addlem  23331  ply0  23768  coeeulem  23784  dgrnznn  23807  coe0  23816  dgr0  23822  dgreq0  23825  dgrmulc  23831  plymul0or  23840  plydiveu  23857  fta1lem  23866  fta1  23867  quotcan  23868  plyexmo  23872  elqaalem3  23880  aaliou2  23899  plymul02  29949  mpaaeu  36739
  Copyright terms: Public domain W3C validator