HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-1 7015
Description: Define the complex number 1 (base 10).
Assertion
Ref Expression
df-1 |- 1 = <.1R, 0R>.

Detailed syntax breakdown of Definition df-1
StepHypRef Expression
1 c1 7008 . 2 class 1
2 c1r 6759 . . 3 class 1R
3 c0r 6758 . . 3 class 0R
42, 3cop 3082 . 2 class <.1R, 0R>.
51, 4wceq 1434 1 wff 1 = <.1R, 0R>.
Colors of variables: wff set class
This definition is referenced by:  ax1cn 7040  axi2m1 7050  ax1ne0 7051  ax1rid 7052  axrrecex 7054
Copyright terms: Public domain