Axiom ax-1cn 7069

Description: 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 7029. (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 6982	. 2 class 1
2		cc 6979	. 2 class CC
3	1, 2	wcel 1433	1 wff 1 e. CC

This axiom is referenced by:  0cn  7111  1ex  7114  mulid1  7116  mulid2  7117  1cnd  7135  muladd11  7241  1p1times  7242  peano2cn  7243  peano2cnm  7374  0reALT  7405  pncan1  7481  npcan1  7482  kcnktkm1cn  7487  ine0  7498  mulm1  7504  mulsubfacd  7522  ixi  7683  inelr  7684  muleqadd  7758  recclap  7767  recap0  7773  recidap  7774  recidap2  7775  div1  7791  1div1e1  7792  diveqap1  7793  recdivap  7806  divdivap1  7811  divdivap2  7812  recdivap2  7813  conjmulap  7817  eqneg  7820  div2negap  7823  recreclt  7978  nn1m1nn  8057  nn1suc  8058  nnaddcl  8059  nnmulcl  8060  nnsub  8077  1m1e0  8108  neg1cn  8144  neg1ne0  8146  neg1ap0  8148  negneg1e1  8149  1pneg1e0  8150  1m0e1  8152  0p1e1  8153  1p0e1  8154  2m1e1  8156  3m1e2  8158  2p2e4  8159  1p2e3  8166  3p2e5  8173  3p3e6  8174  4p2e6  8175  4p3e7  8176  4p4e8  8177  5p2e7  8178  5p3e8  8179  5p4e9  8180  6p2e8  8181  6p3e9  8182  7p2e9  8183  1t1e1  8184  3t3e9  8189  neg1mulneg1e1  8243  1mhlfehlf  8249  8th4div3  8250  halfpm6th  8251  addltmul  8267  elnn0nn  8330  peano2z  8387  zlem1lt  8407  zltlem1  8408  nnaddm1cl  8412  elz2  8419  zextlt  8439  zeo  8452  peano5uzti  8455  numsuc  8490  numltc  8502  numsucc  8516  numaddc  8524  6p5lem  8546  5p5e10  8547  6p4e10  8548  7p3e10  8551  8p2e10  8556  10m1e9  8572  4t3lem  8573  7t4e28  8587  9t11e99  8606  decbin2  8617  uzp1  8652  peano2uzr  8673  uzaddcl  8674  qreccl  8727  iccf1o  9026  fz01en  9072  fztp  9095  fzsuc2  9096  fztpval  9100  fseq1m1p1  9112  elfzp1b  9114  fzoss2  9181  fzval3  9213  fzosplitsnm1  9218  fzo0to42pr  9229  fzosplitprm1  9243  fldiv4p1lem1div2  9307  flqdiv  9323  frecfzen2  9420  nn0ennn  9425  iseqm1  9447  iseqshft2  9452  monoord2  9456  isermono  9457  expival  9478  expcl  9494  m1expcl2  9498  expclzaplem  9500  expm1t  9504  1exp  9505  mulexpzap  9516  expadd  9518  expaddzap  9520  expmul  9521  expubnd  9533  neg1sqe1  9570  irec  9574  i4  9577  binom21  9586  bernneq  9593  bernneq2  9594  facndiv  9666  faclbnd6  9671  bcnp1n  9686  bcm1k  9687  bcp1nk  9689  bcn2  9691  bcp1m1  9692  bcpasc  9693  4bc3eq4  9700  rei  9786  imi  9787  caucvgrelemrec  9865  recan  9995  iiserex  10177  serif0  10189  3dvdsdec  10264  3dvds2dec  10265  odd2np1lem  10271  odd2np1  10272  opoe  10295  omoe  10296  opeo  10297  omeo  10298  m1exp1  10301  n2dvdsm1  10313  flodddiv4  10334  gcdmultiple  10409  sqgcd  10418  nn0seqcvgd  10423  prmind2  10502  ex-fl  10563