Axiom ax-1cn 8272

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

This axiom is used by:  0cn  8318  1ex  8321  mulrid  8323  mullid  8324  1cnd  8342  muladd11  8460  1p1times  8461  peano2cn  8462  peano2cnm  8593  0reALT  8624  pncan1  8705  npcan1  8706  kcnktkm1cn  8711  ine0  8722  mulm1  8728  mulsubfacd  8747  ixi  8913  inelr  8914  muleqadd  9000  recclap  9011  recap0  9017  recidap  9018  recidap2  9019  div1  9035  1div1e1  9036  diveqap1  9037  recdivap  9050  divdivap1  9055  divdivap2  9056  recdivap2  9057  conjmulap  9061  eqneg  9064  div2negap  9067  recreclt  9232  ofnegsub  9294  nn1m1nn  9324  nn1suc  9325  nnaddcl  9326  nnmulcl  9327  nnsub  9345  1m1e0  9375  neg1cn  9411  neg1ne0  9413  neg1ap0  9415  negneg1e1  9416  1pneg1e0  9417  1m0e1  9419  0p1e1  9420  1p0e1  9422  2m1e1  9424  3m1e2  9426  4m1e3  9427  5m1e4  9428  6m1e5  9429  7m1e6  9430  8m1e7  9431  9m1e8  9432  2p2e4  9433  1p2e3  9441  3p2e5  9448  3p3e6  9449  4p2e6  9450  4p3e7  9451  4p4e8  9452  5p2e7  9453  5p3e8  9454  5p4e9  9455  6p2e8  9456  6p3e9  9457  7p2e9  9458  1t1e1  9459  3t3e9  9465  neg1mulneg1e1  9521  1mhlfehlf  9527  8th4div3  9528  halfpm6th  9529  addltmul  9546  elnn0nn  9609  peano2z  9684  zlem1lt  9705  zltlem1  9706  nnaddm1cl  9710  elz2  9720  zextlt  9742  zeo  9755  peano5uzti  9758  numsuc  9794  numltc  9811  numsucc  9825  numaddc  9833  6p5lem  9855  5p5e10  9856  6p4e10  9857  7p3e10  9860  8p2e10  9865  10m1e9  9881  4t3lem  9882  7t4e28  9896  9t11e99  9915  decbin2  9926  halfthird  9928  5recm6rec  9929  uzp1  9965  peano2uzr  9994  uzaddcl  9995  qreccl  10051  iccf1o  10417  fz01en  10469  fztp  10495  fzsuc2  10496  fztpval  10500  fseq1m1p1  10512  elfzp1b  10514  fz0to4untppr  10541  fzoss2  10591  fzval3  10632  fzosplitsnm1  10637  fzo0to42pr  10648  fzosplitprm1  10663  fldiv4p1lem1div2  10753  flqdiv  10771  frecfzen2  10877  nn0ennn  10883  xnn0nnen  10887  seq3m1  10923  seqshft2g  10932  monoord2  10936  ser3mono  10937  seqf1oglem1  10969  seqf1oglem2  10970  expcl  11007  m1expcl2  11011  expclzaplem  11013  expm1t  11017  1exp  11018  mulexpzap  11029  expadd  11031  expaddzap  11033  expmul  11034  expubnd  11046  neg1sqe1  11084  irec  11089  i4  11092  binom21  11102  bernneq  11111  bernneq2  11112  facndiv  11191  faclbnd6  11196  bcnp1n  11211  bcm1k  11212  bcp1nk  11214  bcn2  11216  bcp1m1  11217  bcpasc  11218  4bc3eq4  11226  hashfz  11276  hashfzo  11277  hashfibclem  11296  hashf1  11301  seq3coll  11308  swrds1  11454  swrdlsw  11455  wrdind  11508  wrd2ind  11509  rei  11679  imi  11680  caucvgrelemrec  11759  recan  11890  iserex  12121  serf0  12134  fsumm1  12199  fsump1  12203  telfsumo  12249  fsumparts  12253  hashiun  12261  binomlem  12266  binom  12267  binom1p  12268  binom11  12269  binom1dif  12270  bcxmas  12272  isumsplit  12274  isum1p  12275  arisum  12281  arisum2  12282  trireciplem  12283  geosergap  12289  geolim  12294  geolim2  12295  georeclim  12296  geo2sum  12297  geo2sum2  12298  0.999...  12304  geoihalfsum  12305  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  prodf1  12325  prodfclim1  12327  prodrbdclem  12354  fproddccvg  12355  prodmodclem2a  12359  fprodntrivap  12367  prodssdc  12372  fprodssdc  12373  esum  12445  ege2le3  12454  efexp  12465  efzval  12466  eftlub  12473  effsumlt  12475  ef4p  12477  tanval3ap  12497  efi4p  12500  tan0  12514  efival  12515  tanaddap  12522  cos2t  12533  cos2tsin  12534  ef01bndlem  12539  cos1bnd  12542  cos2bnd  12543  demoivreALT  12557  eirraplem  12560  3dvds  12647  3dvdsdec  12648  3dvds2dec  12649  odd2np1lem  12655  odd2np1  12656  opoe  12678  omoe  12679  opeo  12680  omeo  12681  m1exp1  12684  n2dvdsm1  12696  flodddiv4  12719  bitsfzo  12738  gcdmultiple  12813  sqgcd  12822  nn0seqcvgd  12835  prmind2  12914  hashdvds  13019  phiprmpw  13020  phiprm  13021  eulerthlemth  13030  sumhashdc  13146  fldivp1  13147  prmpwdvds  13154  pockthlem  13155  pockthi  13157  4sqlem11  13200  4sqlem19  13208  dec5nprm  13213  prmlem0  13240  43prm  13256  83prm  13257  139prm  13258  163prm  13259  317prm  13260  631prm  13261  1259lem2  13263  1259lem3  13264  1259lem4  13265  1259lem5  13266  1259prm  13267  ballotfilem2  13277  mulgnndir  14003  mulgneg2  14008  cnfld1  14958  zsssubrg  14971  mulgrhm2  14994  expcncf  15759  divcncfap  15764  hovercncf  15796  dvid  15845  dvidre  15847  dvexp  15861  dvexp2  15862  dveflem  15876  plyaddlem1  15897  plymullem1  15898  dvply1  15915  reeff1olem  15921  eulerid  15953  cos2pi  15955  sincosq3sgn  15979  sincosq4sgn  15980  cosq23lt0  15984  tangtx  15989  sincos4thpi  15991  sincos6thpi  15993  pigt3  15995  abssinper  15997  coskpi  15999  cosq34lt1  16001  logdivlti  16033  rpcxpp1  16061  rpcxpsqrt  16077  rprelogbdiv  16112  binom4  16138  log2tlbndlog2  16139  log2ublem3  16142  log2ublog2  16143  birthdaylem2  16145  birthdaylog2  16147  wilthlem1  16151  0sgm  16166  ppiprm  16170  ppinprm  16171  1sgmprm  16189  1sgm2ppw  16190  ppiqub  16194  mersenne  16195  perfect1  16196  perfectlem1  16197  perfectlem2  16198  perfect  16199  bcp1ctr  16204  zabsle1  16216  lgslem1  16217  lgslem2  16218  lgsfcl2  16223  lgsvalmod  16236  lgsneg  16241  lgsdilem  16244  lgsdir2lem1  16245  lgsdir2lem2  16246  lgsdir2lem3  16247  lgsdir2lem5  16249  lgsne0  16255  lgseisenlem1  16287  lgseisenlem2  16288  lgseisen  16291  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem1  16298  lgsquad2  16300  m1lgs  16302  2lgslem3c  16312  2lgsoddprmlem3c  16326  2lgsoddprmlem3d  16327  2sqlem10  16342  clwwlknonex2lem2  16777  ex-fl  16837  trilpolemeq1  17187