This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Construction and axiomatization of real and complex numbers Dedekind-cut construction of real and complex numbers df-c
Definition df-c
Description: Define the set of complex numbers. The 23 axioms for complex numbers
start at axresscn . (Contributed by NM , 22-Feb-1996)
(New usage is discouraged.)
Ref
Expression
Assertion
df-c |- CC = ( R. X. R. )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cc |- CC
1
cnr |- R.
2
1 1
cxp |- ( R. X. R. )
3
0 2
wceq |- CC = ( R. X. R. )