Axiom ax-1cn 8265

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

This axiom is referenced by:  0cn  8311  1ex  8314  mulrid  8316  mullid  8317  1cnd  8335  muladd11  8452  1p1times  8453  peano2cn  8454  peano2cnm  8585  0reALT  8616  pncan1  8697  npcan1  8698  kcnktkm1cn  8703  ine0  8714  mulm1  8720  mulsubfacd  8739  ixi  8904  inelr  8905  muleqadd  8991  recclap  9002  recap0  9008  recidap  9009  recidap2  9010  div1  9026  1div1e1  9027  diveqap1  9028  recdivap  9041  divdivap1  9046  divdivap2  9047  recdivap2  9048  conjmulap  9052  eqneg  9055  div2negap  9058  recreclt  9223  ofnegsub  9285  nn1m1nn  9304  nn1suc  9305  nnaddcl  9306  nnmulcl  9307  nnsub  9325  1m1e0  9355  neg1cn  9391  neg1ne0  9393  neg1ap0  9395  negneg1e1  9396  1pneg1e0  9397  1m0e1  9399  0p1e1  9400  1p0e1  9402  2m1e1  9404  3m1e2  9406  4m1e3  9407  5m1e4  9408  6m1e5  9409  7m1e6  9410  8m1e7  9411  9m1e8  9412  2p2e4  9413  1p2e3  9421  3p2e5  9428  3p3e6  9429  4p2e6  9430  4p3e7  9431  4p4e8  9432  5p2e7  9433  5p3e8  9434  5p4e9  9435  6p2e8  9436  6p3e9  9437  7p2e9  9438  1t1e1  9439  3t3e9  9444  neg1mulneg1e1  9499  1mhlfehlf  9505  8th4div3  9506  halfpm6th  9507  addltmul  9524  elnn0nn  9587  peano2z  9662  zlem1lt  9683  zltlem1  9684  nnaddm1cl  9688  elz2  9698  zextlt  9720  zeo  9733  peano5uzti  9736  numsuc  9772  numltc  9784  numsucc  9798  numaddc  9806  6p5lem  9828  5p5e10  9829  6p4e10  9830  7p3e10  9833  8p2e10  9838  10m1e9  9854  4t3lem  9855  7t4e28  9869  9t11e99  9888  decbin2  9899  halfthird  9901  5recm6rec  9902  uzp1  9938  peano2uzr  9967  uzaddcl  9968  qreccl  10024  iccf1o  10389  fz01en  10440  fztp  10466  fzsuc2  10467  fztpval  10471  fseq1m1p1  10483  elfzp1b  10485  fz0to4untppr  10512  fzoss2  10562  fzval3  10603  fzosplitsnm1  10608  fzo0to42pr  10619  fzosplitprm1  10634  fldiv4p1lem1div2  10721  flqdiv  10739  frecfzen2  10845  nn0ennn  10851  xnn0nnen  10855  seq3m1  10891  seqshft2g  10900  monoord2  10904  ser3mono  10905  seqf1oglem1  10937  seqf1oglem2  10938  expcl  10975  m1expcl2  10979  expclzaplem  10981  expm1t  10985  1exp  10986  mulexpzap  10997  expadd  10999  expaddzap  11001  expmul  11002  expubnd  11014  neg1sqe1  11052  irec  11057  i4  11060  binom21  11070  bernneq  11079  bernneq2  11080  facndiv  11158  faclbnd6  11163  bcnp1n  11178  bcm1k  11179  bcp1nk  11181  bcn2  11183  bcp1m1  11184  bcpasc  11185  4bc3eq4  11193  hashfz  11243  hashfzo  11244  hashfibclem  11263  hashf1  11268  seq3coll  11275  swrds1  11421  swrdlsw  11422  wrdind  11475  wrd2ind  11476  rei  11646  imi  11647  caucvgrelemrec  11726  recan  11856  iserex  12086  serf0  12099  fsumm1  12164  fsump1  12168  telfsumo  12214  fsumparts  12218  hashiun  12226  binomlem  12231  binom  12232  binom1p  12233  binom11  12234  binom1dif  12235  bcxmas  12237  isumsplit  12239  isum1p  12240  arisum  12246  arisum2  12247  trireciplem  12248  geosergap  12254  geolim  12259  geolim2  12260  georeclim  12261  geo2sum  12262  geo2sum2  12263  0.999...  12269  geoihalfsum  12270  mertenslemi1  12283  mertenslem2  12284  mertensabs  12285  prodf1  12290  prodfclim1  12292  prodrbdclem  12319  fproddccvg  12320  prodmodclem2a  12324  fprodntrivap  12332  prodssdc  12337  fprodssdc  12338  esum  12410  ege2le3  12419  efexp  12430  efzval  12431  eftlub  12438  effsumlt  12440  ef4p  12442  tanval3ap  12462  efi4p  12465  tan0  12479  efival  12480  tanaddap  12487  cos2t  12498  cos2tsin  12499  ef01bndlem  12504  cos1bnd  12507  cos2bnd  12508  demoivreALT  12522  eirraplem  12525  3dvds  12612  3dvdsdec  12613  3dvds2dec  12614  odd2np1lem  12620  odd2np1  12621  opoe  12643  omoe  12644  opeo  12645  omeo  12646  m1exp1  12649  n2dvdsm1  12661  flodddiv4  12684  bitsfzo  12703  gcdmultiple  12778  sqgcd  12787  nn0seqcvgd  12800  prmind2  12879  hashdvds  12980  phiprmpw  12981  phiprm  12982  eulerthlemth  12991  sumhashdc  13107  fldivp1  13108  prmpwdvds  13115  pockthlem  13116  pockthi  13118  4sqlem11  13161  4sqlem19  13169  dec5nprm  13174  ballotfilem2  13209  mulgnndir  13934  mulgneg2  13939  cnfld1  14884  zsssubrg  14897  mulgrhm2  14920  expcncf  15636  divcncfap  15641  hovercncf  15673  dvid  15722  dvidre  15724  dvexp  15738  dvexp2  15739  dveflem  15753  plyaddlem1  15774  plymullem1  15775  dvply1  15792  reeff1olem  15798  eulerid  15829  cos2pi  15831  sincosq3sgn  15855  sincosq4sgn  15856  cosq23lt0  15860  tangtx  15865  sincos4thpi  15867  sincos6thpi  15869  pigt3  15871  abssinper  15873  coskpi  15875  cosq34lt1  15877  logdivlti  15908  rpcxpp1  15934  rpcxpsqrt  15950  rprelogbdiv  15985  binom4  16007  wilthlem1  16011  0sgm  16016  1sgmprm  16025  1sgm2ppw  16026  mersenne  16028  perfect1  16029  perfectlem1  16030  perfectlem2  16031  perfect  16032  zabsle1  16035  lgslem1  16036  lgslem2  16037  lgsfcl2  16042  lgsvalmod  16055  lgsneg  16060  lgsdilem  16063  lgsdir2lem1  16064  lgsdir2lem2  16065  lgsdir2lem3  16066  lgsdir2lem5  16068  lgsne0  16074  lgseisenlem1  16106  lgseisenlem2  16107  lgseisen  16110  lgsquadlem1  16113  lgsquadlem2  16114  lgsquad2lem1  16117  lgsquad2  16119  m1lgs  16121  2lgslem3c  16131  2lgsoddprmlem3c  16145  2lgsoddprmlem3d  16146  2sqlem10  16161  clwwlknonex2lem2  16596  ex-fl  16656  trilpolemeq1  16997