Axiom ax-1cn 7385

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

Assertion

Ref	Expression
ax-1cn	⊢ 1 ∈ ℂ

Detailed syntax breakdown of Axiom ax-1cn

Step	Hyp	Ref	Expression
1		c1 7298	. 2 class 1
2		cc 7295	. 2 class ℂ
3	1, 2	wcel 1436	1 wff 1 ∈ ℂ

This axiom is referenced by:  0cn  7427  1ex  7430  mulid1  7432  mulid2  7433  1cnd  7451  muladd11  7562  1p1times  7563  peano2cn  7564  peano2cnm  7695  0reALT  7726  pncan1  7802  npcan1  7803  kcnktkm1cn  7808  ine0  7819  mulm1  7825  mulsubfacd  7843  ixi  8004  inelr  8005  muleqadd  8079  recclap  8088  recap0  8094  recidap  8095  recidap2  8096  div1  8112  1div1e1  8113  diveqap1  8114  recdivap  8127  divdivap1  8132  divdivap2  8133  recdivap2  8134  conjmulap  8138  eqneg  8141  div2negap  8144  recreclt  8299  nn1m1nn  8378  nn1suc  8379  nnaddcl  8380  nnmulcl  8381  nnsub  8398  1m1e0  8429  neg1cn  8465  neg1ne0  8467  neg1ap0  8469  negneg1e1  8470  1pneg1e0  8471  1m0e1  8473  0p1e1  8474  1p0e1  8475  2m1e1  8477  3m1e2  8479  2p2e4  8480  1p2e3  8487  3p2e5  8494  3p3e6  8495  4p2e6  8496  4p3e7  8497  4p4e8  8498  5p2e7  8499  5p3e8  8500  5p4e9  8501  6p2e8  8502  6p3e9  8503  7p2e9  8504  1t1e1  8505  3t3e9  8510  neg1mulneg1e1  8564  1mhlfehlf  8570  8th4div3  8571  halfpm6th  8572  addltmul  8588  elnn0nn  8651  peano2z  8722  zlem1lt  8742  zltlem1  8743  nnaddm1cl  8747  elz2  8754  zextlt  8774  zeo  8787  peano5uzti  8790  numsuc  8825  numltc  8837  numsucc  8851  numaddc  8859  6p5lem  8881  5p5e10  8882  6p4e10  8883  7p3e10  8886  8p2e10  8891  10m1e9  8907  4t3lem  8908  7t4e28  8922  9t11e99  8941  decbin2  8952  uzp1  8987  peano2uzr  9008  uzaddcl  9009  qreccl  9062  iccf1o  9356  fz01en  9402  fztp  9425  fzsuc2  9426  fztpval  9430  fseq1m1p1  9442  elfzp1b  9444  fzoss2  9514  fzval3  9546  fzosplitsnm1  9551  fzo0to42pr  9562  fzosplitprm1  9576  fldiv4p1lem1div2  9643  flqdiv  9659  frecfzen2  9765  nn0ennn  9771  iseqm1  9805  iseqshft2  9810  monoord2  9814  isermono  9815  expival  9859  expcl  9875  m1expcl2  9879  expclzaplem  9881  expm1t  9885  1exp  9886  mulexpzap  9897  expadd  9899  expaddzap  9901  expmul  9902  expubnd  9914  neg1sqe1  9951  irec  9955  i4  9958  binom21  9967  bernneq  9974  bernneq2  9975  facndiv  10047  faclbnd6  10052  bcnp1n  10067  bcm1k  10068  bcp1nk  10070  bcn2  10072  bcp1m1  10073  bcpasc  10074  4bc3eq4  10081  hashfz  10129  hashfzo  10130  iseqcoll  10147  rei  10232  imi  10233  caucvgrelemrec  10311  recan  10441  iiserex  10624  serif0  10636  fsumm1  10697  fsump1  10701  3dvdsdec  10771  3dvds2dec  10772  odd2np1lem  10778  odd2np1  10779  opoe  10801  omoe  10802  opeo  10803  omeo  10804  m1exp1  10807  n2dvdsm1  10819  flodddiv4  10840  gcdmultiple  10915  sqgcd  10924  nn0seqcvgd  10929  prmind2  11008  hashdvds  11103  phiprmpw  11104  phiprm  11105  ex-fl  11122