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 9979
Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn 9955. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-1cn 1 ∈ ℂ

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 9922 . 2 class 1
2 cc 9919 . 2 class
31, 2wcel 1988 1 wff 1 ∈ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  10017  1ex  10020  mulid1  10022  mulid2  10023  1re  10024  1cnd  10041  muladd11  10191  peano2cn  10193  mul02lem2  10198  addid1  10201  cnegex2  10203  peano2cnm  10332  0reALT  10363  ine0  10450  mulm1  10456  0lt1  10535  ixi  10641  muleqadd  10656  reccl  10677  recne0  10683  recid  10684  recid2  10685  div1  10701  1div1e1  10702  diveq1  10703  recdiv  10716  divdiv1  10721  divdiv2  10722  recdiv2  10723  conjmul  10727  eqneg  10730  div2neg  10733  recp1lt1  10906  recreclt  10907  recgt0ii  10914  inelr  10995  ofnegsub  11003  peano5nni  11008  nn1m1nn  11025  nn1suc  11026  nnaddcl  11027  nnmulcl  11028  nnsub  11044  1m1e0  11074  neg1cn  11109  neg1ne0  11111  negneg1e1  11113  1pneg1e0  11114  1m0e1  11116  0p1e1  11117  1p0e1  11118  2m1e1  11120  3m1e2  11122  4m1e3  11123  5m1e4  11124  6m1e5  11125  7m1e6  11126  8m1e7  11127  9m1e8  11128  2p2e4  11129  1p2e3  11137  3p2e5  11145  3p3e6  11146  4p2e6  11147  4p3e7  11148  4p4e8  11149  5p2e7  11150  5p3e8  11151  5p4e9  11152  5p5e10OLD  11153  6p2e8  11154  6p3e9  11155  6p4e10OLD  11156  7p2e9  11157  7p3e10OLD  11158  8p2e10OLD  11159  1t1e1  11160  3t3e9  11165  neg1mulneg1e1  11230  1mhlfehlf  11236  8th4div3  11237  halfpm6th  11238  addltmul  11253  elnn0nn  11320  elz2  11379  zlem1lt  11414  zltlem1  11415  nnaddm1cl  11419  zextlt  11436  zeo  11448  peano5uzi  11451  numsuc  11496  numltc  11513  numsucc  11534  numaddc  11546  6p5lem  11580  5p5e10  11581  6p4e10  11583  7p3e10  11588  8p2e10  11595  10m1e9  11615  4t3lem  11616  7t4e28  11635  9t11e99  11656  9t11e99OLD  11657  decbin2  11668  halfthird  11670  5recm6rec  11671  uzp1  11706  peano2uzr  11728  uzaddcl  11729  rebtwnz  11772  qbtwnre  12015  iccf1o  12301  fz01en  12354  fztp  12382  fzsuc2  12383  fztpval  12387  fseq1m1p1  12399  elfzp1b  12401  fz0to4untppr  12426  predfz  12448  fzoss2  12480  fzval3  12520  fzosplitsnm1  12526  fzo0to42pr  12539  fzo1to4tp  12540  fzosplitprm1  12561  fldiv4p1lem1div2  12619  ceim1l  12629  fldiv  12642  uzrdgxfr  12749  fzen2  12751  nn0ennn  12761  seqm1  12801  seqshft2  12810  monoord2  12815  sermono  12816  seqf1olem1  12823  seqf1olem2  12824  seqz  12832  ser1const  12840  expcl  12861  m1expcl2  12865  expclzlem  12867  expm1t  12871  1exp  12872  mulexpz  12883  expadd  12885  expaddz  12887  expmul  12888  expubnd  12904  sqrecii  12929  neg1sqe1  12942  irec  12947  i4  12950  binom21  12963  sq01  12969  crreczi  12972  bernneq  12973  bernneq2  12974  nn0opthlem1  13038  facndiv  13058  faclbnd4lem1  13063  faclbnd6  13069  bcnp1n  13084  bcm1k  13085  bcp1nk  13087  bcn2  13089  bcp1m1  13090  bcpasc  13091  4bc3eq4  13098  hashgadd  13149  hashfz  13197  hashfzo  13199  hashxplem  13203  hashbclem  13219  hashf1  13224  seqcoll  13231  swrds1  13433  swrdlsw  13434  wrdind  13458  wrd2ind  13459  swrds2  13666  relexpaddg  13774  rei  13877  imi  13878  recan  14057  iserex  14368  isercoll2  14380  serf0  14392  iseraltlem2  14394  iseraltlem3  14395  iseralt  14396  sumrblem  14423  fsumm1  14461  fsump1  14468  telfsumo  14515  fsumparts  14519  hashiun  14535  binomlem  14542  binom  14543  binom1p  14544  binom11  14545  binom1dif  14546  bcxmas  14548  isumsplit  14553  isum1p  14554  climcndslem1  14562  supcvg  14569  harmonic  14572  arisum  14573  arisum2  14574  trireciplem  14575  geoserg  14579  geolim  14582  geolim2  14583  georeclim  14584  geo2sum  14585  geo2sum2  14586  geoisum1c  14592  0.999...  14593  0.999...OLD  14594  geoihalfsum  14595  cvgrat  14596  mertenslem1  14597  mertenslem2  14598  mertens  14599  prodf1  14604  prodfclim1  14606  prodrblem  14640  fprodcvg  14641  prodmolem2a  14645  zprod  14648  fprodntriv  14653  prodss  14658  fprodss  14659  fprodsplit  14677  fprodn0f  14703  fprodclf  14704  risefaccl  14727  fallfaccl  14728  risefacfac  14747  binomfallfac  14753  bpolycl  14764  bpolysum  14765  bpolydiflem  14766  fsumkthpow  14768  bpoly2  14769  bpoly3  14770  bpoly4  14771  fsumcube  14772  esum  14792  ege2le3  14801  efsub  14811  efexp  14812  efzval  14813  eftlub  14820  effsumlt  14822  ef4p  14824  tanval3  14845  efi4p  14848  tan0  14862  efival  14863  tanadd  14878  cos2t  14889  cos2tsin  14890  ef01bndlem  14895  cos1bnd  14898  cos2bnd  14899  demoivreALT  14912  eirrlem  14913  rpnnen2lem3  14926  rpnnen2lem11  14934  ruclem12  14951  3dvds  15033  3dvdsOLD  15034  3dvdsdec  15035  3dvdsdecOLD  15036  3dvds2dec  15037  3dvds2decOLD  15038  odd2np1lem  15045  odd2np1  15046  opoe  15068  omoe  15069  opeo  15070  omeo  15071  m1exp1  15074  n2dvdsm1  15086  flodddiv4  15118  bitsfzo  15138  gcdmultiple  15250  sqgcd  15259  nn0seqcvgd  15264  prmind2  15379  hashdvds  15461  phiprmpw  15462  phiprm  15463  eulerthlem2  15468  iserodd  15521  sumhash  15581  fldivp1  15582  prmpwdvds  15589  pockthlem  15590  pockthi  15592  prmreclem4  15604  prmreclem6  15606  4sqlem11  15640  4sqlem19  15648  vdwapun  15659  vdwapid1  15660  vdwlem3  15668  vdwlem5  15670  vdwlem6  15671  vdwlem8  15673  vdwlem9  15674  vdwnnlem2  15681  ramub1lem1  15711  ramub1lem2  15712  ramcl  15714  prmo1  15722  dec5nprm  15751  decexp2  15760  prmlem0  15793  43prm  15810  83prm  15811  139prm  15812  163prm  15813  317prm  15814  631prm  15815  prmo4  15816  prmo5  15817  prmo6  15818  1259lem2  15820  1259lem3  15821  1259lem4  15822  1259lem5  15823  1259prm  15824  2503lem1  15825  2503lem2  15826  2503lem3  15827  2503prm  15828  4001lem1  15829  4001lem2  15830  4001lem3  15831  4001lem4  15832  4001prm  15833  gsumccat  17359  mulgnndir  17550  mulgnndirOLD  17551  mulgneg2  17556  m1expaddsub  17899  sylow1lem1  17994  sylow2a  18015  efgsval2  18127  efgsrel  18128  efgsres  18132  cnfld1  19752  zsssubrg  19785  cnmgpid  19789  zringcyg  19820  mulgrhm2  19828  cnmsgnsubg  19904  cnmsgnbas  19905  cnmsgngrp  19906  psgninv  19909  evpmodpmf1o  19923  blcvx  22582  iihalf2  22713  icopnfcnv  22722  iccpnfhmeo  22725  xrhmeo  22726  icccvx  22730  lebnumii  22746  reparphti  22778  pcoass  22805  pcorevlem  22807  pcorev2  22809  pi1xfrcnv  22838  cnstrcvs  22922  cncvs  22926  ncvsm1  22935  pjthlem1  23189  divcncf  23197  ovolunlem1a  23245  ovolunlem1  23246  ovolicc2lem4  23269  uniioombllem3  23334  uniioombllem4  23335  dyadovol  23342  vitalilem4  23361  iblitg  23516  iblcnlem1  23535  itgcnlem  23537  dvid  23662  dvexp  23697  dvexp2  23698  dvexp3  23722  dveflem  23723  dvef  23724  dvlipcn  23738  dvcvx  23764  dvfsumle  23765  dvfsumlem1  23770  degltp1le  23814  ply1divex  23877  fta1glem1  23906  plyaddlem1  23950  plymullem1  23951  coeidp  24000  dgrid  24001  dvply1  24020  dvply2g  24021  plyremlem  24040  fta1lem  24043  vieta1lem1  24046  vieta1lem2  24047  qaa  24059  iaa  24061  aalioulem3  24070  geolim3  24075  aaliou3lem2  24079  aaliou3lem7  24085  taylply2  24103  dvradcnv  24156  pserdvlem2  24163  pserdv2  24165  abelthlem1  24166  abelthlem2  24167  abelthlem6  24171  abelthlem7  24173  abelth  24176  reeff1olem  24181  reeff1o  24182  efcvx  24184  sinhalfpilem  24196  eulerid  24207  cos2pi  24209  sincosq3sgn  24233  sincosq4sgn  24234  tangtx  24238  sincos4thpi  24246  sincos6thpi  24248  pige3  24250  abssinper  24251  coskpi  24253  coseq1  24255  efeq1  24256  tanregt0  24266  logneg2  24342  logdivlti  24347  logcnlem4  24372  dvlog2lem  24379  dvlog2  24380  advlog  24381  advlogexp  24382  logtayl  24387  logtayl2  24389  logccv  24390  cxpval  24391  1cxp  24399  cxpcl  24401  cxpp1  24407  cxpsqrt  24430  dvsqrt  24464  dvcnsqrt  24466  sqrtcn  24472  cxpaddlelem  24473  root1id  24476  root1cj  24478  logrec  24482  logb1  24488  logbmpt  24507  ang180lem1  24520  ang180lem2  24521  ang180lem3  24522  isosctrlem1  24529  isosctrlem2  24530  1cubrlem  24549  1cubr  24550  mcubic  24555  binom4  24558  dquartlem1  24559  quartlem1  24565  asinlem  24576  asinlem2  24577  asinlem3a  24578  asinlem3  24579  asinf  24580  atandm2  24585  atandm4  24587  atanf  24588  asinneg  24594  efiasin  24596  sinasin  24597  asinsin  24600  asin1  24602  acos1  24603  reasinsin  24604  asinbnd  24607  cosasin  24612  atanneg  24615  atancj  24618  efiatan  24620  atanlogaddlem  24621  atanlogadd  24622  atanlogsublem  24623  atanlogsub  24624  efiatan2  24625  2efiatan  24626  tanatan  24627  cosatan  24629  cosatanne0  24630  atantan  24631  atanbndlem  24633  bndatandm  24637  atans2  24639  dvatan  24643  atantayl  24645  atantayl2  24646  atantayl3  24647  leibpilem1  24648  leibpilem2  24649  leibpi  24650  log2cnv  24652  log2tlbnd  24653  log2ublem3  24656  log2ub  24657  birthdaylem2  24660  birthday  24662  efrlim  24677  dfef2  24678  cvxcl  24692  scvxcvx  24693  emcllem2  24704  emcllem4  24706  emcllem7  24709  harmonicbnd4  24718  fsumharmonic  24719  zetacvg  24722  lgamcvg2  24762  lgam1  24771  gam1  24772  wilthlem1  24775  wilthlem2  24776  wilthlem3  24777  basellem2  24789  basellem5  24792  basellem6  24793  basellem7  24794  basellem8  24795  basellem9  24796  0sgm  24851  mule1  24855  ppiprm  24858  ppinprm  24859  chtprm  24860  chtnprm  24861  chpp1  24862  mumullem2  24887  1sgmprm  24905  1sgm2ppw  24906  ppiublem2  24909  ppiub  24910  chtublem  24917  chtub  24918  logfaclbnd  24928  logfacbnd3  24929  logfacrlim  24930  logexprlim  24931  mersenne  24933  perfect1  24934  perfectlem1  24935  perfectlem2  24936  perfect  24937  dchrelbasd  24945  dchrmulid2  24958  dchrfi  24961  dchrsum2  24974  sumdchr2  24976  bcp1ctr  24985  bposlem8  24997  zabsle1  25002  lgslem1  25003  lgslem2  25004  lgsfcl2  25009  lgsvalmod  25022  lgsneg  25027  lgsdilem  25030  lgsdir2lem1  25031  lgsdir2lem2  25032  lgsdir2lem3  25033  lgsdir2lem5  25035  lgsdir2  25036  lgsdir  25038  lgsdi  25040  lgsne0  25041  lgseisenlem1  25081  lgseisenlem2  25082  lgseisen  25085  lgsquadlem1  25086  lgsquadlem2  25087  lgsquad2lem1  25090  lgsquad2  25092  m1lgs  25094  2lgslem3c  25104  2lgsoddprmlem3b  25117  2lgsoddprmlem3c  25118  2lgsoddprmlem3d  25119  2sqlem10  25134  2sqlem11  25135  2sqblem  25137  chtppilimlem2  25144  chebbnd2  25147  chto1lb  25148  rplogsumlem1  25154  rpvmasumlem  25157  dchrmusumlema  25163  dchrmusum2  25164  dchrisum0flblem1  25178  rpvmasum2  25182  mudivsum  25200  mulogsum  25202  vmalogdivsum2  25208  selberg2lem  25220  logdivbnd  25226  pntrmax  25234  pntrsumo1  25235  pntrsumbnd2  25237  pntrlog2bndlem5  25251  pntpbnd1a  25255  pntpbnd2  25257  pntibndlem2  25261  pntlemd  25264  pntlemc  25265  pntlemr  25272  brbtwn2  25766  colinearalglem4  25770  ax5seglem1  25789  ax5seglem2  25790  ax5seglem3  25792  ax5seglem5  25794  ax5seglem7  25796  ax5seglem9  25798  axbtwnid  25800  axpaschlem  25801  axlowdimlem13  25815  axlowdimlem14  25816  axlowdimlem16  25818  axeuclidlem  25823  axcontlem2  25826  axcontlem4  25828  axcontlem7  25831  axcontlem8  25832  crctcshwlkn0lem6  26688  wwlksnext  26769  clwwlksf1  26897  wwlksext2clwwlk  26904  numclwwlkovf2ex  27191  ex-fl  27274  ex-ind-dvds  27288  vc2OLD  27393  vc0  27399  vcm  27401  nvm1  27490  nvmtri  27496  nvge0  27498  ipval2lem3  27530  ipidsq  27535  lnoadd  27583  ip1ilem  27651  ip1i  27652  ip2i  27653  ipdirilem  27654  ipasslem1  27656  ipasslem2  27657  ipasslem10  27664  minvecolem2  27701  hvsubid  27853  hv2times  27888  hisubcomi  27931  normlem9  27945  normlem7tALT  27946  norm-ii-i  27964  normsubi  27968  hhssnv  28091  pjhthlem1  28220  h1de2bi  28383  homulid2  28629  ho2times  28648  lnop0  28795  lnopaddi  28800  lnophmlem2  28846  lnfn0i  28871  lnfnaddi  28872  hst1h  29056  sto2i  29066  stadd3i  29077  addltmulALT  29275  dpmul4  29596  isarchi3  29715  archirngz  29717  psgnid  29821  lmatfvlem  29855  qqhval2lem  29999  dya2ub  30306  omssubadd  30336  eulerpartlemgs2  30416  fib5  30441  fib6  30442  ballotlem2  30524  sgnneg  30576  signswch  30612  signlem0  30638  itgexpif  30658  reprlt  30671  breprexp  30685  breprexpnat  30686  hgt750lem2  30704  subfacp1lem5  31140  subfacp1lem6  31141  subfacval2  31143  subfaclim  31144  subfacval3  31145  cvxsconn  31199  resconn  31202  cvmliftlem7  31247  cvmliftlem10  31250  problem4  31536  sinccvglem  31540  sqdivzi  31585  faclimlem1  31604  dnibndlem5  32447  dnibndlem10  32452  ltflcei  33368  sin2h  33370  cos2h  33371  tan2h  33372  pigt3  33373  poimirlem13  33393  poimirlem16  33396  poimirlem17  33397  poimirlem19  33399  poimirlem20  33400  poimirlem31  33411  mblfinlem2  33418  mblfinlem3  33419  0mbf  33426  dvtan  33431  itg2addnclem3  33434  dvasin  33467  dvacos  33468  areacirc  33476  fdc  33512  mettrifi  33524  heiborlem4  33584  heiborlem6  33586  eldioph2lem1  37142  lzenom  37152  irrapxlem1  37205  rmspecsqrtnq  37289  rmspecsqrtnqOLD  37290  rmxm1  37318  rmym1  37319  2nn0ind  37329  jm2.24nn  37345  jm2.17a  37346  jm2.17b  37347  jm2.17c  37348  jm2.24  37349  acongeq  37369  jm2.18  37374  jm2.27c  37393  jm3.1lem2  37404  rngunsnply  37562  flcidc  37563  inductionexd  38273  unitadd  38318  hashnzfzclim  38341  ofdivrec  38345  lhe4.4ex1a  38348  expgrowth  38354  dvradcnv2  38366  binomcxplemrat  38369  binomcxplemnotnn0  38375  isosctrlem1ALT  38990  dvsinax  39890  dvnprodlem3  39926  itgsin0pilem1  39928  itgsbtaddcnst  39961  stoweidlem13  39993  stoweidlem26  40006  stoweidlem34  40014  stoweidlem38  40018  wallispilem2  40046  wallispilem4  40048  wallispi2lem1  40051  stirlinglem1  40054  stirlinglem5  40058  stirlinglem10  40063  dirkerper  40076  dirkertrigeqlem1  40078  dirkertrigeqlem3  40080  dirkertrigeq  40081  dirkercncflem4  40086  fourierdlem24  40111  sqwvfoura  40208  sqwvfourb  40209  fourierswlem  40210  1t10e1p1e11  41082  1t10e1p1e11OLD  41083  fmtnorec3  41225  fmtno5lem4  41233  fmtno5  41234  257prm  41238  fmtno4nprmfac193  41251  m3prm  41271  139prmALT  41276  127prm  41280  m7prm  41281  lighneallem3  41289  proththd  41296  3exp4mod41  41298  41prothprmlem2  41300  perfectALTVlem2  41396  perfectALTV  41397  evengpop3  41451  nnsum4primeseven  41453  nnsum4primesevenALTV  41454  bgoldbtbndlem1  41458  0nodd  41575  altgsumbcALT  41896  exple2lt6  41910  nn0sumshdiglemB  42179  onetansqsecsq  42267  cotsqcscsq  42268  5m4e1  42308
  Copyright terms: Public domain W3C validator