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  9689  zlem1lt  9710  zltlem1  9711  nnaddm1cl  9715  elz2  9725  zextlt  9748  zeo  9761  peano5uzti  9764  numsuc  9800  numltc  9817  numsucc  9831  numaddc  9839  6p5lem  9861  5p5e10  9862  6p4e10  9863  7p3e10  9866  8p2e10  9871  10m1e9  9887  4t3lem  9888  7t4e28  9902  9t11e99  9921  decbin2  9932  halfthird  9934  5recm6rec  9935  uzp1  9971  peano2uzr  10000  uzaddcl  10001  qreccl  10057  iccf1o  10423  fz01en  10475  fztp  10501  fzsuc2  10502  fztpval  10506  fseq1m1p1  10518  elfzp1b  10520  fz0to4untppr  10547  fzoss2  10597  fzval3  10638  fzosplitsnm1  10643  fzo0to42pr  10654  fzosplitprm1  10669  fldiv4p1lem1div2  10760  flqdiv  10778  frecfzen2  10884  nn0ennn  10890  xnn0nnen  10894  seq3m1  10930  seqshft2g  10939  monoord2  10943  ser3mono  10944  seqf1oglem1  10976  seqf1oglem2  10977  expcl  11014  m1expcl2  11018  expclzaplem  11020  expm1t  11024  1exp  11025  mulexpzap  11036  expadd  11038  expaddzap  11040  expmul  11041  expubnd  11053  neg1sqe1  11091  irec  11096  i4  11099  binom21  11109  bernneq  11118  bernneq2  11119  facndiv  11198  faclbnd6  11203  bcnp1n  11218  bcm1k  11219  bcp1nk  11221  bcn2  11223  bcp1m1  11224  bcpasc  11225  4bc3eq4  11233  hashfz  11283  hashfzo  11284  hashfibclem  11303  hashf1  11308  seq3coll  11315  swrds1  11461  swrdlsw  11462  wrdind  11515  wrd2ind  11516  rei  11686  imi  11687  caucvgrelemrec  11766  recan  11897  iserex  12129  serf0  12142  fsumm1  12207  fsump1  12211  telfsumo  12257  fsumparts  12261  hashiun  12269  binomlem  12274  binom  12275  binom1p  12276  binom11  12277  binom1dif  12278  bcxmas  12280  isumsplit  12282  isum1p  12283  arisum  12289  arisum2  12290  trireciplem  12291  geosergap  12297  geolim  12302  geolim2  12303  georeclim  12304  geo2sum  12305  geo2sum2  12306  0.999...  12312  geoihalfsum  12313  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  prodf1  12333  prodfclim1  12335  prodrbdclem  12362  fproddccvg  12363  prodmodclem2a  12367  fprodntrivap  12375  prodssdc  12380  fprodssdc  12381  esum  12453  ege2le3  12462  efexp  12473  efzval  12474  eftlub  12481  effsumlt  12483  ef4p  12485  tanval3ap  12505  efi4p  12508  tan0  12522  efival  12523  tanaddap  12530  cos2t  12541  cos2tsin  12542  ef01bndlem  12547  cos1bnd  12550  cos2bnd  12551  demoivreALT  12565  eirraplem  12568  3dvds  12655  3dvdsdec  12656  3dvds2dec  12657  odd2np1lem  12663  odd2np1  12664  opoe  12686  omoe  12687  opeo  12688  omeo  12689  m1exp1  12692  n2dvdsm1  12704  flodddiv4  12727  bitsfzo  12746  gcdmultiple  12821  sqgcd  12830  nn0seqcvgd  12843  prmind2  12922  hashdvds  13027  phiprmpw  13028  phiprm  13029  eulerthlemth  13038  sumhashdc  13154  fldivp1  13155  prmpwdvds  13162  pockthlem  13163  pockthi  13165  4sqlem11  13208  4sqlem19  13216  dec5nprm  13221  prmlem0  13248  43prm  13264  83prm  13265  139prm  13266  163prm  13267  317prm  13268  631prm  13269  1259lem2  13271  1259lem3  13272  1259lem4  13273  1259lem5  13274  1259prm  13275  ballotfilem2  13285  mulgnndir  14012  mulgneg2  14017  cnfld1  15017  zsssubrg  15030  mulgrhm2  15053  expcncf  15852  divcncfap  15857  hovercncf  15889  dvid  15938  dvidre  15940  dvexp  15954  dvexp2  15955  dveflem  15969  plyaddlem1  15990  plymullem1  15991  dvply1  16008  reeff1olem  16014  eulerid  16046  cos2pi  16048  sincosq3sgn  16072  sincosq4sgn  16073  cosq23lt0  16077  tangtx  16082  sincos4thpi  16084  sincos6thpi  16086  pigt3  16088  abssinper  16090  coskpi  16092  cosq34lt1  16095  logdivlti  16128  rpcxpp1  16156  rpcxpsqrt  16174  rprelogbdiv  16210  binom4  16236  log2tlbndlog2  16237  log2ublem3  16240  log2ublog2  16241  birthdaylem2  16243  birthdaylog2  16245  wilthlem1  16249  0sgm  16271  ppiprm  16276  ppinprm  16277  chtprm  16278  chtnprm  16279  1sgmprm  16305  1sgm2ppw  16306  ppiqub  16310  chtublem  16312  chtqub  16313  mersenne  16314  perfect1  16315  perfectlem1  16316  perfectlem2  16317  perfect  16318  bcp1ctr  16323  bposlem8  16335  zabsle1  16340  lgslem1  16341  lgslem2  16342  lgsfcl2  16347  lgsvalmod  16360  lgsneg  16365  lgsdilem  16368  lgsdir2lem1  16369  lgsdir2lem2  16370  lgsdir2lem3  16371  lgsdir2lem5  16373  lgsne0  16379  lgseisenlem1  16411  lgseisenlem2  16412  lgseisen  16415  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem1  16422  lgsquad2  16424  m1lgs  16426  2lgslem3c  16436  2lgsoddprmlem3c  16450  2lgsoddprmlem3d  16451  2sqlem10  16466  clwwlknonex2lem2  16901  ex-fl  16961  trilpolemeq1  17313