Axiom ax-1cn 8128

Description: 1 is a complex number. Axiom for real and complex numbers, justified by Theorem ax1cn 8084. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-1cn	|- 1 e. CC

Detailed syntax breakdown of Axiom ax-1cn

Step	Hyp	Ref	Expression
1		c1 8036	. 2 class 1
2		cc 8033	. 2 class CC
3	1, 2	wcel 2202	1 wff 1 e. CC

This axiom is referenced by:  0cn  8174  1ex  8177  mulrid  8179  mullid  8180  1cnd  8198  muladd11  8315  1p1times  8316  peano2cn  8317  peano2cnm  8448  0reALT  8479  pncan1  8559  npcan1  8560  kcnktkm1cn  8565  ine0  8576  mulm1  8582  mulsubfacd  8601  ixi  8766  inelr  8767  muleqadd  8851  recclap  8862  recap0  8868  recidap  8869  recidap2  8870  div1  8886  1div1e1  8887  diveqap1  8888  recdivap  8901  divdivap1  8906  divdivap2  8907  recdivap2  8908  conjmulap  8912  eqneg  8915  div2negap  8918  recreclt  9083  ofnegsub  9145  nn1m1nn  9164  nn1suc  9165  nnaddcl  9166  nnmulcl  9167  nnsub  9185  1m1e0  9215  neg1cn  9251  neg1ne0  9253  neg1ap0  9255  negneg1e1  9256  1pneg1e0  9257  1m0e1  9259  0p1e1  9260  1p0e1  9262  2m1e1  9264  3m1e2  9266  4m1e3  9267  5m1e4  9268  6m1e5  9269  7m1e6  9270  8m1e7  9271  9m1e8  9272  2p2e4  9273  1p2e3  9281  3p2e5  9288  3p3e6  9289  4p2e6  9290  4p3e7  9291  4p4e8  9292  5p2e7  9293  5p3e8  9294  5p4e9  9295  6p2e8  9296  6p3e9  9297  7p2e9  9298  1t1e1  9299  3t3e9  9304  neg1mulneg1e1  9359  1mhlfehlf  9365  8th4div3  9366  halfpm6th  9367  addltmul  9384  elnn0nn  9447  peano2z  9518  zlem1lt  9539  zltlem1  9540  nnaddm1cl  9544  elz2  9554  zextlt  9575  zeo  9588  peano5uzti  9591  numsuc  9627  numltc  9639  numsucc  9653  numaddc  9661  6p5lem  9683  5p5e10  9684  6p4e10  9685  7p3e10  9688  8p2e10  9693  10m1e9  9709  4t3lem  9710  7t4e28  9724  9t11e99  9743  decbin2  9754  halfthird  9756  5recm6rec  9757  uzp1  9793  peano2uzr  9822  uzaddcl  9823  qreccl  9879  iccf1o  10242  fz01en  10291  fztp  10316  fzsuc2  10317  fztpval  10321  fseq1m1p1  10333  elfzp1b  10335  fz0to4untppr  10362  fzoss2  10412  fzval3  10453  fzosplitsnm1  10458  fzo0to42pr  10469  fzosplitprm1  10484  fldiv4p1lem1div2  10569  flqdiv  10587  frecfzen2  10693  nn0ennn  10699  xnn0nnen  10703  seq3m1  10739  seqshft2g  10748  monoord2  10752  ser3mono  10753  seqf1oglem1  10785  seqf1oglem2  10786  expcl  10823  m1expcl2  10827  expclzaplem  10829  expm1t  10833  1exp  10834  mulexpzap  10845  expadd  10847  expaddzap  10849  expmul  10850  expubnd  10862  neg1sqe1  10900  irec  10905  i4  10908  binom21  10918  bernneq  10926  bernneq2  10927  facndiv  11005  faclbnd6  11010  bcnp1n  11025  bcm1k  11026  bcp1nk  11028  bcn2  11030  bcp1m1  11031  bcpasc  11032  4bc3eq4  11039  hashfz  11089  hashfzo  11090  seq3coll  11110  swrds1  11256  swrdlsw  11257  wrdind  11310  wrd2ind  11311  rei  11480  imi  11481  caucvgrelemrec  11560  recan  11690  iserex  11920  serf0  11933  fsumm1  11998  fsump1  12002  telfsumo  12048  fsumparts  12052  hashiun  12060  binomlem  12065  binom  12066  binom1p  12067  binom11  12068  binom1dif  12069  bcxmas  12071  isumsplit  12073  isum1p  12074  arisum  12080  arisum2  12081  trireciplem  12082  geosergap  12088  geolim  12093  geolim2  12094  georeclim  12095  geo2sum  12096  geo2sum2  12097  0.999...  12103  geoihalfsum  12104  mertenslemi1  12117  mertenslem2  12118  mertensabs  12119  prodf1  12124  prodfclim1  12126  prodrbdclem  12153  fproddccvg  12154  prodmodclem2a  12158  fprodntrivap  12166  prodssdc  12171  fprodssdc  12172  esum  12244  ege2le3  12253  efexp  12264  efzval  12265  eftlub  12272  effsumlt  12274  ef4p  12276  tanval3ap  12296  efi4p  12299  tan0  12313  efival  12314  tanaddap  12321  cos2t  12332  cos2tsin  12333  ef01bndlem  12338  cos1bnd  12341  cos2bnd  12342  demoivreALT  12356  eirraplem  12359  3dvds  12446  3dvdsdec  12447  3dvds2dec  12448  odd2np1lem  12454  odd2np1  12455  opoe  12477  omoe  12478  opeo  12479  omeo  12480  m1exp1  12483  n2dvdsm1  12495  flodddiv4  12518  bitsfzo  12537  gcdmultiple  12612  sqgcd  12621  nn0seqcvgd  12634  prmind2  12713  hashdvds  12814  phiprmpw  12815  phiprm  12816  eulerthlemth  12825  sumhashdc  12941  fldivp1  12942  prmpwdvds  12949  pockthlem  12950  pockthi  12952  4sqlem11  12995  4sqlem19  13003  dec5nprm  13008  mulgnndir  13759  mulgneg2  13764  cnfld1  14608  zsssubrg  14621  mulgrhm2  14646  expcncf  15360  divcncfap  15365  hovercncf  15397  dvid  15446  dvidre  15448  dvexp  15462  dvexp2  15463  dveflem  15477  plyaddlem1  15498  plymullem1  15499  dvply1  15516  reeff1olem  15522  eulerid  15553  cos2pi  15555  sincosq3sgn  15579  sincosq4sgn  15580  cosq23lt0  15584  tangtx  15589  sincos4thpi  15591  sincos6thpi  15593  pigt3  15595  abssinper  15597  coskpi  15599  cosq34lt1  15601  logdivlti  15632  rpcxpp1  15657  rpcxpsqrt  15673  rprelogbdiv  15708  binom4  15730  wilthlem1  15731  0sgm  15736  1sgmprm  15745  1sgm2ppw  15746  mersenne  15748  perfect1  15749  perfectlem1  15750  perfectlem2  15751  perfect  15752  zabsle1  15755  lgslem1  15756  lgslem2  15757  lgsfcl2  15762  lgsvalmod  15775  lgsneg  15780  lgsdilem  15783  lgsdir2lem1  15784  lgsdir2lem2  15785  lgsdir2lem3  15786  lgsdir2lem5  15788  lgsne0  15794  lgseisenlem1  15826  lgseisenlem2  15827  lgseisen  15830  lgsquadlem1  15833  lgsquadlem2  15834  lgsquad2lem1  15837  lgsquad2  15839  m1lgs  15841  2lgslem3c  15851  2lgsoddprmlem3c  15865  2lgsoddprmlem3d  15866  2sqlem10  15881  clwwlknonex2lem2  16316  ex-fl  16376  trilpolemeq1  16703