Axiom ax-1cn 8017

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

This axiom is referenced by:  0cn  8063  1ex  8066  mulrid  8068  mullid  8069  1cnd  8087  muladd11  8204  1p1times  8205  peano2cn  8206  peano2cnm  8337  0reALT  8368  pncan1  8448  npcan1  8449  kcnktkm1cn  8454  ine0  8465  mulm1  8471  mulsubfacd  8490  ixi  8655  inelr  8656  muleqadd  8740  recclap  8751  recap0  8757  recidap  8758  recidap2  8759  div1  8775  1div1e1  8776  diveqap1  8777  recdivap  8790  divdivap1  8795  divdivap2  8796  recdivap2  8797  conjmulap  8801  eqneg  8804  div2negap  8807  recreclt  8972  ofnegsub  9034  nn1m1nn  9053  nn1suc  9054  nnaddcl  9055  nnmulcl  9056  nnsub  9074  1m1e0  9104  neg1cn  9140  neg1ne0  9142  neg1ap0  9144  negneg1e1  9145  1pneg1e0  9146  1m0e1  9148  0p1e1  9149  1p0e1  9151  2m1e1  9153  3m1e2  9155  4m1e3  9156  5m1e4  9157  6m1e5  9158  7m1e6  9159  8m1e7  9160  9m1e8  9161  2p2e4  9162  1p2e3  9170  3p2e5  9177  3p3e6  9178  4p2e6  9179  4p3e7  9180  4p4e8  9181  5p2e7  9182  5p3e8  9183  5p4e9  9184  6p2e8  9185  6p3e9  9186  7p2e9  9187  1t1e1  9188  3t3e9  9193  neg1mulneg1e1  9248  1mhlfehlf  9254  8th4div3  9255  halfpm6th  9256  addltmul  9273  elnn0nn  9336  peano2z  9407  zlem1lt  9428  zltlem1  9429  nnaddm1cl  9433  elz2  9443  zextlt  9464  zeo  9477  peano5uzti  9480  numsuc  9516  numltc  9528  numsucc  9542  numaddc  9550  6p5lem  9572  5p5e10  9573  6p4e10  9574  7p3e10  9577  8p2e10  9582  10m1e9  9598  4t3lem  9599  7t4e28  9613  9t11e99  9632  decbin2  9643  halfthird  9645  5recm6rec  9646  uzp1  9681  peano2uzr  9705  uzaddcl  9706  qreccl  9762  iccf1o  10125  fz01en  10174  fztp  10199  fzsuc2  10200  fztpval  10204  fseq1m1p1  10216  elfzp1b  10218  fz0to4untppr  10245  fzoss2  10294  fzval3  10331  fzosplitsnm1  10336  fzo0to42pr  10347  fzosplitprm1  10361  fldiv4p1lem1div2  10446  flqdiv  10464  frecfzen2  10570  nn0ennn  10576  xnn0nnen  10580  seq3m1  10616  seqshft2g  10625  monoord2  10629  ser3mono  10630  seqf1oglem1  10662  seqf1oglem2  10663  expcl  10700  m1expcl2  10704  expclzaplem  10706  expm1t  10710  1exp  10711  mulexpzap  10722  expadd  10724  expaddzap  10726  expmul  10727  expubnd  10739  neg1sqe1  10777  irec  10782  i4  10785  binom21  10795  bernneq  10803  bernneq2  10804  facndiv  10882  faclbnd6  10887  bcnp1n  10902  bcm1k  10903  bcp1nk  10905  bcn2  10907  bcp1m1  10908  bcpasc  10909  4bc3eq4  10916  hashfz  10964  hashfzo  10965  seq3coll  10985  rei  11181  imi  11182  caucvgrelemrec  11261  recan  11391  iserex  11621  serf0  11634  fsumm1  11698  fsump1  11702  telfsumo  11748  fsumparts  11752  hashiun  11760  binomlem  11765  binom  11766  binom1p  11767  binom11  11768  binom1dif  11769  bcxmas  11771  isumsplit  11773  isum1p  11774  arisum  11780  arisum2  11781  trireciplem  11782  geosergap  11788  geolim  11793  geolim2  11794  georeclim  11795  geo2sum  11796  geo2sum2  11797  0.999...  11803  geoihalfsum  11804  mertenslemi1  11817  mertenslem2  11818  mertensabs  11819  prodf1  11824  prodfclim1  11826  prodrbdclem  11853  fproddccvg  11854  prodmodclem2a  11858  fprodntrivap  11866  prodssdc  11871  fprodssdc  11872  esum  11944  ege2le3  11953  efexp  11964  efzval  11965  eftlub  11972  effsumlt  11974  ef4p  11976  tanval3ap  11996  efi4p  11999  tan0  12013  efival  12014  tanaddap  12021  cos2t  12032  cos2tsin  12033  ef01bndlem  12038  cos1bnd  12041  cos2bnd  12042  demoivreALT  12056  eirraplem  12059  3dvds  12146  3dvdsdec  12147  3dvds2dec  12148  odd2np1lem  12154  odd2np1  12155  opoe  12177  omoe  12178  opeo  12179  omeo  12180  m1exp1  12183  n2dvdsm1  12195  flodddiv4  12218  bitsfzo  12237  gcdmultiple  12312  sqgcd  12321  nn0seqcvgd  12334  prmind2  12413  hashdvds  12514  phiprmpw  12515  phiprm  12516  eulerthlemth  12525  sumhashdc  12641  fldivp1  12642  prmpwdvds  12649  pockthlem  12650  pockthi  12652  4sqlem11  12695  4sqlem19  12703  dec5nprm  12708  mulgnndir  13458  mulgneg2  13463  cnfld1  14305  zsssubrg  14318  mulgrhm2  14343  expcncf  15052  divcncfap  15057  hovercncf  15089  dvid  15138  dvidre  15140  dvexp  15154  dvexp2  15155  dveflem  15169  plyaddlem1  15190  plymullem1  15191  dvply1  15208  reeff1olem  15214  eulerid  15245  cos2pi  15247  sincosq3sgn  15271  sincosq4sgn  15272  cosq23lt0  15276  tangtx  15281  sincos4thpi  15283  sincos6thpi  15285  pigt3  15287  abssinper  15289  coskpi  15291  cosq34lt1  15293  logdivlti  15324  rpcxpp1  15349  rpcxpsqrt  15365  rprelogbdiv  15400  binom4  15422  wilthlem1  15423  0sgm  15428  1sgmprm  15437  1sgm2ppw  15438  mersenne  15440  perfect1  15441  perfectlem1  15442  perfectlem2  15443  perfect  15444  zabsle1  15447  lgslem1  15448  lgslem2  15449  lgsfcl2  15454  lgsvalmod  15467  lgsneg  15472  lgsdilem  15475  lgsdir2lem1  15476  lgsdir2lem2  15477  lgsdir2lem3  15478  lgsdir2lem5  15480  lgsne0  15486  lgseisenlem1  15518  lgseisenlem2  15519  lgseisen  15522  lgsquadlem1  15525  lgsquadlem2  15526  lgsquad2lem1  15529  lgsquad2  15531  m1lgs  15533  2lgslem3c  15543  2lgsoddprmlem3c  15557  2lgsoddprmlem3d  15558  2sqlem10  15573  ex-fl  15623  trilpolemeq1  15941