Axiom ax-1cn 7879

Description: 1 is a complex number. Axiom for real and complex numbers, justified by Theorem ax1cn 7835. (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 7787	. 2 class 1
2		cc 7784	. 2 class ℂ
3	1, 2	wcel 2146	1 wff 1 ∈ ℂ

This axiom is referenced by:  0cn  7924  1ex  7927  mulid1  7929  mulid2  7930  1cnd  7948  muladd11  8064  1p1times  8065  peano2cn  8066  peano2cnm  8197  0reALT  8228  pncan1  8308  npcan1  8309  kcnktkm1cn  8314  ine0  8325  mulm1  8331  mulsubfacd  8349  ixi  8514  inelr  8515  muleqadd  8598  recclap  8609  recap0  8615  recidap  8616  recidap2  8617  div1  8633  1div1e1  8634  diveqap1  8635  recdivap  8648  divdivap1  8653  divdivap2  8654  recdivap2  8655  conjmulap  8659  eqneg  8662  div2negap  8665  recreclt  8830  nn1m1nn  8910  nn1suc  8911  nnaddcl  8912  nnmulcl  8913  nnsub  8931  1m1e0  8961  neg1cn  8997  neg1ne0  8999  neg1ap0  9001  negneg1e1  9002  1pneg1e0  9003  1m0e1  9005  0p1e1  9006  1p0e1  9008  2m1e1  9010  3m1e2  9012  4m1e3  9013  5m1e4  9014  6m1e5  9015  7m1e6  9016  8m1e7  9017  9m1e8  9018  2p2e4  9019  1p2e3  9026  3p2e5  9033  3p3e6  9034  4p2e6  9035  4p3e7  9036  4p4e8  9037  5p2e7  9038  5p3e8  9039  5p4e9  9040  6p2e8  9041  6p3e9  9042  7p2e9  9043  1t1e1  9044  3t3e9  9049  neg1mulneg1e1  9104  1mhlfehlf  9110  8th4div3  9111  halfpm6th  9112  addltmul  9128  elnn0nn  9191  peano2z  9262  zlem1lt  9282  zltlem1  9283  nnaddm1cl  9287  elz2  9297  zextlt  9318  zeo  9331  peano5uzti  9334  numsuc  9370  numltc  9382  numsucc  9396  numaddc  9404  6p5lem  9426  5p5e10  9427  6p4e10  9428  7p3e10  9431  8p2e10  9436  10m1e9  9452  4t3lem  9453  7t4e28  9467  9t11e99  9486  decbin2  9497  halfthird  9499  5recm6rec  9500  uzp1  9534  peano2uzr  9558  uzaddcl  9559  qreccl  9615  iccf1o  9975  fz01en  10023  fztp  10048  fzsuc2  10049  fztpval  10053  fseq1m1p1  10065  elfzp1b  10067  fz0to4untppr  10094  fzoss2  10142  fzval3  10174  fzosplitsnm1  10179  fzo0to42pr  10190  fzosplitprm1  10204  fldiv4p1lem1div2  10275  flqdiv  10291  frecfzen2  10397  nn0ennn  10403  seq3m1  10438  monoord2  10447  ser3mono  10448  expcl  10508  m1expcl2  10512  expclzaplem  10514  expm1t  10518  1exp  10519  mulexpzap  10530  expadd  10532  expaddzap  10534  expmul  10535  expubnd  10547  neg1sqe1  10584  irec  10589  i4  10592  binom21  10602  bernneq  10610  bernneq2  10611  facndiv  10687  faclbnd6  10692  bcnp1n  10707  bcm1k  10708  bcp1nk  10710  bcn2  10712  bcp1m1  10713  bcpasc  10714  4bc3eq4  10721  hashfz  10769  hashfzo  10770  seq3coll  10790  rei  10876  imi  10877  caucvgrelemrec  10956  recan  11086  iserex  11315  serf0  11328  fsumm1  11392  fsump1  11396  telfsumo  11442  fsumparts  11446  hashiun  11454  binomlem  11459  binom  11460  binom1p  11461  binom11  11462  binom1dif  11463  bcxmas  11465  isumsplit  11467  isum1p  11468  arisum  11474  arisum2  11475  trireciplem  11476  geosergap  11482  geolim  11487  geolim2  11488  georeclim  11489  geo2sum  11490  geo2sum2  11491  0.999...  11497  geoihalfsum  11498  mertenslemi1  11511  mertenslem2  11512  mertensabs  11513  prodf1  11518  prodfclim1  11520  prodrbdclem  11547  fproddccvg  11548  prodmodclem2a  11552  fprodntrivap  11560  prodssdc  11565  fprodssdc  11566  esum  11638  ege2le3  11647  efexp  11658  efzval  11659  eftlub  11666  effsumlt  11668  ef4p  11670  tanval3ap  11690  efi4p  11693  tan0  11707  efival  11708  tanaddap  11715  cos2t  11726  cos2tsin  11727  ef01bndlem  11732  cos1bnd  11735  cos2bnd  11736  demoivreALT  11749  eirraplem  11752  3dvdsdec  11837  3dvds2dec  11838  odd2np1lem  11844  odd2np1  11845  opoe  11867  omoe  11868  opeo  11869  omeo  11870  m1exp1  11873  n2dvdsm1  11885  flodddiv4  11906  gcdmultiple  11988  sqgcd  11997  nn0seqcvgd  12008  prmind2  12087  hashdvds  12188  phiprmpw  12189  phiprm  12190  eulerthlemth  12199  sumhashdc  12312  fldivp1  12313  prmpwdvds  12320  pockthlem  12321  pockthi  12323  mulgnndir  12881  mulgneg2  12886  expcncf  13672  dvid  13742  dvexp  13755  dvexp2  13756  dveflem  13767  reeff1olem  13772  eulerid  13803  cos2pi  13805  sincosq3sgn  13829  sincosq4sgn  13830  cosq23lt0  13834  tangtx  13839  sincos4thpi  13841  sincos6thpi  13843  pigt3  13845  abssinper  13847  coskpi  13849  cosq34lt1  13851  logdivlti  13882  rpcxpp1  13907  rpcxpsqrt  13922  rprelogbdiv  13955  binom4  13977  zabsle1  13980  lgslem1  13981  lgslem2  13982  lgsfcl2  13987  lgsvalmod  14000  lgsneg  14005  lgsdilem  14008  lgsdir2lem1  14009  lgsdir2lem2  14010  lgsdir2lem3  14011  lgsdir2lem5  14013  lgsne0  14019  2sqlem10  14041  ex-fl  14046  trilpolemeq1  14358