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

Axiom ax-1cn 9040
Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn 9016. (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 8983 . 2  class  1
2 cc 8980 . 2  class  CC
31, 2wcel 1725 1  wff  1  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  9076  1ex  9078  mulid1  9080  mulid2  9081  1re  9082  muladd11  9228  1p1times  9229  peano2cn  9230  mul02lem2  9235  addid1  9238  cnegex2  9240  addcom  9244  addcomd  9260  0reALT  9389  ine0  9461  mulm1  9467  0lt1  9542  ixi  9643  muleqadd  9658  reccl  9677  recne0  9683  recid  9684  recid2  9685  div1  9699  diveq1  9700  recrec  9703  rec11  9704  rec11r  9705  recdiv  9712  divdiv1  9717  divdiv2  9718  recdiv2  9719  conjmul  9723  rereccl  9724  eqneg  9726  div2neg  9729  subrec  9835  reclt1  9897  recgt1  9898  recp1lt1  9900  recreclt  9901  recgt0ii  9908  inelr  9982  ofnegsub  9990  peano5nni  9995  nn1m1nn  10012  nn1suc  10013  nnaddcl  10014  nnmulcl  10015  nnsub  10030  neg1cn  10059  1m1e0  10060  0p1e1  10085  2m1e1  10087  3m1e2  10088  3m1e2OLD  10089  2p2e4  10090  2times  10091  3p2e5  10103  3p3e6  10104  4p2e6  10105  4p3e7  10106  4p4e8  10107  5p2e7  10108  5p3e8  10109  5p4e9  10110  5p5e10  10111  6p2e8  10112  6p3e9  10113  6p4e10  10114  7p2e9  10115  7p3e10  10116  8p2e10  10117  1t1e1  10118  3t3e9  10121  halflt1  10181  1mhlfehlf  10182  8th4div3  10183  halfpm6th  10184  addltmul  10195  elnn0nn  10254  elnnnn0  10255  nn0n0n1ge2  10272  elz2  10290  zlem1lt  10319  zltlem1  10320  nnaddm1cl  10323  zextlt  10336  zneo  10344  nneo  10345  zeo  10347  peano5uzi  10350  uzindOLD  10356  numsuc  10386  numltc  10394  numsucc  10400  numaddc  10409  6p5lem  10423  4t3lem  10445  7t4e28  10458  decbin2  10478  uzp1  10511  peano2uzr  10524  uzaddcl  10525  rebtwnz  10565  rpnnen1lem5  10596  qbtwnre  10777  lincmb01cmp  11030  iccf1o  11031  xov1plusxeqvd  11033  fz01en  11071  fztp  11094  fzsuc2  11096  fztpval  11099  fseq1m1p1  11115  fzm1  11119  fzoss2  11155  fzval3  11172  fzo0to42pr  11178  fladdz  11219  ceim1l  11226  fldiv  11233  modnegd  11273  uzrdgxfr  11298  fzen2  11300  nn0ennn  11310  seqm1  11332  seqshft2  11341  monoord2  11346  sermono  11347  seqf1olem1  11354  seqf1olem2  11355  seqz  11363  ser1const  11371  expneg  11381  expcl  11391  m1expcl2  11395  expclzlem  11397  expm1t  11400  1exp  11401  mulexpz  11412  expadd  11414  expaddz  11416  expmul  11417  expubnd  11432  sqrecii  11456  irec  11472  i4  11475  binom21  11489  binom3  11492  sq01  11493  zesq  11494  crreczi  11496  bernneq  11497  bernneq2  11498  nn0opthlem1  11553  facnn2  11567  facndiv  11571  faclbnd4lem1  11576  faclbnd6  11582  bcnp1n  11597  bcm1k  11598  bcp1n  11599  bcp1nk  11600  bcn2  11602  bcp1m1  11603  bcpasc  11604  bcn2m1  11607  hashgadd  11643  hashfz  11684  hashfzo  11686  hashxplem  11688  hashbclem  11693  hashf1lem2  11697  hashf1  11698  fz1isolem  11702  seqcoll  11704  brfi1indlem  11706  swrds1  11779  wrdeqcats1  11780  wrdind  11783  revccat  11790  swrds2  11872  rei  11953  imi  11954  resqrex  12048  absi  12083  absexpz  12102  recan  12132  reccn2  12382  iserex  12442  isercolllem1  12450  isercoll2  12454  serf0  12466  iseraltlem2  12468  iseraltlem3  12469  iseralt  12470  sumrblem  12497  fsumm1  12529  fsump1  12532  fsumtscopo  12573  fsumparts  12577  hashiun  12593  binomlem  12600  binom  12601  binom1p  12602  binom11  12603  binom1dif  12604  bcxmas  12607  incexc  12609  incexc2  12610  isumsplit  12612  isum1p  12613  climcndslem1  12621  supcvg  12627  harmonic  12630  arisum  12631  arisum2  12632  trireciplem  12633  geoserg  12637  geolim  12639  geolim2  12640  georeclim  12641  geo2sum  12642  geo2sum2  12643  geoisum1c  12649  0.999...  12650  geoihalfsum  12651  cvgrat  12652  mertenslem1  12653  mertenslem2  12654  mertens  12655  ef0lem  12673  esum  12675  ege2le3  12684  efsub  12693  efexp  12694  efzval  12695  eftlub  12702  effsumlt  12704  eft0val  12705  ef4p  12706  tanval3  12727  efi4p  12730  tan0  12744  efival  12745  sinhval  12747  coshval  12748  tanaddlem  12759  tanadd  12760  cos2t  12771  cos2tsin  12772  ef01bndlem  12777  cos01bnd  12779  cos1bnd  12780  cos2bnd  12781  demoivreALT  12794  eirrlem  12795  rpnnen2lem3  12808  rpnnen2lem11  12816  ruclem12  12832  odd2np1lem  12899  odd2np1  12900  oddm1even  12901  oddp1even  12902  oexpneg  12903  3dvds  12904  bitsp1o  12937  bitsfzo  12939  bitsf1  12950  sadcp1  12959  gcdmultiple  13042  sqgcd  13050  nn0seqcvgd  13053  prmind2  13082  qredeu  13099  hashdvds  13156  phiprmpw  13157  phiprm  13158  eulerthlem2  13163  prmdiv  13166  prmdiveq  13167  opoe  13177  omoe  13178  opeo  13179  omeo  13180  iserodd  13201  pcexp  13225  pc2dvds  13244  sumhash  13257  fldivp1  13258  prmpwdvds  13264  pockthlem  13265  pockthi  13267  prmreclem2  13277  prmreclem4  13279  prmreclem6  13281  4sqlem11  13315  4sqlem12  13316  4sqlem19  13323  vdwapun  13334  vdwapid1  13335  vdwlem3  13343  vdwlem5  13345  vdwlem6  13346  vdwlem8  13348  vdwlem9  13349  vdwnnlem2  13356  ramub1lem1  13386  ramub1lem2  13387  ramcl  13389  dec5nprm  13394  decexp2  13403  2exp16  13416  prmlem0  13420  prmlem1a  13421  23prm  13433  prmlem2  13434  43prm  13436  83prm  13437  139prm  13438  163prm  13439  317prm  13440  631prm  13441  1259lem1  13442  1259lem2  13443  1259lem3  13444  1259lem4  13445  1259lem5  13446  1259prm  13447  2503lem1  13448  2503lem2  13449  2503lem3  13450  2503prm  13451  4001lem1  13452  4001lem2  13453  4001lem3  13454  4001lem4  13455  4001prm  13456  gsumccat  14779  mulgnndir  14904  mulgneg2  14909  mulgnnass  14910  sylow1lem1  15224  sylow2a  15245  efgsval2  15357  efgsrel  15358  efgsres  15362  efgredlemc  15369  odadd2  15456  cncrng  16714  cnfld1  16718  cnfldmulg  16725  zsssubrg  16749  gzrngunit  16756  zrngunit  16757  zcyg  16764  prmirredlem  16765  mulgrhm2  16780  nminvr  18697  blcvx  18821  expcn  18894  iirevcn  18947  iihalf2  18950  icchmeo  18958  icopnfcnv  18959  icopnfhmeo  18960  iccpnfhmeo  18962  xrhmeo  18963  icccvx  18967  evth  18976  lebnumii  18983  htpycom  18993  reparphti  19014  pcoass  19041  pcorevcl  19042  pcorevlem  19043  pcorev2  19045  pi1xfrcnv  19074  pjthlem1  19330  ovolunlem1a  19384  ovolunlem1  19385  ovolicc2lem4  19408  uniioombllem3  19469  uniioombllem4  19470  dyadovol  19477  opnmbllem  19485  vitalilem4  19495  vitalilem5  19496  vitali  19497  mbfi1fseqlem6  19604  iblitg  19652  iblcnlem1  19671  itgcnlem  19673  bddibl  19723  dvid  19796  dvnadd  19807  dvexp  19831  dvexp2  19832  dvmptid  19835  dvcnvlem  19852  dvexp3  19854  dveflem  19855  dvef  19856  dvsincos  19857  dvlipcn  19870  dvivthlem1  19884  lhop2  19891  dvcvx  19896  dvfsumle  19897  dvfsumabs  19899  dvfsumlem1  19902  dvfsumlem2  19903  degltp1le  19988  ply1divex  20051  fta1glem1  20080  plyaddlem1  20124  plymullem1  20125  coeidp  20173  dgrid  20174  dgrsub  20182  dgrcolem1  20183  dgrcolem2  20184  dvply1  20193  dvply2g  20194  plydivlem1  20202  plyremlem  20213  fta1lem  20216  vieta1lem1  20219  vieta1lem2  20220  qaa  20232  iaa  20234  aalioulem3  20243  geolim3  20248  aaliou3lem2  20252  aaliou3lem8  20254  aaliou3lem7  20258  taylply2  20276  dvtaylp  20278  dvntaylp  20279  taylthlem1  20281  taylthlem2  20282  dvradcnv  20329  pserdvlem2  20336  pserdv2  20338  abelthlem1  20339  abelthlem2  20340  abelthlem6  20344  abelthlem7  20346  abelth  20349  reeff1olem  20354  reeff1o  20355  efcvx  20357  sinhalfpilem  20366  eulerid  20374  cos2pi  20376  ef2pi  20377  sincosq3sgn  20400  sincosq4sgn  20401  coseq00topi  20402  tangtx  20405  sincos4thpi  20413  sincos6thpi  20415  pige3  20417  abssinper  20418  coskpi  20420  coseq1  20422  efeq1  20423  tanregt0  20433  logneg2  20502  logdivlti  20507  logcnlem4  20528  dvlog2lem  20535  dvlog2  20536  advlog  20537  advlogexp  20538  logtayllem  20542  logtayl  20543  logtayl2  20545  logccv  20546  cxpval  20547  1cxp  20555  cxpcl  20557  cxpp1  20563  cxpmul2  20572  cxpsqr  20586  dvcxp1  20618  dvcxp2  20619  dvsqr  20620  resqrcn  20625  sqrcn  20626  cxpaddlelem  20627  root1id  20630  root1eq1  20631  root1cj  20632  cxpeq  20633  loglesqr  20634  angneg  20637  ang180lem1  20643  ang180lem2  20644  ang180lem3  20645  ang180lem4  20646  ang180lem5  20647  logrec  20653  isosctrlem1  20654  isosctrlem2  20655  isosctrlem3  20656  affineequiv  20659  affineequiv2  20660  angpieqvdlem  20661  chordthmlem2  20666  chordthmlem3  20667  chordthmlem5  20669  1cubrlem  20673  1cubr  20674  dcubic2  20676  dcubic  20678  mcubic  20679  binom4  20682  dquartlem1  20683  quart1lem  20687  quart1  20688  quartlem1  20689  quart  20693  asinlem  20700  asinlem2  20701  asinlem3a  20702  asinlem3  20703  asinf  20704  atandm2  20709  atandm4  20711  atanf  20712  asinneg  20718  efiasin  20720  sinasin  20721  asinsinlem  20723  asinsin  20724  asin1  20726  acos1  20727  reasinsin  20728  asinbnd  20731  cosasin  20736  atanneg  20739  atancj  20742  efiatan  20744  atanlogaddlem  20745  atanlogadd  20746  atanlogsublem  20747  atanlogsub  20748  efiatan2  20749  2efiatan  20750  tanatan  20751  cosatan  20753  cosatanne0  20754  atantan  20755  atanbndlem  20757  bndatandm  20761  atans2  20763  atansopn  20764  dvatan  20767  atantayl  20769  atantayl2  20770  atantayl3  20771  leibpilem1  20772  leibpilem2  20773  leibpi  20774  log2cnv  20776  log2tlbnd  20777  log2ublem3  20780  log2ub  20781  birthdaylem2  20783  birthday  20785  efrlim  20800  dfef2  20801  cxplim  20802  divsqrsumlem  20810  cvxcl  20815  scvxcvx  20816  logdifbnd  20824  emcllem2  20827  emcllem3  20828  emcllem4  20829  emcllem5  20830  emcllem7  20832  harmonicbnd4  20841  fsumharmonic  20842  wilthlem1  20843  wilthlem2  20844  wilthlem3  20845  ftalem5  20851  basellem2  20856  basellem3  20857  basellem5  20859  basellem6  20860  basellem7  20861  basellem8  20862  basellem9  20863  isnsqf  20910  0sgm  20919  mule1  20923  ppiprm  20926  ppinprm  20927  chtprm  20928  chtnprm  20929  chpp1  20930  mumullem2  20955  sqff1o  20957  musum  20968  muinv  20970  1sgmprm  20975  1sgm2ppw  20976  ppiublem2  20979  ppiub  20980  chtublem  20987  chtub  20988  logfaclbnd  20998  logfacbnd3  20999  logfacrlim  21000  logexprlim  21001  mersenne  21003  perfect1  21004  perfectlem1  21005  perfectlem2  21006  perfect  21007  dchrelbasd  21015  dchr1cl  21027  dchrmulid2  21028  dchrinvcl  21029  dchrfi  21031  dchr1  21033  dchrptlem1  21040  dchrptlem2  21041  dchrsum2  21044  sumdchr2  21046  bcmono  21053  bcp1ctr  21055  bclbnd  21056  bposlem1  21060  bposlem8  21067  bposlem9  21068  lgslem1  21072  lgslem2  21073  lgsfcl2  21078  lgsvalmod  21091  lgsneg  21095  lgsdilem  21098  lgsdir2lem1  21099  lgsdir2lem2  21100  lgsdir2lem3  21101  lgsdir2lem4  21102  lgsdir2lem5  21103  lgsdir2  21104  lgsdir  21106  lgsdi  21108  lgsne0  21109  lgseisenlem1  21125  lgseisenlem2  21126  lgseisenlem4  21128  lgseisen  21129  lgsquadlem1  21130  lgsquadlem2  21131  lgsquad2lem1  21134  lgsquad2  21136  lgsquad3  21137  m1lgs  21138  2sqlem8  21148  2sqlem10  21150  2sqlem11  21151  2sqblem  21153  chtppilimlem2  21160  chtppilim  21161  chebbnd2  21163  chto1lb  21164  chpchtlim  21165  rplogsumlem1  21170  rpvmasumlem  21173  dchrisumlem1  21175  dchrmusumlema  21179  dchrmusum2  21180  dchrvmasum2lem  21182  dchrisum0flblem1  21194  rpvmasum2  21198  dchrisum0re  21199  dchrisum0lem2a  21203  rpvmasum  21212  mudivsum  21216  mulogsumlem  21217  mulogsum  21218  vmalogdivsum2  21224  selberg2lem  21236  logdivbnd  21242  pntrmax  21250  pntrsumo1  21251  pntrsumbnd2  21253  selberg34r  21257  pntrlog2bndlem2  21264  pntrlog2bndlem4  21266  pntrlog2bndlem5  21267  pntrlog2bndlem6  21269  pntpbnd1a  21271  pntpbnd2  21273  pntibndlem2  21277  pntlemd  21280  pntlemc  21281  pntlemg  21284  pntlemr  21288  pntlemf  21291  pntlemk  21292  pntlemo  21293  pntlem3  21295  pnt2  21299  pnt  21300  ostth2lem2  21320  usgraexvlem  21406  cusgrasizeinds  21477  cusgrasize2inds  21478  wlkdvspthlem  21599  fargshiftf1  21616  fargshiftfo  21617  vdgr1b  21667  eupatrl  21682  eupares  21689  eupap1  21690  eupath2lem3  21693  ex-pr  21730  1kp2ke3k  21746  ex-fl  21747  gxsuc  21852  gxnn0add  21854  gxnn0mul  21857  ablomul  21935  mulid  21936  cnrngo  21983  vc2  22026  vc0  22040  vcm  22042  vcnegneg  22045  vcoprne  22050  nvnncan  22136  nvm1  22145  nvpi  22147  nvmtri  22152  nvge0  22155  smcnlem  22185  ipval2lem3  22193  ipval2lem6  22199  ipidsq  22201  lnoadd  22251  ip1ilem  22319  ip1i  22320  ip2i  22321  ipdirilem  22322  ipasslem1  22324  ipasslem2  22325  ipasslem10  22332  minvecolem2  22369  hvsubid  22520  hvaddsubval  22527  hv2times  22555  hvnegdii  22556  hvsubcan  22568  hvsubcan2  22569  hisubcomi  22598  normlem9  22612  normlem7tALT  22613  norm-ii-i  22631  normsubi  22635  polid2i  22651  hhssnv  22756  pjhthlem1  22885  h1de2bi  23048  homulid2  23295  honegneg  23301  ho2times  23314  lnop0  23461  lnopaddi  23466  lnophmlem2  23512  lnfn0i  23537  lnfnaddi  23538  hst1h  23722  sto2i  23732  stadd3i  23743  superpos  23849  addltmulALT  23941  bcm1n  24143  ltesubnnd  24154  qqhval2lem  24357  qqh1  24361  logb1  24395  dya2ub  24612  dya2icoseg  24619  ballotlem2  24738  ballotlemfp1  24741  ballotlemfc0  24742  ballotlemfcc  24743  ballotlemic  24756  ballotlem1c  24757  ballotlemsgt1  24760  ballotlemsdom  24761  ballotlemsel1i  24762  ballotlemsi  24764  ballotlemsima  24765  ballotlem1ri  24784  zetacvg  24791  lgamgulmlem2  24806  lgamgulmlem3  24807  lgamgulmlem4  24808  lgamgulmlem5  24809  lgamgulmlem6  24810  lgamgulm2  24812  lgamcvg2  24831  gamcvg  24832  gamcvg2lem  24835  lgam1  24840  gam1  24841  gamfac  24843  subfacp1lem1  24857  subfacp1lem5  24862  subfacp1lem6  24863  subfacval2  24865  subfaclim  24866  subfacval3  24867  m1expevenALT  24897  cvxpcon  24921  cvxscon  24922  rescon  24925  cvmliftlem7  24970  cvmliftlem10  24973  sinccvglem  25101  elfzp1b  25108  relexpadd  25130  sqdivzi  25176  4bc3eq4  25195  halfthird  25197  5recm6rec  25198  divcnvlin  25204  muls1d  25205  prodf1  25211  prodfclim1  25213  prodfrec  25215  ntrivcvg  25217  ntrivcvgtail  25220  prodrblem  25247  fprodcvg  25248  prodmolem2a  25252  zprod  25255  fprodntriv  25260  prod1  25262  prodss  25265  fprodss  25266  fprodser  25267  fprodcl  25270  fproddiv  25277  fprodsplit  25281  fprodm1  25282  fprodp1  25284  iprodgam  25311  risefacval2  25318  fallfacval2  25319  risefaccl  25323  fallfaccl  25324  risefacp1  25337  fallfacp1  25338  risefacfac  25343  fallfacfwd  25344  binomfallfaclem2  25348  binomfallfac  25349  fallfacval4  25351  faclimlem1  25354  faclimlem2  25355  faclimlem3  25356  faclim  25357  iprodfac  25358  faclim2  25359  predfz  25470  brbtwn2  25836  colinearalglem4  25840  axsegconlem1  25848  ax5seglem1  25859  ax5seglem2  25860  ax5seglem3  25862  ax5seglem4  25863  ax5seglem5  25864  ax5seglem7  25866  ax5seglem9  25868  axbtwnid  25870  axpaschlem  25871  axlowdimlem6  25878  axlowdimlem13  25885  axlowdimlem14  25886  axlowdimlem16  25888  axeuclidlem  25893  axeuclid  25894  axcontlem2  25896  axcontlem4  25898  axcontlem7  25901  axcontlem8  25902  bpoly0  26088  bpoly1  26089  bpolycl  26090  bpolysum  26091  bpolydiflem  26092  fsumkthpow  26094  bpoly2  26095  bpoly3  26096  bpoly4  26097  fsumcube  26098  ltflcei  26231  mblfinlem  26234  mblfinlem2  26235  0mbf  26242  itg2addnclem2  26247  itg2addnclem3  26248  dvreasin  26280  dvreacos  26281  areacirclem2  26282  areacirclem5  26286  areacirc  26288  fdc  26440  mettrifi  26454  heiborlem4  26514  heiborlem6  26516  bfp  26524  eldioph2lem1  26809  lzenom  26819  rabren3dioph  26867  irrapxlem1  26876  irrapxlem2  26877  pellexlem2  26884  pell1qrge1  26924  pell1qr1  26925  elpell1qr2  26926  pell1qrgaplem  26927  rmspecsqrnq  26960  rmspecfund  26963  rmxy0  26977  rmxm1  26988  rmym1  26989  2nn0ind  26999  jm2.24nn  27015  jm2.17a  27016  jm2.17b  27017  jm2.17c  27018  jm2.24  27019  acongeq  27039  jm2.18  27050  jm2.19lem3  27053  jm2.25  27061  jm2.16nn0  27066  jm2.27c  27069  jm3.1lem1  27079  jm3.1lem2  27080  rngunsnply  27346  flcidc  27347  psgnunilem5  27385  psgnunilem2  27386  psgnunilem4  27388  m1expaddsub  27389  psgnuni  27390  cnmsgnsubg  27402  cnmsgnbas  27403  cnmsgngrp  27404  proot1ex  27488  ofdivrec  27511  lhe4.4ex1a  27514  expgrowthi  27518  expgrowth  27520  refsum2cnlem1  27675  fmul01lt1lem2  27682  m1expeven  27692  clim1fr1  27694  isumneg  27695  climneg  27703  itgsin0pilem1  27711  itgsinexp  27716  stoweidlem1  27717  stoweidlem7  27723  stoweidlem10  27726  stoweidlem11  27727  stoweidlem13  27729  stoweidlem14  27730  stoweidlem17  27733  stoweidlem26  27742  stoweidlem34  27750  stoweidlem38  27754  stoweidlem41  27757  stoweidlem42  27758  stoweidlem45  27761  wallispilem2  27782  wallispilem3  27783  wallispilem4  27784  wallispilem5  27785  wallispi  27786  wallispi2lem1  27787  wallispi2lem2  27788  wallispi2  27789  stirlinglem1  27790  stirlinglem3  27792  stirlinglem4  27793  stirlinglem5  27794  stirlinglem6  27795  stirlinglem7  27796  stirlinglem8  27797  stirlinglem10  27799  stirlinglem11  27800  stirlinglem12  27801  stirlinglem13  27802  stirlinglem15  27804  sigaradd  27823  cnm1cn  28073  kcnktkm1cn  28074  ubmelm1fzo  28110  fzosplitsnm1  28114  ltdifltdiv  28126  modvalp1  28129  cshwidxm1  28211  cshwidxn  28213  cshweqrep  28237  cshwssizensame  28252  frghash2spot  28389  usgreghash2spotv  28392  frgregordn0  28396  sec0  28440  onetansqsecsq  28441  cotsqcscsq  28442  5m4e1  28472  isosctrlem1ALT  28983
  Copyright terms: Public domain W3C validator