Axiom ax-1cn 8273

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

This axiom is used by:  0cn  8319  1ex  8322  mulrid  8324  mullid  8325  1cnd  8343  muladd11  8461  1p1times  8462  peano2cn  8463  peano2cnm  8594  0reALT  8625  pncan1  8706  npcan1  8707  kcnktkm1cn  8712  ine0  8723  mulm1  8729  mulsubfacd  8748  ixi  8914  inelr  8915  muleqadd  9001  recclap  9012  recap0  9018  recidap  9019  recidap2  9020  div1  9036  1div1e1  9037  diveqap1  9038  recdivap  9051  divdivap1  9056  divdivap2  9057  recdivap2  9058  conjmulap  9062  eqneg  9065  div2negap  9068  recreclt  9233  ofnegsub  9295  nn1m1nn  9325  nn1suc  9326  nnaddcl  9327  nnmulcl  9328  nnsub  9346  1m1e0  9376  neg1cn  9412  neg1ne0  9414  neg1ap0  9416  negneg1e1  9417  1pneg1e0  9418  1m0e1  9420  0p1e1  9421  1p0e1  9423  2m1e1  9425  3m1e2  9427  4m1e3  9428  5m1e4  9429  6m1e5  9430  7m1e6  9431  8m1e7  9432  9m1e8  9433  2p2e4  9434  1p2e3  9442  3p2e5  9449  3p3e6  9450  4p2e6  9451  4p3e7  9452  4p4e8  9453  5p2e7  9454  5p3e8  9455  5p4e9  9456  6p2e8  9457  6p3e9  9458  7p2e9  9459  1t1e1  9460  3t3e9  9466  neg1mulneg1e1  9522  1mhlfehlf  9528  8th4div3  9529  halfpm6th  9530  addltmul  9547  elnn0nn  9610  peano2z  9685  zlem1lt  9706  zltlem1  9707  nnaddm1cl  9711  elz2  9721  zextlt  9743  zeo  9756  peano5uzti  9759  numsuc  9795  numltc  9812  numsucc  9826  numaddc  9834  6p5lem  9856  5p5e10  9857  6p4e10  9858  7p3e10  9861  8p2e10  9866  10m1e9  9882  4t3lem  9883  7t4e28  9897  9t11e99  9916  decbin2  9927  halfthird  9929  5recm6rec  9930  uzp1  9966  peano2uzr  9995  uzaddcl  9996  qreccl  10052  iccf1o  10418  fz01en  10470  fztp  10496  fzsuc2  10497  fztpval  10501  fseq1m1p1  10513  elfzp1b  10515  fz0to4untppr  10542  fzoss2  10592  fzval3  10633  fzosplitsnm1  10638  fzo0to42pr  10649  fzosplitprm1  10664  fldiv4p1lem1div2  10755  flqdiv  10773  frecfzen2  10879  nn0ennn  10885  xnn0nnen  10889  seq3m1  10925  seqshft2g  10934  monoord2  10938  ser3mono  10939  seqf1oglem1  10971  seqf1oglem2  10972  expcl  11009  m1expcl2  11013  expclzaplem  11015  expm1t  11019  1exp  11020  mulexpzap  11031  expadd  11033  expaddzap  11035  expmul  11036  expubnd  11048  neg1sqe1  11086  irec  11091  i4  11094  binom21  11104  bernneq  11113  bernneq2  11114  facndiv  11193  faclbnd6  11198  bcnp1n  11213  bcm1k  11214  bcp1nk  11216  bcn2  11218  bcp1m1  11219  bcpasc  11220  4bc3eq4  11228  hashfz  11278  hashfzo  11279  hashfibclem  11298  hashf1  11303  seq3coll  11310  swrds1  11456  swrdlsw  11457  wrdind  11510  wrd2ind  11511  rei  11681  imi  11682  caucvgrelemrec  11761  recan  11892  iserex  12124  serf0  12137  fsumm1  12202  fsump1  12206  telfsumo  12252  fsumparts  12256  hashiun  12264  binomlem  12269  binom  12270  binom1p  12271  binom11  12272  binom1dif  12273  bcxmas  12275  isumsplit  12277  isum1p  12278  arisum  12284  arisum2  12285  trireciplem  12286  geosergap  12292  geolim  12297  geolim2  12298  georeclim  12299  geo2sum  12300  geo2sum2  12301  0.999...  12307  geoihalfsum  12308  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  prodf1  12328  prodfclim1  12330  prodrbdclem  12357  fproddccvg  12358  prodmodclem2a  12362  fprodntrivap  12370  prodssdc  12375  fprodssdc  12376  esum  12448  ege2le3  12457  efexp  12468  efzval  12469  eftlub  12476  effsumlt  12478  ef4p  12480  tanval3ap  12500  efi4p  12503  tan0  12517  efival  12518  tanaddap  12525  cos2t  12536  cos2tsin  12537  ef01bndlem  12542  cos1bnd  12545  cos2bnd  12546  demoivreALT  12560  eirraplem  12563  3dvds  12650  3dvdsdec  12651  3dvds2dec  12652  odd2np1lem  12658  odd2np1  12659  opoe  12681  omoe  12682  opeo  12683  omeo  12684  m1exp1  12687  n2dvdsm1  12699  flodddiv4  12722  bitsfzo  12741  gcdmultiple  12816  sqgcd  12825  nn0seqcvgd  12838  prmind2  12917  hashdvds  13022  phiprmpw  13023  phiprm  13024  eulerthlemth  13033  sumhashdc  13149  fldivp1  13150  prmpwdvds  13157  pockthlem  13158  pockthi  13160  4sqlem11  13203  4sqlem19  13211  dec5nprm  13216  prmlem0  13243  43prm  13259  83prm  13260  139prm  13261  163prm  13262  317prm  13263  631prm  13264  1259lem2  13266  1259lem3  13267  1259lem4  13268  1259lem5  13269  1259prm  13270  ballotfilem2  13280  mulgnndir  14007  mulgneg2  14012  cnfld1  14993  zsssubrg  15006  mulgrhm2  15029  expcncf  15801  divcncfap  15806  hovercncf  15838  dvid  15887  dvidre  15889  dvexp  15903  dvexp2  15904  dveflem  15918  plyaddlem1  15939  plymullem1  15940  dvply1  15957  reeff1olem  15963  eulerid  15995  cos2pi  15997  sincosq3sgn  16021  sincosq4sgn  16022  cosq23lt0  16026  tangtx  16031  sincos4thpi  16033  sincos6thpi  16035  pigt3  16037  abssinper  16039  coskpi  16041  cosq34lt1  16043  logdivlti  16075  rpcxpp1  16103  rpcxpsqrt  16119  rprelogbdiv  16154  binom4  16180  log2tlbndlog2  16181  log2ublem3  16184  log2ublog2  16185  birthdaylem2  16187  birthdaylog2  16189  wilthlem1  16193  0sgm  16215  ppiprm  16220  ppinprm  16221  chtprm  16222  chtnprm  16223  1sgmprm  16249  1sgm2ppw  16250  ppiqub  16254  chtublem  16256  chtqub  16257  mersenne  16258  perfect1  16259  perfectlem1  16260  perfectlem2  16261  perfect  16262  bcp1ctr  16267  bposlem8  16279  zabsle1  16284  lgslem1  16285  lgslem2  16286  lgsfcl2  16291  lgsvalmod  16304  lgsneg  16309  lgsdilem  16312  lgsdir2lem1  16313  lgsdir2lem2  16314  lgsdir2lem3  16315  lgsdir2lem5  16317  lgsne0  16323  lgseisenlem1  16355  lgseisenlem2  16356  lgseisen  16359  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2lem1  16366  lgsquad2  16368  m1lgs  16370  2lgslem3c  16380  2lgsoddprmlem3c  16394  2lgsoddprmlem3d  16395  2sqlem10  16410  clwwlknonex2lem2  16845  ex-fl  16905  trilpolemeq1  17256