Axiom ax-1cn 8278

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

This axiom is used by:  0cn  8324  1ex  8327  mulrid  8329  mullid  8330  1cnd  8348  muladd11  8466  1p1times  8467  peano2cn  8468  peano2cnm  8599  0reALT  8630  pncan1  8711  npcan1  8712  kcnktkm1cn  8717  ine0  8728  mulm1  8734  mulsubfacd  8753  ixi  8919  inelr  8920  muleqadd  9006  recclap  9017  recap0  9023  recidap  9024  recidap2  9025  div1  9041  1div1e1  9042  diveqap1  9043  recdivap  9056  divdivap1  9061  divdivap2  9062  recdivap2  9063  conjmulap  9067  eqneg  9070  div2negap  9073  recreclt  9238  ofnegsub  9301  nn1m1nn  9331  nn1suc  9332  nnaddcl  9333  nnmulcl  9334  nnsub  9352  1m1e0  9382  neg1cn  9418  neg1ne0  9420  neg1ap0  9422  negneg1e1  9423  1pneg1e0  9424  1m0e1  9426  0p1e1  9427  1p0e1  9429  2m1e1  9431  3m1e2  9433  4m1e3  9434  5m1e4  9435  6m1e5  9436  7m1e6  9437  8m1e7  9438  9m1e8  9439  2p2e4  9440  1p2e3  9448  3p2e5  9455  3p3e6  9456  4p2e6  9457  4p3e7  9458  4p4e8  9459  5p2e7  9460  5p3e8  9461  5p4e9  9462  6p2e8  9463  6p3e9  9464  7p2e9  9465  1t1e1  9466  3t3e9  9472  neg1mulneg1e1  9528  1mhlfehlf  9534  8th4div3  9535  halfpm6th  9536  addltmul  9553  elnn0nn  9616  peano2z  9691  zlem1lt  9712  zltlem1  9713  nnaddm1cl  9717  elz2  9727  zextlt  9749  zeo  9762  peano5uzti  9765  numsuc  9801  numltc  9818  numsucc  9832  numaddc  9840  6p5lem  9862  5p5e10  9863  6p4e10  9864  7p3e10  9867  8p2e10  9872  10m1e9  9888  4t3lem  9889  7t4e28  9903  9t11e99  9922  decbin2  9933  halfthird  9935  5recm6rec  9936  uzp1  9972  peano2uzr  10001  uzaddcl  10002  qreccl  10058  iccf1o  10424  fz01en  10476  fztp  10502  fzsuc2  10503  fztpval  10507  fseq1m1p1  10519  elfzp1b  10521  fz0to4untppr  10548  fzoss2  10598  fzval3  10639  fzosplitsnm1  10644  fzo0to42pr  10655  fzosplitprm1  10670  fldiv4p1lem1div2  10761  flqdiv  10779  frecfzen2  10885  nn0ennn  10891  xnn0nnen  10895  seq3m1  10931  seqshft2g  10940  monoord2  10944  ser3mono  10945  seqf1oglem1  10977  seqf1oglem2  10978  expcl  11015  m1expcl2  11019  expclzaplem  11021  expm1t  11025  1exp  11026  mulexpzap  11037  expadd  11039  expaddzap  11041  expmul  11042  expubnd  11054  neg1sqe1  11092  irec  11097  i4  11100  binom21  11110  bernneq  11119  bernneq2  11120  facndiv  11199  faclbnd6  11204  bcnp1n  11219  bcm1k  11220  bcp1nk  11222  bcn2  11224  bcp1m1  11225  bcpasc  11226  4bc3eq4  11234  hashfz  11284  hashfzo  11285  hashfibclem  11304  hashf1  11309  seq3coll  11316  swrds1  11462  swrdlsw  11463  wrdind  11516  wrd2ind  11517  rei  11687  imi  11688  caucvgrelemrec  11767  recan  11898  iserex  12130  serf0  12143  fsumm1  12208  fsump1  12212  telfsumo  12258  fsumparts  12262  hashiun  12270  binomlem  12275  binom  12276  binom1p  12277  binom11  12278  binom1dif  12279  bcxmas  12281  isumsplit  12283  isum1p  12284  arisum  12290  arisum2  12291  trireciplem  12292  geosergap  12298  geolim  12303  geolim2  12304  georeclim  12305  geo2sum  12306  geo2sum2  12307  0.999...  12313  geoihalfsum  12314  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  prodf1  12334  prodfclim1  12336  prodrbdclem  12363  fproddccvg  12364  prodmodclem2a  12368  fprodntrivap  12376  prodssdc  12381  fprodssdc  12382  esum  12454  ege2le3  12463  efexp  12474  efzval  12475  eftlub  12482  effsumlt  12484  ef4p  12486  tanval3ap  12506  efi4p  12509  tan0  12523  efival  12524  tanaddap  12531  cos2t  12542  cos2tsin  12543  ef01bndlem  12548  cos1bnd  12551  cos2bnd  12552  demoivreALT  12566  eirraplem  12569  3dvds  12656  3dvdsdec  12657  3dvds2dec  12658  odd2np1lem  12664  odd2np1  12665  opoe  12687  omoe  12688  opeo  12689  omeo  12690  m1exp1  12693  n2dvdsm1  12705  flodddiv4  12728  bitsfzo  12747  gcdmultiple  12822  sqgcd  12831  nn0seqcvgd  12844  prmind2  12923  hashdvds  13028  phiprmpw  13029  phiprm  13030  eulerthlemth  13039  sumhashdc  13155  fldivp1  13156  prmpwdvds  13163  pockthlem  13164  pockthi  13166  4sqlem11  13209  4sqlem19  13217  dec5nprm  13222  prmlem0  13249  43prm  13265  83prm  13266  139prm  13267  163prm  13268  317prm  13269  631prm  13270  1259lem2  13272  1259lem3  13273  1259lem4  13274  1259lem5  13275  1259prm  13276  ballotfilem2  13286  mulgnndir  14013  mulgneg2  14018  cnfld1  15018  zsssubrg  15031  mulgrhm2  15054  expcncf  15835  divcncfap  15840  hovercncf  15872  dvid  15921  dvidre  15923  dvexp  15937  dvexp2  15938  dveflem  15952  plyaddlem1  15973  plymullem1  15974  dvply1  15991  reeff1olem  15997  eulerid  16029  cos2pi  16031  sincosq3sgn  16055  sincosq4sgn  16056  cosq23lt0  16060  tangtx  16065  sincos4thpi  16067  sincos6thpi  16069  pigt3  16071  abssinper  16073  coskpi  16075  cosq34lt1  16078  logdivlti  16111  rpcxpp1  16139  rpcxpsqrt  16157  rprelogbdiv  16193  binom4  16219  log2tlbndlog2  16220  log2ublem3  16223  log2ublog2  16224  birthdaylem2  16226  birthdaylog2  16228  wilthlem1  16232  0sgm  16254  ppiprm  16259  ppinprm  16260  chtprm  16261  chtnprm  16262  1sgmprm  16288  1sgm2ppw  16289  ppiqub  16293  chtublem  16295  chtqub  16296  mersenne  16297  perfect1  16298  perfectlem1  16299  perfectlem2  16300  perfect  16301  bcp1ctr  16306  bposlem8  16318  zabsle1  16323  lgslem1  16324  lgslem2  16325  lgsfcl2  16330  lgsvalmod  16343  lgsneg  16348  lgsdilem  16351  lgsdir2lem1  16352  lgsdir2lem2  16353  lgsdir2lem3  16354  lgsdir2lem5  16356  lgsne0  16362  lgseisenlem1  16394  lgseisenlem2  16395  lgseisen  16398  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem1  16405  lgsquad2  16407  m1lgs  16409  2lgslem3c  16419  2lgsoddprmlem3c  16433  2lgsoddprmlem3d  16434  2sqlem10  16449  clwwlknonex2lem2  16884  ex-fl  16944  trilpolemeq1  17296