Axiom ax-1cn 8236

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

This axiom is referenced by:  0cn  8282  1ex  8285  mulrid  8287  mullid  8288  1cnd  8306  muladd11  8422  1p1times  8423  peano2cn  8424  peano2cnm  8555  0reALT  8586  pncan1  8667  npcan1  8668  kcnktkm1cn  8673  ine0  8684  mulm1  8690  mulsubfacd  8709  ixi  8874  inelr  8875  muleqadd  8959  recclap  8970  recap0  8976  recidap  8977  recidap2  8978  div1  8994  1div1e1  8995  diveqap1  8996  recdivap  9009  divdivap1  9014  divdivap2  9015  recdivap2  9016  conjmulap  9020  eqneg  9023  div2negap  9026  recreclt  9191  ofnegsub  9253  nn1m1nn  9272  nn1suc  9273  nnaddcl  9274  nnmulcl  9275  nnsub  9293  1m1e0  9323  neg1cn  9359  neg1ne0  9361  neg1ap0  9363  negneg1e1  9364  1pneg1e0  9365  1m0e1  9367  0p1e1  9368  1p0e1  9370  2m1e1  9372  3m1e2  9374  4m1e3  9375  5m1e4  9376  6m1e5  9377  7m1e6  9378  8m1e7  9379  9m1e8  9380  2p2e4  9381  1p2e3  9389  3p2e5  9396  3p3e6  9397  4p2e6  9398  4p3e7  9399  4p4e8  9400  5p2e7  9401  5p3e8  9402  5p4e9  9403  6p2e8  9404  6p3e9  9405  7p2e9  9406  1t1e1  9407  3t3e9  9412  neg1mulneg1e1  9467  1mhlfehlf  9473  8th4div3  9474  halfpm6th  9475  addltmul  9492  elnn0nn  9555  peano2z  9630  zlem1lt  9651  zltlem1  9652  nnaddm1cl  9656  elz2  9666  zextlt  9688  zeo  9701  peano5uzti  9704  numsuc  9740  numltc  9752  numsucc  9766  numaddc  9774  6p5lem  9796  5p5e10  9797  6p4e10  9798  7p3e10  9801  8p2e10  9806  10m1e9  9822  4t3lem  9823  7t4e28  9837  9t11e99  9856  decbin2  9867  halfthird  9869  5recm6rec  9870  uzp1  9906  peano2uzr  9935  uzaddcl  9936  qreccl  9992  iccf1o  10357  fz01en  10408  fztp  10434  fzsuc2  10435  fztpval  10439  fseq1m1p1  10451  elfzp1b  10453  fz0to4untppr  10480  fzoss2  10530  fzval3  10571  fzosplitsnm1  10576  fzo0to42pr  10587  fzosplitprm1  10602  fldiv4p1lem1div2  10689  flqdiv  10707  frecfzen2  10813  nn0ennn  10819  xnn0nnen  10823  seq3m1  10859  seqshft2g  10868  monoord2  10872  ser3mono  10873  seqf1oglem1  10905  seqf1oglem2  10906  expcl  10943  m1expcl2  10947  expclzaplem  10949  expm1t  10953  1exp  10954  mulexpzap  10965  expadd  10967  expaddzap  10969  expmul  10970  expubnd  10982  neg1sqe1  11020  irec  11025  i4  11028  binom21  11038  bernneq  11047  bernneq2  11048  facndiv  11126  faclbnd6  11131  bcnp1n  11146  bcm1k  11147  bcp1nk  11149  bcn2  11151  bcp1m1  11152  bcpasc  11153  4bc3eq4  11161  hashfz  11211  hashfzo  11212  hashfibclem  11231  seq3coll  11239  swrds1  11385  swrdlsw  11386  wrdind  11439  wrd2ind  11440  rei  11609  imi  11610  caucvgrelemrec  11689  recan  11819  iserex  12049  serf0  12062  fsumm1  12127  fsump1  12131  telfsumo  12177  fsumparts  12181  hashiun  12189  binomlem  12194  binom  12195  binom1p  12196  binom11  12197  binom1dif  12198  bcxmas  12200  isumsplit  12202  isum1p  12203  arisum  12209  arisum2  12210  trireciplem  12211  geosergap  12217  geolim  12222  geolim2  12223  georeclim  12224  geo2sum  12225  geo2sum2  12226  0.999...  12232  geoihalfsum  12233  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  prodf1  12253  prodfclim1  12255  prodrbdclem  12282  fproddccvg  12283  prodmodclem2a  12287  fprodntrivap  12295  prodssdc  12300  fprodssdc  12301  esum  12373  ege2le3  12382  efexp  12393  efzval  12394  eftlub  12401  effsumlt  12403  ef4p  12405  tanval3ap  12425  efi4p  12428  tan0  12442  efival  12443  tanaddap  12450  cos2t  12461  cos2tsin  12462  ef01bndlem  12467  cos1bnd  12470  cos2bnd  12471  demoivreALT  12485  eirraplem  12488  3dvds  12575  3dvdsdec  12576  3dvds2dec  12577  odd2np1lem  12583  odd2np1  12584  opoe  12606  omoe  12607  opeo  12608  omeo  12609  m1exp1  12612  n2dvdsm1  12624  flodddiv4  12647  bitsfzo  12666  gcdmultiple  12741  sqgcd  12750  nn0seqcvgd  12763  prmind2  12842  hashdvds  12943  phiprmpw  12944  phiprm  12945  eulerthlemth  12954  sumhashdc  13070  fldivp1  13071  prmpwdvds  13078  pockthlem  13079  pockthi  13081  4sqlem11  13124  4sqlem19  13132  dec5nprm  13137  ballotfilem2  13172  mulgnndir  13904  mulgneg2  13909  cnfld1  14846  zsssubrg  14859  mulgrhm2  14884  expcncf  15600  divcncfap  15605  hovercncf  15637  dvid  15686  dvidre  15688  dvexp  15702  dvexp2  15703  dveflem  15717  plyaddlem1  15738  plymullem1  15739  dvply1  15756  reeff1olem  15762  eulerid  15793  cos2pi  15795  sincosq3sgn  15819  sincosq4sgn  15820  cosq23lt0  15824  tangtx  15829  sincos4thpi  15831  sincos6thpi  15833  pigt3  15835  abssinper  15837  coskpi  15839  cosq34lt1  15841  logdivlti  15872  rpcxpp1  15897  rpcxpsqrt  15913  rprelogbdiv  15948  binom4  15970  wilthlem1  15974  0sgm  15979  1sgmprm  15988  1sgm2ppw  15989  mersenne  15991  perfect1  15992  perfectlem1  15993  perfectlem2  15994  perfect  15995  zabsle1  15998  lgslem1  15999  lgslem2  16000  lgsfcl2  16005  lgsvalmod  16018  lgsneg  16023  lgsdilem  16026  lgsdir2lem1  16027  lgsdir2lem2  16028  lgsdir2lem3  16029  lgsdir2lem5  16031  lgsne0  16037  lgseisenlem1  16069  lgseisenlem2  16070  lgseisen  16073  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2lem1  16080  lgsquad2  16082  m1lgs  16084  2lgslem3c  16094  2lgsoddprmlem3c  16108  2lgsoddprmlem3d  16109  2sqlem10  16124  clwwlknonex2lem2  16559  ex-fl  16619  trilpolemeq1  16950