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

Axiom ax-1cn 8981
Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn 8957. (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 8924 . 2  class  1
2 cc 8921 . 2  class  CC
31, 2wcel 1717 1  wff  1  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  9017  1ex  9019  mulid1  9021  mulid2  9022  1re  9023  muladd11  9168  1p1times  9169  peano2cn  9170  mul02lem2  9175  addid1  9178  cnegex2  9180  addcom  9184  addcomd  9200  0reALT  9329  ine0  9401  mulm1  9407  0lt1  9482  ixi  9583  muleqadd  9598  reccl  9617  recne0  9623  recid  9624  recid2  9625  div1  9639  diveq1  9640  recrec  9643  rec11  9644  rec11r  9645  recdiv  9652  divdiv1  9657  divdiv2  9658  recdiv2  9659  conjmul  9663  rereccl  9664  eqneg  9666  div2neg  9669  subrec  9775  reclt1  9837  recgt1  9838  recp1lt1  9840  recreclt  9841  recgt0ii  9848  inelr  9922  ofnegsub  9930  peano5nni  9935  nn1m1nn  9952  nn1suc  9953  nnaddcl  9954  nnmulcl  9955  nnsub  9970  neg1cn  9999  1m1e0  10000  0p1e1  10025  2m1e1  10027  3m1e2  10028  3m1e2OLD  10029  2p2e4  10030  2times  10031  3p2e5  10043  3p3e6  10044  4p2e6  10045  4p3e7  10046  4p4e8  10047  5p2e7  10048  5p3e8  10049  5p4e9  10050  5p5e10  10051  6p2e8  10052  6p3e9  10053  6p4e10  10054  7p2e9  10055  7p3e10  10056  8p2e10  10057  1t1e1  10058  3t3e9  10061  halflt1  10121  1mhlfehlf  10122  8th4div3  10123  halfpm6th  10124  addltmul  10135  elnn0nn  10194  elnnnn0  10195  nn0n0n1ge2  10212  elz2  10230  zlem1lt  10259  zltlem1  10260  nnaddm1cl  10263  zextlt  10276  zneo  10284  nneo  10285  zeo  10287  peano5uzi  10290  uzindOLD  10296  numsuc  10326  numltc  10334  numsucc  10340  numaddc  10349  6p5lem  10363  4t3lem  10385  7t4e28  10398  decbin2  10418  uzp1  10451  peano2uzr  10464  uzaddcl  10465  rebtwnz  10505  rpnnen1lem5  10536  qbtwnre  10717  lincmb01cmp  10970  iccf1o  10971  xov1plusxeqvd  10973  fz01en  11011  fztp  11034  fzsuc2  11035  fztpval  11038  fseq1m1p1  11053  fzm1  11057  fzoss2  11093  fzval3  11108  fzo0to42pr  11113  fladdz  11154  ceim1l  11161  fldiv  11168  modnegd  11208  uzrdgxfr  11233  fzen2  11235  nn0ennn  11245  seqm1  11267  seqshft2  11276  monoord2  11281  sermono  11282  seqf1olem1  11289  seqf1olem2  11290  seqz  11298  ser1const  11306  expneg  11316  expcl  11326  m1expcl2  11330  expclzlem  11332  expm1t  11335  1exp  11336  mulexpz  11347  expadd  11349  expaddz  11351  expmul  11352  expubnd  11367  sqrecii  11391  irec  11407  i4  11410  binom21  11424  binom3  11427  sq01  11428  zesq  11429  crreczi  11431  bernneq  11432  bernneq2  11433  nn0opthlem1  11488  facnn2  11502  facndiv  11506  faclbnd4lem1  11511  faclbnd6  11517  bcnp1n  11532  bcm1k  11533  bcp1n  11534  bcp1nk  11535  bcn2  11537  bcp1m1  11538  bcpasc  11539  bcn2m1  11542  hashgadd  11578  hashfz  11619  hashfzo  11621  hashxplem  11623  hashbclem  11628  hashf1lem2  11632  hashf1  11633  fz1isolem  11637  seqcoll  11639  brfi1indlem  11641  swrds1  11714  wrdeqcats1  11715  wrdind  11718  revccat  11725  swrds2  11807  rei  11888  imi  11889  resqrex  11983  absi  12018  absexpz  12037  recan  12067  reccn2  12317  iserex  12377  isercolllem1  12385  isercoll2  12389  serf0  12401  iseraltlem2  12403  iseraltlem3  12404  iseralt  12405  sumrblem  12432  fsumm1  12464  fsump1  12467  fsumtscopo  12508  fsumparts  12512  hashiun  12528  binomlem  12535  binom  12536  binom1p  12537  binom11  12538  binom1dif  12539  bcxmas  12542  incexc  12544  incexc2  12545  isumsplit  12547  isum1p  12548  climcndslem1  12556  supcvg  12562  harmonic  12565  arisum  12566  arisum2  12567  trireciplem  12568  geoserg  12572  geolim  12574  geolim2  12575  georeclim  12576  geo2sum  12577  geo2sum2  12578  geoisum1c  12584  0.999...  12585  geoihalfsum  12586  cvgrat  12587  mertenslem1  12588  mertenslem2  12589  mertens  12590  ef0lem  12608  esum  12610  ege2le3  12619  efsub  12628  efexp  12629  efzval  12630  eftlub  12637  effsumlt  12639  eft0val  12640  ef4p  12641  tanval3  12662  efi4p  12665  tan0  12679  efival  12680  sinhval  12682  coshval  12683  tanaddlem  12694  tanadd  12695  cos2t  12706  cos2tsin  12707  ef01bndlem  12712  cos01bnd  12714  cos1bnd  12715  cos2bnd  12716  demoivreALT  12729  eirrlem  12730  rpnnen2lem3  12743  rpnnen2lem11  12751  ruclem12  12767  odd2np1lem  12834  odd2np1  12835  oddm1even  12836  oddp1even  12837  oexpneg  12838  3dvds  12839  bitsp1o  12872  bitsfzo  12874  bitsf1  12885  sadcp1  12894  gcdmultiple  12977  sqgcd  12985  nn0seqcvgd  12988  prmind2  13017  qredeu  13034  hashdvds  13091  phiprmpw  13092  phiprm  13093  eulerthlem2  13098  prmdiv  13101  prmdiveq  13102  opoe  13112  omoe  13113  opeo  13114  omeo  13115  iserodd  13136  pcexp  13160  pc2dvds  13179  sumhash  13192  fldivp1  13193  prmpwdvds  13199  pockthlem  13200  pockthi  13202  prmreclem2  13212  prmreclem4  13214  prmreclem6  13216  4sqlem11  13250  4sqlem12  13251  4sqlem19  13258  vdwapun  13269  vdwapid1  13270  vdwlem3  13278  vdwlem5  13280  vdwlem6  13281  vdwlem8  13283  vdwlem9  13284  vdwnnlem2  13291  ramub1lem1  13321  ramub1lem2  13322  ramcl  13324  dec5nprm  13329  decexp2  13338  2exp16  13351  prmlem0  13355  prmlem1a  13356  23prm  13368  prmlem2  13369  43prm  13371  83prm  13372  139prm  13373  163prm  13374  317prm  13375  631prm  13376  1259lem1  13377  1259lem2  13378  1259lem3  13379  1259lem4  13380  1259lem5  13381  1259prm  13382  2503lem1  13383  2503lem2  13384  2503lem3  13385  2503prm  13386  4001lem1  13387  4001lem2  13388  4001lem3  13389  4001lem4  13390  4001prm  13391  gsumccat  14714  mulgnndir  14839  mulgneg2  14844  mulgnnass  14845  sylow1lem1  15159  sylow2a  15180  efgsval2  15292  efgsrel  15293  efgsres  15297  efgredlemc  15304  odadd2  15391  cncrng  16645  cnfld1  16649  cnfldmulg  16656  zsssubrg  16680  gzrngunit  16687  zrngunit  16688  zcyg  16695  prmirredlem  16696  mulgrhm2  16711  nminvr  18576  blcvx  18700  expcn  18773  iirevcn  18826  iihalf2  18829  icchmeo  18837  icopnfcnv  18838  icopnfhmeo  18839  iccpnfhmeo  18841  xrhmeo  18842  icccvx  18846  evth  18855  lebnumii  18862  htpycom  18872  reparphti  18893  pcoass  18920  pcorevcl  18921  pcorevlem  18922  pcorev2  18924  pi1xfrcnv  18953  pjthlem1  19205  ovolunlem1a  19259  ovolunlem1  19260  ovolicc2lem4  19283  uniioombllem3  19344  uniioombllem4  19345  dyadovol  19352  opnmbllem  19360  vitalilem4  19370  vitalilem5  19371  vitali  19372  mbfi1fseqlem6  19479  iblitg  19527  iblcnlem1  19546  itgcnlem  19548  bddibl  19598  dvid  19671  dvnadd  19682  dvexp  19706  dvexp2  19707  dvmptid  19710  dvcnvlem  19727  dvexp3  19729  dveflem  19730  dvef  19731  dvsincos  19732  dvlipcn  19745  dvivthlem1  19759  lhop2  19766  dvcvx  19771  dvfsumle  19772  dvfsumabs  19774  dvfsumlem1  19777  dvfsumlem2  19778  degltp1le  19863  ply1divex  19926  fta1glem1  19955  plyaddlem1  19999  plymullem1  20000  coeidp  20048  dgrid  20049  dgrsub  20057  dgrcolem1  20058  dgrcolem2  20059  dvply1  20068  dvply2g  20069  plydivlem1  20077  plyremlem  20088  fta1lem  20091  vieta1lem1  20094  vieta1lem2  20095  qaa  20107  iaa  20109  aalioulem3  20118  geolim3  20123  aaliou3lem2  20127  aaliou3lem8  20129  aaliou3lem7  20133  taylply2  20151  dvtaylp  20153  dvntaylp  20154  taylthlem1  20156  taylthlem2  20157  dvradcnv  20204  pserdvlem2  20211  pserdv2  20213  abelthlem1  20214  abelthlem2  20215  abelthlem6  20219  abelthlem7  20221  abelth  20224  reeff1olem  20229  reeff1o  20230  efcvx  20232  sinhalfpilem  20241  eulerid  20249  cos2pi  20251  ef2pi  20252  sincosq3sgn  20275  sincosq4sgn  20276  coseq00topi  20277  tangtx  20280  sincos4thpi  20288  sincos6thpi  20290  pige3  20292  abssinper  20293  coskpi  20295  coseq1  20297  efeq1  20298  tanregt0  20308  logneg2  20377  logdivlti  20382  logcnlem4  20403  dvlog2lem  20410  dvlog2  20411  advlog  20412  advlogexp  20413  logtayllem  20417  logtayl  20418  logtayl2  20420  logccv  20421  cxpval  20422  1cxp  20430  cxpcl  20432  cxpp1  20438  cxpmul2  20447  cxpsqr  20461  dvcxp1  20493  dvcxp2  20494  dvsqr  20495  resqrcn  20500  sqrcn  20501  cxpaddlelem  20502  root1id  20505  root1eq1  20506  root1cj  20507  cxpeq  20508  loglesqr  20509  angneg  20512  ang180lem1  20518  ang180lem2  20519  ang180lem3  20520  ang180lem4  20521  ang180lem5  20522  logrec  20528  isosctrlem1  20529  isosctrlem2  20530  isosctrlem3  20531  affineequiv  20534  affineequiv2  20535  angpieqvdlem  20536  chordthmlem2  20541  chordthmlem3  20542  chordthmlem5  20544  1cubrlem  20548  1cubr  20549  dcubic2  20551  dcubic  20553  mcubic  20554  binom4  20557  dquartlem1  20558  quart1lem  20562  quart1  20563  quartlem1  20564  quart  20568  asinlem  20575  asinlem2  20576  asinlem3a  20577  asinlem3  20578  asinf  20579  atandm2  20584  atandm4  20586  atanf  20587  asinneg  20593  efiasin  20595  sinasin  20596  asinsinlem  20598  asinsin  20599  asin1  20601  acos1  20602  reasinsin  20603  asinbnd  20606  cosasin  20611  atanneg  20614  atancj  20617  efiatan  20619  atanlogaddlem  20620  atanlogadd  20621  atanlogsublem  20622  atanlogsub  20623  efiatan2  20624  2efiatan  20625  tanatan  20626  cosatan  20628  cosatanne0  20629  atantan  20630  atanbndlem  20632  bndatandm  20636  atans2  20638  atansopn  20639  dvatan  20642  atantayl  20644  atantayl2  20645  atantayl3  20646  leibpilem1  20647  leibpilem2  20648  leibpi  20649  log2cnv  20651  log2tlbnd  20652  log2ublem3  20655  log2ub  20656  birthdaylem2  20658  birthday  20660  efrlim  20675  dfef2  20676  cxplim  20677  divsqrsumlem  20685  cvxcl  20690  scvxcvx  20691  logdifbnd  20699  emcllem2  20702  emcllem3  20703  emcllem4  20704  emcllem5  20705  emcllem7  20707  harmonicbnd4  20716  fsumharmonic  20717  wilthlem1  20718  wilthlem2  20719  wilthlem3  20720  ftalem5  20726  basellem2  20731  basellem3  20732  basellem5  20734  basellem6  20735  basellem7  20736  basellem8  20737  basellem9  20738  isnsqf  20785  0sgm  20794  mule1  20798  ppiprm  20801  ppinprm  20802  chtprm  20803  chtnprm  20804  chpp1  20805  mumullem2  20830  sqff1o  20832  musum  20843  muinv  20845  1sgmprm  20850  1sgm2ppw  20851  ppiublem2  20854  ppiub  20855  chtublem  20862  chtub  20863  logfaclbnd  20873  logfacbnd3  20874  logfacrlim  20875  logexprlim  20876  mersenne  20878  perfect1  20879  perfectlem1  20880  perfectlem2  20881  perfect  20882  dchrelbasd  20890  dchr1cl  20902  dchrmulid2  20903  dchrinvcl  20904  dchrfi  20906  dchr1  20908  dchrptlem1  20915  dchrptlem2  20916  dchrsum2  20919  sumdchr2  20921  bcmono  20928  bcp1ctr  20930  bclbnd  20931  bposlem1  20935  bposlem8  20942  bposlem9  20943  lgslem1  20947  lgslem2  20948  lgsfcl2  20953  lgsvalmod  20966  lgsneg  20970  lgsdilem  20973  lgsdir2lem1  20974  lgsdir2lem2  20975  lgsdir2lem3  20976  lgsdir2lem4  20977  lgsdir2lem5  20978  lgsdir2  20979  lgsdir  20981  lgsdi  20983  lgsne0  20984  lgseisenlem1  21000  lgseisenlem2  21001  lgseisenlem4  21003  lgseisen  21004  lgsquadlem1  21005  lgsquadlem2  21006  lgsquad2lem1  21009  lgsquad2  21011  lgsquad3  21012  m1lgs  21013  2sqlem8  21023  2sqlem10  21025  2sqlem11  21026  2sqblem  21028  chtppilimlem2  21035  chtppilim  21036  chebbnd2  21038  chto1lb  21039  chpchtlim  21040  rplogsumlem1  21045  rpvmasumlem  21048  dchrisumlem1  21050  dchrmusumlema  21054  dchrmusum2  21055  dchrvmasum2lem  21057  dchrisum0flblem1  21069  rpvmasum2  21073  dchrisum0re  21074  dchrisum0lem2a  21078  rpvmasum  21087  mudivsum  21091  mulogsumlem  21092  mulogsum  21093  vmalogdivsum2  21099  selberg2lem  21111  logdivbnd  21117  pntrmax  21125  pntrsumo1  21126  pntrsumbnd2  21128  selberg34r  21132  pntrlog2bndlem2  21139  pntrlog2bndlem4  21141  pntrlog2bndlem5  21142  pntrlog2bndlem6  21144  pntpbnd1a  21146  pntpbnd2  21148  pntibndlem2  21152  pntlemd  21155  pntlemc  21156  pntlemg  21159  pntlemr  21163  pntlemf  21166  pntlemk  21167  pntlemo  21168  pntlem3  21170  pnt2  21174  pnt  21175  ostth2lem2  21195  usgraexvlem  21280  cusgrasizeinds  21351  cusgrasize2inds  21352  wlkdvspthlem  21455  fargshiftf1  21472  fargshiftfo  21473  vdgr1b  21523  eupatrl  21538  eupares  21545  eupap1  21546  eupath2lem3  21549  ex-pr  21586  1kp2ke3k  21602  ex-fl  21603  gxsuc  21708  gxnn0add  21710  gxnn0mul  21713  ablomul  21791  mulid  21792  cnrngo  21839  vc2  21882  vc0  21896  vcm  21898  vcnegneg  21901  vcoprne  21906  nvnncan  21992  nvm1  22001  nvpi  22003  nvmtri  22008  nvge0  22011  smcnlem  22041  ipval2lem3  22049  ipval2lem6  22055  ipidsq  22057  lnoadd  22107  ip1ilem  22175  ip1i  22176  ip2i  22177  ipdirilem  22178  ipasslem1  22180  ipasslem2  22181  ipasslem10  22188  minvecolem2  22225  hvsubid  22376  hvaddsubval  22383  hv2times  22411  hvnegdii  22412  hvsubcan  22424  hvsubcan2  22425  hisubcomi  22454  normlem9  22468  normlem7tALT  22469  norm-ii-i  22487  normsubi  22491  polid2i  22507  hhssnv  22612  pjhthlem1  22741  h1de2bi  22904  homulid2  23151  honegneg  23157  ho2times  23170  lnop0  23317  lnopaddi  23322  lnophmlem2  23368  lnfn0i  23393  lnfnaddi  23394  hst1h  23578  sto2i  23588  stadd3i  23599  superpos  23705  addltmulALT  23797  bcm1n  23987  ltesubnnd  24000  qqhval2lem  24164  qqh1  24168  logb1  24199  dya2ub  24414  dya2icoseg  24421  ballotlem2  24525  ballotlemfp1  24528  ballotlemfc0  24529  ballotlemfcc  24530  ballotlemic  24543  ballotlem1c  24544  ballotlemsgt1  24547  ballotlemsdom  24548  ballotlemsel1i  24549  ballotlemsi  24551  ballotlemsima  24552  ballotlem1ri  24571  zetacvg  24578  lgamgulmlem2  24593  lgamgulmlem3  24594  lgamgulmlem4  24595  lgamgulmlem5  24596  lgamgulmlem6  24597  lgamgulm2  24599  lgamcvg2  24618  gamcvg  24619  gamcvg2lem  24622  lgam1  24627  gam1  24628  gamfac  24630  subfacp1lem1  24644  subfacp1lem5  24649  subfacp1lem6  24650  subfacval2  24652  subfaclim  24653  subfacval3  24654  m1expevenALT  24684  cvxpcon  24708  cvxscon  24709  rescon  24712  cvmliftlem7  24757  cvmliftlem10  24760  sinccvglem  24888  elfzp1b  24895  relexpadd  24917  sqdivzi  24963  4bc3eq4  24982  halfthird  24984  5recm6rec  24985  divcnvlin  24991  muls1d  24992  prodf1  24998  prodfclim1  25000  prodfrec  25002  ntrivcvg  25004  ntrivcvgtail  25007  prodrblem  25034  fprodcvg  25035  prodmolem2a  25039  zprod  25042  fprodntriv  25047  prod1  25049  prodss  25052  fprodss  25053  fprodser  25054  fprodcl  25057  fproddiv  25064  fprodsplit  25068  fprodm1  25069  fprodp1  25071  risefacval2  25095  fallfacval2  25096  risefaccl  25099  fallfaccl  25100  risefacp1  25113  fallfacp1  25114  risefacfac  25117  fallfacfac  25118  fallfacfwd  25119  faclimlem1  25120  faclimlem2  25121  faclimlem3  25122  faclim  25123  iprodfac  25124  faclim2  25125  predfz  25227  brbtwn2  25558  colinearalglem4  25562  axsegconlem1  25570  ax5seglem1  25581  ax5seglem2  25582  ax5seglem3  25584  ax5seglem4  25585  ax5seglem5  25586  ax5seglem7  25588  ax5seglem9  25590  axbtwnid  25592  axpaschlem  25593  axlowdimlem6  25600  axlowdimlem13  25607  axlowdimlem14  25608  axlowdimlem16  25610  axeuclidlem  25615  axeuclid  25616  axcontlem2  25618  axcontlem4  25620  axcontlem7  25623  axcontlem8  25624  bpoly0  25810  bpoly1  25811  bpolycl  25812  bpolysum  25813  bpolydiflem  25814  fsumkthpow  25816  bpoly2  25817  bpoly3  25818  bpoly4  25819  fsumcube  25820  ltflcei  25950  itg2addnclem2  25958  itg2addnc  25959  dvreasin  25980  dvreacos  25981  areacirclem2  25982  areacirclem5  25986  areacirc  25988  fdc  26140  mettrifi  26154  heiborlem4  26214  heiborlem6  26216  bfp  26224  eldioph2lem1  26509  lzenom  26519  rabren3dioph  26567  irrapxlem1  26576  irrapxlem2  26577  pellexlem2  26584  pell1qrge1  26624  pell1qr1  26625  elpell1qr2  26626  pell1qrgaplem  26627  rmspecsqrnq  26660  rmspecfund  26663  rmxy0  26677  rmxm1  26688  rmym1  26689  2nn0ind  26699  jm2.24nn  26715  jm2.17a  26716  jm2.17b  26717  jm2.17c  26718  jm2.24  26719  acongeq  26739  jm2.18  26750  jm2.19lem3  26753  jm2.25  26761  jm2.16nn0  26766  jm2.27c  26769  jm3.1lem1  26779  jm3.1lem2  26780  rngunsnply  27047  flcidc  27048  psgnunilem5  27086  psgnunilem2  27087  psgnunilem4  27089  m1expaddsub  27090  psgnuni  27091  cnmsgnsubg  27103  cnmsgnbas  27104  cnmsgngrp  27105  proot1ex  27189  ofdivrec  27212  lhe4.4ex1a  27215  expgrowthi  27219  expgrowth  27221  refsum2cnlem1  27376  fmul01lt1lem2  27383  m1expeven  27393  clim1fr1  27395  isumneg  27396  climneg  27404  itgsin0pilem1  27412  itgsinexp  27417  stoweidlem1  27418  stoweidlem7  27424  stoweidlem10  27427  stoweidlem11  27428  stoweidlem13  27430  stoweidlem14  27431  stoweidlem17  27434  stoweidlem26  27443  stoweidlem34  27451  stoweidlem38  27455  stoweidlem41  27458  stoweidlem42  27459  stoweidlem45  27462  wallispilem2  27483  wallispilem3  27484  wallispilem4  27485  wallispilem5  27486  wallispi  27487  wallispi2lem1  27488  wallispi2lem2  27489  wallispi2  27490  stirlinglem1  27491  stirlinglem3  27493  stirlinglem4  27494  stirlinglem5  27495  stirlinglem6  27496  stirlinglem7  27497  stirlinglem8  27498  stirlinglem10  27500  stirlinglem11  27501  stirlinglem12  27502  stirlinglem13  27503  stirlinglem15  27505  sigaradd  27524  sec0  27849  onetansqsecsq  27850  cotsqcscsq  27851  5m4e1  27881
  Copyright terms: Public domain W3C validator