Axiom ax-1cn 8100

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

This axiom is referenced by:  0cn  8146  1ex  8149  mulrid  8151  mullid  8152  1cnd  8170  muladd11  8287  1p1times  8288  peano2cn  8289  peano2cnm  8420  0reALT  8451  pncan1  8531  npcan1  8532  kcnktkm1cn  8537  ine0  8548  mulm1  8554  mulsubfacd  8573  ixi  8738  inelr  8739  muleqadd  8823  recclap  8834  recap0  8840  recidap  8841  recidap2  8842  div1  8858  1div1e1  8859  diveqap1  8860  recdivap  8873  divdivap1  8878  divdivap2  8879  recdivap2  8880  conjmulap  8884  eqneg  8887  div2negap  8890  recreclt  9055  ofnegsub  9117  nn1m1nn  9136  nn1suc  9137  nnaddcl  9138  nnmulcl  9139  nnsub  9157  1m1e0  9187  neg1cn  9223  neg1ne0  9225  neg1ap0  9227  negneg1e1  9228  1pneg1e0  9229  1m0e1  9231  0p1e1  9232  1p0e1  9234  2m1e1  9236  3m1e2  9238  4m1e3  9239  5m1e4  9240  6m1e5  9241  7m1e6  9242  8m1e7  9243  9m1e8  9244  2p2e4  9245  1p2e3  9253  3p2e5  9260  3p3e6  9261  4p2e6  9262  4p3e7  9263  4p4e8  9264  5p2e7  9265  5p3e8  9266  5p4e9  9267  6p2e8  9268  6p3e9  9269  7p2e9  9270  1t1e1  9271  3t3e9  9276  neg1mulneg1e1  9331  1mhlfehlf  9337  8th4div3  9338  halfpm6th  9339  addltmul  9356  elnn0nn  9419  peano2z  9490  zlem1lt  9511  zltlem1  9512  nnaddm1cl  9516  elz2  9526  zextlt  9547  zeo  9560  peano5uzti  9563  numsuc  9599  numltc  9611  numsucc  9625  numaddc  9633  6p5lem  9655  5p5e10  9656  6p4e10  9657  7p3e10  9660  8p2e10  9665  10m1e9  9681  4t3lem  9682  7t4e28  9696  9t11e99  9715  decbin2  9726  halfthird  9728  5recm6rec  9729  uzp1  9764  peano2uzr  9788  uzaddcl  9789  qreccl  9845  iccf1o  10208  fz01en  10257  fztp  10282  fzsuc2  10283  fztpval  10287  fseq1m1p1  10299  elfzp1b  10301  fz0to4untppr  10328  fzoss2  10378  fzval3  10418  fzosplitsnm1  10423  fzo0to42pr  10434  fzosplitprm1  10448  fldiv4p1lem1div2  10533  flqdiv  10551  frecfzen2  10657  nn0ennn  10663  xnn0nnen  10667  seq3m1  10703  seqshft2g  10712  monoord2  10716  ser3mono  10717  seqf1oglem1  10749  seqf1oglem2  10750  expcl  10787  m1expcl2  10791  expclzaplem  10793  expm1t  10797  1exp  10798  mulexpzap  10809  expadd  10811  expaddzap  10813  expmul  10814  expubnd  10826  neg1sqe1  10864  irec  10869  i4  10872  binom21  10882  bernneq  10890  bernneq2  10891  facndiv  10969  faclbnd6  10974  bcnp1n  10989  bcm1k  10990  bcp1nk  10992  bcn2  10994  bcp1m1  10995  bcpasc  10996  4bc3eq4  11003  hashfz  11051  hashfzo  11052  seq3coll  11072  swrds1  11208  swrdlsw  11209  wrdind  11262  wrd2ind  11263  rei  11418  imi  11419  caucvgrelemrec  11498  recan  11628  iserex  11858  serf0  11871  fsumm1  11935  fsump1  11939  telfsumo  11985  fsumparts  11989  hashiun  11997  binomlem  12002  binom  12003  binom1p  12004  binom11  12005  binom1dif  12006  bcxmas  12008  isumsplit  12010  isum1p  12011  arisum  12017  arisum2  12018  trireciplem  12019  geosergap  12025  geolim  12030  geolim2  12031  georeclim  12032  geo2sum  12033  geo2sum2  12034  0.999...  12040  geoihalfsum  12041  mertenslemi1  12054  mertenslem2  12055  mertensabs  12056  prodf1  12061  prodfclim1  12063  prodrbdclem  12090  fproddccvg  12091  prodmodclem2a  12095  fprodntrivap  12103  prodssdc  12108  fprodssdc  12109  esum  12181  ege2le3  12190  efexp  12201  efzval  12202  eftlub  12209  effsumlt  12211  ef4p  12213  tanval3ap  12233  efi4p  12236  tan0  12250  efival  12251  tanaddap  12258  cos2t  12269  cos2tsin  12270  ef01bndlem  12275  cos1bnd  12278  cos2bnd  12279  demoivreALT  12293  eirraplem  12296  3dvds  12383  3dvdsdec  12384  3dvds2dec  12385  odd2np1lem  12391  odd2np1  12392  opoe  12414  omoe  12415  opeo  12416  omeo  12417  m1exp1  12420  n2dvdsm1  12432  flodddiv4  12455  bitsfzo  12474  gcdmultiple  12549  sqgcd  12558  nn0seqcvgd  12571  prmind2  12650  hashdvds  12751  phiprmpw  12752  phiprm  12753  eulerthlemth  12762  sumhashdc  12878  fldivp1  12879  prmpwdvds  12886  pockthlem  12887  pockthi  12889  4sqlem11  12932  4sqlem19  12940  dec5nprm  12945  mulgnndir  13696  mulgneg2  13701  cnfld1  14544  zsssubrg  14557  mulgrhm2  14582  expcncf  15291  divcncfap  15296  hovercncf  15328  dvid  15377  dvidre  15379  dvexp  15393  dvexp2  15394  dveflem  15408  plyaddlem1  15429  plymullem1  15430  dvply1  15447  reeff1olem  15453  eulerid  15484  cos2pi  15486  sincosq3sgn  15510  sincosq4sgn  15511  cosq23lt0  15515  tangtx  15520  sincos4thpi  15522  sincos6thpi  15524  pigt3  15526  abssinper  15528  coskpi  15530  cosq34lt1  15532  logdivlti  15563  rpcxpp1  15588  rpcxpsqrt  15604  rprelogbdiv  15639  binom4  15661  wilthlem1  15662  0sgm  15667  1sgmprm  15676  1sgm2ppw  15677  mersenne  15679  perfect1  15680  perfectlem1  15681  perfectlem2  15682  perfect  15683  zabsle1  15686  lgslem1  15687  lgslem2  15688  lgsfcl2  15693  lgsvalmod  15706  lgsneg  15711  lgsdilem  15714  lgsdir2lem1  15715  lgsdir2lem2  15716  lgsdir2lem3  15717  lgsdir2lem5  15719  lgsne0  15725  lgseisenlem1  15757  lgseisenlem2  15758  lgseisen  15761  lgsquadlem1  15764  lgsquadlem2  15765  lgsquad2lem1  15768  lgsquad2  15770  m1lgs  15772  2lgslem3c  15782  2lgsoddprmlem3c  15796  2lgsoddprmlem3d  15797  2sqlem10  15812  ex-fl  16113  trilpolemeq1  16438