Axiom ax-1cn 8033

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

This axiom is referenced by:  0cn  8079  1ex  8082  mulrid  8084  mullid  8085  1cnd  8103  muladd11  8220  1p1times  8221  peano2cn  8222  peano2cnm  8353  0reALT  8384  pncan1  8464  npcan1  8465  kcnktkm1cn  8470  ine0  8481  mulm1  8487  mulsubfacd  8506  ixi  8671  inelr  8672  muleqadd  8756  recclap  8767  recap0  8773  recidap  8774  recidap2  8775  div1  8791  1div1e1  8792  diveqap1  8793  recdivap  8806  divdivap1  8811  divdivap2  8812  recdivap2  8813  conjmulap  8817  eqneg  8820  div2negap  8823  recreclt  8988  ofnegsub  9050  nn1m1nn  9069  nn1suc  9070  nnaddcl  9071  nnmulcl  9072  nnsub  9090  1m1e0  9120  neg1cn  9156  neg1ne0  9158  neg1ap0  9160  negneg1e1  9161  1pneg1e0  9162  1m0e1  9164  0p1e1  9165  1p0e1  9167  2m1e1  9169  3m1e2  9171  4m1e3  9172  5m1e4  9173  6m1e5  9174  7m1e6  9175  8m1e7  9176  9m1e8  9177  2p2e4  9178  1p2e3  9186  3p2e5  9193  3p3e6  9194  4p2e6  9195  4p3e7  9196  4p4e8  9197  5p2e7  9198  5p3e8  9199  5p4e9  9200  6p2e8  9201  6p3e9  9202  7p2e9  9203  1t1e1  9204  3t3e9  9209  neg1mulneg1e1  9264  1mhlfehlf  9270  8th4div3  9271  halfpm6th  9272  addltmul  9289  elnn0nn  9352  peano2z  9423  zlem1lt  9444  zltlem1  9445  nnaddm1cl  9449  elz2  9459  zextlt  9480  zeo  9493  peano5uzti  9496  numsuc  9532  numltc  9544  numsucc  9558  numaddc  9566  6p5lem  9588  5p5e10  9589  6p4e10  9590  7p3e10  9593  8p2e10  9598  10m1e9  9614  4t3lem  9615  7t4e28  9629  9t11e99  9648  decbin2  9659  halfthird  9661  5recm6rec  9662  uzp1  9697  peano2uzr  9721  uzaddcl  9722  qreccl  9778  iccf1o  10141  fz01en  10190  fztp  10215  fzsuc2  10216  fztpval  10220  fseq1m1p1  10232  elfzp1b  10234  fz0to4untppr  10261  fzoss2  10311  fzval3  10350  fzosplitsnm1  10355  fzo0to42pr  10366  fzosplitprm1  10380  fldiv4p1lem1div2  10465  flqdiv  10483  frecfzen2  10589  nn0ennn  10595  xnn0nnen  10599  seq3m1  10635  seqshft2g  10644  monoord2  10648  ser3mono  10649  seqf1oglem1  10681  seqf1oglem2  10682  expcl  10719  m1expcl2  10723  expclzaplem  10725  expm1t  10729  1exp  10730  mulexpzap  10741  expadd  10743  expaddzap  10745  expmul  10746  expubnd  10758  neg1sqe1  10796  irec  10801  i4  10804  binom21  10814  bernneq  10822  bernneq2  10823  facndiv  10901  faclbnd6  10906  bcnp1n  10921  bcm1k  10922  bcp1nk  10924  bcn2  10926  bcp1m1  10927  bcpasc  10928  4bc3eq4  10935  hashfz  10983  hashfzo  10984  seq3coll  11004  swrds1  11139  swrdlsw  11140  wrdind  11193  wrd2ind  11194  rei  11280  imi  11281  caucvgrelemrec  11360  recan  11490  iserex  11720  serf0  11733  fsumm1  11797  fsump1  11801  telfsumo  11847  fsumparts  11851  hashiun  11859  binomlem  11864  binom  11865  binom1p  11866  binom11  11867  binom1dif  11868  bcxmas  11870  isumsplit  11872  isum1p  11873  arisum  11879  arisum2  11880  trireciplem  11881  geosergap  11887  geolim  11892  geolim2  11893  georeclim  11894  geo2sum  11895  geo2sum2  11896  0.999...  11902  geoihalfsum  11903  mertenslemi1  11916  mertenslem2  11917  mertensabs  11918  prodf1  11923  prodfclim1  11925  prodrbdclem  11952  fproddccvg  11953  prodmodclem2a  11957  fprodntrivap  11965  prodssdc  11970  fprodssdc  11971  esum  12043  ege2le3  12052  efexp  12063  efzval  12064  eftlub  12071  effsumlt  12073  ef4p  12075  tanval3ap  12095  efi4p  12098  tan0  12112  efival  12113  tanaddap  12120  cos2t  12131  cos2tsin  12132  ef01bndlem  12137  cos1bnd  12140  cos2bnd  12141  demoivreALT  12155  eirraplem  12158  3dvds  12245  3dvdsdec  12246  3dvds2dec  12247  odd2np1lem  12253  odd2np1  12254  opoe  12276  omoe  12277  opeo  12278  omeo  12279  m1exp1  12282  n2dvdsm1  12294  flodddiv4  12317  bitsfzo  12336  gcdmultiple  12411  sqgcd  12420  nn0seqcvgd  12433  prmind2  12512  hashdvds  12613  phiprmpw  12614  phiprm  12615  eulerthlemth  12624  sumhashdc  12740  fldivp1  12741  prmpwdvds  12748  pockthlem  12749  pockthi  12751  4sqlem11  12794  4sqlem19  12802  dec5nprm  12807  mulgnndir  13557  mulgneg2  13562  cnfld1  14404  zsssubrg  14417  mulgrhm2  14442  expcncf  15151  divcncfap  15156  hovercncf  15188  dvid  15237  dvidre  15239  dvexp  15253  dvexp2  15254  dveflem  15268  plyaddlem1  15289  plymullem1  15290  dvply1  15307  reeff1olem  15313  eulerid  15344  cos2pi  15346  sincosq3sgn  15370  sincosq4sgn  15371  cosq23lt0  15375  tangtx  15380  sincos4thpi  15382  sincos6thpi  15384  pigt3  15386  abssinper  15388  coskpi  15390  cosq34lt1  15392  logdivlti  15423  rpcxpp1  15448  rpcxpsqrt  15464  rprelogbdiv  15499  binom4  15521  wilthlem1  15522  0sgm  15527  1sgmprm  15536  1sgm2ppw  15537  mersenne  15539  perfect1  15540  perfectlem1  15541  perfectlem2  15542  perfect  15543  zabsle1  15546  lgslem1  15547  lgslem2  15548  lgsfcl2  15553  lgsvalmod  15566  lgsneg  15571  lgsdilem  15574  lgsdir2lem1  15575  lgsdir2lem2  15576  lgsdir2lem3  15577  lgsdir2lem5  15579  lgsne0  15585  lgseisenlem1  15617  lgseisenlem2  15618  lgseisen  15621  lgsquadlem1  15624  lgsquadlem2  15625  lgsquad2lem1  15628  lgsquad2  15630  m1lgs  15632  2lgslem3c  15642  2lgsoddprmlem3c  15656  2lgsoddprmlem3d  15657  2sqlem10  15672  ex-fl  15795  trilpolemeq1  16114