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

Axiom ax-1cn 9873
Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn 9849. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-1cn 1 ∈ ℂ

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 9816 . 2 class 1
2 cc 9813 . 2 class
31, 2wcel 1977 1 wff 1 ∈ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  9911  1ex  9914  mulid1  9916  mulid2  9917  1re  9918  1cnd  9935  muladd11  10085  peano2cn  10087  mul02lem2  10092  addid1  10095  cnegex2  10097  peano2cnm  10226  0reALT  10257  ine0  10344  mulm1  10350  0lt1  10429  ixi  10535  muleqadd  10550  reccl  10571  recne0  10577  recid  10578  recid2  10579  div1  10595  1div1e1  10596  diveq1  10597  recdiv  10610  divdiv1  10615  divdiv2  10616  recdiv2  10617  conjmul  10621  eqneg  10624  div2neg  10627  recp1lt1  10800  recreclt  10801  recgt0ii  10808  inelr  10887  ofnegsub  10895  peano5nni  10900  nn1m1nn  10917  nn1suc  10918  nnaddcl  10919  nnmulcl  10920  nnsub  10936  1m1e0  10966  neg1cn  11001  neg1ne0  11003  negneg1e1  11005  1pneg1e0  11006  1m0e1  11008  0p1e1  11009  1p0e1  11010  2m1e1  11012  3m1e2  11014  4m1e3  11015  5m1e4  11016  6m1e5  11017  7m1e6  11018  8m1e7  11019  9m1e8  11020  2p2e4  11021  1p2e3  11029  3p2e5  11037  3p3e6  11038  4p2e6  11039  4p3e7  11040  4p4e8  11041  5p2e7  11042  5p3e8  11043  5p4e9  11044  5p5e10OLD  11045  6p2e8  11046  6p3e9  11047  6p4e10OLD  11048  7p2e9  11049  7p3e10OLD  11050  8p2e10OLD  11051  1t1e1  11052  3t3e9  11057  neg1mulneg1e1  11122  1mhlfehlf  11128  8th4div3  11129  halfpm6th  11130  addltmul  11145  elnn0nn  11212  elz2  11271  zlem1lt  11306  zltlem1  11307  nnaddm1cl  11311  zextlt  11327  zeo  11339  peano5uzi  11342  numsuc  11387  numltc  11404  numsucc  11425  numaddc  11437  6p5lem  11471  5p5e10  11472  6p4e10  11474  7p3e10  11479  8p2e10  11486  10m1e9  11506  4t3lem  11507  7t4e28  11526  9t11e99  11547  9t11e99OLD  11548  decbin2  11559  halfthird  11561  5recm6rec  11562  uzp1  11597  peano2uzr  11619  uzaddcl  11620  rebtwnz  11663  qbtwnre  11904  iccf1o  12187  fz01en  12240  fztp  12267  fzsuc2  12268  fztpval  12272  fseq1m1p1  12284  elfzp1b  12286  fz0to4untppr  12311  predfz  12333  fzoss2  12365  fzval3  12404  fzosplitsnm1  12409  fzo0to42pr  12422  fzo1to4tp  12423  fzosplitprm1  12443  fldiv4p1lem1div2  12498  ceim1l  12508  fldiv  12521  uzrdgxfr  12628  fzen2  12630  nn0ennn  12640  seqm1  12680  seqshft2  12689  monoord2  12694  sermono  12695  seqf1olem1  12702  seqf1olem2  12703  seqz  12711  ser1const  12719  expcl  12740  m1expcl2  12744  expclzlem  12746  expm1t  12750  1exp  12751  mulexpz  12762  expadd  12764  expaddz  12766  expmul  12767  expubnd  12783  sqrecii  12808  neg1sqe1  12821  irec  12826  i4  12829  binom21  12842  sq01  12848  crreczi  12851  bernneq  12852  bernneq2  12853  nn0opthlem1  12917  facndiv  12937  faclbnd4lem1  12942  faclbnd6  12948  bcnp1n  12963  bcm1k  12964  bcp1nk  12966  bcn2  12968  bcp1m1  12969  bcpasc  12970  4bc3eq4  12977  hashgadd  13027  hashfz  13074  hashfzo  13076  hashxplem  13080  hashbclem  13093  hashf1  13098  seqcoll  13105  swrds1  13303  swrdlsw  13304  wrdind  13328  wrd2ind  13329  swrds2  13533  relexpaddg  13641  rei  13744  imi  13745  recan  13924  iserex  14235  isercoll2  14247  serf0  14259  iseraltlem2  14261  iseraltlem3  14262  iseralt  14263  sumrblem  14289  fsumm1  14324  fsump1  14329  telfsumo  14375  fsumparts  14379  hashiun  14395  binomlem  14400  binom  14401  binom1p  14402  binom11  14403  binom1dif  14404  bcxmas  14406  isumsplit  14411  isum1p  14412  climcndslem1  14420  supcvg  14427  harmonic  14430  arisum  14431  arisum2  14432  trireciplem  14433  geoserg  14437  geolim  14440  geolim2  14441  georeclim  14442  geo2sum  14443  geo2sum2  14444  geoisum1c  14450  0.999...  14451  0.999...OLD  14452  geoihalfsum  14453  cvgrat  14454  mertenslem1  14455  mertenslem2  14456  mertens  14457  prodf1  14462  prodfclim1  14464  prodrblem  14498  fprodcvg  14499  prodmolem2a  14503  zprod  14506  fprodntriv  14511  prodss  14516  fprodss  14517  fprodsplit  14535  fprodn0f  14561  fprodclf  14562  risefaccl  14585  fallfaccl  14586  risefacfac  14605  binomfallfac  14611  bpolycl  14622  bpolysum  14623  bpolydiflem  14624  fsumkthpow  14626  bpoly2  14627  bpoly3  14628  bpoly4  14629  fsumcube  14630  esum  14650  ege2le3  14659  efsub  14669  efexp  14670  efzval  14671  eftlub  14678  effsumlt  14680  ef4p  14682  tanval3  14703  efi4p  14706  tan0  14720  efival  14721  tanadd  14736  cos2t  14747  cos2tsin  14748  ef01bndlem  14753  cos1bnd  14756  cos2bnd  14757  demoivreALT  14770  eirrlem  14771  rpnnen2lem3  14784  rpnnen2lem11  14792  ruclem12  14809  3dvds  14890  3dvdsOLD  14891  3dvdsdec  14892  3dvdsdecOLD  14893  3dvds2dec  14894  3dvds2decOLD  14895  odd2np1lem  14902  odd2np1  14903  opoe  14925  omoe  14926  opeo  14927  omeo  14928  m1exp1  14931  n2dvdsm1  14943  flodddiv4  14975  bitsfzo  14995  gcdmultiple  15107  sqgcd  15116  nn0seqcvgd  15121  prmind2  15236  hashdvds  15318  phiprmpw  15319  phiprm  15320  eulerthlem2  15325  iserodd  15378  sumhash  15438  fldivp1  15439  prmpwdvds  15446  pockthlem  15447  pockthi  15449  prmreclem4  15461  prmreclem6  15463  4sqlem11  15497  4sqlem19  15505  vdwapun  15516  vdwapid1  15517  vdwlem3  15525  vdwlem5  15527  vdwlem6  15528  vdwlem8  15530  vdwlem9  15531  vdwnnlem2  15538  ramub1lem1  15568  ramub1lem2  15569  ramcl  15571  prmo1  15579  dec5nprm  15608  decexp2  15617  prmlem0  15650  43prm  15667  83prm  15668  139prm  15669  163prm  15670  317prm  15671  631prm  15672  prmo4  15673  prmo5  15674  prmo6  15675  1259lem2  15677  1259lem3  15678  1259lem4  15679  1259lem5  15680  1259prm  15681  2503lem1  15682  2503lem2  15683  2503lem3  15684  2503prm  15685  4001lem1  15686  4001lem2  15687  4001lem3  15688  4001lem4  15689  4001prm  15690  gsumccat  17201  mulgnndir  17392  mulgnndirOLD  17393  mulgneg2  17398  m1expaddsub  17741  sylow1lem1  17836  sylow2a  17857  efgsval2  17969  efgsrel  17970  efgsres  17974  cnfld1  19590  zsssubrg  19623  cnmgpid  19627  zringcyg  19658  mulgrhm2  19666  cnmsgnsubg  19742  cnmsgnbas  19743  cnmsgngrp  19744  psgninv  19747  evpmodpmf1o  19761  blcvx  22409  iihalf2  22540  icopnfcnv  22549  iccpnfhmeo  22552  xrhmeo  22553  icccvx  22557  lebnumii  22573  reparphti  22605  pcoass  22632  pcorevlem  22634  pcorev2  22636  pi1xfrcnv  22665  cnstrcvs  22749  cncvs  22753  ncvsm1  22762  pjthlem1  23016  ovolunlem1a  23071  ovolunlem1  23072  ovolicc2lem4  23095  uniioombllem3  23159  uniioombllem4  23160  dyadovol  23167  vitalilem4  23186  iblitg  23341  iblcnlem1  23360  itgcnlem  23362  dvid  23487  dvexp  23522  dvexp2  23523  dvexp3  23545  dveflem  23546  dvef  23547  dvlipcn  23561  dvcvx  23587  dvfsumle  23588  dvfsumlem1  23593  degltp1le  23637  ply1divex  23700  fta1glem1  23729  plyaddlem1  23773  plymullem1  23774  coeidp  23823  dgrid  23824  dvply1  23843  dvply2g  23844  plyremlem  23863  fta1lem  23866  vieta1lem1  23869  vieta1lem2  23870  qaa  23882  iaa  23884  aalioulem3  23893  geolim3  23898  aaliou3lem2  23902  aaliou3lem7  23908  taylply2  23926  dvradcnv  23979  pserdvlem2  23986  pserdv2  23988  abelthlem1  23989  abelthlem2  23990  abelthlem6  23994  abelthlem7  23996  abelth  23999  reeff1olem  24004  reeff1o  24005  efcvx  24007  sinhalfpilem  24019  eulerid  24030  cos2pi  24032  sincosq3sgn  24056  sincosq4sgn  24057  tangtx  24061  sincos4thpi  24069  sincos6thpi  24071  pige3  24073  abssinper  24074  coskpi  24076  coseq1  24078  efeq1  24079  tanregt0  24089  logneg2  24165  logdivlti  24170  logcnlem4  24191  dvlog2lem  24198  dvlog2  24199  advlog  24200  advlogexp  24201  logtayl  24206  logtayl2  24208  logccv  24209  cxpval  24210  1cxp  24218  cxpcl  24220  cxpp1  24226  cxpsqrt  24249  dvsqrt  24283  dvcnsqrt  24285  sqrtcn  24291  cxpaddlelem  24292  root1id  24295  root1cj  24297  logrec  24301  logb1  24307  logbmpt  24326  ang180lem1  24339  ang180lem2  24340  ang180lem3  24341  isosctrlem1  24348  isosctrlem2  24349  1cubrlem  24368  1cubr  24369  mcubic  24374  binom4  24377  dquartlem1  24378  quartlem1  24384  asinlem  24395  asinlem2  24396  asinlem3a  24397  asinlem3  24398  asinf  24399  atandm2  24404  atandm4  24406  atanf  24407  asinneg  24413  efiasin  24415  sinasin  24416  asinsin  24419  asin1  24421  acos1  24422  reasinsin  24423  asinbnd  24426  cosasin  24431  atanneg  24434  atancj  24437  efiatan  24439  atanlogaddlem  24440  atanlogadd  24441  atanlogsublem  24442  atanlogsub  24443  efiatan2  24444  2efiatan  24445  tanatan  24446  cosatan  24448  cosatanne0  24449  atantan  24450  atanbndlem  24452  bndatandm  24456  atans2  24458  dvatan  24462  atantayl  24464  atantayl2  24465  atantayl3  24466  leibpilem1  24467  leibpilem2  24468  leibpi  24469  log2cnv  24471  log2tlbnd  24472  log2ublem3  24475  log2ub  24476  birthdaylem2  24479  birthday  24481  efrlim  24496  dfef2  24497  cvxcl  24511  scvxcvx  24512  emcllem2  24523  emcllem4  24525  emcllem7  24528  harmonicbnd4  24537  fsumharmonic  24538  zetacvg  24541  lgamcvg2  24581  lgam1  24590  gam1  24591  wilthlem1  24594  wilthlem2  24595  wilthlem3  24596  basellem2  24608  basellem5  24611  basellem6  24612  basellem7  24613  basellem8  24614  basellem9  24615  0sgm  24670  mule1  24674  ppiprm  24677  ppinprm  24678  chtprm  24679  chtnprm  24680  chpp1  24681  mumullem2  24706  1sgmprm  24724  1sgm2ppw  24725  ppiublem2  24728  ppiub  24729  chtublem  24736  chtub  24737  logfaclbnd  24747  logfacbnd3  24748  logfacrlim  24749  logexprlim  24750  mersenne  24752  perfect1  24753  perfectlem1  24754  perfectlem2  24755  perfect  24756  dchrelbasd  24764  dchrmulid2  24777  dchrfi  24780  dchrsum2  24793  sumdchr2  24795  bcp1ctr  24804  bposlem8  24816  zabsle1  24821  lgslem1  24822  lgslem2  24823  lgsfcl2  24828  lgsvalmod  24841  lgsneg  24846  lgsdilem  24849  lgsdir2lem1  24850  lgsdir2lem2  24851  lgsdir2lem3  24852  lgsdir2lem5  24854  lgsdir2  24855  lgsdir  24857  lgsdi  24859  lgsne0  24860  lgseisenlem1  24900  lgseisenlem2  24901  lgseisen  24904  lgsquadlem1  24905  lgsquadlem2  24906  lgsquad2lem1  24909  lgsquad2  24911  m1lgs  24913  2lgslem3c  24923  2lgsoddprmlem3b  24936  2lgsoddprmlem3c  24937  2lgsoddprmlem3d  24938  2sqlem10  24953  2sqlem11  24954  2sqblem  24956  chtppilimlem2  24963  chebbnd2  24966  chto1lb  24967  rplogsumlem1  24973  rpvmasumlem  24976  dchrmusumlema  24982  dchrmusum2  24983  dchrisum0flblem1  24997  rpvmasum2  25001  mudivsum  25019  mulogsum  25021  vmalogdivsum2  25027  selberg2lem  25039  logdivbnd  25045  pntrmax  25053  pntrsumo1  25054  pntrsumbnd2  25056  pntrlog2bndlem5  25070  pntpbnd1a  25074  pntpbnd2  25076  pntibndlem2  25080  pntlemd  25083  pntlemc  25084  pntlemr  25091  brbtwn2  25585  colinearalglem4  25589  ax5seglem1  25608  ax5seglem2  25609  ax5seglem3  25611  ax5seglem5  25613  ax5seglem7  25615  ax5seglem9  25617  axbtwnid  25619  axpaschlem  25620  axlowdimlem13  25634  axlowdimlem14  25635  axlowdimlem16  25637  axeuclidlem  25642  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  axcontlem8  25651  wlklenvm1  26060  wlkiswwlk1  26218  wwlknext  26252  clwwlkf1  26324  wwlkext2clwwlk  26331  eupares  26502  eupap1  26503  eupath2lem3  26506  frghash2spot  26590  usgreghash2spotv  26593  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwwlk6  26640  ex-fl  26696  ex-ind-dvds  26710  vc2OLD  26807  vc0  26813  vcm  26815  nvm1  26904  nvmtri  26910  nvge0  26912  ipval2lem3  26944  ipidsq  26949  lnoadd  26997  ip1ilem  27065  ip1i  27066  ip2i  27067  ipdirilem  27068  ipasslem1  27070  ipasslem2  27071  ipasslem10  27078  minvecolem2  27115  hvsubid  27267  hv2times  27302  hisubcomi  27345  normlem9  27359  normlem7tALT  27360  norm-ii-i  27378  normsubi  27382  hhssnv  27505  pjhthlem1  27634  h1de2bi  27797  homulid2  28043  ho2times  28062  lnop0  28209  lnopaddi  28214  lnophmlem2  28260  lnfn0i  28285  lnfnaddi  28286  hst1h  28470  sto2i  28480  stadd3i  28491  addltmulALT  28689  isarchi3  29072  archirngz  29074  psgnid  29178  lmatfvlem  29209  qqhval2lem  29353  dya2ub  29659  omssubadd  29689  eulerpartlemgs2  29769  fib5  29794  fib6  29795  ballotlem2  29877  sgnneg  29929  signswch  29964  signlem0  29990  subfacp1lem5  30420  subfacp1lem6  30421  subfacval2  30423  subfaclim  30424  subfacval3  30425  cvxscon  30479  rescon  30482  cvmliftlem7  30527  cvmliftlem10  30530  problem4  30816  sinccvglem  30820  sqdivzi  30863  faclimlem1  30882  dnibndlem5  31642  dnibndlem10  31647  ltflcei  32567  sin2h  32569  cos2h  32570  tan2h  32571  pigt3  32572  poimirlem13  32592  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem31  32610  mblfinlem2  32617  mblfinlem3  32618  0mbf  32625  dvtan  32630  itg2addnclem3  32633  dvasin  32666  dvacos  32667  areacirc  32675  fdc  32711  mettrifi  32723  heiborlem4  32783  heiborlem6  32785  eldioph2lem1  36341  lzenom  36351  irrapxlem1  36404  rmspecsqrtnq  36488  rmspecsqrtnqOLD  36489  rmxm1  36517  rmym1  36518  2nn0ind  36528  jm2.24nn  36544  jm2.17a  36545  jm2.17b  36546  jm2.17c  36547  jm2.24  36548  acongeq  36568  jm2.18  36573  jm2.27c  36592  jm3.1lem2  36603  rngunsnply  36762  flcidc  36763  inductionexd  37473  unitadd  37520  hashnzfzclim  37543  ofdivrec  37547  lhe4.4ex1a  37550  expgrowth  37556  dvradcnv2  37568  binomcxplemrat  37571  binomcxplemnotnn0  37577  isosctrlem1ALT  38192  divcncf  38769  dvsinax  38801  dvnprodlem3  38838  itgsin0pilem1  38841  itgsbtaddcnst  38874  stoweidlem13  38906  stoweidlem26  38919  stoweidlem34  38927  stoweidlem38  38931  wallispilem2  38959  wallispilem4  38961  wallispi2lem1  38964  stirlinglem1  38967  stirlinglem5  38971  stirlinglem10  38976  dirkerper  38989  dirkertrigeqlem1  38991  dirkertrigeqlem3  38993  dirkertrigeq  38994  dirkercncflem4  38999  fourierdlem24  39024  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  1t10e1p1e11  39937  1t10e1p1e11OLD  39938  fmtnorec3  39998  fmtno5lem4  40006  fmtno5  40007  257prm  40011  fmtno4nprmfac193  40024  m3prm  40044  139prmALT  40049  127prm  40053  m7prm  40054  lighneallem3  40062  proththd  40069  3exp4mod41  40071  41prothprmlem2  40073  perfectALTVlem2  40165  perfectALTV  40166  evengpop3  40214  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  bgoldbtbndlem1  40221  crctcsh1wlkn0lem6  41018  wwlksnext  41099  clwwlksf1  41224  wwlksext2clwwlk  41231  frgrhash2wsp  41497  fusgreghash2wspv  41499  av-numclwwlkovf2ex  41517  0nodd  41600  altgsumbcALT  41924  exple2lt6  41939  nn0sumshdiglemB  42212  onetansqsecsq  42301  cotsqcscsq  42302  5m4e1  42352
  Copyright terms: Public domain W3C validator