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

Axiom ax-1cn 9053
Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn 9029. (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 8996 . 2  class  1
2 cc 8993 . 2  class  CC
31, 2wcel 1726 1  wff  1  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  9089  1ex  9091  mulid1  9093  mulid2  9094  1re  9095  muladd11  9241  1p1times  9242  peano2cn  9243  mul02lem2  9248  addid1  9251  cnegex2  9253  addcom  9257  addcomd  9273  0reALT  9402  ine0  9474  mulm1  9480  0lt1  9555  ixi  9656  muleqadd  9671  reccl  9690  recne0  9696  recid  9697  recid2  9698  div1  9712  diveq1  9713  recrec  9716  rec11  9717  rec11r  9718  recdiv  9725  divdiv1  9730  divdiv2  9731  recdiv2  9732  conjmul  9736  rereccl  9737  eqneg  9739  div2neg  9742  subrec  9848  reclt1  9910  recgt1  9911  recp1lt1  9913  recreclt  9914  recgt0ii  9921  inelr  9995  ofnegsub  10003  peano5nni  10008  nn1m1nn  10025  nn1suc  10026  nnaddcl  10027  nnmulcl  10028  nnsub  10043  neg1cn  10072  1m1e0  10073  0p1e1  10098  2m1e1  10100  3m1e2  10101  3m1e2OLD  10102  2p2e4  10103  2times  10104  3p2e5  10116  3p3e6  10117  4p2e6  10118  4p3e7  10119  4p4e8  10120  5p2e7  10121  5p3e8  10122  5p4e9  10123  5p5e10  10124  6p2e8  10125  6p3e9  10126  6p4e10  10127  7p2e9  10128  7p3e10  10129  8p2e10  10130  1t1e1  10131  3t3e9  10134  halflt1  10194  1mhlfehlf  10195  8th4div3  10196  halfpm6th  10197  addltmul  10208  elnn0nn  10267  elnnnn0  10268  nn0n0n1ge2  10285  elz2  10303  zlem1lt  10332  zltlem1  10333  nnaddm1cl  10336  zextlt  10349  zneo  10357  nneo  10358  zeo  10360  peano5uzi  10363  uzindOLD  10369  numsuc  10399  numltc  10407  numsucc  10413  numaddc  10422  6p5lem  10436  4t3lem  10458  7t4e28  10471  decbin2  10491  uzp1  10524  peano2uzr  10537  uzaddcl  10538  rebtwnz  10578  rpnnen1lem5  10609  qbtwnre  10790  lincmb01cmp  11043  iccf1o  11044  xov1plusxeqvd  11046  fz01en  11084  fztp  11107  fzsuc2  11109  fztpval  11112  fseq1m1p1  11128  fzm1  11132  fzoss2  11168  fzval3  11185  fzo0to42pr  11191  fladdz  11232  ceim1l  11239  fldiv  11246  modnegd  11286  uzrdgxfr  11311  fzen2  11313  nn0ennn  11323  seqm1  11345  seqshft2  11354  monoord2  11359  sermono  11360  seqf1olem1  11367  seqf1olem2  11368  seqz  11376  ser1const  11384  expneg  11394  expcl  11404  m1expcl2  11408  expclzlem  11410  expm1t  11413  1exp  11414  mulexpz  11425  expadd  11427  expaddz  11429  expmul  11430  expubnd  11445  sqrecii  11469  irec  11485  i4  11488  binom21  11502  binom3  11505  sq01  11506  zesq  11507  crreczi  11509  bernneq  11510  bernneq2  11511  nn0opthlem1  11566  facnn2  11580  facndiv  11584  faclbnd4lem1  11589  faclbnd6  11595  bcnp1n  11610  bcm1k  11611  bcp1n  11612  bcp1nk  11613  bcn2  11615  bcp1m1  11616  bcpasc  11617  bcn2m1  11620  hashgadd  11656  hashfz  11697  hashfzo  11699  hashxplem  11701  hashbclem  11706  hashf1lem2  11710  hashf1  11711  fz1isolem  11715  seqcoll  11717  brfi1indlem  11719  swrds1  11792  wrdeqcats1  11793  wrdind  11796  revccat  11803  swrds2  11885  rei  11966  imi  11967  resqrex  12061  absi  12096  absexpz  12115  recan  12145  reccn2  12395  iserex  12455  isercolllem1  12463  isercoll2  12467  serf0  12479  iseraltlem2  12481  iseraltlem3  12482  iseralt  12483  sumrblem  12510  fsumm1  12542  fsump1  12545  fsumtscopo  12586  fsumparts  12590  hashiun  12606  binomlem  12613  binom  12614  binom1p  12615  binom11  12616  binom1dif  12617  bcxmas  12620  incexc  12622  incexc2  12623  isumsplit  12625  isum1p  12626  climcndslem1  12634  supcvg  12640  harmonic  12643  arisum  12644  arisum2  12645  trireciplem  12646  geoserg  12650  geolim  12652  geolim2  12653  georeclim  12654  geo2sum  12655  geo2sum2  12656  geoisum1c  12662  0.999...  12663  geoihalfsum  12664  cvgrat  12665  mertenslem1  12666  mertenslem2  12667  mertens  12668  ef0lem  12686  esum  12688  ege2le3  12697  efsub  12706  efexp  12707  efzval  12708  eftlub  12715  effsumlt  12717  eft0val  12718  ef4p  12719  tanval3  12740  efi4p  12743  tan0  12757  efival  12758  sinhval  12760  coshval  12761  tanaddlem  12772  tanadd  12773  cos2t  12784  cos2tsin  12785  ef01bndlem  12790  cos01bnd  12792  cos1bnd  12793  cos2bnd  12794  demoivreALT  12807  eirrlem  12808  rpnnen2lem3  12821  rpnnen2lem11  12829  ruclem12  12845  odd2np1lem  12912  odd2np1  12913  oddm1even  12914  oddp1even  12915  oexpneg  12916  3dvds  12917  bitsp1o  12950  bitsfzo  12952  bitsf1  12963  sadcp1  12972  gcdmultiple  13055  sqgcd  13063  nn0seqcvgd  13066  prmind2  13095  qredeu  13112  hashdvds  13169  phiprmpw  13170  phiprm  13171  eulerthlem2  13176  prmdiv  13179  prmdiveq  13180  opoe  13190  omoe  13191  opeo  13192  omeo  13193  iserodd  13214  pcexp  13238  pc2dvds  13257  sumhash  13270  fldivp1  13271  prmpwdvds  13277  pockthlem  13278  pockthi  13280  prmreclem2  13290  prmreclem4  13292  prmreclem6  13294  4sqlem11  13328  4sqlem12  13329  4sqlem19  13336  vdwapun  13347  vdwapid1  13348  vdwlem3  13356  vdwlem5  13358  vdwlem6  13359  vdwlem8  13361  vdwlem9  13362  vdwnnlem2  13369  ramub1lem1  13399  ramub1lem2  13400  ramcl  13402  dec5nprm  13407  decexp2  13416  2exp16  13429  prmlem0  13433  prmlem1a  13434  23prm  13446  prmlem2  13447  43prm  13449  83prm  13450  139prm  13451  163prm  13452  317prm  13453  631prm  13454  1259lem1  13455  1259lem2  13456  1259lem3  13457  1259lem4  13458  1259lem5  13459  1259prm  13460  2503lem1  13461  2503lem2  13462  2503lem3  13463  2503prm  13464  4001lem1  13465  4001lem2  13466  4001lem3  13467  4001lem4  13468  4001prm  13469  gsumccat  14792  mulgnndir  14917  mulgneg2  14922  mulgnnass  14923  sylow1lem1  15237  sylow2a  15258  efgsval2  15370  efgsrel  15371  efgsres  15375  efgredlemc  15382  odadd2  15469  cncrng  16727  cnfld1  16731  cnfldmulg  16738  zsssubrg  16762  gzrngunit  16769  zrngunit  16770  zcyg  16777  prmirredlem  16778  mulgrhm2  16793  nminvr  18710  blcvx  18834  expcn  18907  iirevcn  18960  iihalf2  18963  icchmeo  18971  icopnfcnv  18972  icopnfhmeo  18973  iccpnfhmeo  18975  xrhmeo  18976  icccvx  18980  evth  18989  lebnumii  18996  htpycom  19006  reparphti  19027  pcoass  19054  pcorevcl  19055  pcorevlem  19056  pcorev2  19058  pi1xfrcnv  19087  pjthlem1  19343  ovolunlem1a  19397  ovolunlem1  19398  ovolicc2lem4  19421  uniioombllem3  19482  uniioombllem4  19483  dyadovol  19490  opnmbllem  19498  vitalilem4  19508  vitalilem5  19509  vitali  19510  mbfi1fseqlem6  19615  iblitg  19663  iblcnlem1  19682  itgcnlem  19684  bddibl  19734  dvid  19809  dvnadd  19820  dvexp  19844  dvexp2  19845  dvmptid  19848  dvcnvlem  19865  dvexp3  19867  dveflem  19868  dvef  19869  dvsincos  19870  dvlipcn  19883  dvivthlem1  19897  lhop2  19904  dvcvx  19909  dvfsumle  19910  dvfsumabs  19912  dvfsumlem1  19915  dvfsumlem2  19916  degltp1le  20001  ply1divex  20064  fta1glem1  20093  plyaddlem1  20137  plymullem1  20138  coeidp  20186  dgrid  20187  dgrsub  20195  dgrcolem1  20196  dgrcolem2  20197  dvply1  20206  dvply2g  20207  plydivlem1  20215  plyremlem  20226  fta1lem  20229  vieta1lem1  20232  vieta1lem2  20233  qaa  20245  iaa  20247  aalioulem3  20256  geolim3  20261  aaliou3lem2  20265  aaliou3lem8  20267  aaliou3lem7  20271  taylply2  20289  dvtaylp  20291  dvntaylp  20292  taylthlem1  20294  taylthlem2  20295  dvradcnv  20342  pserdvlem2  20349  pserdv2  20351  abelthlem1  20352  abelthlem2  20353  abelthlem6  20357  abelthlem7  20359  abelth  20362  reeff1olem  20367  reeff1o  20368  efcvx  20370  sinhalfpilem  20379  eulerid  20387  cos2pi  20389  ef2pi  20390  sincosq3sgn  20413  sincosq4sgn  20414  coseq00topi  20415  tangtx  20418  sincos4thpi  20426  sincos6thpi  20428  pige3  20430  abssinper  20431  coskpi  20433  coseq1  20435  efeq1  20436  tanregt0  20446  logneg2  20515  logdivlti  20520  logcnlem4  20541  dvlog2lem  20548  dvlog2  20549  advlog  20550  advlogexp  20551  logtayllem  20555  logtayl  20556  logtayl2  20558  logccv  20559  cxpval  20560  1cxp  20568  cxpcl  20570  cxpp1  20576  cxpmul2  20585  cxpsqr  20599  dvcxp1  20631  dvcxp2  20632  dvsqr  20633  resqrcn  20638  sqrcn  20639  cxpaddlelem  20640  root1id  20643  root1eq1  20644  root1cj  20645  cxpeq  20646  loglesqr  20647  angneg  20650  ang180lem1  20656  ang180lem2  20657  ang180lem3  20658  ang180lem4  20659  ang180lem5  20660  logrec  20666  isosctrlem1  20667  isosctrlem2  20668  isosctrlem3  20669  affineequiv  20672  affineequiv2  20673  angpieqvdlem  20674  chordthmlem2  20679  chordthmlem3  20680  chordthmlem5  20682  1cubrlem  20686  1cubr  20687  dcubic2  20689  dcubic  20691  mcubic  20692  binom4  20695  dquartlem1  20696  quart1lem  20700  quart1  20701  quartlem1  20702  quart  20706  asinlem  20713  asinlem2  20714  asinlem3a  20715  asinlem3  20716  asinf  20717  atandm2  20722  atandm4  20724  atanf  20725  asinneg  20731  efiasin  20733  sinasin  20734  asinsinlem  20736  asinsin  20737  asin1  20739  acos1  20740  reasinsin  20741  asinbnd  20744  cosasin  20749  atanneg  20752  atancj  20755  efiatan  20757  atanlogaddlem  20758  atanlogadd  20759  atanlogsublem  20760  atanlogsub  20761  efiatan2  20762  2efiatan  20763  tanatan  20764  cosatan  20766  cosatanne0  20767  atantan  20768  atanbndlem  20770  bndatandm  20774  atans2  20776  atansopn  20777  dvatan  20780  atantayl  20782  atantayl2  20783  atantayl3  20784  leibpilem1  20785  leibpilem2  20786  leibpi  20787  log2cnv  20789  log2tlbnd  20790  log2ublem3  20793  log2ub  20794  birthdaylem2  20796  birthday  20798  efrlim  20813  dfef2  20814  cxplim  20815  divsqrsumlem  20823  cvxcl  20828  scvxcvx  20829  logdifbnd  20837  emcllem2  20840  emcllem3  20841  emcllem4  20842  emcllem5  20843  emcllem7  20845  harmonicbnd4  20854  fsumharmonic  20855  wilthlem1  20856  wilthlem2  20857  wilthlem3  20858  ftalem5  20864  basellem2  20869  basellem3  20870  basellem5  20872  basellem6  20873  basellem7  20874  basellem8  20875  basellem9  20876  isnsqf  20923  0sgm  20932  mule1  20936  ppiprm  20939  ppinprm  20940  chtprm  20941  chtnprm  20942  chpp1  20943  mumullem2  20968  sqff1o  20970  musum  20981  muinv  20983  1sgmprm  20988  1sgm2ppw  20989  ppiublem2  20992  ppiub  20993  chtublem  21000  chtub  21001  logfaclbnd  21011  logfacbnd3  21012  logfacrlim  21013  logexprlim  21014  mersenne  21016  perfect1  21017  perfectlem1  21018  perfectlem2  21019  perfect  21020  dchrelbasd  21028  dchr1cl  21040  dchrmulid2  21041  dchrinvcl  21042  dchrfi  21044  dchr1  21046  dchrptlem1  21053  dchrptlem2  21054  dchrsum2  21057  sumdchr2  21059  bcmono  21066  bcp1ctr  21068  bclbnd  21069  bposlem1  21073  bposlem8  21080  bposlem9  21081  lgslem1  21085  lgslem2  21086  lgsfcl2  21091  lgsvalmod  21104  lgsneg  21108  lgsdilem  21111  lgsdir2lem1  21112  lgsdir2lem2  21113  lgsdir2lem3  21114  lgsdir2lem4  21115  lgsdir2lem5  21116  lgsdir2  21117  lgsdir  21119  lgsdi  21121  lgsne0  21122  lgseisenlem1  21138  lgseisenlem2  21139  lgseisenlem4  21141  lgseisen  21142  lgsquadlem1  21143  lgsquadlem2  21144  lgsquad2lem1  21147  lgsquad2  21149  lgsquad3  21150  m1lgs  21151  2sqlem8  21161  2sqlem10  21163  2sqlem11  21164  2sqblem  21166  chtppilimlem2  21173  chtppilim  21174  chebbnd2  21176  chto1lb  21177  chpchtlim  21178  rplogsumlem1  21183  rpvmasumlem  21186  dchrisumlem1  21188  dchrmusumlema  21192  dchrmusum2  21193  dchrvmasum2lem  21195  dchrisum0flblem1  21207  rpvmasum2  21211  dchrisum0re  21212  dchrisum0lem2a  21216  rpvmasum  21225  mudivsum  21229  mulogsumlem  21230  mulogsum  21231  vmalogdivsum2  21237  selberg2lem  21249  logdivbnd  21255  pntrmax  21263  pntrsumo1  21264  pntrsumbnd2  21266  selberg34r  21270  pntrlog2bndlem2  21277  pntrlog2bndlem4  21279  pntrlog2bndlem5  21280  pntrlog2bndlem6  21282  pntpbnd1a  21284  pntpbnd2  21286  pntibndlem2  21290  pntlemd  21293  pntlemc  21294  pntlemg  21297  pntlemr  21301  pntlemf  21304  pntlemk  21305  pntlemo  21306  pntlem3  21308  pnt2  21312  pnt  21313  ostth2lem2  21333  usgraexvlem  21419  cusgrasizeinds  21490  cusgrasize2inds  21491  wlkdvspthlem  21612  fargshiftf1  21629  fargshiftfo  21630  vdgr1b  21680  eupatrl  21695  eupares  21702  eupap1  21703  eupath2lem3  21706  ex-pr  21743  1kp2ke3k  21759  ex-fl  21760  gxsuc  21865  gxnn0add  21867  gxnn0mul  21870  ablomul  21948  mulid  21949  cnrngo  21996  vc2  22039  vc0  22053  vcm  22055  vcnegneg  22058  vcoprne  22063  nvnncan  22149  nvm1  22158  nvpi  22160  nvmtri  22165  nvge0  22168  smcnlem  22198  ipval2lem3  22206  ipval2lem6  22212  ipidsq  22214  lnoadd  22264  ip1ilem  22332  ip1i  22333  ip2i  22334  ipdirilem  22335  ipasslem1  22337  ipasslem2  22338  ipasslem10  22345  minvecolem2  22382  hvsubid  22533  hvaddsubval  22540  hv2times  22568  hvnegdii  22569  hvsubcan  22581  hvsubcan2  22582  hisubcomi  22611  normlem9  22625  normlem7tALT  22626  norm-ii-i  22644  normsubi  22648  polid2i  22664  hhssnv  22769  pjhthlem1  22898  h1de2bi  23061  homulid2  23308  honegneg  23314  ho2times  23327  lnop0  23474  lnopaddi  23479  lnophmlem2  23525  lnfn0i  23550  lnfnaddi  23551  hst1h  23735  sto2i  23745  stadd3i  23756  superpos  23862  addltmulALT  23954  bcm1n  24156  ltesubnnd  24167  qqhval2lem  24370  qqh1  24374  logb1  24408  dya2ub  24625  dya2icoseg  24632  ballotlem2  24751  ballotlemfp1  24754  ballotlemfc0  24755  ballotlemfcc  24756  ballotlemic  24769  ballotlem1c  24770  ballotlemsgt1  24773  ballotlemsdom  24774  ballotlemsel1i  24775  ballotlemsi  24777  ballotlemsima  24778  ballotlem1ri  24797  zetacvg  24804  lgamgulmlem2  24819  lgamgulmlem3  24820  lgamgulmlem4  24821  lgamgulmlem5  24822  lgamgulmlem6  24823  lgamgulm2  24825  lgamcvg2  24844  gamcvg  24845  gamcvg2lem  24848  lgam1  24853  gam1  24854  gamfac  24856  subfacp1lem1  24870  subfacp1lem5  24875  subfacp1lem6  24876  subfacval2  24878  subfaclim  24879  subfacval3  24880  m1expevenALT  24910  cvxpcon  24934  cvxscon  24935  rescon  24938  cvmliftlem7  24983  cvmliftlem10  24986  sinccvglem  25114  elfzp1b  25121  relexpadd  25143  sqdivzi  25189  4bc3eq4  25208  halfthird  25210  5recm6rec  25211  divcnvlin  25217  muls1d  25218  prodf1  25224  prodfclim1  25226  prodfrec  25228  ntrivcvg  25230  ntrivcvgtail  25233  prodrblem  25260  fprodcvg  25261  prodmolem2a  25265  zprod  25268  fprodntriv  25273  prod1  25275  prodss  25278  fprodss  25279  fprodser  25280  fprodcl  25283  fproddiv  25290  fprodsplit  25294  fprodm1  25295  fprodp1  25297  iprodgam  25324  risefacval2  25331  fallfacval2  25332  risefaccl  25336  fallfaccl  25337  risefacp1  25350  fallfacp1  25351  risefacfac  25356  fallfacfwd  25357  binomfallfaclem2  25361  binomfallfac  25362  fallfacval4  25364  faclimlem1  25367  faclimlem2  25368  faclimlem3  25369  faclim  25370  iprodfac  25371  faclim2  25372  predfz  25483  brbtwn2  25849  colinearalglem4  25853  axsegconlem1  25861  ax5seglem1  25872  ax5seglem2  25873  ax5seglem3  25875  ax5seglem4  25876  ax5seglem5  25877  ax5seglem7  25879  ax5seglem9  25881  axbtwnid  25883  axpaschlem  25884  axlowdimlem6  25891  axlowdimlem13  25898  axlowdimlem14  25899  axlowdimlem16  25901  axeuclidlem  25906  axeuclid  25907  axcontlem2  25909  axcontlem4  25911  axcontlem7  25914  axcontlem8  25915  bpoly0  26101  bpoly1  26102  bpolycl  26103  bpolysum  26104  bpolydiflem  26105  fsumkthpow  26107  bpoly2  26108  bpoly3  26109  bpoly4  26110  fsumcube  26111  ltflcei  26247  sin2h  26250  cos2h  26251  tan2h  26252  opnmbllem0  26254  mblfinlem2  26256  mblfinlem3  26257  0mbf  26264  dvtan  26269  itg2addnclem2  26271  itg2addnclem3  26272  dvreasin  26304  dvreacos  26305  areacirclem1  26306  areacirclem4  26309  areacirc  26311  fdc  26463  mettrifi  26477  heiborlem4  26537  heiborlem6  26539  bfp  26547  eldioph2lem1  26832  lzenom  26842  rabren3dioph  26890  irrapxlem1  26899  irrapxlem2  26900  pellexlem2  26907  pell1qrge1  26947  pell1qr1  26948  elpell1qr2  26949  pell1qrgaplem  26950  rmspecsqrnq  26983  rmspecfund  26986  rmxy0  27000  rmxm1  27011  rmym1  27012  2nn0ind  27022  jm2.24nn  27038  jm2.17a  27039  jm2.17b  27040  jm2.17c  27041  jm2.24  27042  acongeq  27062  jm2.18  27073  jm2.19lem3  27076  jm2.25  27084  jm2.16nn0  27089  jm2.27c  27092  jm3.1lem1  27102  jm3.1lem2  27103  rngunsnply  27369  flcidc  27370  psgnunilem5  27408  psgnunilem2  27409  psgnunilem4  27411  m1expaddsub  27412  psgnuni  27413  cnmsgnsubg  27425  cnmsgnbas  27426  cnmsgngrp  27427  proot1ex  27511  ofdivrec  27534  lhe4.4ex1a  27537  expgrowthi  27541  expgrowth  27543  refsum2cnlem1  27698  fmul01lt1lem2  27705  m1expeven  27715  clim1fr1  27717  isumneg  27718  climneg  27726  itgsin0pilem1  27734  itgsinexp  27739  stoweidlem1  27740  stoweidlem7  27746  stoweidlem10  27749  stoweidlem11  27750  stoweidlem13  27752  stoweidlem14  27753  stoweidlem17  27756  stoweidlem26  27765  stoweidlem34  27773  stoweidlem38  27777  stoweidlem41  27780  stoweidlem42  27781  stoweidlem45  27784  wallispilem2  27805  wallispilem3  27806  wallispilem4  27807  wallispilem5  27808  wallispi  27809  wallispi2lem1  27810  wallispi2lem2  27811  wallispi2  27812  stirlinglem1  27813  stirlinglem3  27815  stirlinglem4  27816  stirlinglem5  27817  stirlinglem6  27818  stirlinglem7  27819  stirlinglem8  27820  stirlinglem10  27822  stirlinglem11  27823  stirlinglem12  27824  stirlinglem13  27825  stirlinglem15  27827  sigaradd  27846  cnm1cn  28111  kcnktkm1cn  28112  ubmelm1fzo  28150  fzosplitsnm1  28154  ltdifltdiv  28171  modvalp1  28174  wrdlenccats1lenm1  28212  cshwidxm1  28279  cshwidxn  28281  swrdtrcfvl  28299  cshweqrep  28308  cshwssizensame  28323  wlklenfislenpm1  28337  wwlknimp  28369  wlkiswwlk1  28372  wlklniswwlkn2  28382  nbhashuvtx1  28431  frghash2spot  28526  usgreghash2spotv  28529  frgregordn0  28533  sec0  28577  onetansqsecsq  28578  cotsqcscsq  28579  5m4e1  28609  isosctrlem1ALT  29120
  Copyright terms: Public domain W3C validator