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

Axiom ax-1cn 9050
Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn 9026. (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 8993 . 2  class  1
2 cc 8990 . 2  class  CC
31, 2wcel 1726 1  wff  1  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  9086  1ex  9088  mulid1  9090  mulid2  9091  1re  9092  muladd11  9238  1p1times  9239  peano2cn  9240  mul02lem2  9245  addid1  9248  cnegex2  9250  addcom  9254  addcomd  9270  0reALT  9399  ine0  9471  mulm1  9477  0lt1  9552  ixi  9653  muleqadd  9668  reccl  9687  recne0  9693  recid  9694  recid2  9695  div1  9709  diveq1  9710  recrec  9713  rec11  9714  rec11r  9715  recdiv  9722  divdiv1  9727  divdiv2  9728  recdiv2  9729  conjmul  9733  rereccl  9734  eqneg  9736  div2neg  9739  subrec  9845  reclt1  9907  recgt1  9908  recp1lt1  9910  recreclt  9911  recgt0ii  9918  inelr  9992  ofnegsub  10000  peano5nni  10005  nn1m1nn  10022  nn1suc  10023  nnaddcl  10024  nnmulcl  10025  nnsub  10040  neg1cn  10069  1m1e0  10070  0p1e1  10095  2m1e1  10097  3m1e2  10098  3m1e2OLD  10099  2p2e4  10100  2times  10101  3p2e5  10113  3p3e6  10114  4p2e6  10115  4p3e7  10116  4p4e8  10117  5p2e7  10118  5p3e8  10119  5p4e9  10120  5p5e10  10121  6p2e8  10122  6p3e9  10123  6p4e10  10124  7p2e9  10125  7p3e10  10126  8p2e10  10127  1t1e1  10128  3t3e9  10131  halflt1  10191  1mhlfehlf  10192  8th4div3  10193  halfpm6th  10194  addltmul  10205  elnn0nn  10264  elnnnn0  10265  nn0n0n1ge2  10282  elz2  10300  zlem1lt  10329  zltlem1  10330  nnaddm1cl  10333  zextlt  10346  zneo  10354  nneo  10355  zeo  10357  peano5uzi  10360  uzindOLD  10366  numsuc  10396  numltc  10404  numsucc  10410  numaddc  10419  6p5lem  10433  4t3lem  10455  7t4e28  10468  decbin2  10488  uzp1  10521  peano2uzr  10534  uzaddcl  10535  rebtwnz  10575  rpnnen1lem5  10606  qbtwnre  10787  lincmb01cmp  11040  iccf1o  11041  xov1plusxeqvd  11043  fz01en  11081  fztp  11104  fzsuc2  11106  fztpval  11109  fseq1m1p1  11125  fzm1  11129  fzoss2  11165  fzval3  11182  fzo0to42pr  11188  fladdz  11229  ceim1l  11236  fldiv  11243  modnegd  11283  uzrdgxfr  11308  fzen2  11310  nn0ennn  11320  seqm1  11342  seqshft2  11351  monoord2  11356  sermono  11357  seqf1olem1  11364  seqf1olem2  11365  seqz  11373  ser1const  11381  expneg  11391  expcl  11401  m1expcl2  11405  expclzlem  11407  expm1t  11410  1exp  11411  mulexpz  11422  expadd  11424  expaddz  11426  expmul  11427  expubnd  11442  sqrecii  11466  irec  11482  i4  11485  binom21  11499  binom3  11502  sq01  11503  zesq  11504  crreczi  11506  bernneq  11507  bernneq2  11508  nn0opthlem1  11563  facnn2  11577  facndiv  11581  faclbnd4lem1  11586  faclbnd6  11592  bcnp1n  11607  bcm1k  11608  bcp1n  11609  bcp1nk  11610  bcn2  11612  bcp1m1  11613  bcpasc  11614  bcn2m1  11617  hashgadd  11653  hashfz  11694  hashfzo  11696  hashxplem  11698  hashbclem  11703  hashf1lem2  11707  hashf1  11708  fz1isolem  11712  seqcoll  11714  brfi1indlem  11716  swrds1  11789  wrdeqcats1  11790  wrdind  11793  revccat  11800  swrds2  11882  rei  11963  imi  11964  resqrex  12058  absi  12093  absexpz  12112  recan  12142  reccn2  12392  iserex  12452  isercolllem1  12460  isercoll2  12464  serf0  12476  iseraltlem2  12478  iseraltlem3  12479  iseralt  12480  sumrblem  12507  fsumm1  12539  fsump1  12542  fsumtscopo  12583  fsumparts  12587  hashiun  12603  binomlem  12610  binom  12611  binom1p  12612  binom11  12613  binom1dif  12614  bcxmas  12617  incexc  12619  incexc2  12620  isumsplit  12622  isum1p  12623  climcndslem1  12631  supcvg  12637  harmonic  12640  arisum  12641  arisum2  12642  trireciplem  12643  geoserg  12647  geolim  12649  geolim2  12650  georeclim  12651  geo2sum  12652  geo2sum2  12653  geoisum1c  12659  0.999...  12660  geoihalfsum  12661  cvgrat  12662  mertenslem1  12663  mertenslem2  12664  mertens  12665  ef0lem  12683  esum  12685  ege2le3  12694  efsub  12703  efexp  12704  efzval  12705  eftlub  12712  effsumlt  12714  eft0val  12715  ef4p  12716  tanval3  12737  efi4p  12740  tan0  12754  efival  12755  sinhval  12757  coshval  12758  tanaddlem  12769  tanadd  12770  cos2t  12781  cos2tsin  12782  ef01bndlem  12787  cos01bnd  12789  cos1bnd  12790  cos2bnd  12791  demoivreALT  12804  eirrlem  12805  rpnnen2lem3  12818  rpnnen2lem11  12826  ruclem12  12842  odd2np1lem  12909  odd2np1  12910  oddm1even  12911  oddp1even  12912  oexpneg  12913  3dvds  12914  bitsp1o  12947  bitsfzo  12949  bitsf1  12960  sadcp1  12969  gcdmultiple  13052  sqgcd  13060  nn0seqcvgd  13063  prmind2  13092  qredeu  13109  hashdvds  13166  phiprmpw  13167  phiprm  13168  eulerthlem2  13173  prmdiv  13176  prmdiveq  13177  opoe  13187  omoe  13188  opeo  13189  omeo  13190  iserodd  13211  pcexp  13235  pc2dvds  13254  sumhash  13267  fldivp1  13268  prmpwdvds  13274  pockthlem  13275  pockthi  13277  prmreclem2  13287  prmreclem4  13289  prmreclem6  13291  4sqlem11  13325  4sqlem12  13326  4sqlem19  13333  vdwapun  13344  vdwapid1  13345  vdwlem3  13353  vdwlem5  13355  vdwlem6  13356  vdwlem8  13358  vdwlem9  13359  vdwnnlem2  13366  ramub1lem1  13396  ramub1lem2  13397  ramcl  13399  dec5nprm  13404  decexp2  13413  2exp16  13426  prmlem0  13430  prmlem1a  13431  23prm  13443  prmlem2  13444  43prm  13446  83prm  13447  139prm  13448  163prm  13449  317prm  13450  631prm  13451  1259lem1  13452  1259lem2  13453  1259lem3  13454  1259lem4  13455  1259lem5  13456  1259prm  13457  2503lem1  13458  2503lem2  13459  2503lem3  13460  2503prm  13461  4001lem1  13462  4001lem2  13463  4001lem3  13464  4001lem4  13465  4001prm  13466  gsumccat  14789  mulgnndir  14914  mulgneg2  14919  mulgnnass  14920  sylow1lem1  15234  sylow2a  15255  efgsval2  15367  efgsrel  15368  efgsres  15372  efgredlemc  15379  odadd2  15466  cncrng  16724  cnfld1  16728  cnfldmulg  16735  zsssubrg  16759  gzrngunit  16766  zrngunit  16767  zcyg  16774  prmirredlem  16775  mulgrhm2  16790  nminvr  18707  blcvx  18831  expcn  18904  iirevcn  18957  iihalf2  18960  icchmeo  18968  icopnfcnv  18969  icopnfhmeo  18970  iccpnfhmeo  18972  xrhmeo  18973  icccvx  18977  evth  18986  lebnumii  18993  htpycom  19003  reparphti  19024  pcoass  19051  pcorevcl  19052  pcorevlem  19053  pcorev2  19055  pi1xfrcnv  19084  pjthlem1  19340  ovolunlem1a  19394  ovolunlem1  19395  ovolicc2lem4  19418  uniioombllem3  19479  uniioombllem4  19480  dyadovol  19487  opnmbllem  19495  vitalilem4  19505  vitalilem5  19506  vitali  19507  mbfi1fseqlem6  19614  iblitg  19662  iblcnlem1  19681  itgcnlem  19683  bddibl  19733  dvid  19806  dvnadd  19817  dvexp  19841  dvexp2  19842  dvmptid  19845  dvcnvlem  19862  dvexp3  19864  dveflem  19865  dvef  19866  dvsincos  19867  dvlipcn  19880  dvivthlem1  19894  lhop2  19901  dvcvx  19906  dvfsumle  19907  dvfsumabs  19909  dvfsumlem1  19912  dvfsumlem2  19913  degltp1le  19998  ply1divex  20061  fta1glem1  20090  plyaddlem1  20134  plymullem1  20135  coeidp  20183  dgrid  20184  dgrsub  20192  dgrcolem1  20193  dgrcolem2  20194  dvply1  20203  dvply2g  20204  plydivlem1  20212  plyremlem  20223  fta1lem  20226  vieta1lem1  20229  vieta1lem2  20230  qaa  20242  iaa  20244  aalioulem3  20253  geolim3  20258  aaliou3lem2  20262  aaliou3lem8  20264  aaliou3lem7  20268  taylply2  20286  dvtaylp  20288  dvntaylp  20289  taylthlem1  20291  taylthlem2  20292  dvradcnv  20339  pserdvlem2  20346  pserdv2  20348  abelthlem1  20349  abelthlem2  20350  abelthlem6  20354  abelthlem7  20356  abelth  20359  reeff1olem  20364  reeff1o  20365  efcvx  20367  sinhalfpilem  20376  eulerid  20384  cos2pi  20386  ef2pi  20387  sincosq3sgn  20410  sincosq4sgn  20411  coseq00topi  20412  tangtx  20415  sincos4thpi  20423  sincos6thpi  20425  pige3  20427  abssinper  20428  coskpi  20430  coseq1  20432  efeq1  20433  tanregt0  20443  logneg2  20512  logdivlti  20517  logcnlem4  20538  dvlog2lem  20545  dvlog2  20546  advlog  20547  advlogexp  20548  logtayllem  20552  logtayl  20553  logtayl2  20555  logccv  20556  cxpval  20557  1cxp  20565  cxpcl  20567  cxpp1  20573  cxpmul2  20582  cxpsqr  20596  dvcxp1  20628  dvcxp2  20629  dvsqr  20630  resqrcn  20635  sqrcn  20636  cxpaddlelem  20637  root1id  20640  root1eq1  20641  root1cj  20642  cxpeq  20643  loglesqr  20644  angneg  20647  ang180lem1  20653  ang180lem2  20654  ang180lem3  20655  ang180lem4  20656  ang180lem5  20657  logrec  20663  isosctrlem1  20664  isosctrlem2  20665  isosctrlem3  20666  affineequiv  20669  affineequiv2  20670  angpieqvdlem  20671  chordthmlem2  20676  chordthmlem3  20677  chordthmlem5  20679  1cubrlem  20683  1cubr  20684  dcubic2  20686  dcubic  20688  mcubic  20689  binom4  20692  dquartlem1  20693  quart1lem  20697  quart1  20698  quartlem1  20699  quart  20703  asinlem  20710  asinlem2  20711  asinlem3a  20712  asinlem3  20713  asinf  20714  atandm2  20719  atandm4  20721  atanf  20722  asinneg  20728  efiasin  20730  sinasin  20731  asinsinlem  20733  asinsin  20734  asin1  20736  acos1  20737  reasinsin  20738  asinbnd  20741  cosasin  20746  atanneg  20749  atancj  20752  efiatan  20754  atanlogaddlem  20755  atanlogadd  20756  atanlogsublem  20757  atanlogsub  20758  efiatan2  20759  2efiatan  20760  tanatan  20761  cosatan  20763  cosatanne0  20764  atantan  20765  atanbndlem  20767  bndatandm  20771  atans2  20773  atansopn  20774  dvatan  20777  atantayl  20779  atantayl2  20780  atantayl3  20781  leibpilem1  20782  leibpilem2  20783  leibpi  20784  log2cnv  20786  log2tlbnd  20787  log2ublem3  20790  log2ub  20791  birthdaylem2  20793  birthday  20795  efrlim  20810  dfef2  20811  cxplim  20812  divsqrsumlem  20820  cvxcl  20825  scvxcvx  20826  logdifbnd  20834  emcllem2  20837  emcllem3  20838  emcllem4  20839  emcllem5  20840  emcllem7  20842  harmonicbnd4  20851  fsumharmonic  20852  wilthlem1  20853  wilthlem2  20854  wilthlem3  20855  ftalem5  20861  basellem2  20866  basellem3  20867  basellem5  20869  basellem6  20870  basellem7  20871  basellem8  20872  basellem9  20873  isnsqf  20920  0sgm  20929  mule1  20933  ppiprm  20936  ppinprm  20937  chtprm  20938  chtnprm  20939  chpp1  20940  mumullem2  20965  sqff1o  20967  musum  20978  muinv  20980  1sgmprm  20985  1sgm2ppw  20986  ppiublem2  20989  ppiub  20990  chtublem  20997  chtub  20998  logfaclbnd  21008  logfacbnd3  21009  logfacrlim  21010  logexprlim  21011  mersenne  21013  perfect1  21014  perfectlem1  21015  perfectlem2  21016  perfect  21017  dchrelbasd  21025  dchr1cl  21037  dchrmulid2  21038  dchrinvcl  21039  dchrfi  21041  dchr1  21043  dchrptlem1  21050  dchrptlem2  21051  dchrsum2  21054  sumdchr2  21056  bcmono  21063  bcp1ctr  21065  bclbnd  21066  bposlem1  21070  bposlem8  21077  bposlem9  21078  lgslem1  21082  lgslem2  21083  lgsfcl2  21088  lgsvalmod  21101  lgsneg  21105  lgsdilem  21108  lgsdir2lem1  21109  lgsdir2lem2  21110  lgsdir2lem3  21111  lgsdir2lem4  21112  lgsdir2lem5  21113  lgsdir2  21114  lgsdir  21116  lgsdi  21118  lgsne0  21119  lgseisenlem1  21135  lgseisenlem2  21136  lgseisenlem4  21138  lgseisen  21139  lgsquadlem1  21140  lgsquadlem2  21141  lgsquad2lem1  21144  lgsquad2  21146  lgsquad3  21147  m1lgs  21148  2sqlem8  21158  2sqlem10  21160  2sqlem11  21161  2sqblem  21163  chtppilimlem2  21170  chtppilim  21171  chebbnd2  21173  chto1lb  21174  chpchtlim  21175  rplogsumlem1  21180  rpvmasumlem  21183  dchrisumlem1  21185  dchrmusumlema  21189  dchrmusum2  21190  dchrvmasum2lem  21192  dchrisum0flblem1  21204  rpvmasum2  21208  dchrisum0re  21209  dchrisum0lem2a  21213  rpvmasum  21222  mudivsum  21226  mulogsumlem  21227  mulogsum  21228  vmalogdivsum2  21234  selberg2lem  21246  logdivbnd  21252  pntrmax  21260  pntrsumo1  21261  pntrsumbnd2  21263  selberg34r  21267  pntrlog2bndlem2  21274  pntrlog2bndlem4  21276  pntrlog2bndlem5  21277  pntrlog2bndlem6  21279  pntpbnd1a  21281  pntpbnd2  21283  pntibndlem2  21287  pntlemd  21290  pntlemc  21291  pntlemg  21294  pntlemr  21298  pntlemf  21301  pntlemk  21302  pntlemo  21303  pntlem3  21305  pnt2  21309  pnt  21310  ostth2lem2  21330  usgraexvlem  21416  cusgrasizeinds  21487  cusgrasize2inds  21488  wlkdvspthlem  21609  fargshiftf1  21626  fargshiftfo  21627  vdgr1b  21677  eupatrl  21692  eupares  21699  eupap1  21700  eupath2lem3  21703  ex-pr  21740  1kp2ke3k  21756  ex-fl  21757  gxsuc  21862  gxnn0add  21864  gxnn0mul  21867  ablomul  21945  mulid  21946  cnrngo  21993  vc2  22036  vc0  22050  vcm  22052  vcnegneg  22055  vcoprne  22060  nvnncan  22146  nvm1  22155  nvpi  22157  nvmtri  22162  nvge0  22165  smcnlem  22195  ipval2lem3  22203  ipval2lem6  22209  ipidsq  22211  lnoadd  22261  ip1ilem  22329  ip1i  22330  ip2i  22331  ipdirilem  22332  ipasslem1  22334  ipasslem2  22335  ipasslem10  22342  minvecolem2  22379  hvsubid  22530  hvaddsubval  22537  hv2times  22565  hvnegdii  22566  hvsubcan  22578  hvsubcan2  22579  hisubcomi  22608  normlem9  22622  normlem7tALT  22623  norm-ii-i  22641  normsubi  22645  polid2i  22661  hhssnv  22766  pjhthlem1  22895  h1de2bi  23058  homulid2  23305  honegneg  23311  ho2times  23324  lnop0  23471  lnopaddi  23476  lnophmlem2  23522  lnfn0i  23547  lnfnaddi  23548  hst1h  23732  sto2i  23742  stadd3i  23753  superpos  23859  addltmulALT  23951  bcm1n  24153  ltesubnnd  24164  qqhval2lem  24367  qqh1  24371  logb1  24405  dya2ub  24622  dya2icoseg  24629  ballotlem2  24748  ballotlemfp1  24751  ballotlemfc0  24752  ballotlemfcc  24753  ballotlemic  24766  ballotlem1c  24767  ballotlemsgt1  24770  ballotlemsdom  24771  ballotlemsel1i  24772  ballotlemsi  24774  ballotlemsima  24775  ballotlem1ri  24794  zetacvg  24801  lgamgulmlem2  24816  lgamgulmlem3  24817  lgamgulmlem4  24818  lgamgulmlem5  24819  lgamgulmlem6  24820  lgamgulm2  24822  lgamcvg2  24841  gamcvg  24842  gamcvg2lem  24845  lgam1  24850  gam1  24851  gamfac  24853  subfacp1lem1  24867  subfacp1lem5  24872  subfacp1lem6  24873  subfacval2  24875  subfaclim  24876  subfacval3  24877  m1expevenALT  24907  cvxpcon  24931  cvxscon  24932  rescon  24935  cvmliftlem7  24980  cvmliftlem10  24983  sinccvglem  25111  elfzp1b  25118  relexpadd  25140  sqdivzi  25186  4bc3eq4  25205  halfthird  25207  5recm6rec  25208  divcnvlin  25214  muls1d  25215  prodf1  25221  prodfclim1  25223  prodfrec  25225  ntrivcvg  25227  ntrivcvgtail  25230  prodrblem  25257  fprodcvg  25258  prodmolem2a  25262  zprod  25265  fprodntriv  25270  prod1  25272  prodss  25275  fprodss  25276  fprodser  25277  fprodcl  25280  fproddiv  25287  fprodsplit  25291  fprodm1  25292  fprodp1  25294  iprodgam  25321  risefacval2  25328  fallfacval2  25329  risefaccl  25333  fallfaccl  25334  risefacp1  25347  fallfacp1  25348  risefacfac  25353  fallfacfwd  25354  binomfallfaclem2  25358  binomfallfac  25359  fallfacval4  25361  faclimlem1  25364  faclimlem2  25365  faclimlem3  25366  faclim  25367  iprodfac  25368  faclim2  25369  predfz  25480  brbtwn2  25846  colinearalglem4  25850  axsegconlem1  25858  ax5seglem1  25869  ax5seglem2  25870  ax5seglem3  25872  ax5seglem4  25873  ax5seglem5  25874  ax5seglem7  25876  ax5seglem9  25878  axbtwnid  25880  axpaschlem  25881  axlowdimlem6  25888  axlowdimlem13  25895  axlowdimlem14  25896  axlowdimlem16  25898  axeuclidlem  25903  axeuclid  25904  axcontlem2  25906  axcontlem4  25908  axcontlem7  25911  axcontlem8  25912  bpoly0  26098  bpoly1  26099  bpolycl  26100  bpolysum  26101  bpolydiflem  26102  fsumkthpow  26104  bpoly2  26105  bpoly3  26106  bpoly4  26107  fsumcube  26108  ltflcei  26241  opnmbllem0  26244  mblfinlem2  26246  mblfinlem3  26247  0mbf  26254  itg2addnclem2  26259  itg2addnclem3  26260  dvreasin  26292  dvreacos  26293  areacirclem1  26294  areacirclem4  26297  areacirc  26299  fdc  26451  mettrifi  26465  heiborlem4  26525  heiborlem6  26527  bfp  26535  eldioph2lem1  26820  lzenom  26830  rabren3dioph  26878  irrapxlem1  26887  irrapxlem2  26888  pellexlem2  26895  pell1qrge1  26935  pell1qr1  26936  elpell1qr2  26937  pell1qrgaplem  26938  rmspecsqrnq  26971  rmspecfund  26974  rmxy0  26988  rmxm1  26999  rmym1  27000  2nn0ind  27010  jm2.24nn  27026  jm2.17a  27027  jm2.17b  27028  jm2.17c  27029  jm2.24  27030  acongeq  27050  jm2.18  27061  jm2.19lem3  27064  jm2.25  27072  jm2.16nn0  27077  jm2.27c  27080  jm3.1lem1  27090  jm3.1lem2  27091  rngunsnply  27357  flcidc  27358  psgnunilem5  27396  psgnunilem2  27397  psgnunilem4  27399  m1expaddsub  27400  psgnuni  27401  cnmsgnsubg  27413  cnmsgnbas  27414  cnmsgngrp  27415  proot1ex  27499  ofdivrec  27522  lhe4.4ex1a  27525  expgrowthi  27529  expgrowth  27531  refsum2cnlem1  27686  fmul01lt1lem2  27693  m1expeven  27703  clim1fr1  27705  isumneg  27706  climneg  27714  itgsin0pilem1  27722  itgsinexp  27727  stoweidlem1  27728  stoweidlem7  27734  stoweidlem10  27737  stoweidlem11  27738  stoweidlem13  27740  stoweidlem14  27741  stoweidlem17  27744  stoweidlem26  27753  stoweidlem34  27761  stoweidlem38  27765  stoweidlem41  27768  stoweidlem42  27769  stoweidlem45  27772  wallispilem2  27793  wallispilem3  27794  wallispilem4  27795  wallispilem5  27796  wallispi  27797  wallispi2lem1  27798  wallispi2lem2  27799  wallispi2  27800  stirlinglem1  27801  stirlinglem3  27803  stirlinglem4  27804  stirlinglem5  27805  stirlinglem6  27806  stirlinglem7  27807  stirlinglem8  27808  stirlinglem10  27810  stirlinglem11  27811  stirlinglem12  27812  stirlinglem13  27813  stirlinglem15  27815  sigaradd  27834  cnm1cn  28099  kcnktkm1cn  28100  ubmelm1fzo  28138  fzosplitsnm1  28142  ltdifltdiv  28159  modvalp1  28162  wrdlenccats1lenm1  28200  cshwidxm1  28267  cshwidxn  28269  swrdtrcfvl  28287  cshweqrep  28296  cshwssizensame  28311  wlklenfislenpm1  28325  wwlknimp  28357  wlkiswwlk1  28360  wlklniswwlkn2  28370  nbhashuvtx1  28419  frghash2spot  28514  usgreghash2spotv  28517  frgregordn0  28521  sec0  28565  onetansqsecsq  28566  cotsqcscsq  28567  5m4e1  28597  isosctrlem1ALT  29108
  Copyright terms: Public domain W3C validator