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

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

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 9514 . 2
2 cc 9511 . 2
31, 2wcel 1818 1
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  9609  1ex  9612  mulid1  9614  mulid2  9615  1re  9616  1cnd  9633  muladd11  9771  peano2cn  9773  mul02lem2  9778  addid1  9781  cnegex2  9783  peano2cnm  9908  0reALT  9940  ine0  10017  mulm1  10023  0lt1  10100  ixi  10203  muleqadd  10218  reccl  10239  recne0  10245  recid  10246  recid2  10247  div1  10261  1div1e1  10262  diveq1  10263  recdiv  10275  divdiv1  10280  divdiv2  10281  recdiv2  10282  conjmul  10286  eqneg  10289  div2neg  10292  recp1lt1  10468  recreclt  10469  recgt0ii  10476  inelr  10551  ofnegsub  10559  peano5nni  10564  nn1m1nn  10581  nn1suc  10582  nnaddcl  10583  nnmulcl  10584  nnsub  10599  1m1e0  10629  neg1cn  10664  neg1ne0  10666  negneg1e1  10668  1pneg1e0  10669  1m0e1  10671  0p1e1  10672  1p0e1  10673  2m1e1  10675  3m1e2  10677  2p2e4  10678  1p2e3  10685  3p2e5  10693  3p3e6  10694  4p2e6  10695  4p3e7  10696  4p4e8  10697  5p2e7  10698  5p3e8  10699  5p4e9  10700  5p5e10  10701  6p2e8  10702  6p3e9  10703  6p4e10  10704  7p2e9  10705  7p3e10  10706  8p2e10  10707  1t1e1  10708  3t3e9  10713  neg1mulneg1e1  10778  1mhlfehlf  10783  8th4div3  10784  halfpm6th  10785  addltmul  10799  elnn0nn  10863  elz2  10906  zlem1lt  10940  zltlem1  10941  nnaddm1cl  10945  zextlt  10962  zeo  10973  peano5uzi  10976  uzindOLD  10982  numsuc  11016  numltc  11024  numsucc  11030  numaddc  11039  6p5lem  11053  4t3lem  11075  7t4e28  11088  decbin2  11108  uzp1  11143  peano2uzr  11165  uzaddcl  11166  rebtwnz  11210  qbtwnre  11427  iccf1o  11693  fz01en  11742  fztp  11765  fzsuc2  11766  fztpval  11770  fseq1m1p1  11782  elfzp1b  11784  fzoss2  11853  fzval3  11885  fzosplitsnm1  11890  fzo0to42pr  11901  fzosplitprm1  11919  ceim1l  11974  fldiv  11987  uzrdgxfr  12077  fzen2  12079  nn0ennn  12089  seqm1  12124  seqshft2  12133  monoord2  12138  sermono  12139  seqf1olem1  12146  seqf1olem2  12147  seqz  12155  ser1const  12163  expcl  12184  m1expcl2  12188  expclzlem  12190  expm1t  12194  1exp  12195  mulexpz  12206  expadd  12208  expaddz  12210  expmul  12211  expubnd  12226  sqrecii  12250  neg1sqe1  12263  irec  12267  i4  12270  binom21  12284  sq01  12288  crreczi  12291  bernneq  12292  bernneq2  12293  nn0opthlem1  12348  facndiv  12366  faclbnd4lem1  12371  faclbnd6  12377  bcnp1n  12392  bcm1k  12393  bcp1nk  12395  bcn2  12397  bcp1m1  12398  bcpasc  12399  hashgadd  12445  hashfz  12485  hashfzo  12487  hashxplem  12491  hashbclem  12501  hashf1  12506  seqcoll  12512  swrds1  12676  swrdlsw  12677  wrdeqcats1  12699  wrdind  12702  wrd2ind  12703  swrds2  12883  rei  12989  imi  12990  recan  13169  iserex  13479  isercoll2  13491  serf0  13503  iseraltlem2  13505  iseraltlem3  13506  iseralt  13507  sumrblem  13533  fsumm1  13566  fsump1  13571  telfsumo  13616  fsumparts  13620  hashiun  13636  binomlem  13641  binom  13642  binom1p  13643  binom11  13644  binom1dif  13645  bcxmas  13647  isumsplit  13652  isum1p  13653  climcndslem1  13661  supcvg  13667  harmonic  13670  arisum  13671  arisum2  13672  trireciplem  13673  geoserg  13677  geolim  13679  geolim2  13680  georeclim  13681  geo2sum  13682  geo2sum2  13683  geoisum1c  13689  0.999...  13690  geoihalfsum  13691  cvgrat  13692  mertenslem1  13693  mertenslem2  13694  mertens  13695  prodf1  13700  prodfclim1  13702  prodrblem  13736  fprodcvg  13737  prodmolem2a  13741  zprod  13744  fprodntriv  13749  prodss  13754  fprodss  13755  fprodsplit  13770  esum  13816  ege2le3  13825  efsub  13835  efexp  13836  efzval  13837  eftlub  13844  effsumlt  13846  ef4p  13848  tanval3  13869  efi4p  13872  tan0  13886  efival  13887  tanadd  13902  cos2t  13913  cos2tsin  13914  ef01bndlem  13919  cos1bnd  13922  cos2bnd  13923  demoivreALT  13936  eirrlem  13937  rpnnen2lem3  13950  rpnnen2lem11  13958  ruclem12  13974  odd2np1lem  14045  odd2np1  14046  3dvds  14050  bitsfzo  14085  gcdmultiple  14188  sqgcd  14196  nn0seqcvgd  14199  prmind2  14228  hashdvds  14305  phiprmpw  14306  phiprm  14307  eulerthlem2  14312  opoe  14335  omoe  14336  opeo  14337  omeo  14338  iserodd  14359  sumhash  14415  fldivp1  14416  prmpwdvds  14422  pockthlem  14423  pockthi  14425  prmreclem2  14435  prmreclem4  14437  prmreclem6  14439  4sqlem11  14473  4sqlem19  14481  vdwapun  14492  vdwapid1  14493  vdwlem3  14501  vdwlem5  14503  vdwlem6  14504  vdwlem8  14506  vdwlem9  14507  vdwnnlem2  14514  ramub1lem1  14544  ramub1lem2  14545  ramcl  14547  dec5nprm  14552  decexp2  14561  prmlem0  14591  43prm  14607  83prm  14608  139prm  14609  163prm  14610  317prm  14611  631prm  14612  1259lem1  14613  1259lem2  14614  1259lem3  14615  1259lem4  14616  1259lem5  14617  1259prm  14618  2503lem1  14619  2503lem2  14620  2503lem3  14621  2503prm  14622  4001lem1  14623  4001lem2  14624  4001lem3  14625  4001lem4  14626  4001prm  14627  gsumccat  16009  mulgnndir  16164  mulgneg2  16169  m1expaddsub  16523  sylow1lem1  16618  sylow2a  16639  efgsval2  16751  efgsrel  16752  efgsres  16756  cnfld1  18443  zsssubrg  18476  zringcyg  18513  zcyg  18518  prmirredlemOLD  18526  mulgrhm2  18533  mulgrhm2OLD  18536  cnmsgnsubg  18613  cnmsgnbas  18614  cnmsgngrp  18615  psgninv  18618  evpmodpmf1o  18632  blcvx  21303  iihalf2  21433  icopnfcnv  21442  iccpnfhmeo  21445  xrhmeo  21446  icccvx  21450  lebnumii  21466  reparphti  21497  pcoass  21524  pcorevlem  21526  pcorev2  21528  pi1xfrcnv  21557  pjthlem1  21852  ovolunlem1a  21907  ovolunlem1  21908  ovolicc2lem4  21931  uniioombllem3  21994  uniioombllem4  21995  dyadovol  22002  vitalilem4  22020  iblitg  22175  iblcnlem1  22194  itgcnlem  22196  dvid  22321  dvexp  22356  dvexp2  22357  dvexp3  22379  dveflem  22380  dvef  22381  dvlipcn  22395  dvcvx  22421  dvfsumle  22422  dvfsumlem1  22427  degltp1le  22473  ply1divex  22537  fta1glem1  22566  plyaddlem1  22610  plymullem1  22611  coeidp  22660  dgrid  22661  dvply1  22680  dvply2g  22681  plyremlem  22700  fta1lem  22703  vieta1lem1  22706  vieta1lem2  22707  qaa  22719  iaa  22721  aalioulem3  22730  geolim3  22735  aaliou3lem2  22739  aaliou3lem7  22745  taylply2  22763  dvradcnv  22816  pserdvlem2  22823  pserdv2  22825  abelthlem1  22826  abelthlem2  22827  abelthlem6  22831  abelthlem7  22833  abelth  22836  reeff1olem  22841  reeff1o  22842  efcvx  22844  sinhalfpilem  22856  eulerid  22867  cos2pi  22869  sincosq3sgn  22893  sincosq4sgn  22894  tangtx  22898  sincos4thpi  22906  sincos6thpi  22908  pige3  22910  abssinper  22911  coskpi  22913  coseq1  22915  efeq1  22916  tanregt0  22926  logneg2  23000  logdivlti  23005  logcnlem4  23026  dvlog2lem  23033  dvlog2  23034  advlog  23035  advlogexp  23036  logtayl  23041  logtayl2  23043  logccv  23044  cxpval  23045  1cxp  23053  cxpcl  23055  cxpp1  23061  cxpsqrt  23084  dvsqrt  23118  sqrtcn  23124  cxpaddlelem  23125  root1id  23128  root1cj  23130  loglesqrt  23132  ang180lem1  23141  ang180lem2  23142  ang180lem3  23143  logrec  23151  isosctrlem1  23152  isosctrlem2  23153  1cubrlem  23172  1cubr  23173  mcubic  23178  binom4  23181  dquartlem1  23182  quartlem1  23188  asinlem  23199  asinlem2  23200  asinlem3a  23201  asinlem3  23202  asinf  23203  atandm2  23208  atandm4  23210  atanf  23211  asinneg  23217  efiasin  23219  sinasin  23220  asinsin  23223  asin1  23225  acos1  23226  reasinsin  23227  asinbnd  23230  cosasin  23235  atanneg  23238  atancj  23241  efiatan  23243  atanlogaddlem  23244  atanlogadd  23245  atanlogsublem  23246  atanlogsub  23247  efiatan2  23248  2efiatan  23249  tanatan  23250  cosatan  23252  cosatanne0  23253  atantan  23254  atanbndlem  23256  bndatandm  23260  atans2  23262  dvatan  23266  atantayl  23268  atantayl2  23269  atantayl3  23270  leibpilem1  23271  leibpilem2  23272  leibpi  23273  log2cnv  23275  log2tlbnd  23276  log2ublem3  23279  log2ub  23280  birthdaylem2  23282  birthday  23284  efrlim  23299  dfef2  23300  cvxcl  23314  scvxcvx  23315  emcllem2  23326  emcllem4  23328  emcllem7  23331  harmonicbnd4  23340  fsumharmonic  23341  wilthlem1  23342  wilthlem2  23343  wilthlem3  23344  basellem2  23355  basellem5  23358  basellem6  23359  basellem7  23360  basellem8  23361  basellem9  23362  0sgm  23418  mule1  23422  ppiprm  23425  ppinprm  23426  chtprm  23427  chtnprm  23428  chpp1  23429  mumullem2  23454  1sgmprm  23474  1sgm2ppw  23475  ppiublem2  23478  ppiub  23479  chtublem  23486  chtub  23487  logfaclbnd  23497  logfacbnd3  23498  logfacrlim  23499  logexprlim  23500  mersenne  23502  perfect1  23503  perfectlem1  23504  perfectlem2  23505  perfect  23506  dchrelbasd  23514  dchrmulid2  23527  dchrfi  23530  dchrsum2  23543  sumdchr2  23545  bcp1ctr  23554  bclbnd  23555  bposlem8  23566  lgslem1  23571  lgslem2  23572  lgsfcl2  23577  lgsvalmod  23590  lgsneg  23594  lgsdilem  23597  lgsdir2lem1  23598  lgsdir2lem2  23599  lgsdir2lem3  23600  lgsdir2lem5  23602  lgsdir2  23603  lgsdir  23605  lgsdi  23607  lgsne0  23608  lgseisenlem1  23624  lgseisenlem2  23625  lgseisen  23628  lgsquadlem1  23629  lgsquadlem2  23630  lgsquad2lem1  23633  lgsquad2  23635  m1lgs  23637  2sqlem10  23649  2sqlem11  23650  2sqblem  23652  chtppilimlem2  23659  chebbnd2  23662  chto1lb  23663  rplogsumlem1  23669  rpvmasumlem  23672  dchrmusumlema  23678  dchrmusum2  23679  dchrisum0flblem1  23693  rpvmasum2  23697  mudivsum  23715  mulogsum  23717  vmalogdivsum2  23723  selberg2lem  23735  logdivbnd  23741  pntrmax  23749  pntrsumo1  23750  pntrsumbnd2  23752  pntrlog2bndlem5  23766  pntpbnd1a  23770  pntpbnd2  23772  pntibndlem2  23776  pntlemd  23779  pntlemc  23780  pntlemr  23787  brbtwn2  24208  colinearalglem4  24212  ax5seglem1  24231  ax5seglem2  24232  ax5seglem3  24234  ax5seglem5  24236  ax5seglem7  24238  ax5seglem9  24240  axbtwnid  24242  axpaschlem  24243  axlowdimlem13  24257  axlowdimlem14  24258  axlowdimlem16  24260  axeuclidlem  24265  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  axcontlem8  24274  usgraexvlem  24395  wlklenvm1  24532  wlkiswwlk1  24690  wwlknext  24724  clwwlkf1  24796  wwlkext2clwwlk  24803  eupares  24975  eupap1  24976  eupath2lem3  24979  frghash2spot  25063  usgreghash2spotv  25066  extwwlkfablem2  25078  numclwwlkovf2ex  25086  numclwwlk6  25113  ex-fl  25168  ex-ind-dvds  25170  gxsuc  25274  gxnn0add  25276  gxnn0mul  25279  ablomul  25357  mulid  25358  cnrngo  25405  vc2  25448  vc0  25462  vcm  25464  vcoprne  25472  nvm1  25567  nvmtri  25574  nvge0  25577  ipval2lem3  25615  ipval2lem6  25621  ipidsq  25623  lnoadd  25673  ip1ilem  25741  ip1i  25742  ip2i  25743  ipdirilem  25744  ipasslem1  25746  ipasslem2  25747  ipasslem10  25754  minvecolem2  25791  hvsubid  25943  hv2times  25978  hisubcomi  26021  normlem9  26035  normlem7tALT  26036  norm-ii-i  26054  normsubi  26058  hhssnv  26180  pjhthlem1  26309  h1de2bi  26472  homulid2  26719  ho2times  26738  lnop0  26885  lnopaddi  26890  lnophmlem2  26936  lnfn0i  26961  lnfnaddi  26962  hst1h  27146  sto2i  27156  stadd3i  27167  addltmulALT  27365  isarchi3  27731  archirngz  27733  qqhval2lem  27962  logb1  28019  dya2ub  28241  eulerpartlemgs2  28319  fib5  28344  fib6  28345  ballotlem2  28427  sgnneg  28479  signswch  28518  signlem0  28544  zetacvg  28557  lgamcvg2  28597  lgam1  28606  gam1  28607  subfacp1lem5  28628  subfacp1lem6  28629  subfacval2  28631  subfaclim  28632  subfacval3  28633  cvxscon  28688  rescon  28691  cvmliftlem7  28736  cvmliftlem10  28739  problem4  29022  sinccvglem  29038  sqdivzi  29104  4bc3eq4  29111  halfthird  29113  5recm6rec  29114  risefaccl  29137  fallfaccl  29138  risefacfac  29157  binomfallfac  29163  faclimlem1  29168  predfz  29283  bpolycl  29814  bpolysum  29815  bpolydiflem  29816  fsumkthpow  29818  bpoly2  29819  bpoly3  29820  bpoly4  29821  fsumcube  29822  ltflcei  30043  sin2h  30045  cos2h  30046  tan2h  30047  mblfinlem2  30052  mblfinlem3  30053  0mbf  30060  dvtan  30065  itg2addnclem3  30068  dvcnsqrt  30101  dvasin  30103  dvacos  30104  areacirc  30112  fdc  30238  mettrifi  30250  heiborlem4  30310  heiborlem6  30312  eldioph2lem1  30693  lzenom  30703  irrapxlem1  30758  rmspecsqrtnq  30842  rmxm1  30870  rmym1  30871  2nn0ind  30881  jm2.24nn  30897  jm2.17a  30898  jm2.17b  30899  jm2.17c  30900  jm2.24  30901  acongeq  30921  jm2.18  30930  jm2.27c  30949  jm3.1lem2  30960  rngunsnply  31122  flcidc  31123  hashnzfzclim  31227  ofdivrec  31231  lhe4.4ex1a  31234  expgrowth  31240  dvradcnv2  31252  binomcxplemrat  31255  binomcxplemnotnn0  31261  fprodn0f  31594  fprodclf  31595  divcncf  31686  dvsinax  31708  dvnprodlem3  31745  itgsin0pilem1  31748  itgsbtaddcnst  31781  stoweidlem13  31795  stoweidlem26  31808  stoweidlem34  31816  stoweidlem38  31820  wallispilem2  31848  wallispilem4  31850  wallispi2lem1  31853  stirlinglem1  31856  stirlinglem5  31860  stirlinglem10  31865  dirkerper  31878  dirkertrigeqlem1  31880  dirkertrigeqlem3  31882  dirkertrigeq  31883  dirkercncflem4  31888  fourierdlem24  31913  sqwvfoura  32011  sqwvfourb  32012  fourierswlem  32013  0nodd  32498  altgsumbcALT  32942  exple2lt6  32957  onetansqsecsq  33155  cotsqcscsq  33156  5m4e1  33212  isosctrlem1ALT  33734  inductionexd  37967  unitadd  38016
  Copyright terms: Public domain W3C validator