Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-0p | Structured version Visualization version GIF version |
Description: Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.) |
Ref | Expression |
---|---|
df-0p | ⊢ 0𝑝 = (ℂ × {0}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c0p 23242 | . 2 class 0𝑝 | |
2 | cc 9813 | . . 3 class ℂ | |
3 | cc0 9815 | . . . 4 class 0 | |
4 | 3 | csn 4125 | . . 3 class {0} |
5 | 2, 4 | cxp 5036 | . 2 class (ℂ × {0}) |
6 | 1, 5 | wceq 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 |