Axiom ax-1cn 6977

Description: 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 6937. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-1cn	|- 1 e. CC

Detailed syntax breakdown of Axiom ax-1cn

Step	Hyp	Ref	Expression
1		c1 6890	. 2 class 1
2		cc 6887	. 2 class CC
3	1, 2	wcel 1393	1 wff 1 e. CC

This axiom is referenced by:  0cn  7019  1ex  7022  mulid1  7024  mulid2  7025  1cnd  7043  muladd11  7146  1p1times  7147  peano2cn  7148  peano2cnm  7277  0reALT  7308  pncan1  7375  npcan1  7376  kcnktkm1cn  7380  ine0  7391  mulm1  7397  mulsubfacd  7415  ixi  7574  inelr  7575  muleqadd  7649  recclap  7658  recap0  7664  recidap  7665  recidap2  7666  div1  7680  1div1e1  7681  diveqap1  7682  recdivap  7694  divdivap1  7699  divdivap2  7700  recdivap2  7701  conjmulap  7705  eqneg  7708  div2negap  7711  recreclt  7866  nn1m1nn  7932  nn1suc  7933  nnaddcl  7934  nnmulcl  7935  nnsub  7952  1m1e0  7984  neg1cn  8022  neg1ne0  8024  neg1ap0  8026  negneg1e1  8027  1pneg1e0  8028  1m0e1  8030  0p1e1  8031  1p0e1  8032  2m1e1  8034  3m1e2  8036  2p2e4  8037  1p2e3  8044  3p2e5  8052  3p3e6  8053  4p2e6  8054  4p3e7  8055  4p4e8  8056  5p2e7  8057  5p3e8  8058  5p4e9  8059  5p5e10  8060  6p2e8  8061  6p3e9  8062  6p4e10  8063  7p2e9  8064  7p3e10  8065  8p2e10  8066  1t1e1  8067  3t3e9  8072  neg1mulneg1e1  8137  1mhlfehlf  8143  8th4div3  8144  halfpm6th  8145  addltmul  8161  elnn0nn  8224  peano2z  8281  zlem1lt  8300  zltlem1  8301  nnaddm1cl  8305  elz2  8312  zextlt  8332  zeo  8343  peano5uzti  8346  numsuc  8379  numltc  8387  numsucc  8393  numaddc  8402  6p5lem  8416  4t3lem  8438  7t4e28  8451  decbin2  8471  uzp1  8506  peano2uzr  8528  uzaddcl  8529  qreccl  8576  iccf1o  8872  fz01en  8917  fztp  8940  fzsuc2  8941  fztpval  8945  fseq1m1p1  8957  elfzp1b  8959  fzoss2  9028  fzval3  9060  fzosplitsnm1  9065  fzo0to42pr  9076  fzosplitprm1  9090  fldiv4p1lem1div2  9147  flqdiv  9163  frecfzen2  9204  nn0ennn  9209  iseqm1  9227  iseqshft2  9232  monoord2  9236  isermono  9237  expival  9257  expcl  9273  m1expcl2  9277  expclzaplem  9279  expm1t  9283  1exp  9284  mulexpzap  9295  expadd  9297  expaddzap  9299  expmul  9300  expubnd  9311  neg1sqe1  9348  irec  9352  i4  9355  binom21  9363  bernneq  9369  bernneq2  9370  rei  9499  imi  9500  caucvgrelemrec  9578  recan  9705  iiserex  9859  serif0  9871  nn0seqcvgd  9880  ex-fl  9895