Axiom ax-1cn 7967

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

This axiom is referenced by:  0cn  8013  1ex  8016  mulrid  8018  mullid  8019  1cnd  8037  muladd11  8154  1p1times  8155  peano2cn  8156  peano2cnm  8287  0reALT  8318  pncan1  8398  npcan1  8399  kcnktkm1cn  8404  ine0  8415  mulm1  8421  mulsubfacd  8439  ixi  8604  inelr  8605  muleqadd  8689  recclap  8700  recap0  8706  recidap  8707  recidap2  8708  div1  8724  1div1e1  8725  diveqap1  8726  recdivap  8739  divdivap1  8744  divdivap2  8745  recdivap2  8746  conjmulap  8750  eqneg  8753  div2negap  8756  recreclt  8921  ofnegsub  8983  nn1m1nn  9002  nn1suc  9003  nnaddcl  9004  nnmulcl  9005  nnsub  9023  1m1e0  9053  neg1cn  9089  neg1ne0  9091  neg1ap0  9093  negneg1e1  9094  1pneg1e0  9095  1m0e1  9097  0p1e1  9098  1p0e1  9100  2m1e1  9102  3m1e2  9104  4m1e3  9105  5m1e4  9106  6m1e5  9107  7m1e6  9108  8m1e7  9109  9m1e8  9110  2p2e4  9111  1p2e3  9119  3p2e5  9126  3p3e6  9127  4p2e6  9128  4p3e7  9129  4p4e8  9130  5p2e7  9131  5p3e8  9132  5p4e9  9133  6p2e8  9134  6p3e9  9135  7p2e9  9136  1t1e1  9137  3t3e9  9142  neg1mulneg1e1  9197  1mhlfehlf  9203  8th4div3  9204  halfpm6th  9205  addltmul  9222  elnn0nn  9285  peano2z  9356  zlem1lt  9376  zltlem1  9377  nnaddm1cl  9381  elz2  9391  zextlt  9412  zeo  9425  peano5uzti  9428  numsuc  9464  numltc  9476  numsucc  9490  numaddc  9498  6p5lem  9520  5p5e10  9521  6p4e10  9522  7p3e10  9525  8p2e10  9530  10m1e9  9546  4t3lem  9547  7t4e28  9561  9t11e99  9580  decbin2  9591  halfthird  9593  5recm6rec  9594  uzp1  9629  peano2uzr  9653  uzaddcl  9654  qreccl  9710  iccf1o  10073  fz01en  10122  fztp  10147  fzsuc2  10148  fztpval  10152  fseq1m1p1  10164  elfzp1b  10166  fz0to4untppr  10193  fzoss2  10242  fzval3  10274  fzosplitsnm1  10279  fzo0to42pr  10290  fzosplitprm1  10304  fldiv4p1lem1div2  10377  flqdiv  10395  frecfzen2  10501  nn0ennn  10507  xnn0nnen  10511  seq3m1  10547  seqshft2g  10556  monoord2  10560  ser3mono  10561  seqf1oglem1  10593  seqf1oglem2  10594  expcl  10631  m1expcl2  10635  expclzaplem  10637  expm1t  10641  1exp  10642  mulexpzap  10653  expadd  10655  expaddzap  10657  expmul  10658  expubnd  10670  neg1sqe1  10708  irec  10713  i4  10716  binom21  10726  bernneq  10734  bernneq2  10735  facndiv  10813  faclbnd6  10818  bcnp1n  10833  bcm1k  10834  bcp1nk  10836  bcn2  10838  bcp1m1  10839  bcpasc  10840  4bc3eq4  10847  hashfz  10895  hashfzo  10896  seq3coll  10916  rei  11046  imi  11047  caucvgrelemrec  11126  recan  11256  iserex  11485  serf0  11498  fsumm1  11562  fsump1  11566  telfsumo  11612  fsumparts  11616  hashiun  11624  binomlem  11629  binom  11630  binom1p  11631  binom11  11632  binom1dif  11633  bcxmas  11635  isumsplit  11637  isum1p  11638  arisum  11644  arisum2  11645  trireciplem  11646  geosergap  11652  geolim  11657  geolim2  11658  georeclim  11659  geo2sum  11660  geo2sum2  11661  0.999...  11667  geoihalfsum  11668  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  prodf1  11688  prodfclim1  11690  prodrbdclem  11717  fproddccvg  11718  prodmodclem2a  11722  fprodntrivap  11730  prodssdc  11735  fprodssdc  11736  esum  11808  ege2le3  11817  efexp  11828  efzval  11829  eftlub  11836  effsumlt  11838  ef4p  11840  tanval3ap  11860  efi4p  11863  tan0  11877  efival  11878  tanaddap  11885  cos2t  11896  cos2tsin  11897  ef01bndlem  11902  cos1bnd  11905  cos2bnd  11906  demoivreALT  11920  eirraplem  11923  3dvdsdec  12009  3dvds2dec  12010  odd2np1lem  12016  odd2np1  12017  opoe  12039  omoe  12040  opeo  12041  omeo  12042  m1exp1  12045  n2dvdsm1  12057  flodddiv4  12078  gcdmultiple  12160  sqgcd  12169  nn0seqcvgd  12182  prmind2  12261  hashdvds  12362  phiprmpw  12363  phiprm  12364  eulerthlemth  12373  sumhashdc  12488  fldivp1  12489  prmpwdvds  12496  pockthlem  12497  pockthi  12499  4sqlem11  12542  4sqlem19  12550  mulgnndir  13224  mulgneg2  13229  cnfld1  14071  zsssubrg  14084  mulgrhm2  14109  expcncf  14788  divcncfap  14793  hovercncf  14825  dvid  14874  dvidre  14876  dvexp  14890  dvexp2  14891  dveflem  14905  plyaddlem1  14926  plymullem1  14927  dvply1  14943  reeff1olem  14947  eulerid  14978  cos2pi  14980  sincosq3sgn  15004  sincosq4sgn  15005  cosq23lt0  15009  tangtx  15014  sincos4thpi  15016  sincos6thpi  15018  pigt3  15020  abssinper  15022  coskpi  15024  cosq34lt1  15026  logdivlti  15057  rpcxpp1  15082  rpcxpsqrt  15097  rprelogbdiv  15130  binom4  15152  wilthlem1  15153  zabsle1  15156  lgslem1  15157  lgslem2  15158  lgsfcl2  15163  lgsvalmod  15176  lgsneg  15181  lgsdilem  15184  lgsdir2lem1  15185  lgsdir2lem2  15186  lgsdir2lem3  15187  lgsdir2lem5  15189  lgsne0  15195  lgseisenlem1  15227  lgseisenlem2  15228  lgseisen  15231  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem1  15238  lgsquad2  15240  m1lgs  15242  2lgslem3c  15252  2lgsoddprmlem3c  15266  2lgsoddprmlem3d  15267  2sqlem10  15282  ex-fl  15287  trilpolemeq1  15600