Axiom ax-1cn 8103

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

This axiom is referenced by:  0cn  8149  1ex  8152  mulrid  8154  mullid  8155  1cnd  8173  muladd11  8290  1p1times  8291  peano2cn  8292  peano2cnm  8423  0reALT  8454  pncan1  8534  npcan1  8535  kcnktkm1cn  8540  ine0  8551  mulm1  8557  mulsubfacd  8576  ixi  8741  inelr  8742  muleqadd  8826  recclap  8837  recap0  8843  recidap  8844  recidap2  8845  div1  8861  1div1e1  8862  diveqap1  8863  recdivap  8876  divdivap1  8881  divdivap2  8882  recdivap2  8883  conjmulap  8887  eqneg  8890  div2negap  8893  recreclt  9058  ofnegsub  9120  nn1m1nn  9139  nn1suc  9140  nnaddcl  9141  nnmulcl  9142  nnsub  9160  1m1e0  9190  neg1cn  9226  neg1ne0  9228  neg1ap0  9230  negneg1e1  9231  1pneg1e0  9232  1m0e1  9234  0p1e1  9235  1p0e1  9237  2m1e1  9239  3m1e2  9241  4m1e3  9242  5m1e4  9243  6m1e5  9244  7m1e6  9245  8m1e7  9246  9m1e8  9247  2p2e4  9248  1p2e3  9256  3p2e5  9263  3p3e6  9264  4p2e6  9265  4p3e7  9266  4p4e8  9267  5p2e7  9268  5p3e8  9269  5p4e9  9270  6p2e8  9271  6p3e9  9272  7p2e9  9273  1t1e1  9274  3t3e9  9279  neg1mulneg1e1  9334  1mhlfehlf  9340  8th4div3  9341  halfpm6th  9342  addltmul  9359  elnn0nn  9422  peano2z  9493  zlem1lt  9514  zltlem1  9515  nnaddm1cl  9519  elz2  9529  zextlt  9550  zeo  9563  peano5uzti  9566  numsuc  9602  numltc  9614  numsucc  9628  numaddc  9636  6p5lem  9658  5p5e10  9659  6p4e10  9660  7p3e10  9663  8p2e10  9668  10m1e9  9684  4t3lem  9685  7t4e28  9699  9t11e99  9718  decbin2  9729  halfthird  9731  5recm6rec  9732  uzp1  9768  peano2uzr  9792  uzaddcl  9793  qreccl  9849  iccf1o  10212  fz01en  10261  fztp  10286  fzsuc2  10287  fztpval  10291  fseq1m1p1  10303  elfzp1b  10305  fz0to4untppr  10332  fzoss2  10382  fzval3  10422  fzosplitsnm1  10427  fzo0to42pr  10438  fzosplitprm1  10452  fldiv4p1lem1div2  10537  flqdiv  10555  frecfzen2  10661  nn0ennn  10667  xnn0nnen  10671  seq3m1  10707  seqshft2g  10716  monoord2  10720  ser3mono  10721  seqf1oglem1  10753  seqf1oglem2  10754  expcl  10791  m1expcl2  10795  expclzaplem  10797  expm1t  10801  1exp  10802  mulexpzap  10813  expadd  10815  expaddzap  10817  expmul  10818  expubnd  10830  neg1sqe1  10868  irec  10873  i4  10876  binom21  10886  bernneq  10894  bernneq2  10895  facndiv  10973  faclbnd6  10978  bcnp1n  10993  bcm1k  10994  bcp1nk  10996  bcn2  10998  bcp1m1  10999  bcpasc  11000  4bc3eq4  11007  hashfz  11056  hashfzo  11057  seq3coll  11077  swrds1  11215  swrdlsw  11216  wrdind  11269  wrd2ind  11270  rei  11425  imi  11426  caucvgrelemrec  11505  recan  11635  iserex  11865  serf0  11878  fsumm1  11942  fsump1  11946  telfsumo  11992  fsumparts  11996  hashiun  12004  binomlem  12009  binom  12010  binom1p  12011  binom11  12012  binom1dif  12013  bcxmas  12015  isumsplit  12017  isum1p  12018  arisum  12024  arisum2  12025  trireciplem  12026  geosergap  12032  geolim  12037  geolim2  12038  georeclim  12039  geo2sum  12040  geo2sum2  12041  0.999...  12047  geoihalfsum  12048  mertenslemi1  12061  mertenslem2  12062  mertensabs  12063  prodf1  12068  prodfclim1  12070  prodrbdclem  12097  fproddccvg  12098  prodmodclem2a  12102  fprodntrivap  12110  prodssdc  12115  fprodssdc  12116  esum  12188  ege2le3  12197  efexp  12208  efzval  12209  eftlub  12216  effsumlt  12218  ef4p  12220  tanval3ap  12240  efi4p  12243  tan0  12257  efival  12258  tanaddap  12265  cos2t  12276  cos2tsin  12277  ef01bndlem  12282  cos1bnd  12285  cos2bnd  12286  demoivreALT  12300  eirraplem  12303  3dvds  12390  3dvdsdec  12391  3dvds2dec  12392  odd2np1lem  12398  odd2np1  12399  opoe  12421  omoe  12422  opeo  12423  omeo  12424  m1exp1  12427  n2dvdsm1  12439  flodddiv4  12462  bitsfzo  12481  gcdmultiple  12556  sqgcd  12565  nn0seqcvgd  12578  prmind2  12657  hashdvds  12758  phiprmpw  12759  phiprm  12760  eulerthlemth  12769  sumhashdc  12885  fldivp1  12886  prmpwdvds  12893  pockthlem  12894  pockthi  12896  4sqlem11  12939  4sqlem19  12947  dec5nprm  12952  mulgnndir  13703  mulgneg2  13708  cnfld1  14551  zsssubrg  14564  mulgrhm2  14589  expcncf  15298  divcncfap  15303  hovercncf  15335  dvid  15384  dvidre  15386  dvexp  15400  dvexp2  15401  dveflem  15415  plyaddlem1  15436  plymullem1  15437  dvply1  15454  reeff1olem  15460  eulerid  15491  cos2pi  15493  sincosq3sgn  15517  sincosq4sgn  15518  cosq23lt0  15522  tangtx  15527  sincos4thpi  15529  sincos6thpi  15531  pigt3  15533  abssinper  15535  coskpi  15537  cosq34lt1  15539  logdivlti  15570  rpcxpp1  15595  rpcxpsqrt  15611  rprelogbdiv  15646  binom4  15668  wilthlem1  15669  0sgm  15674  1sgmprm  15683  1sgm2ppw  15684  mersenne  15686  perfect1  15687  perfectlem1  15688  perfectlem2  15689  perfect  15690  zabsle1  15693  lgslem1  15694  lgslem2  15695  lgsfcl2  15700  lgsvalmod  15713  lgsneg  15718  lgsdilem  15721  lgsdir2lem1  15722  lgsdir2lem2  15723  lgsdir2lem3  15724  lgsdir2lem5  15726  lgsne0  15732  lgseisenlem1  15764  lgseisenlem2  15765  lgseisen  15768  lgsquadlem1  15771  lgsquadlem2  15772  lgsquad2lem1  15775  lgsquad2  15777  m1lgs  15779  2lgslem3c  15789  2lgsoddprmlem3c  15803  2lgsoddprmlem3d  15804  2sqlem10  15819  ex-fl  16144  trilpolemeq1  16468