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

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 9975 . 2 class 1
2 cc 9972 . 2 class
31, 2wcel 2030 1 wff 1 ∈ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  10070  1ex  10073  mulid1  10075  mulid2  10076  1re  10077  1cnd  10094  muladd11  10244  peano2cn  10246  mul02lem2  10251  addid1  10254  cnegex2  10256  peano2cnm  10385  0reALT  10416  ine0  10503  mulm1  10509  0lt1  10588  ixi  10694  muleqadd  10709  reccl  10730  recne0  10736  recid  10737  recid2  10738  div1  10754  1div1e1  10755  diveq1  10756  recdiv  10769  divdiv1  10774  divdiv2  10775  recdiv2  10776  conjmul  10780  eqneg  10783  div2neg  10786  recp1lt1  10959  recreclt  10960  recgt0ii  10967  inelr  11048  ofnegsub  11056  peano5nni  11061  nn1m1nn  11078  nn1suc  11079  nnaddcl  11080  nnmulcl  11081  nnsub  11097  1m1e0  11127  neg1cn  11162  neg1ne0  11164  negneg1e1  11166  1pneg1e0  11167  1m0e1  11169  0p1e1  11170  1p0e1  11171  2m1e1  11173  3m1e2  11175  4m1e3  11176  5m1e4  11177  6m1e5  11178  7m1e6  11179  8m1e7  11180  9m1e8  11181  2p2e4  11182  1p2e3  11190  3p2e5  11198  3p3e6  11199  4p2e6  11200  4p3e7  11201  4p4e8  11202  5p2e7  11203  5p3e8  11204  5p4e9  11205  5p5e10OLD  11206  6p2e8  11207  6p3e9  11208  6p4e10OLD  11209  7p2e9  11210  7p3e10OLD  11211  8p2e10OLD  11212  1t1e1  11213  3t3e9  11218  neg1mulneg1e1  11283  1mhlfehlf  11289  8th4div3  11290  halfpm6th  11291  addltmul  11306  elnn0nn  11373  elz2  11432  zlem1lt  11467  zltlem1  11468  nnaddm1cl  11472  zextlt  11489  zeo  11501  peano5uzi  11504  numsuc  11549  numltc  11566  numsucc  11587  numaddc  11599  6p5lem  11633  5p5e10  11634  6p4e10  11636  7p3e10  11641  8p2e10  11648  10m1e9  11668  4t3lem  11669  7t4e28  11688  9t11e99  11709  9t11e99OLD  11710  decbin2  11721  halfthird  11723  5recm6rec  11724  uzp1  11759  peano2uzr  11781  uzaddcl  11782  rebtwnz  11825  qbtwnre  12068  iccf1o  12354  fz01en  12407  fztp  12435  fzsuc2  12436  fztpval  12440  fseq1m1p1  12453  elfzp1b  12455  fz0to4untppr  12481  predfz  12503  fzoss2  12535  fzval3  12576  fzosplitsnm1  12582  fzo0to42pr  12595  fzo1to4tp  12596  fldiv4p1lem1div2  12676  ceim1l  12686  fldiv  12699  uzrdgxfr  12806  fzen2  12808  nn0ennn  12818  seqm1  12858  seqshft2  12867  monoord2  12872  sermono  12873  seqf1olem1  12880  seqf1olem2  12881  seqz  12889  ser1const  12897  expcl  12918  m1expcl2  12922  expclzlem  12924  expm1t  12928  1exp  12929  mulexpz  12940  expadd  12942  expaddz  12944  expmul  12945  expubnd  12961  sqrecii  12986  neg1sqe1  12999  irec  13004  i4  13007  binom21  13020  sq01  13026  crreczi  13029  bernneq  13030  bernneq2  13031  nn0opthlem1  13095  facndiv  13115  faclbnd4lem1  13120  faclbnd6  13126  bcnp1n  13141  bcm1k  13142  bcp1nk  13144  bcn2  13146  bcp1m1  13147  bcpasc  13148  4bc3eq4  13155  hashgadd  13204  hashfz  13252  hashfzo  13254  hashxplem  13258  hashbclem  13274  hashf1  13279  seqcoll  13286  swrds1  13497  swrdlsw  13498  wrdind  13522  wrd2ind  13523  swrds2  13731  relexpaddg  13837  rei  13940  imi  13941  recan  14120  iserex  14431  isercoll2  14443  serf0  14455  iseraltlem2  14457  iseraltlem3  14458  iseralt  14459  sumrblem  14486  fsumm1  14524  fsump1  14531  telfsumo  14578  fsumparts  14582  hashiun  14598  binomlem  14605  binom  14606  binom1p  14607  binom11  14608  binom1dif  14609  bcxmas  14611  isumsplit  14616  isum1p  14617  climcndslem1  14625  supcvg  14632  harmonic  14635  arisum  14636  arisum2  14637  trireciplem  14638  geoserg  14642  geolim  14645  geolim2  14646  georeclim  14647  geo2sum  14648  geo2sum2  14649  geoisum1c  14655  0.999...  14656  0.999...OLD  14657  geoihalfsum  14658  cvgrat  14659  mertenslem1  14660  mertenslem2  14661  mertens  14662  prodf1  14667  prodfclim1  14669  prodrblem  14703  fprodcvg  14704  prodmolem2a  14708  zprod  14711  fprodntriv  14716  prodss  14721  fprodss  14722  fprodsplit  14740  fprodn0f  14766  fprodclf  14767  risefaccl  14790  fallfaccl  14791  risefacfac  14810  binomfallfac  14816  bpolycl  14827  bpolysum  14828  bpolydiflem  14829  fsumkthpow  14831  bpoly2  14832  bpoly3  14833  bpoly4  14834  fsumcube  14835  esum  14855  ege2le3  14864  efsub  14874  efexp  14875  efzval  14876  eftlub  14883  effsumlt  14885  ef4p  14887  tanval3  14908  efi4p  14911  tan0  14925  efival  14926  tanadd  14941  cos2t  14952  cos2tsin  14953  ef01bndlem  14958  cos1bnd  14961  cos2bnd  14962  demoivreALT  14975  eirrlem  14976  rpnnen2lem3  14989  rpnnen2lem11  14997  ruclem12  15014  3dvds  15099  3dvdsOLD  15100  3dvdsdec  15101  3dvdsdecOLD  15102  3dvds2dec  15103  3dvds2decOLD  15104  odd2np1lem  15111  odd2np1  15112  opoe  15134  omoe  15135  opeo  15136  omeo  15137  m1exp1  15140  n2dvdsm1  15152  flodddiv4  15184  bitsfzo  15204  gcdmultiple  15316  sqgcd  15325  nn0seqcvgd  15330  prmind2  15445  hashdvds  15527  phiprmpw  15528  phiprm  15529  eulerthlem2  15534  iserodd  15587  sumhash  15647  fldivp1  15648  prmpwdvds  15655  pockthlem  15656  pockthi  15658  prmreclem4  15670  prmreclem6  15672  4sqlem11  15706  4sqlem19  15714  vdwapun  15725  vdwapid1  15726  vdwlem3  15734  vdwlem5  15736  vdwlem6  15737  vdwlem8  15739  vdwlem9  15740  vdwnnlem2  15747  ramub1lem1  15777  ramub1lem2  15778  ramcl  15780  prmo1  15788  dec5nprm  15817  decexp2  15826  prmlem0  15859  43prm  15876  83prm  15877  139prm  15878  163prm  15879  317prm  15880  631prm  15881  prmo4  15882  prmo5  15883  prmo6  15884  1259lem2  15886  1259lem3  15887  1259lem4  15888  1259lem5  15889  1259prm  15890  2503lem1  15891  2503lem2  15892  2503lem3  15893  2503prm  15894  4001lem1  15895  4001lem2  15896  4001lem3  15897  4001lem4  15898  4001prm  15899  gsumccat  17425  mulgnndir  17616  mulgnndirOLD  17617  mulgneg2  17622  m1expaddsub  17964  sylow1lem1  18059  sylow2a  18080  efgsval2  18192  efgsrel  18193  efgsres  18197  cnfld1  19819  zsssubrg  19852  cnmgpid  19856  zringcyg  19887  mulgrhm2  19895  cnmsgnsubg  19971  cnmsgnbas  19972  cnmsgngrp  19973  psgninv  19976  evpmodpmf1o  19990  blcvx  22648  iihalf2  22779  icopnfcnv  22788  iccpnfhmeo  22791  xrhmeo  22792  icccvx  22796  lebnumii  22812  reparphti  22843  pcoass  22870  pcorevlem  22872  pcorev2  22874  pi1xfrcnv  22903  cnstrcvs  22987  cncvs  22991  ncvsm1  23000  pjthlem1  23254  divcncf  23262  ovolunlem1a  23310  ovolunlem1  23311  ovolicc2lem4  23334  uniioombllem3  23399  uniioombllem4  23400  dyadovol  23407  vitalilem4  23425  iblitg  23580  iblcnlem1  23599  itgcnlem  23601  dvid  23726  dvexp  23761  dvexp2  23762  dvexp3  23786  dveflem  23787  dvef  23788  dvlipcn  23802  dvcvx  23828  dvfsumle  23829  dvfsumlem1  23834  degltp1le  23878  ply1divex  23941  fta1glem1  23970  plyaddlem1  24014  plymullem1  24015  coeidp  24064  dgrid  24065  dvply1  24084  dvply2g  24085  plyremlem  24104  fta1lem  24107  vieta1lem1  24110  vieta1lem2  24111  qaa  24123  iaa  24125  aalioulem3  24134  geolim3  24139  aaliou3lem2  24143  aaliou3lem7  24149  taylply2  24167  dvradcnv  24220  pserdvlem2  24227  pserdv2  24229  abelthlem1  24230  abelthlem2  24231  abelthlem6  24235  abelthlem7  24237  abelth  24240  reeff1olem  24245  reeff1o  24246  efcvx  24248  sinhalfpilem  24260  eulerid  24271  cos2pi  24273  sincosq3sgn  24297  sincosq4sgn  24298  tangtx  24302  sincos4thpi  24310  sincos6thpi  24312  pige3  24314  abssinper  24315  coskpi  24317  coseq1  24319  efeq1  24320  tanregt0  24330  logneg2  24406  logdivlti  24411  logcnlem4  24436  dvlog2lem  24443  dvlog2  24444  advlog  24445  advlogexp  24446  logtayl  24451  logtayl2  24453  logccv  24454  cxpval  24455  1cxp  24463  cxpcl  24465  cxpp1  24471  cxpsqrt  24494  dvsqrt  24528  dvcnsqrt  24530  sqrtcn  24536  cxpaddlelem  24537  root1id  24540  root1cj  24542  logrec  24546  logb1  24552  logbmpt  24571  ang180lem1  24584  ang180lem2  24585  ang180lem3  24586  isosctrlem1  24593  isosctrlem2  24594  1cubrlem  24613  1cubr  24614  mcubic  24619  binom4  24622  dquartlem1  24623  quartlem1  24629  asinlem  24640  asinlem2  24641  asinlem3a  24642  asinlem3  24643  asinf  24644  atandm2  24649  atandm4  24651  atanf  24652  asinneg  24658  efiasin  24660  sinasin  24661  asinsin  24664  asin1  24666  acos1  24667  reasinsin  24668  asinbnd  24671  cosasin  24676  atanneg  24679  atancj  24682  efiatan  24684  atanlogaddlem  24685  atanlogadd  24686  atanlogsublem  24687  atanlogsub  24688  efiatan2  24689  2efiatan  24690  tanatan  24691  cosatan  24693  cosatanne0  24694  atantan  24695  atanbndlem  24697  bndatandm  24701  atans2  24703  dvatan  24707  atantayl  24709  atantayl2  24710  atantayl3  24711  leibpilem1  24712  leibpilem2  24713  leibpi  24714  log2cnv  24716  log2tlbnd  24717  log2ublem3  24720  log2ub  24721  birthdaylem2  24724  birthday  24726  efrlim  24741  dfef2  24742  cvxcl  24756  scvxcvx  24757  emcllem2  24768  emcllem4  24770  emcllem7  24773  harmonicbnd4  24782  fsumharmonic  24783  zetacvg  24786  lgamcvg2  24826  lgam1  24835  gam1  24836  wilthlem1  24839  wilthlem2  24840  wilthlem3  24841  basellem2  24853  basellem5  24856  basellem6  24857  basellem7  24858  basellem8  24859  basellem9  24860  0sgm  24915  mule1  24919  ppiprm  24922  ppinprm  24923  chtprm  24924  chtnprm  24925  chpp1  24926  mumullem2  24951  1sgmprm  24969  1sgm2ppw  24970  ppiublem2  24973  ppiub  24974  chtublem  24981  chtub  24982  logfaclbnd  24992  logfacbnd3  24993  logfacrlim  24994  logexprlim  24995  mersenne  24997  perfect1  24998  perfectlem1  24999  perfectlem2  25000  perfect  25001  dchrelbasd  25009  dchrmulid2  25022  dchrfi  25025  dchrsum2  25038  sumdchr2  25040  bcp1ctr  25049  bposlem8  25061  zabsle1  25066  lgslem1  25067  lgslem2  25068  lgsfcl2  25073  lgsvalmod  25086  lgsneg  25091  lgsdilem  25094  lgsdir2lem1  25095  lgsdir2lem2  25096  lgsdir2lem3  25097  lgsdir2lem5  25099  lgsdir2  25100  lgsdir  25102  lgsdi  25104  lgsne0  25105  lgseisenlem1  25145  lgseisenlem2  25146  lgseisen  25149  lgsquadlem1  25150  lgsquadlem2  25151  lgsquad2lem1  25154  lgsquad2  25156  m1lgs  25158  2lgslem3c  25168  2lgsoddprmlem3b  25181  2lgsoddprmlem3c  25182  2lgsoddprmlem3d  25183  2sqlem10  25198  2sqlem11  25199  2sqblem  25201  chtppilimlem2  25208  chebbnd2  25211  chto1lb  25212  rplogsumlem1  25218  rpvmasumlem  25221  dchrmusumlema  25227  dchrmusum2  25228  dchrisum0flblem1  25242  rpvmasum2  25246  mudivsum  25264  mulogsum  25266  vmalogdivsum2  25272  selberg2lem  25284  logdivbnd  25290  pntrmax  25298  pntrsumo1  25299  pntrsumbnd2  25301  pntrlog2bndlem5  25315  pntpbnd1a  25319  pntpbnd2  25321  pntibndlem2  25325  pntlemd  25328  pntlemc  25329  pntlemr  25336  brbtwn2  25830  colinearalglem4  25834  ax5seglem1  25853  ax5seglem2  25854  ax5seglem3  25856  ax5seglem5  25858  ax5seglem7  25860  ax5seglem9  25862  axbtwnid  25864  axpaschlem  25865  axlowdimlem13  25879  axlowdimlem14  25880  axlowdimlem16  25882  axeuclidlem  25887  axcontlem2  25890  axcontlem4  25892  axcontlem7  25895  axcontlem8  25896  crctcshwlkn0lem6  26763  wwlksnext  26856  clwwlkf1  27012  wwlksext2clwwlkOLD  27022  clwwlknonex2lem2  27083  ex-fl  27434  ex-ind-dvds  27448  vc2OLD  27551  vc0  27557  vcm  27559  nvm1  27648  nvmtri  27654  nvge0  27656  ipval2lem3  27688  ipidsq  27693  lnoadd  27741  ip1ilem  27809  ip1i  27810  ip2i  27811  ipdirilem  27812  ipasslem1  27814  ipasslem2  27815  ipasslem10  27822  minvecolem2  27859  hvsubid  28011  hv2times  28046  hisubcomi  28089  normlem9  28103  normlem7tALT  28104  norm-ii-i  28122  normsubi  28126  hhssnv  28249  pjhthlem1  28378  h1de2bi  28541  homulid2  28787  ho2times  28806  lnop0  28953  lnopaddi  28958  lnophmlem2  29004  lnfn0i  29029  lnfnaddi  29030  hst1h  29214  sto2i  29224  stadd3i  29235  addltmulALT  29433  dpmul4  29750  isarchi3  29869  archirngz  29871  psgnid  29975  lmatfvlem  30009  qqhval2lem  30153  dya2ub  30460  omssubadd  30490  eulerpartlemgs2  30570  fib5  30595  fib6  30596  ballotlem2  30678  sgnneg  30730  signswch  30766  signlem0  30792  itgexpif  30812  reprlt  30825  breprexp  30839  breprexpnat  30840  hgt750lem2  30858  subfacp1lem5  31292  subfacp1lem6  31293  subfacval2  31295  subfaclim  31296  subfacval3  31297  cvxsconn  31351  resconn  31354  cvmliftlem7  31399  cvmliftlem10  31402  problem4  31688  sinccvglem  31692  sqdivzi  31736  faclimlem1  31755  dnibndlem5  32597  dnibndlem10  32602  ltflcei  33527  sin2h  33529  cos2h  33530  tan2h  33531  pigt3  33532  poimirlem13  33552  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem31  33570  mblfinlem2  33577  mblfinlem3  33578  0mbf  33585  dvtan  33590  itg2addnclem3  33593  dvasin  33626  dvacos  33627  areacirc  33635  fdc  33671  mettrifi  33683  heiborlem4  33743  heiborlem6  33745  eldioph2lem1  37640  lzenom  37650  irrapxlem1  37703  rmspecsqrtnq  37787  rmspecsqrtnqOLD  37788  rmxm1  37816  rmym1  37817  2nn0ind  37827  jm2.24nn  37843  jm2.17a  37844  jm2.17b  37845  jm2.17c  37846  jm2.24  37847  acongeq  37867  jm2.18  37872  jm2.27c  37891  jm3.1lem2  37902  rngunsnply  38060  flcidc  38061  inductionexd  38770  unitadd  38815  hashnzfzclim  38838  ofdivrec  38842  lhe4.4ex1a  38845  expgrowth  38851  dvradcnv2  38863  binomcxplemrat  38866  binomcxplemnotnn0  38872  isosctrlem1ALT  39484  monoord2xrv  40027  dvsinax  40445  dvnprodlem3  40481  itgsin0pilem1  40483  itgsbtaddcnst  40516  stoweidlem13  40548  stoweidlem26  40561  stoweidlem34  40569  stoweidlem38  40573  wallispilem2  40601  wallispilem4  40603  wallispi2lem1  40606  stirlinglem1  40609  stirlinglem5  40613  stirlinglem10  40618  dirkerper  40631  dirkertrigeqlem1  40633  dirkertrigeqlem3  40635  dirkertrigeq  40636  dirkercncflem4  40641  fourierdlem24  40666  sqwvfoura  40763  sqwvfourb  40764  fourierswlem  40765  1t10e1p1e11  41644  1t10e1p1e11OLD  41645  fmtnorec3  41785  fmtno5lem4  41793  fmtno5  41794  257prm  41798  fmtno4nprmfac193  41811  m3prm  41831  139prmALT  41836  127prm  41840  m7prm  41841  lighneallem3  41849  proththd  41856  3exp4mod41  41858  41prothprmlem2  41860  perfectALTVlem2  41956  perfectALTV  41957  evengpop3  42011  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  bgoldbtbndlem1  42018  0nodd  42135  altgsumbcALT  42456  exple2lt6  42470  nn0sumshdiglemB  42739  onetansqsecsq  42830  cotsqcscsq  42831  5m4e1  42871
  Copyright terms: Public domain W3C validator