Axiom ax-1cn 8236

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

This axiom is referenced by:  0cn  8282  1ex  8285  mulrid  8287  mullid  8288  1cnd  8306  muladd11  8423  1p1times  8424  peano2cn  8425  peano2cnm  8556  0reALT  8587  pncan1  8668  npcan1  8669  kcnktkm1cn  8674  ine0  8685  mulm1  8691  mulsubfacd  8710  ixi  8875  inelr  8876  muleqadd  8962  recclap  8973  recap0  8979  recidap  8980  recidap2  8981  div1  8997  1div1e1  8998  diveqap1  8999  recdivap  9012  divdivap1  9017  divdivap2  9018  recdivap2  9019  conjmulap  9023  eqneg  9026  div2negap  9029  recreclt  9194  ofnegsub  9256  nn1m1nn  9275  nn1suc  9276  nnaddcl  9277  nnmulcl  9278  nnsub  9296  1m1e0  9326  neg1cn  9362  neg1ne0  9364  neg1ap0  9366  negneg1e1  9367  1pneg1e0  9368  1m0e1  9370  0p1e1  9371  1p0e1  9373  2m1e1  9375  3m1e2  9377  4m1e3  9378  5m1e4  9379  6m1e5  9380  7m1e6  9381  8m1e7  9382  9m1e8  9383  2p2e4  9384  1p2e3  9392  3p2e5  9399  3p3e6  9400  4p2e6  9401  4p3e7  9402  4p4e8  9403  5p2e7  9404  5p3e8  9405  5p4e9  9406  6p2e8  9407  6p3e9  9408  7p2e9  9409  1t1e1  9410  3t3e9  9415  neg1mulneg1e1  9470  1mhlfehlf  9476  8th4div3  9477  halfpm6th  9478  addltmul  9495  elnn0nn  9558  peano2z  9633  zlem1lt  9654  zltlem1  9655  nnaddm1cl  9659  elz2  9669  zextlt  9691  zeo  9704  peano5uzti  9707  numsuc  9743  numltc  9755  numsucc  9769  numaddc  9777  6p5lem  9799  5p5e10  9800  6p4e10  9801  7p3e10  9804  8p2e10  9809  10m1e9  9825  4t3lem  9826  7t4e28  9840  9t11e99  9859  decbin2  9870  halfthird  9872  5recm6rec  9873  uzp1  9909  peano2uzr  9938  uzaddcl  9939  qreccl  9995  iccf1o  10360  fz01en  10411  fztp  10437  fzsuc2  10438  fztpval  10442  fseq1m1p1  10454  elfzp1b  10456  fz0to4untppr  10483  fzoss2  10533  fzval3  10574  fzosplitsnm1  10579  fzo0to42pr  10590  fzosplitprm1  10605  fldiv4p1lem1div2  10692  flqdiv  10710  frecfzen2  10816  nn0ennn  10822  xnn0nnen  10826  seq3m1  10862  seqshft2g  10871  monoord2  10875  ser3mono  10876  seqf1oglem1  10908  seqf1oglem2  10909  expcl  10946  m1expcl2  10950  expclzaplem  10952  expm1t  10956  1exp  10957  mulexpzap  10968  expadd  10970  expaddzap  10972  expmul  10973  expubnd  10985  neg1sqe1  11023  irec  11028  i4  11031  binom21  11041  bernneq  11050  bernneq2  11051  facndiv  11129  faclbnd6  11134  bcnp1n  11149  bcm1k  11150  bcp1nk  11152  bcn2  11154  bcp1m1  11155  bcpasc  11156  4bc3eq4  11164  hashfz  11214  hashfzo  11215  hashfibclem  11234  seq3coll  11242  swrds1  11388  swrdlsw  11389  wrdind  11442  wrd2ind  11443  rei  11612  imi  11613  caucvgrelemrec  11692  recan  11822  iserex  12052  serf0  12065  fsumm1  12130  fsump1  12134  telfsumo  12180  fsumparts  12184  hashiun  12192  binomlem  12197  binom  12198  binom1p  12199  binom11  12200  binom1dif  12201  bcxmas  12203  isumsplit  12205  isum1p  12206  arisum  12212  arisum2  12213  trireciplem  12214  geosergap  12220  geolim  12225  geolim2  12226  georeclim  12227  geo2sum  12228  geo2sum2  12229  0.999...  12235  geoihalfsum  12236  mertenslemi1  12249  mertenslem2  12250  mertensabs  12251  prodf1  12256  prodfclim1  12258  prodrbdclem  12285  fproddccvg  12286  prodmodclem2a  12290  fprodntrivap  12298  prodssdc  12303  fprodssdc  12304  esum  12376  ege2le3  12385  efexp  12396  efzval  12397  eftlub  12404  effsumlt  12406  ef4p  12408  tanval3ap  12428  efi4p  12431  tan0  12445  efival  12446  tanaddap  12453  cos2t  12464  cos2tsin  12465  ef01bndlem  12470  cos1bnd  12473  cos2bnd  12474  demoivreALT  12488  eirraplem  12491  3dvds  12578  3dvdsdec  12579  3dvds2dec  12580  odd2np1lem  12586  odd2np1  12587  opoe  12609  omoe  12610  opeo  12611  omeo  12612  m1exp1  12615  n2dvdsm1  12627  flodddiv4  12650  bitsfzo  12669  gcdmultiple  12744  sqgcd  12753  nn0seqcvgd  12766  prmind2  12845  hashdvds  12946  phiprmpw  12947  phiprm  12948  eulerthlemth  12957  sumhashdc  13073  fldivp1  13074  prmpwdvds  13081  pockthlem  13082  pockthi  13084  4sqlem11  13127  4sqlem19  13135  dec5nprm  13140  ballotfilem2  13175  mulgnndir  13907  mulgneg2  13912  cnfld1  14849  zsssubrg  14862  mulgrhm2  14887  expcncf  15603  divcncfap  15608  hovercncf  15640  dvid  15689  dvidre  15691  dvexp  15705  dvexp2  15706  dveflem  15720  plyaddlem1  15741  plymullem1  15742  dvply1  15759  reeff1olem  15765  eulerid  15796  cos2pi  15798  sincosq3sgn  15822  sincosq4sgn  15823  cosq23lt0  15827  tangtx  15832  sincos4thpi  15834  sincos6thpi  15836  pigt3  15838  abssinper  15840  coskpi  15842  cosq34lt1  15844  logdivlti  15875  rpcxpp1  15900  rpcxpsqrt  15916  rprelogbdiv  15951  binom4  15973  wilthlem1  15977  0sgm  15982  1sgmprm  15991  1sgm2ppw  15992  mersenne  15994  perfect1  15995  perfectlem1  15996  perfectlem2  15997  perfect  15998  zabsle1  16001  lgslem1  16002  lgslem2  16003  lgsfcl2  16008  lgsvalmod  16021  lgsneg  16026  lgsdilem  16029  lgsdir2lem1  16030  lgsdir2lem2  16031  lgsdir2lem3  16032  lgsdir2lem5  16034  lgsne0  16040  lgseisenlem1  16072  lgseisenlem2  16073  lgseisen  16076  lgsquadlem1  16079  lgsquadlem2  16080  lgsquad2lem1  16083  lgsquad2  16085  m1lgs  16087  2lgslem3c  16097  2lgsoddprmlem3c  16111  2lgsoddprmlem3d  16112  2sqlem10  16127  clwwlknonex2lem2  16562  ex-fl  16622  trilpolemeq1  16963