MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-1cn Unicode version

Axiom ax-1cn 8791
Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn 8767. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-1cn  |-  1  e.  CC

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 8734 . 2  class  1
2 cc 8731 . 2  class  CC
31, 2wcel 1685 1  wff  1  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  8827  1ex  8829  mulid1  8831  mulid2  8832  1re  8833  muladd11  8978  1p1times  8979  peano2cn  8980  mul02lem2  8985  addid1  8988  cnegex2  8990  addcom  8994  addcomd  9010  0reALT  9139  ine0  9211  mulm1  9217  0lt1  9292  ixi  9393  muleqadd  9408  reccl  9427  recne0  9433  recid  9434  recid2  9435  div1  9449  diveq1  9450  recrec  9453  rec11  9454  rec11r  9455  recdiv  9462  divdiv1  9467  divdiv2  9468  recdiv2  9469  conjmul  9473  rereccl  9474  eqneg  9476  div2neg  9479  subrec  9585  reclt1  9647  recgt1  9648  recp1lt1  9650  recreclt  9651  recgt0ii  9658  inelr  9732  ofnegsub  9740  peano5nni  9745  nn1m1nn  9762  nn1suc  9763  nnaddcl  9764  nnmulcl  9765  nnsub  9780  neg1cn  9809  1m1e0  9810  0p1e1  9835  2m1e1  9837  2p2e4  9838  2times  9839  3p2e5  9851  3p3e6  9852  4p2e6  9853  4p3e7  9854  4p4e8  9855  5p2e7  9856  5p3e8  9857  5p4e9  9858  5p5e10  9859  6p2e8  9860  6p3e9  9861  6p4e10  9862  7p2e9  9863  7p3e10  9864  8p2e10  9865  1t1e1  9866  3t3e9  9869  halflt1  9929  1mhlfehlf  9930  8th4div3  9931  halfpm6th  9932  addltmul  9943  elnn0nn  10002  elnnnn0  10003  elz2  10036  zlem1lt  10065  zltlem1  10066  nnaddm1cl  10069  zextlt  10082  zneo  10090  nneo  10091  zeo  10093  peano5uzi  10096  uzindOLD  10102  numsuc  10132  numltc  10140  numsucc  10146  numaddc  10155  6p5lem  10169  4t3lem  10191  7t4e28  10204  decbin2  10224  uzp1  10257  peano2uzr  10270  uzaddcl  10271  rebtwnz  10311  rpnnen1lem5  10342  qbtwnre  10521  lincmb01cmp  10772  iccf1o  10773  xov1plusxeqvd  10775  fz01en  10813  fztp  10836  fzsuc2  10837  fztpval  10840  fseq1m1p1  10853  fzm1  10857  fzoss2  10892  fzval3  10906  fladdz  10945  ceim1l  10952  fldiv  10959  modnegd  10999  uzrdgxfr  11024  fzen2  11026  nn0ennn  11036  seqm1  11058  seqshft2  11067  monoord2  11072  sermono  11073  seqf1olem1  11080  seqf1olem2  11081  seqz  11089  ser1const  11097  expneg  11106  expcl  11116  m1expcl2  11120  expclzlem  11122  expm1t  11125  1exp  11126  mulexpz  11137  expadd  11139  expaddz  11141  expmul  11142  expubnd  11157  sqrecii  11181  irec  11197  i4  11200  binom21  11214  binom3  11217  sq01  11218  zesq  11219  crreczi  11221  bernneq  11222  bernneq2  11223  nn0opthlem1  11278  facnn2  11292  facndiv  11296  faclbnd4lem1  11301  faclbnd6  11307  bcnp1n  11321  bcm1k  11322  bcp1n  11323  bcp1nk  11324  bcn2  11326  bcp1m1  11327  bcpasc  11328  hashgadd  11354  hashfz  11376  hashfzo  11378  hashxplem  11380  hashbclem  11385  hashf1lem2  11389  hashf1  11390  fz1isolem  11394  seqcoll  11396  swrds1  11468  wrdeqcats1  11469  wrdind  11472  revccat  11479  swrds2  11555  rei  11636  imi  11637  resqrex  11731  absi  11766  absexpz  11785  recan  11815  reccn2  12065  iserex  12125  isercolllem1  12133  isercoll2  12137  serf0  12148  iseraltlem2  12150  iseraltlem3  12151  iseralt  12152  sumrblem  12179  fsumm1  12211  fsump1  12214  fsumtscopo  12255  fsumparts  12259  hashiun  12275  binomlem  12282  binom  12283  binom1p  12284  binom11  12285  binom1dif  12286  bcxmas  12289  incexc  12291  incexc2  12292  isumsplit  12294  isum1p  12295  climcndslem1  12303  supcvg  12309  harmonic  12312  arisum  12313  arisum2  12314  trireciplem  12315  geoserg  12319  geolim  12321  geolim2  12322  georeclim  12323  geo2sum  12324  geo2sum2  12325  geoisum1c  12331  0.999...  12332  geoihalfsum  12333  cvgrat  12334  mertenslem1  12335  mertenslem2  12336  mertens  12337  ef0lem  12355  esum  12357  ege2le3  12366  efsub  12375  efexp  12376  efzval  12377  eftlub  12384  effsumlt  12386  eft0val  12387  ef4p  12388  tanval3  12409  efi4p  12412  tan0  12426  efival  12427  sinhval  12429  coshval  12430  tanaddlem  12441  tanadd  12442  cos2t  12453  cos2tsin  12454  ef01bndlem  12459  cos01bnd  12461  cos1bnd  12462  cos2bnd  12463  demoivreALT  12476  eirrlem  12477  rpnnen2lem3  12490  rpnnen2lem11  12498  ruclem12  12514  odd2np1lem  12581  odd2np1  12582  oddm1even  12583  oddp1even  12584  oexpneg  12585  3dvds  12586  bitsp1o  12619  bitsfzo  12621  bitsf1  12632  sadcp1  12641  gcdmultiple  12724  sqgcd  12732  nn0seqcvgd  12735  prmind2  12764  3prm  12770  qredeu  12781  hashdvds  12838  phiprmpw  12839  phiprm  12840  eulerthlem2  12845  prmdiv  12848  prmdiveq  12849  opoe  12859  omoe  12860  opeo  12861  omeo  12862  iserodd  12883  pcexp  12907  pc2dvds  12926  sumhash  12939  fldivp1  12940  prmpwdvds  12946  pockthlem  12947  pockthi  12949  prmreclem2  12959  prmreclem4  12961  prmreclem6  12963  4sqlem11  12997  4sqlem12  12998  4sqlem19  13005  vdwapun  13016  vdwapid1  13017  vdwlem3  13025  vdwlem5  13027  vdwlem6  13028  vdwlem8  13030  vdwlem9  13031  vdwnnlem2  13038  ramub1lem1  13068  ramub1lem2  13069  ramcl  13071  dec5nprm  13076  decexp2  13085  2exp16  13098  prmlem0  13102  prmlem1a  13103  23prm  13115  prmlem2  13116  43prm  13118  83prm  13119  139prm  13120  163prm  13121  317prm  13122  631prm  13123  1259lem1  13124  1259lem2  13125  1259lem3  13126  1259lem4  13127  1259lem5  13128  1259prm  13129  2503lem1  13130  2503lem2  13131  2503lem3  13132  2503prm  13133  4001lem1  13134  4001lem2  13135  4001lem3  13136  4001lem4  13137  4001prm  13138  gsumccat  14459  mulgnndir  14584  mulgneg2  14589  mulgnnass  14590  sylow1lem1  14904  sylow2a  14925  efgsval2  15037  efgsrel  15038  efgsres  15042  efgredlemc  15049  odadd2  15136  cncrng  16390  cnfld1  16394  cnfldmulg  16401  zsssubrg  16425  gzrngunit  16432  zrngunit  16433  zcyg  16440  prmirredlem  16441  mulgrhm2  16456  nminvr  18175  blcvx  18299  expcn  18371  iirevcn  18423  iihalf2  18426  icchmeo  18434  icopnfcnv  18435  icopnfhmeo  18436  iccpnfhmeo  18438  xrhmeo  18439  icccvx  18443  evth  18452  lebnumii  18459  htpycom  18469  htpycc  18473  reparphti  18490  pco1  18508  pcohtpylem  18512  pcopt  18515  pcoass  18517  pcorevcl  18518  pcorevlem  18519  pcorev2  18521  pi1xfrcnv  18550  pjthlem1  18796  ovolunlem1a  18850  ovolunlem1  18851  ovolicc2lem4  18874  uniioombllem3  18935  uniioombllem4  18936  dyadovol  18943  opnmbllem  18951  vitalilem4  18961  vitalilem5  18962  vitali  18963  mbfi1fseqlem6  19070  iblitg  19118  iblcnlem1  19137  itgcnlem  19139  bddibl  19189  dvid  19262  dvnadd  19273  dvexp  19297  dvexp2  19298  dvmptid  19301  dvcnvlem  19318  dvexp3  19320  dveflem  19321  dvef  19322  dvsincos  19323  dvlipcn  19336  dvivthlem1  19350  lhop2  19357  dvcvx  19362  dvfsumle  19363  dvfsumabs  19365  dvfsumlem1  19368  dvfsumlem2  19369  degltp1le  19454  ply1divex  19517  fta1glem1  19546  plyaddlem1  19590  plymullem1  19591  coeidp  19639  dgrid  19640  dgrsub  19648  dgrcolem1  19649  dgrcolem2  19650  dvply1  19659  dvply2g  19660  plydivlem1  19668  plyremlem  19679  fta1lem  19682  vieta1lem1  19685  vieta1lem2  19686  qaa  19698  iaa  19700  aalioulem3  19709  geolim3  19714  aaliou3lem2  19718  aaliou3lem3  19719  aaliou3lem8  19720  aaliou3lem7  19724  taylply2  19742  dvtaylp  19744  dvntaylp  19745  taylthlem1  19747  taylthlem2  19748  dvradcnv  19792  pserdvlem2  19799  pserdv2  19801  abelthlem1  19802  abelthlem2  19803  abelthlem6  19807  abelthlem7  19809  abelth  19812  reeff1olem  19817  reeff1o  19818  efcvx  19820  sinhalfpilem  19829  eulerid  19837  cos2pi  19839  ef2pi  19840  sincosq3sgn  19863  sincosq4sgn  19864  coseq00topi  19865  tangtx  19868  sincos4thpi  19876  sincos6thpi  19878  pige3  19880  abssinper  19881  coskpi  19883  coseq1  19885  efeq1  19886  tanregt0  19896  logneg2  19964  logdivlti  19966  logcnlem4  19987  dvlog2lem  19994  dvlog2  19995  advlog  19996  advlogexp  19997  logtayllem  20001  logtayl  20002  logtayl2  20004  logccv  20005  cxpval  20006  1cxp  20014  cxpcl  20016  cxpp1  20022  cxpmul2  20031  cxpsqr  20045  dvcxp1  20077  dvcxp2  20078  dvsqr  20079  resqrcn  20084  sqrcn  20085  cxpaddlelem  20086  root1id  20089  root1eq1  20090  root1cj  20091  cxpeq  20092  loglesqr  20093  angneg  20096  ang180lem1  20102  ang180lem2  20103  ang180lem3  20104  ang180lem4  20105  ang180lem5  20106  logrec  20112  isosctrlem1  20113  isosctrlem2  20114  isosctrlem3  20115  affineequiv  20118  affineequiv2  20119  angpieqvdlem  20120  chordthmlem2  20125  chordthmlem3  20126  chordthmlem5  20128  1cubrlem  20132  1cubr  20133  dcubic2  20135  dcubic  20137  mcubic  20138  binom4  20141  dquartlem1  20142  quart1lem  20146  quart1  20147  quartlem1  20148  quart  20152  asinlem  20159  asinlem2  20160  asinlem3a  20161  asinlem3  20162  asinf  20163  atandm2  20168  atandm4  20170  atanf  20171  asinneg  20177  efiasin  20179  sinasin  20180  asinsinlem  20182  asinsin  20183  asin1  20185  acos1  20186  reasinsin  20187  asinbnd  20190  cosasin  20195  atanneg  20198  atancj  20201  efiatan  20203  atanlogaddlem  20204  atanlogadd  20205  atanlogsublem  20206  atanlogsub  20207  efiatan2  20208  2efiatan  20209  tanatan  20210  cosatan  20212  cosatanne0  20213  atantan  20214  atanbndlem  20216  bndatandm  20220  atans2  20222  atansopn  20223  dvatan  20226  atantayl  20228  atantayl2  20229  atantayl3  20230  leibpilem1  20231  leibpilem2  20232  leibpi  20233  log2cnv  20235  log2tlbnd  20236  log2ublem3  20239  log2ub  20240  birthdaylem2  20242  birthday  20244  efrlim  20259  dfef2  20260  cxplim  20261  divsqrsumlem  20269  cvxcl  20274  scvxcvx  20275  logdifbnd  20283  emcllem2  20285  emcllem3  20286  emcllem4  20287  emcllem5  20288  emcllem7  20290  harmonicbnd4  20299  fsumharmonic  20300  wilthlem1  20301  wilthlem2  20302  wilthlem3  20303  ftalem5  20309  basellem2  20314  basellem3  20315  basellem5  20317  basellem6  20318  basellem7  20319  basellem8  20320  basellem9  20321  isnsqf  20368  0sgm  20377  mule1  20381  ppiprm  20384  ppinprm  20385  chtprm  20386  chtnprm  20387  chpp1  20388  mumullem2  20413  sqff1o  20415  musum  20426  muinv  20428  1sgmprm  20433  1sgm2ppw  20434  ppiublem2  20437  ppiub  20438  chtublem  20445  chtub  20446  logfaclbnd  20456  logfacbnd3  20457  logfacrlim  20458  logexprlim  20459  mersenne  20461  perfect1  20462  perfectlem1  20463  perfectlem2  20464  perfect  20465  dchrelbasd  20473  dchr1cl  20485  dchrmulid2  20486  dchrinvcl  20487  dchrfi  20489  dchr1  20491  dchrptlem1  20498  dchrptlem2  20499  dchrsum2  20502  sumdchr2  20504  bcmono  20511  bcp1ctr  20513  bclbnd  20514  bposlem1  20518  bposlem8  20525  bposlem9  20526  lgslem1  20530  lgslem2  20531  lgslem4  20533  lgsfcl2  20536  lgsvalmod  20549  lgsneg  20553  lgsdilem  20556  lgsdir2lem1  20557  lgsdir2lem2  20558  lgsdir2lem3  20559  lgsdir2lem4  20560  lgsdir2lem5  20561  lgsdir2  20562  lgsdir  20564  lgsdi  20566  lgsne0  20567  lgseisenlem1  20583  lgseisenlem2  20584  lgseisenlem4  20586  lgseisen  20587  lgsquadlem1  20588  lgsquadlem2  20589  lgsquad2lem1  20592  lgsquad2  20594  lgsquad3  20595  m1lgs  20596  2sqlem8  20606  2sqlem10  20608  2sqlem11  20609  2sqblem  20611  chtppilimlem2  20618  chtppilim  20619  chebbnd2  20621  chto1lb  20622  chpchtlim  20623  rplogsumlem1  20628  rpvmasumlem  20631  dchrisumlem1  20633  dchrmusumlema  20637  dchrmusum2  20638  dchrvmasum2lem  20640  dchrisum0flblem1  20652  rpvmasum2  20656  dchrisum0re  20657  dchrisum0lem2a  20661  rpvmasum  20670  mudivsum  20674  mulogsumlem  20675  mulogsum  20676  logdivsum  20677  vmalogdivsum2  20682  log2sumbnd  20688  selberg2lem  20694  logdivbnd  20700  pntrmax  20708  pntrsumo1  20709  pntrsumbnd2  20711  selberg34r  20715  pntrlog2bndlem2  20722  pntrlog2bndlem4  20724  pntrlog2bndlem5  20725  pntrlog2bndlem6  20727  pntpbnd1a  20729  pntpbnd2  20731  pntibndlem2  20735  pntlemd  20738  pntlemc  20739  pntlemg  20742  pntlemr  20746  pntlemf  20749  pntlemk  20750  pntlemo  20751  pntlem3  20753  pnt2  20757  pnt  20758  ostth2lem2  20778  ex-pr  20793  1kp2ke3k  20809  ex-fl  20810  gxsuc  20932  gxnn0add  20934  gxnn0mul  20937  ablomul  21015  mulid  21016  cnrngo  21063  vc2  21104  vc0  21118  vcm  21120  vcnegneg  21123  vcoprne  21128  nvnncan  21214  nvm1  21223  nvpi  21225  nvmtri  21230  nvge0  21233  smcnlem  21263  ipval2lem3  21271  ipval2lem6  21277  ipidsq  21279  lnoadd  21329  ip1ilem  21397  ip1i  21398  ip2i  21399  ipdirilem  21400  ipasslem1  21402  ipasslem2  21403  ipasslem10  21410  minvecolem2  21447  hvsubid  21598  hvaddsubval  21605  hv2times  21633  hvnegdii  21634  hvsubcan  21646  hvsubcan2  21647  hisubcomi  21676  normlem9  21690  normlem7tALT  21691  norm-ii-i  21709  normsubi  21713  polid2i  21729  hhssnv  21834  pjhthlem1  21963  h1de2bi  22126  homulid2  22373  honegneg  22379  ho2times  22392  lnop0  22539  lnopaddi  22544  lnophmlem2  22590  lnfn0i  22615  lnfnaddi  22616  hst1h  22800  sto2i  22810  stadd3i  22821  superpos  22927  addltmulALT  23019  bcm1n  23025  ltesubnnd  23026  ballotlem2  23041  ballotlemfp1  23044  ballotlemfc0  23045  ballotlemfcc  23046  ballotlemodife  23050  ballotlem4  23051  ballotlemi1  23055  ballotlemii  23056  ballotlemic  23059  ballotlem1c  23060  ballotlemsgt1  23063  ballotlemsdom  23064  ballotlemsel1i  23065  ballotlemsi  23067  ballotlemsima  23068  ballotlem1ri  23087  zetacvg  23094  subfacp1lem1  23115  subfacp1lem5  23120  subfacp1lem6  23121  subfacval2  23123  subfaclim  23124  subfacval3  23125  cvxpcon  23178  cvxscon  23179  rescon  23182  cvmliftlem7  23227  cvmliftlem10  23230  vdgr1b  23300  eupares  23304  eupap1  23305  eupath2lem3  23308  sinccvglem  23410  elfzp1b  23417  relexpadd  23440  sqdivzi  23483  4bc3eq4  23502  halfthird  23504  5recm6rec  23505  predfz  23605  brbtwn2  23941  colinearalglem4  23945  axsegconlem1  23953  ax5seglem1  23964  ax5seglem2  23965  ax5seglem3  23967  ax5seglem4  23968  ax5seglem5  23969  ax5seglem7  23971  ax5seglem9  23973  axbtwnid  23975  axpaschlem  23976  axlowdimlem6  23983  axlowdimlem13  23990  axlowdimlem14  23991  axlowdimlem16  23993  axlowdim  23997  axeuclidlem  23998  axeuclid  23999  axcontlem2  24001  axcontlem4  24003  axcontlem7  24006  axcontlem8  24007  bpoly0  24193  bpoly1  24194  bpolycl  24195  bpolysum  24196  bpolydiflem  24197  fsumkthpow  24199  bpoly2  24200  bpoly3  24201  bpoly4  24202  fsumcube  24203  3timesi  24578  2eq3m1  24579  cntrset  25002  cnegvex2  25060  mulone  25085  vecscmonto  25086  clscnc  25410  fdc  25855  mettrifi  25873  heiborlem4  25938  heiborlem6  25940  bfp  25948  eldioph2lem1  26239  lzenom  26249  rabren3dioph  26298  irrapxlem1  26307  irrapxlem2  26308  pellexlem2  26315  pell1qrge1  26355  pell1qr1  26356  elpell1qr2  26357  pell1qrgaplem  26358  rmspecsqrnq  26391  rmspecfund  26394  rmxy0  26408  rmxm1  26419  rmym1  26420  2nn0ind  26430  jm2.24nn  26446  jm2.17a  26447  jm2.17b  26448  jm2.17c  26449  jm2.24  26450  acongeq  26470  jm2.18  26481  jm2.19lem3  26484  jm2.25  26492  jm2.16nn0  26497  jm2.27c  26500  jm3.1lem1  26510  jm3.1lem2  26511  rngunsnply  26778  flcidc  26779  psgnunilem5  26817  psgnunilem2  26818  psgnunilem4  26820  m1expaddsub  26821  psgnuni  26822  cnmsgnsubg  26834  cnmsgnbas  26835  cnmsgngrp  26836  proot1ex  26920  ofdivrec  26943  lhe4.4ex1a  26946  expgrowthi  26950  expgrowth  26952  refsum2cnlem1  27108  fmul01lt1lem2  27115  m1expeven  27125  clim1fr1  27127  isumneg  27128  climneg  27136  itgsin0pilem1  27144  itgsinexp  27149  stoweidlem1  27150  stoweidlem7  27156  stoweidlem10  27159  stoweidlem11  27160  stoweidlem13  27162  stoweidlem14  27163  stoweidlem16  27165  stoweidlem17  27166  stoweidlem26  27175  stoweidlem34  27183  stoweidlem37  27186  stoweidlem38  27187  stoweidlem41  27190  stoweidlem42  27191  stoweidlem45  27194  stoweidlem51  27200  wallispilem2  27215  wallispilem3  27216  wallispilem4  27217  wallispilem5  27218  wallispi  27219  wallispi2lem1  27220  wallispi2lem2  27221  wallispi2  27222  stirlinglem1  27223  stirlinglem3  27225  stirlinglem4  27226  stirlinglem5  27227  stirlinglem6  27228  stirlinglem7  27229  stirlinglem8  27230  stirlinglem10  27232  stirlinglem11  27233  stirlinglem12  27234  stirlinglem13  27235  stirlinglem15  27237  sec0  27491  onetansqsecsq  27492  cotsqcscsq  27493  5m4e1  27531
  Copyright terms: Public domain W3C validator