Axiom ax-1cn 8092

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

This axiom is referenced by:  0cn  8138  1ex  8141  mulrid  8143  mullid  8144  1cnd  8162  muladd11  8279  1p1times  8280  peano2cn  8281  peano2cnm  8412  0reALT  8443  pncan1  8523  npcan1  8524  kcnktkm1cn  8529  ine0  8540  mulm1  8546  mulsubfacd  8565  ixi  8730  inelr  8731  muleqadd  8815  recclap  8826  recap0  8832  recidap  8833  recidap2  8834  div1  8850  1div1e1  8851  diveqap1  8852  recdivap  8865  divdivap1  8870  divdivap2  8871  recdivap2  8872  conjmulap  8876  eqneg  8879  div2negap  8882  recreclt  9047  ofnegsub  9109  nn1m1nn  9128  nn1suc  9129  nnaddcl  9130  nnmulcl  9131  nnsub  9149  1m1e0  9179  neg1cn  9215  neg1ne0  9217  neg1ap0  9219  negneg1e1  9220  1pneg1e0  9221  1m0e1  9223  0p1e1  9224  1p0e1  9226  2m1e1  9228  3m1e2  9230  4m1e3  9231  5m1e4  9232  6m1e5  9233  7m1e6  9234  8m1e7  9235  9m1e8  9236  2p2e4  9237  1p2e3  9245  3p2e5  9252  3p3e6  9253  4p2e6  9254  4p3e7  9255  4p4e8  9256  5p2e7  9257  5p3e8  9258  5p4e9  9259  6p2e8  9260  6p3e9  9261  7p2e9  9262  1t1e1  9263  3t3e9  9268  neg1mulneg1e1  9323  1mhlfehlf  9329  8th4div3  9330  halfpm6th  9331  addltmul  9348  elnn0nn  9411  peano2z  9482  zlem1lt  9503  zltlem1  9504  nnaddm1cl  9508  elz2  9518  zextlt  9539  zeo  9552  peano5uzti  9555  numsuc  9591  numltc  9603  numsucc  9617  numaddc  9625  6p5lem  9647  5p5e10  9648  6p4e10  9649  7p3e10  9652  8p2e10  9657  10m1e9  9673  4t3lem  9674  7t4e28  9688  9t11e99  9707  decbin2  9718  halfthird  9720  5recm6rec  9721  uzp1  9756  peano2uzr  9780  uzaddcl  9781  qreccl  9837  iccf1o  10200  fz01en  10249  fztp  10274  fzsuc2  10275  fztpval  10279  fseq1m1p1  10291  elfzp1b  10293  fz0to4untppr  10320  fzoss2  10370  fzval3  10410  fzosplitsnm1  10415  fzo0to42pr  10426  fzosplitprm1  10440  fldiv4p1lem1div2  10525  flqdiv  10543  frecfzen2  10649  nn0ennn  10655  xnn0nnen  10659  seq3m1  10695  seqshft2g  10704  monoord2  10708  ser3mono  10709  seqf1oglem1  10741  seqf1oglem2  10742  expcl  10779  m1expcl2  10783  expclzaplem  10785  expm1t  10789  1exp  10790  mulexpzap  10801  expadd  10803  expaddzap  10805  expmul  10806  expubnd  10818  neg1sqe1  10856  irec  10861  i4  10864  binom21  10874  bernneq  10882  bernneq2  10883  facndiv  10961  faclbnd6  10966  bcnp1n  10981  bcm1k  10982  bcp1nk  10984  bcn2  10986  bcp1m1  10987  bcpasc  10988  4bc3eq4  10995  hashfz  11043  hashfzo  11044  seq3coll  11064  swrds1  11200  swrdlsw  11201  wrdind  11254  wrd2ind  11255  rei  11410  imi  11411  caucvgrelemrec  11490  recan  11620  iserex  11850  serf0  11863  fsumm1  11927  fsump1  11931  telfsumo  11977  fsumparts  11981  hashiun  11989  binomlem  11994  binom  11995  binom1p  11996  binom11  11997  binom1dif  11998  bcxmas  12000  isumsplit  12002  isum1p  12003  arisum  12009  arisum2  12010  trireciplem  12011  geosergap  12017  geolim  12022  geolim2  12023  georeclim  12024  geo2sum  12025  geo2sum2  12026  0.999...  12032  geoihalfsum  12033  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  prodf1  12053  prodfclim1  12055  prodrbdclem  12082  fproddccvg  12083  prodmodclem2a  12087  fprodntrivap  12095  prodssdc  12100  fprodssdc  12101  esum  12173  ege2le3  12182  efexp  12193  efzval  12194  eftlub  12201  effsumlt  12203  ef4p  12205  tanval3ap  12225  efi4p  12228  tan0  12242  efival  12243  tanaddap  12250  cos2t  12261  cos2tsin  12262  ef01bndlem  12267  cos1bnd  12270  cos2bnd  12271  demoivreALT  12285  eirraplem  12288  3dvds  12375  3dvdsdec  12376  3dvds2dec  12377  odd2np1lem  12383  odd2np1  12384  opoe  12406  omoe  12407  opeo  12408  omeo  12409  m1exp1  12412  n2dvdsm1  12424  flodddiv4  12447  bitsfzo  12466  gcdmultiple  12541  sqgcd  12550  nn0seqcvgd  12563  prmind2  12642  hashdvds  12743  phiprmpw  12744  phiprm  12745  eulerthlemth  12754  sumhashdc  12870  fldivp1  12871  prmpwdvds  12878  pockthlem  12879  pockthi  12881  4sqlem11  12924  4sqlem19  12932  dec5nprm  12937  mulgnndir  13688  mulgneg2  13693  cnfld1  14536  zsssubrg  14549  mulgrhm2  14574  expcncf  15283  divcncfap  15288  hovercncf  15320  dvid  15369  dvidre  15371  dvexp  15385  dvexp2  15386  dveflem  15400  plyaddlem1  15421  plymullem1  15422  dvply1  15439  reeff1olem  15445  eulerid  15476  cos2pi  15478  sincosq3sgn  15502  sincosq4sgn  15503  cosq23lt0  15507  tangtx  15512  sincos4thpi  15514  sincos6thpi  15516  pigt3  15518  abssinper  15520  coskpi  15522  cosq34lt1  15524  logdivlti  15555  rpcxpp1  15580  rpcxpsqrt  15596  rprelogbdiv  15631  binom4  15653  wilthlem1  15654  0sgm  15659  1sgmprm  15668  1sgm2ppw  15669  mersenne  15671  perfect1  15672  perfectlem1  15673  perfectlem2  15674  perfect  15675  zabsle1  15678  lgslem1  15679  lgslem2  15680  lgsfcl2  15685  lgsvalmod  15698  lgsneg  15703  lgsdilem  15706  lgsdir2lem1  15707  lgsdir2lem2  15708  lgsdir2lem3  15709  lgsdir2lem5  15711  lgsne0  15717  lgseisenlem1  15749  lgseisenlem2  15750  lgseisen  15753  lgsquadlem1  15756  lgsquadlem2  15757  lgsquad2lem1  15760  lgsquad2  15762  m1lgs  15764  2lgslem3c  15774  2lgsoddprmlem3c  15788  2lgsoddprmlem3d  15789  2sqlem10  15804  ex-fl  16089  trilpolemeq1  16408