Axiom ax-1cn 8222

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

This axiom is referenced by:  0cn  8268  1ex  8271  mulrid  8273  mullid  8274  1cnd  8292  muladd11  8408  1p1times  8409  peano2cn  8410  peano2cnm  8541  0reALT  8572  pncan1  8652  npcan1  8653  kcnktkm1cn  8658  ine0  8669  mulm1  8675  mulsubfacd  8694  ixi  8859  inelr  8860  muleqadd  8944  recclap  8955  recap0  8961  recidap  8962  recidap2  8963  div1  8979  1div1e1  8980  diveqap1  8981  recdivap  8994  divdivap1  8999  divdivap2  9000  recdivap2  9001  conjmulap  9005  eqneg  9008  div2negap  9011  recreclt  9176  ofnegsub  9238  nn1m1nn  9257  nn1suc  9258  nnaddcl  9259  nnmulcl  9260  nnsub  9278  1m1e0  9308  neg1cn  9344  neg1ne0  9346  neg1ap0  9348  negneg1e1  9349  1pneg1e0  9350  1m0e1  9352  0p1e1  9353  1p0e1  9355  2m1e1  9357  3m1e2  9359  4m1e3  9360  5m1e4  9361  6m1e5  9362  7m1e6  9363  8m1e7  9364  9m1e8  9365  2p2e4  9366  1p2e3  9374  3p2e5  9381  3p3e6  9382  4p2e6  9383  4p3e7  9384  4p4e8  9385  5p2e7  9386  5p3e8  9387  5p4e9  9388  6p2e8  9389  6p3e9  9390  7p2e9  9391  1t1e1  9392  3t3e9  9397  neg1mulneg1e1  9452  1mhlfehlf  9458  8th4div3  9459  halfpm6th  9460  addltmul  9477  elnn0nn  9540  peano2z  9615  zlem1lt  9636  zltlem1  9637  nnaddm1cl  9641  elz2  9651  zextlt  9673  zeo  9686  peano5uzti  9689  numsuc  9725  numltc  9737  numsucc  9751  numaddc  9759  6p5lem  9781  5p5e10  9782  6p4e10  9783  7p3e10  9786  8p2e10  9791  10m1e9  9807  4t3lem  9808  7t4e28  9822  9t11e99  9841  decbin2  9852  halfthird  9854  5recm6rec  9855  uzp1  9891  peano2uzr  9920  uzaddcl  9921  qreccl  9977  iccf1o  10341  fz01en  10390  fztp  10416  fzsuc2  10417  fztpval  10421  fseq1m1p1  10433  elfzp1b  10435  fz0to4untppr  10462  fzoss2  10512  fzval3  10553  fzosplitsnm1  10558  fzo0to42pr  10569  fzosplitprm1  10584  fldiv4p1lem1div2  10669  flqdiv  10687  frecfzen2  10793  nn0ennn  10799  xnn0nnen  10803  seq3m1  10839  seqshft2g  10848  monoord2  10852  ser3mono  10853  seqf1oglem1  10885  seqf1oglem2  10886  expcl  10923  m1expcl2  10927  expclzaplem  10929  expm1t  10933  1exp  10934  mulexpzap  10945  expadd  10947  expaddzap  10949  expmul  10950  expubnd  10962  neg1sqe1  11000  irec  11005  i4  11008  binom21  11018  bernneq  11026  bernneq2  11027  facndiv  11105  faclbnd6  11110  bcnp1n  11125  bcm1k  11126  bcp1nk  11128  bcn2  11130  bcp1m1  11131  bcpasc  11132  4bc3eq4  11140  hashfz  11190  hashfzo  11191  hashfibclem  11210  seq3coll  11218  swrds1  11364  swrdlsw  11365  wrdind  11418  wrd2ind  11419  rei  11588  imi  11589  caucvgrelemrec  11668  recan  11798  iserex  12028  serf0  12041  fsumm1  12106  fsump1  12110  telfsumo  12156  fsumparts  12160  hashiun  12168  binomlem  12173  binom  12174  binom1p  12175  binom11  12176  binom1dif  12177  bcxmas  12179  isumsplit  12181  isum1p  12182  arisum  12188  arisum2  12189  trireciplem  12190  geosergap  12196  geolim  12201  geolim2  12202  georeclim  12203  geo2sum  12204  geo2sum2  12205  0.999...  12211  geoihalfsum  12212  mertenslemi1  12225  mertenslem2  12226  mertensabs  12227  prodf1  12232  prodfclim1  12234  prodrbdclem  12261  fproddccvg  12262  prodmodclem2a  12266  fprodntrivap  12274  prodssdc  12279  fprodssdc  12280  esum  12352  ege2le3  12361  efexp  12372  efzval  12373  eftlub  12380  effsumlt  12382  ef4p  12384  tanval3ap  12404  efi4p  12407  tan0  12421  efival  12422  tanaddap  12429  cos2t  12440  cos2tsin  12441  ef01bndlem  12446  cos1bnd  12449  cos2bnd  12450  demoivreALT  12464  eirraplem  12467  3dvds  12554  3dvdsdec  12555  3dvds2dec  12556  odd2np1lem  12562  odd2np1  12563  opoe  12585  omoe  12586  opeo  12587  omeo  12588  m1exp1  12591  n2dvdsm1  12603  flodddiv4  12626  bitsfzo  12645  gcdmultiple  12720  sqgcd  12729  nn0seqcvgd  12742  prmind2  12821  hashdvds  12922  phiprmpw  12923  phiprm  12924  eulerthlemth  12933  sumhashdc  13049  fldivp1  13050  prmpwdvds  13057  pockthlem  13058  pockthi  13060  4sqlem11  13103  4sqlem19  13111  dec5nprm  13116  ballotfilem2  13149  mulgnndir  13885  mulgneg2  13890  cnfld1  14737  zsssubrg  14750  mulgrhm2  14775  expcncf  15491  divcncfap  15496  hovercncf  15528  dvid  15577  dvidre  15579  dvexp  15593  dvexp2  15594  dveflem  15608  plyaddlem1  15629  plymullem1  15630  dvply1  15647  reeff1olem  15653  eulerid  15684  cos2pi  15686  sincosq3sgn  15710  sincosq4sgn  15711  cosq23lt0  15715  tangtx  15720  sincos4thpi  15722  sincos6thpi  15724  pigt3  15726  abssinper  15728  coskpi  15730  cosq34lt1  15732  logdivlti  15763  rpcxpp1  15788  rpcxpsqrt  15804  rprelogbdiv  15839  binom4  15861  wilthlem1  15865  0sgm  15870  1sgmprm  15879  1sgm2ppw  15880  mersenne  15882  perfect1  15883  perfectlem1  15884  perfectlem2  15885  perfect  15886  zabsle1  15889  lgslem1  15890  lgslem2  15891  lgsfcl2  15896  lgsvalmod  15909  lgsneg  15914  lgsdilem  15917  lgsdir2lem1  15918  lgsdir2lem2  15919  lgsdir2lem3  15920  lgsdir2lem5  15922  lgsne0  15928  lgseisenlem1  15960  lgseisenlem2  15961  lgseisen  15964  lgsquadlem1  15967  lgsquadlem2  15968  lgsquad2lem1  15971  lgsquad2  15973  m1lgs  15975  2lgslem3c  15985  2lgsoddprmlem3c  15999  2lgsoddprmlem3d  16000  2sqlem10  16015  clwwlknonex2lem2  16450  ex-fl  16510  trilpolemeq1  16841