Metamath Proof Explorer

Definition df-0

Description: Define the complex number 0. (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion df-0 
|- 0 = <. 0R , 0R >.

Detailed syntax breakdown

Step Hyp Ref Expression
0 cc0 
 |-  0
1 c0r 
 |-  0R
2 1 1 cop 
 |-  <. 0R , 0R >.
3 0 2 wceq 
 |-  0 = <. 0R , 0R >.