Axiom ax-1cn 8060

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

This axiom is referenced by:  0cn  8106  1ex  8109  mulrid  8111  mullid  8112  1cnd  8130  muladd11  8247  1p1times  8248  peano2cn  8249  peano2cnm  8380  0reALT  8411  pncan1  8491  npcan1  8492  kcnktkm1cn  8497  ine0  8508  mulm1  8514  mulsubfacd  8533  ixi  8698  inelr  8699  muleqadd  8783  recclap  8794  recap0  8800  recidap  8801  recidap2  8802  div1  8818  1div1e1  8819  diveqap1  8820  recdivap  8833  divdivap1  8838  divdivap2  8839  recdivap2  8840  conjmulap  8844  eqneg  8847  div2negap  8850  recreclt  9015  ofnegsub  9077  nn1m1nn  9096  nn1suc  9097  nnaddcl  9098  nnmulcl  9099  nnsub  9117  1m1e0  9147  neg1cn  9183  neg1ne0  9185  neg1ap0  9187  negneg1e1  9188  1pneg1e0  9189  1m0e1  9191  0p1e1  9192  1p0e1  9194  2m1e1  9196  3m1e2  9198  4m1e3  9199  5m1e4  9200  6m1e5  9201  7m1e6  9202  8m1e7  9203  9m1e8  9204  2p2e4  9205  1p2e3  9213  3p2e5  9220  3p3e6  9221  4p2e6  9222  4p3e7  9223  4p4e8  9224  5p2e7  9225  5p3e8  9226  5p4e9  9227  6p2e8  9228  6p3e9  9229  7p2e9  9230  1t1e1  9231  3t3e9  9236  neg1mulneg1e1  9291  1mhlfehlf  9297  8th4div3  9298  halfpm6th  9299  addltmul  9316  elnn0nn  9379  peano2z  9450  zlem1lt  9471  zltlem1  9472  nnaddm1cl  9476  elz2  9486  zextlt  9507  zeo  9520  peano5uzti  9523  numsuc  9559  numltc  9571  numsucc  9585  numaddc  9593  6p5lem  9615  5p5e10  9616  6p4e10  9617  7p3e10  9620  8p2e10  9625  10m1e9  9641  4t3lem  9642  7t4e28  9656  9t11e99  9675  decbin2  9686  halfthird  9688  5recm6rec  9689  uzp1  9724  peano2uzr  9748  uzaddcl  9749  qreccl  9805  iccf1o  10168  fz01en  10217  fztp  10242  fzsuc2  10243  fztpval  10247  fseq1m1p1  10259  elfzp1b  10261  fz0to4untppr  10288  fzoss2  10338  fzval3  10377  fzosplitsnm1  10382  fzo0to42pr  10393  fzosplitprm1  10407  fldiv4p1lem1div2  10492  flqdiv  10510  frecfzen2  10616  nn0ennn  10622  xnn0nnen  10626  seq3m1  10662  seqshft2g  10671  monoord2  10675  ser3mono  10676  seqf1oglem1  10708  seqf1oglem2  10709  expcl  10746  m1expcl2  10750  expclzaplem  10752  expm1t  10756  1exp  10757  mulexpzap  10768  expadd  10770  expaddzap  10772  expmul  10773  expubnd  10785  neg1sqe1  10823  irec  10828  i4  10831  binom21  10841  bernneq  10849  bernneq2  10850  facndiv  10928  faclbnd6  10933  bcnp1n  10948  bcm1k  10949  bcp1nk  10951  bcn2  10953  bcp1m1  10954  bcpasc  10955  4bc3eq4  10962  hashfz  11010  hashfzo  11011  seq3coll  11031  swrds1  11166  swrdlsw  11167  wrdind  11220  wrd2ind  11221  rei  11376  imi  11377  caucvgrelemrec  11456  recan  11586  iserex  11816  serf0  11829  fsumm1  11893  fsump1  11897  telfsumo  11943  fsumparts  11947  hashiun  11955  binomlem  11960  binom  11961  binom1p  11962  binom11  11963  binom1dif  11964  bcxmas  11966  isumsplit  11968  isum1p  11969  arisum  11975  arisum2  11976  trireciplem  11977  geosergap  11983  geolim  11988  geolim2  11989  georeclim  11990  geo2sum  11991  geo2sum2  11992  0.999...  11998  geoihalfsum  11999  mertenslemi1  12012  mertenslem2  12013  mertensabs  12014  prodf1  12019  prodfclim1  12021  prodrbdclem  12048  fproddccvg  12049  prodmodclem2a  12053  fprodntrivap  12061  prodssdc  12066  fprodssdc  12067  esum  12139  ege2le3  12148  efexp  12159  efzval  12160  eftlub  12167  effsumlt  12169  ef4p  12171  tanval3ap  12191  efi4p  12194  tan0  12208  efival  12209  tanaddap  12216  cos2t  12227  cos2tsin  12228  ef01bndlem  12233  cos1bnd  12236  cos2bnd  12237  demoivreALT  12251  eirraplem  12254  3dvds  12341  3dvdsdec  12342  3dvds2dec  12343  odd2np1lem  12349  odd2np1  12350  opoe  12372  omoe  12373  opeo  12374  omeo  12375  m1exp1  12378  n2dvdsm1  12390  flodddiv4  12413  bitsfzo  12432  gcdmultiple  12507  sqgcd  12516  nn0seqcvgd  12529  prmind2  12608  hashdvds  12709  phiprmpw  12710  phiprm  12711  eulerthlemth  12720  sumhashdc  12836  fldivp1  12837  prmpwdvds  12844  pockthlem  12845  pockthi  12847  4sqlem11  12890  4sqlem19  12898  dec5nprm  12903  mulgnndir  13654  mulgneg2  13659  cnfld1  14501  zsssubrg  14514  mulgrhm2  14539  expcncf  15248  divcncfap  15253  hovercncf  15285  dvid  15334  dvidre  15336  dvexp  15350  dvexp2  15351  dveflem  15365  plyaddlem1  15386  plymullem1  15387  dvply1  15404  reeff1olem  15410  eulerid  15441  cos2pi  15443  sincosq3sgn  15467  sincosq4sgn  15468  cosq23lt0  15472  tangtx  15477  sincos4thpi  15479  sincos6thpi  15481  pigt3  15483  abssinper  15485  coskpi  15487  cosq34lt1  15489  logdivlti  15520  rpcxpp1  15545  rpcxpsqrt  15561  rprelogbdiv  15596  binom4  15618  wilthlem1  15619  0sgm  15624  1sgmprm  15633  1sgm2ppw  15634  mersenne  15636  perfect1  15637  perfectlem1  15638  perfectlem2  15639  perfect  15640  zabsle1  15643  lgslem1  15644  lgslem2  15645  lgsfcl2  15650  lgsvalmod  15663  lgsneg  15668  lgsdilem  15671  lgsdir2lem1  15672  lgsdir2lem2  15673  lgsdir2lem3  15674  lgsdir2lem5  15676  lgsne0  15682  lgseisenlem1  15714  lgseisenlem2  15715  lgseisen  15718  lgsquadlem1  15721  lgsquadlem2  15722  lgsquad2lem1  15725  lgsquad2  15727  m1lgs  15729  2lgslem3c  15739  2lgsoddprmlem3c  15753  2lgsoddprmlem3d  15754  2sqlem10  15769  ex-fl  15999  trilpolemeq1  16319