Axiom ax-1cn 8185

Description: 1 is a complex number. Axiom for real and complex numbers, justified by Theorem ax1cn 8141. (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 8093	. 2 class 1
2		cc 8090	. 2 class CC
3	1, 2	wcel 2202	1 wff 1 e. CC

This axiom is referenced by:  0cn  8231  1ex  8234  mulrid  8236  mullid  8237  1cnd  8255  muladd11  8371  1p1times  8372  peano2cn  8373  peano2cnm  8504  0reALT  8535  pncan1  8615  npcan1  8616  kcnktkm1cn  8621  ine0  8632  mulm1  8638  mulsubfacd  8657  ixi  8822  inelr  8823  muleqadd  8907  recclap  8918  recap0  8924  recidap  8925  recidap2  8926  div1  8942  1div1e1  8943  diveqap1  8944  recdivap  8957  divdivap1  8962  divdivap2  8963  recdivap2  8964  conjmulap  8968  eqneg  8971  div2negap  8974  recreclt  9139  ofnegsub  9201  nn1m1nn  9220  nn1suc  9221  nnaddcl  9222  nnmulcl  9223  nnsub  9241  1m1e0  9271  neg1cn  9307  neg1ne0  9309  neg1ap0  9311  negneg1e1  9312  1pneg1e0  9313  1m0e1  9315  0p1e1  9316  1p0e1  9318  2m1e1  9320  3m1e2  9322  4m1e3  9323  5m1e4  9324  6m1e5  9325  7m1e6  9326  8m1e7  9327  9m1e8  9328  2p2e4  9329  1p2e3  9337  3p2e5  9344  3p3e6  9345  4p2e6  9346  4p3e7  9347  4p4e8  9348  5p2e7  9349  5p3e8  9350  5p4e9  9351  6p2e8  9352  6p3e9  9353  7p2e9  9354  1t1e1  9355  3t3e9  9360  neg1mulneg1e1  9415  1mhlfehlf  9421  8th4div3  9422  halfpm6th  9423  addltmul  9440  elnn0nn  9503  peano2z  9576  zlem1lt  9597  zltlem1  9598  nnaddm1cl  9602  elz2  9612  zextlt  9633  zeo  9646  peano5uzti  9649  numsuc  9685  numltc  9697  numsucc  9711  numaddc  9719  6p5lem  9741  5p5e10  9742  6p4e10  9743  7p3e10  9746  8p2e10  9751  10m1e9  9767  4t3lem  9768  7t4e28  9782  9t11e99  9801  decbin2  9812  halfthird  9814  5recm6rec  9815  uzp1  9851  peano2uzr  9880  uzaddcl  9881  qreccl  9937  iccf1o  10301  fz01en  10350  fztp  10375  fzsuc2  10376  fztpval  10380  fseq1m1p1  10392  elfzp1b  10394  fz0to4untppr  10421  fzoss2  10471  fzval3  10512  fzosplitsnm1  10517  fzo0to42pr  10528  fzosplitprm1  10543  fldiv4p1lem1div2  10628  flqdiv  10646  frecfzen2  10752  nn0ennn  10758  xnn0nnen  10762  seq3m1  10798  seqshft2g  10807  monoord2  10811  ser3mono  10812  seqf1oglem1  10844  seqf1oglem2  10845  expcl  10882  m1expcl2  10886  expclzaplem  10888  expm1t  10892  1exp  10893  mulexpzap  10904  expadd  10906  expaddzap  10908  expmul  10909  expubnd  10921  neg1sqe1  10959  irec  10964  i4  10967  binom21  10977  bernneq  10985  bernneq2  10986  facndiv  11064  faclbnd6  11069  bcnp1n  11084  bcm1k  11085  bcp1nk  11087  bcn2  11089  bcp1m1  11090  bcpasc  11091  4bc3eq4  11098  hashfz  11148  hashfzo  11149  seq3coll  11169  swrds1  11315  swrdlsw  11316  wrdind  11369  wrd2ind  11370  rei  11539  imi  11540  caucvgrelemrec  11619  recan  11749  iserex  11979  serf0  11992  fsumm1  12057  fsump1  12061  telfsumo  12107  fsumparts  12111  hashiun  12119  binomlem  12124  binom  12125  binom1p  12126  binom11  12127  binom1dif  12128  bcxmas  12130  isumsplit  12132  isum1p  12133  arisum  12139  arisum2  12140  trireciplem  12141  geosergap  12147  geolim  12152  geolim2  12153  georeclim  12154  geo2sum  12155  geo2sum2  12156  0.999...  12162  geoihalfsum  12163  mertenslemi1  12176  mertenslem2  12177  mertensabs  12178  prodf1  12183  prodfclim1  12185  prodrbdclem  12212  fproddccvg  12213  prodmodclem2a  12217  fprodntrivap  12225  prodssdc  12230  fprodssdc  12231  esum  12303  ege2le3  12312  efexp  12323  efzval  12324  eftlub  12331  effsumlt  12333  ef4p  12335  tanval3ap  12355  efi4p  12358  tan0  12372  efival  12373  tanaddap  12380  cos2t  12391  cos2tsin  12392  ef01bndlem  12397  cos1bnd  12400  cos2bnd  12401  demoivreALT  12415  eirraplem  12418  3dvds  12505  3dvdsdec  12506  3dvds2dec  12507  odd2np1lem  12513  odd2np1  12514  opoe  12536  omoe  12537  opeo  12538  omeo  12539  m1exp1  12542  n2dvdsm1  12554  flodddiv4  12577  bitsfzo  12596  gcdmultiple  12671  sqgcd  12680  nn0seqcvgd  12693  prmind2  12772  hashdvds  12873  phiprmpw  12874  phiprm  12875  eulerthlemth  12884  sumhashdc  13000  fldivp1  13001  prmpwdvds  13008  pockthlem  13009  pockthi  13011  4sqlem11  13054  4sqlem19  13062  dec5nprm  13067  mulgnndir  13818  mulgneg2  13823  cnfld1  14668  zsssubrg  14681  mulgrhm2  14706  expcncf  15420  divcncfap  15425  hovercncf  15457  dvid  15506  dvidre  15508  dvexp  15522  dvexp2  15523  dveflem  15537  plyaddlem1  15558  plymullem1  15559  dvply1  15576  reeff1olem  15582  eulerid  15613  cos2pi  15615  sincosq3sgn  15639  sincosq4sgn  15640  cosq23lt0  15644  tangtx  15649  sincos4thpi  15651  sincos6thpi  15653  pigt3  15655  abssinper  15657  coskpi  15659  cosq34lt1  15661  logdivlti  15692  rpcxpp1  15717  rpcxpsqrt  15733  rprelogbdiv  15768  binom4  15790  wilthlem1  15794  0sgm  15799  1sgmprm  15808  1sgm2ppw  15809  mersenne  15811  perfect1  15812  perfectlem1  15813  perfectlem2  15814  perfect  15815  zabsle1  15818  lgslem1  15819  lgslem2  15820  lgsfcl2  15825  lgsvalmod  15838  lgsneg  15843  lgsdilem  15846  lgsdir2lem1  15847  lgsdir2lem2  15848  lgsdir2lem3  15849  lgsdir2lem5  15851  lgsne0  15857  lgseisenlem1  15889  lgseisenlem2  15890  lgseisen  15893  lgsquadlem1  15896  lgsquadlem2  15897  lgsquad2lem1  15900  lgsquad2  15902  m1lgs  15904  2lgslem3c  15914  2lgsoddprmlem3c  15928  2lgsoddprmlem3d  15929  2sqlem10  15944  clwwlknonex2lem2  16379  ex-fl  16439  trilpolemeq1  16772