Metamath Proof Explorer

Definition df-1

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

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

Detailed syntax breakdown

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