Axiom ax-1cn 7989

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

This axiom is referenced by:  0cn  8035  1ex  8038  mulrid  8040  mullid  8041  1cnd  8059  muladd11  8176  1p1times  8177  peano2cn  8178  peano2cnm  8309  0reALT  8340  pncan1  8420  npcan1  8421  kcnktkm1cn  8426  ine0  8437  mulm1  8443  mulsubfacd  8462  ixi  8627  inelr  8628  muleqadd  8712  recclap  8723  recap0  8729  recidap  8730  recidap2  8731  div1  8747  1div1e1  8748  diveqap1  8749  recdivap  8762  divdivap1  8767  divdivap2  8768  recdivap2  8769  conjmulap  8773  eqneg  8776  div2negap  8779  recreclt  8944  ofnegsub  9006  nn1m1nn  9025  nn1suc  9026  nnaddcl  9027  nnmulcl  9028  nnsub  9046  1m1e0  9076  neg1cn  9112  neg1ne0  9114  neg1ap0  9116  negneg1e1  9117  1pneg1e0  9118  1m0e1  9120  0p1e1  9121  1p0e1  9123  2m1e1  9125  3m1e2  9127  4m1e3  9128  5m1e4  9129  6m1e5  9130  7m1e6  9131  8m1e7  9132  9m1e8  9133  2p2e4  9134  1p2e3  9142  3p2e5  9149  3p3e6  9150  4p2e6  9151  4p3e7  9152  4p4e8  9153  5p2e7  9154  5p3e8  9155  5p4e9  9156  6p2e8  9157  6p3e9  9158  7p2e9  9159  1t1e1  9160  3t3e9  9165  neg1mulneg1e1  9220  1mhlfehlf  9226  8th4div3  9227  halfpm6th  9228  addltmul  9245  elnn0nn  9308  peano2z  9379  zlem1lt  9399  zltlem1  9400  nnaddm1cl  9404  elz2  9414  zextlt  9435  zeo  9448  peano5uzti  9451  numsuc  9487  numltc  9499  numsucc  9513  numaddc  9521  6p5lem  9543  5p5e10  9544  6p4e10  9545  7p3e10  9548  8p2e10  9553  10m1e9  9569  4t3lem  9570  7t4e28  9584  9t11e99  9603  decbin2  9614  halfthird  9616  5recm6rec  9617  uzp1  9652  peano2uzr  9676  uzaddcl  9677  qreccl  9733  iccf1o  10096  fz01en  10145  fztp  10170  fzsuc2  10171  fztpval  10175  fseq1m1p1  10187  elfzp1b  10189  fz0to4untppr  10216  fzoss2  10265  fzval3  10297  fzosplitsnm1  10302  fzo0to42pr  10313  fzosplitprm1  10327  fldiv4p1lem1div2  10412  flqdiv  10430  frecfzen2  10536  nn0ennn  10542  xnn0nnen  10546  seq3m1  10582  seqshft2g  10591  monoord2  10595  ser3mono  10596  seqf1oglem1  10628  seqf1oglem2  10629  expcl  10666  m1expcl2  10670  expclzaplem  10672  expm1t  10676  1exp  10677  mulexpzap  10688  expadd  10690  expaddzap  10692  expmul  10693  expubnd  10705  neg1sqe1  10743  irec  10748  i4  10751  binom21  10761  bernneq  10769  bernneq2  10770  facndiv  10848  faclbnd6  10853  bcnp1n  10868  bcm1k  10869  bcp1nk  10871  bcn2  10873  bcp1m1  10874  bcpasc  10875  4bc3eq4  10882  hashfz  10930  hashfzo  10931  seq3coll  10951  rei  11081  imi  11082  caucvgrelemrec  11161  recan  11291  iserex  11521  serf0  11534  fsumm1  11598  fsump1  11602  telfsumo  11648  fsumparts  11652  hashiun  11660  binomlem  11665  binom  11666  binom1p  11667  binom11  11668  binom1dif  11669  bcxmas  11671  isumsplit  11673  isum1p  11674  arisum  11680  arisum2  11681  trireciplem  11682  geosergap  11688  geolim  11693  geolim2  11694  georeclim  11695  geo2sum  11696  geo2sum2  11697  0.999...  11703  geoihalfsum  11704  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  prodf1  11724  prodfclim1  11726  prodrbdclem  11753  fproddccvg  11754  prodmodclem2a  11758  fprodntrivap  11766  prodssdc  11771  fprodssdc  11772  esum  11844  ege2le3  11853  efexp  11864  efzval  11865  eftlub  11872  effsumlt  11874  ef4p  11876  tanval3ap  11896  efi4p  11899  tan0  11913  efival  11914  tanaddap  11921  cos2t  11932  cos2tsin  11933  ef01bndlem  11938  cos1bnd  11941  cos2bnd  11942  demoivreALT  11956  eirraplem  11959  3dvds  12046  3dvdsdec  12047  3dvds2dec  12048  odd2np1lem  12054  odd2np1  12055  opoe  12077  omoe  12078  opeo  12079  omeo  12080  m1exp1  12083  n2dvdsm1  12095  flodddiv4  12118  bitsfzo  12137  gcdmultiple  12212  sqgcd  12221  nn0seqcvgd  12234  prmind2  12313  hashdvds  12414  phiprmpw  12415  phiprm  12416  eulerthlemth  12425  sumhashdc  12541  fldivp1  12542  prmpwdvds  12549  pockthlem  12550  pockthi  12552  4sqlem11  12595  4sqlem19  12603  dec5nprm  12608  mulgnndir  13357  mulgneg2  13362  cnfld1  14204  zsssubrg  14217  mulgrhm2  14242  expcncf  14929  divcncfap  14934  hovercncf  14966  dvid  15015  dvidre  15017  dvexp  15031  dvexp2  15032  dveflem  15046  plyaddlem1  15067  plymullem1  15068  dvply1  15085  reeff1olem  15091  eulerid  15122  cos2pi  15124  sincosq3sgn  15148  sincosq4sgn  15149  cosq23lt0  15153  tangtx  15158  sincos4thpi  15160  sincos6thpi  15162  pigt3  15164  abssinper  15166  coskpi  15168  cosq34lt1  15170  logdivlti  15201  rpcxpp1  15226  rpcxpsqrt  15242  rprelogbdiv  15277  binom4  15299  wilthlem1  15300  0sgm  15305  1sgmprm  15314  1sgm2ppw  15315  mersenne  15317  perfect1  15318  perfectlem1  15319  perfectlem2  15320  perfect  15321  zabsle1  15324  lgslem1  15325  lgslem2  15326  lgsfcl2  15331  lgsvalmod  15344  lgsneg  15349  lgsdilem  15352  lgsdir2lem1  15353  lgsdir2lem2  15354  lgsdir2lem3  15355  lgsdir2lem5  15357  lgsne0  15363  lgseisenlem1  15395  lgseisenlem2  15396  lgseisen  15399  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem1  15406  lgsquad2  15408  m1lgs  15410  2lgslem3c  15420  2lgsoddprmlem3c  15434  2lgsoddprmlem3d  15435  2sqlem10  15450  ex-fl  15455  trilpolemeq1  15771