Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn . (Contributed by NM, 1Mar1995)
Ref  Expression  

Assertion  ax1cn   1 e. CC 
Step  Hyp  Ref  Expression 

0  c1   1 

1  cc   CC 

2  0 1  wcel   1 e. CC 