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

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 10527 . 2 class 1
2 cc 10524 . 2 class
31, 2wcel 2105 1 wff 1 ∈ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  10622  1cnd  10625  1ex  10626  mulid1  10628  mulid2  10629  1re  10630  0re  10632  muladd11  10799  peano2cn  10801  mul02lem2  10806  addid1  10809  cnegex2  10811  peano2cnm  10941  0reALT  10972  ine0  11064  mulm1  11070  0lt1  11151  ixi  11258  muleqadd  11273  reccl  11294  recne0  11300  recid  11301  recid2  11302  div1  11318  1div1e1  11319  diveq1  11320  recdiv  11335  divdiv1  11340  divdiv2  11341  recdiv2  11342  conjmul  11346  eqneg  11349  div2neg  11352  recp1lt1  11527  recreclt  11528  recgt0ii  11535  inelr  11617  ofnegsub  11625  peano5nni  11630  nnsscn  11632  nn1m1nn  11647  nn1suc  11648  nnaddcl  11649  nnmulcl  11650  nnne0  11660  nnsub  11670  1m1e0  11698  2cn  11701  3cn  11707  4cn  11711  5cn  11714  6cn  11717  7cn  11720  8cn  11723  9cn  11726  neg1cn  11740  neg1ne0  11742  negneg1e1  11744  1pneg1e0  11745  1m0e1  11747  0p1e1  11748  1p0e1  11750  2m1e1  11752  3m1e2  11754  4m1e3  11755  5m1e4  11756  6m1e5  11757  7m1e6  11758  8m1e7  11759  9m1e8  11760  2p2e4  11761  1p2e3  11769  1p2e3ALT  11770  3p2e5  11777  3p3e6  11778  4p2e6  11779  4p3e7  11780  4p4e8  11781  5p2e7  11782  5p3e8  11783  5p4e9  11784  6p2e8  11785  6p3e9  11786  7p2e9  11787  1t1e1  11788  3t3e9  11793  neg1mulneg1e1  11839  1mhlfehlf  11845  8th4div3  11846  halfpm6th  11847  addltmul  11862  elnn0nn  11928  elz2  11988  zlem1lt  12023  zltlem1  12024  nnaddm1cl  12028  zextlt  12045  zeo  12057  peano5uzi  12060  numsuc  12101  numltc  12113  numsucc  12127  numaddc  12135  6p5lem  12157  5p5e10  12158  6p4e10  12159  7p3e10  12162  8p2e10  12167  10m1e9  12183  4t3lem  12184  7t4e28  12198  9t11e99  12217  decbin2  12228  halfthird  12230  5recm6rec  12231  uzp1  12268  peano2uzr  12292  uzaddcl  12293  rebtwnz  12336  qbtwnre  12582  iccf1o  12872  fz01en  12925  fztp  12953  fzsuc2  12955  fztpval  12959  fseq1m1p1  12972  elfzp1b  12974  fz0to4untppr  13000  predfz  13022  fzoss2  13055  fzval3  13096  fzosplitsnm1  13102  fzo1to4tp  13115  fldiv4p1lem1div2  13195  ceim1l  13205  fldiv  13218  uzrdgxfr  13325  fzen2  13327  nn0ennn  13337  seqm1  13377  seqshft2  13386  monoord2  13391  sermono  13392  seqf1olem1  13399  seqf1olem2  13400  seqz  13408  ser1const  13416  expcl  13437  m1expcl2  13441  expclzlem  13443  expm1t  13447  1exp  13448  mulexpz  13459  expadd  13461  expaddz  13463  expmul  13464  expubnd  13531  sqrecii  13536  neg1sqe1  13549  irec  13554  i4  13557  binom21  13570  sq01  13576  crreczi  13579  bernneq  13580  bernneq2  13581  nn0opthlem1  13618  facndiv  13638  faclbnd4lem1  13643  faclbnd6  13649  bcnp1n  13664  bcm1k  13665  bcp1nk  13667  bcn2  13669  bcp1m1  13670  bcpasc  13671  hashgadd  13728  hashfz  13778  hashfzo  13780  hashxplem  13784  hashbclem  13800  hashf1  13805  seqcoll  13812  swrds1  14018  swrdlsw  14019  wrdind  14074  wrd2ind  14075  swrds2  14292  relexpaddg  14402  rei  14505  imi  14506  recan  14686  iserex  15003  isercoll2  15015  serf0  15027  iseraltlem2  15029  iseraltlem3  15030  iseralt  15031  sumrblem  15058  fsumm1  15096  fsump1  15101  telfsumo  15147  fsumparts  15151  hashiun  15167  binomlem  15174  binom  15175  binom1p  15176  binom11  15177  binom1dif  15178  bcxmas  15180  isumsplit  15185  isum1p  15186  climcndslem1  15194  supcvg  15201  harmonic  15204  arisum  15205  arisum2  15206  trireciplem  15207  geoserg  15211  geolim  15216  geolim2  15217  georeclim  15218  geo2sum  15219  geo2sum2  15220  geoisum1c  15226  0.999...  15227  geoihalfsum  15228  cvgrat  15229  mertenslem1  15230  mertenslem2  15231  mertens  15232  prodf1  15237  prodfclim1  15239  prodrblem  15273  fprodcvg  15274  prodmolem2a  15278  zprod  15281  fprodntriv  15286  prodss  15291  fprodss  15292  fprodsplit  15310  fprodn0f  15335  risefaccl  15359  fallfaccl  15360  risefacfac  15379  binomfallfac  15385  bpolycl  15396  bpolysum  15397  bpolydiflem  15398  fsumkthpow  15400  bpoly2  15401  bpoly3  15402  bpoly4  15403  fsumcube  15404  esum  15424  ege2le3  15433  efsub  15443  efexp  15444  efzval  15445  eftlub  15452  effsumlt  15454  ef4p  15456  tanval3  15477  efi4p  15480  tan0  15494  efival  15495  tanadd  15510  cos2t  15521  cos2tsin  15522  ef01bndlem  15527  cos1bnd  15530  cos2bnd  15531  demoivreALT  15544  eirrlem  15547  rpnnen2lem3  15559  rpnnen2lem11  15567  ruclem12  15584  3dvds  15670  3dvdsdec  15671  3dvds2dec  15672  odd2np1lem  15679  odd2np1  15680  opoe  15702  omoe  15703  opeo  15704  omeo  15705  n2dvdsm1  15709  m1exp1  15717  flodddiv4  15754  bitsfzo  15774  gcdmultipleOLD  15890  sqgcd  15899  nn0seqcvgd  15904  prmind2  16019  hashdvds  16102  phiprmpw  16103  phiprm  16104  eulerthlem2  16109  iserodd  16162  sumhash  16222  fldivp1  16223  prmpwdvds  16230  pockthlem  16231  pockthi  16233  prmreclem4  16245  prmreclem6  16247  4sqlem11  16281  4sqlem19  16289  vdwapun  16300  vdwapid1  16301  vdwlem3  16309  vdwlem5  16311  vdwlem6  16312  vdwlem8  16314  vdwlem9  16315  vdwnnlem2  16322  ramub1lem1  16352  ramub1lem2  16353  ramcl  16355  prmo1  16363  dec5nprm  16392  decexp2  16401  prmlem0  16429  43prm  16445  83prm  16446  139prm  16447  163prm  16448  317prm  16449  631prm  16450  1259lem2  16455  1259lem3  16456  1259lem4  16457  1259lem5  16458  1259prm  16459  2503lem1  16460  2503lem2  16461  2503lem3  16462  2503prm  16463  4001lem1  16464  4001lem2  16465  4001lem3  16466  4001lem4  16467  4001prm  16468  gsumsgrpccat  17994  gsumccatOLD  17995  mulgnndir  18196  mulgneg2  18201  m1expaddsub  18557  sylow1lem1  18654  sylow2a  18675  efgsval2  18790  efgsrel  18791  efgsres  18795  cnfld1  20500  zsssubrg  20533  cnmgpid  20537  zringcyg  20568  mulgrhm2  20576  cnmsgnsubg  20651  cnmsgnbas  20652  cnmsgngrp  20653  psgninv  20656  evpmodpmf1o  20670  blcvx  23335  iihalf2  23466  icopnfcnv  23475  iccpnfhmeo  23478  xrhmeo  23479  icccvx  23483  lebnumii  23499  reparphti  23530  pcoass  23557  pcorevlem  23559  pcorev2  23561  pi1xfrcnv  23590  cnstrcvs  23674  cncvs  23678  ncvsm1  23687  pjthlem1  23969  divcncf  23977  ovolunlem1a  24026  ovolunlem1  24027  ovolicc2lem4  24050  uniioombllem3  24115  uniioombllem4  24116  dyadovol  24123  vitalilem4  24141  mbf0  24164  iblcnlem1  24317  itgcnlem  24319  dvid  24444  dvexp  24479  dvexp2  24480  dvexp3  24504  dveflem  24505  dvlipcn  24520  dvcvx  24546  dvfsumle  24547  dvfsumlem1  24552  degltp1le  24596  ply1divex  24659  fta1glem1  24688  plyaddlem1  24732  plymullem1  24733  coeidp  24782  dgrid  24783  dvply1  24802  dvply2g  24803  plyremlem  24822  fta1lem  24825  vieta1lem1  24828  vieta1lem2  24829  qaa  24841  iaa  24843  aalioulem3  24852  geolim3  24857  aaliou3lem2  24861  aaliou3lem7  24867  taylply2  24885  dvradcnv  24938  pserdvlem2  24945  pserdv2  24947  abelthlem1  24948  abelthlem2  24949  abelthlem6  24953  abelthlem7  24955  abelth  24958  reeff1olem  24963  reeff1o  24964  efcvx  24966  sinhalfpilem  24978  eulerid  24989  cos2pi  24991  sincosq3sgn  25015  sincosq4sgn  25016  tangtx  25020  sincos4thpi  25028  sincos6thpi  25030  pigt3  25032  pige3ALT  25034  abssinper  25035  coskpi  25037  coseq1  25039  efeq1  25040  tanregt0  25050  logneg2  25125  logdivlti  25130  logcnlem4  25155  dvlog2lem  25162  dvlog2  25163  advlog  25164  advlogexp  25165  logtayl  25170  logtayl2  25172  logccv  25173  cxpval  25174  1cxp  25182  cxpcl  25184  cxpp1  25190  cxpsqrt  25213  dvsqrt  25250  dvcnsqrt  25252  sqrtcn  25258  cxpaddlelem  25259  root1id  25262  root1cj  25264  logrec  25268  logb1  25274  logbmpt  25293  ang180lem1  25314  ang180lem2  25315  ang180lem3  25316  isosctrlem1  25323  isosctrlem2  25324  1cubrlem  25346  1cubr  25347  mcubic  25352  binom4  25355  dquartlem1  25356  quartlem1  25362  asinlem  25373  asinlem2  25374  asinlem3a  25375  asinlem3  25376  asinf  25377  atandm2  25382  atandm4  25384  atanf  25385  asinneg  25391  efiasin  25393  sinasin  25394  asinsin  25397  asin1  25399  acos1  25400  reasinsin  25401  asinbnd  25404  cosasin  25409  atanneg  25412  atancj  25415  efiatan  25417  atanlogaddlem  25418  atanlogadd  25419  atanlogsublem  25420  atanlogsub  25421  efiatan2  25422  2efiatan  25423  tanatan  25424  cosatan  25426  cosatanne0  25427  atantan  25428  atanbndlem  25430  bndatandm  25434  atans2  25436  dvatan  25440  atantayl  25442  atantayl2  25443  atantayl3  25444  leibpilem1OLD  25446  leibpilem2  25447  leibpi  25448  log2cnv  25450  log2tlbnd  25451  log2ublem3  25454  log2ub  25455  birthdaylem2  25458  birthday  25460  efrlim  25475  dfef2  25476  cvxcl  25490  scvxcvx  25491  emcllem2  25502  emcllem4  25504  emcllem7  25507  harmonicbnd4  25516  fsumharmonic  25517  zetacvg  25520  lgamcvg2  25560  lgam1  25569  gam1  25570  wilthlem1  25573  wilthlem2  25574  wilthlem3  25575  basellem2  25587  basellem5  25590  basellem6  25591  basellem7  25592  basellem8  25593  basellem9  25594  0sgm  25649  mule1  25653  ppiprm  25656  ppinprm  25657  chtprm  25658  chtnprm  25659  chpp1  25660  mumullem2  25685  1sgmprm  25703  1sgm2ppw  25704  ppiub  25708  chtublem  25715  chtub  25716  logfaclbnd  25726  logfacbnd3  25727  logfacrlim  25728  logexprlim  25729  mersenne  25731  perfect1  25732  perfectlem1  25733  perfectlem2  25734  perfect  25735  dchrelbasd  25743  dchrmulid2  25756  dchrfi  25759  dchrsum2  25772  sumdchr2  25774  bcp1ctr  25783  bposlem8  25795  zabsle1  25800  lgslem1  25801  lgslem2  25802  lgsfcl2  25807  lgsvalmod  25820  lgsneg  25825  lgsdilem  25828  lgsdir2lem1  25829  lgsdir2lem2  25830  lgsdir2lem3  25831  lgsdir2lem5  25833  lgsdir2  25834  lgsdir  25836  lgsdi  25838  lgsne0  25839  lgseisenlem1  25879  lgseisenlem2  25880  lgseisen  25883  lgsquadlem1  25884  lgsquadlem2  25885  lgsquad2lem1  25888  lgsquad2  25890  m1lgs  25892  2lgslem3c  25902  2lgsoddprmlem3c  25916  2lgsoddprmlem3d  25917  2sqlem10  25932  2sqlem11  25933  2sqblem  25935  addsqn2reu  25945  addsqrexnreu  25946  addsqnreup  25947  chtppilimlem2  25978  chebbnd2  25981  chto1lb  25982  rplogsumlem1  25988  rpvmasumlem  25991  dchrmusumlema  25997  dchrmusum2  25998  dchrisum0flblem1  26012  rpvmasum2  26016  mudivsum  26034  mulogsum  26036  vmalogdivsum2  26042  selberg2lem  26054  logdivbnd  26060  pntrmax  26068  pntrsumo1  26069  pntrsumbnd2  26071  pntrlog2bndlem5  26085  pntpbnd1a  26089  pntpbnd2  26091  pntibndlem2  26095  pntlemd  26098  pntlemc  26099  pntlemr  26106  brbtwn2  26619  colinearalglem4  26623  ax5seglem1  26642  ax5seglem2  26643  ax5seglem3  26645  ax5seglem5  26647  ax5seglem7  26649  ax5seglem9  26651  axbtwnid  26653  axpaschlem  26654  axlowdimlem13  26668  axlowdimlem14  26669  axlowdimlem16  26671  axeuclidlem  26676  axcontlem2  26679  axcontlem4  26681  axcontlem7  26684  axcontlem8  26685  crctcshwlkn0lem6  27521  clwwlkf1  27756  clwwlknonex2lem2  27815  ex-fl  28154  ex-ind-dvds  28168  vc2OLD  28273  vc0  28279  vcm  28281  nvm1  28370  nvmtri  28376  nvge0  28378  ipval2lem3  28410  ipidsq  28415  lnoadd  28463  ip1ilem  28531  ip1i  28532  ip2i  28533  ipdirilem  28534  ipasslem1  28536  ipasslem2  28537  ipasslem10  28544  minvecolem2  28580  hvsubid  28731  hv2times  28766  hisubcomi  28809  normlem9  28823  normlem7tALT  28824  norm-ii-i  28842  normsubi  28846  hhssnv  28969  pjhthlem1  29096  h1de2bi  29259  homulid2  29505  ho2times  29524  lnop0  29671  lnopaddi  29676  lnophmlem2  29722  lnfn0i  29747  lnfnaddi  29748  hst1h  29932  sto2i  29942  stadd3i  29953  addltmulALT  30151  dpmul4  30518  psgnid  30667  cnmsgn0g  30716  altgnsg  30719  isarchi3  30744  archirngz  30746  ccfldextdgrr  30957  lmatfvlem  30980  qqhval2lem  31122  dya2ub  31428  omssubadd  31458  eulerpartlemgs2  31538  fib5  31563  fib6  31564  ballotlem2  31646  sgnneg  31698  signswch  31731  signlem0  31757  itgexpif  31777  reprlt  31790  breprexp  31804  breprexpnat  31805  hgt750lem2  31823  subfacp1lem5  32329  subfacp1lem6  32330  subfacval2  32332  subfaclim  32333  subfacval3  32334  cvxsconn  32388  resconn  32391  cvmliftlem7  32436  cvmliftlem10  32439  problem4  32809  sinccvglem  32813  sqdivzi  32857  faclimlem1  32873  dnibndlem5  33719  dnibndlem10  33724  ltflcei  34762  sin2h  34764  cos2h  34765  tan2h  34766  poimirlem13  34787  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem31  34805  mblfinlem2  34812  mblfinlem3  34813  dvtan  34824  itg2addnclem3  34827  dvasin  34860  dvacos  34861  areacirc  34869  fdc  34903  mettrifi  34915  heiborlem4  34975  heiborlem6  34977  sn-1ne2  39038  sqdeccom12  39055  235t711  39057  expgcd  39063  re1m1e0m0  39107  fltnltalem  39154  3cubeslem3l  39163  3cubeslem3r  39164  eldioph2lem1  39237  lzenom  39247  irrapxlem1  39299  rmspecsqrtnq  39383  rmxm1  39411  rmym1  39412  2nn0ind  39422  jm2.24nn  39436  jm2.17a  39437  jm2.17b  39438  jm2.17c  39439  jm2.24  39440  acongeq  39460  jm2.18  39465  jm2.27c  39484  jm3.1lem2  39495  rngunsnply  39653  flcidc  39654  inductionexd  40385  unitadd  40429  hashnzfzclim  40534  ofdivrec  40538  lhe4.4ex1a  40541  expgrowth  40547  dvradcnv2  40559  binomcxplemrat  40562  binomcxplemnotnn0  40568  isosctrlem1ALT  41148  monoord2xrv  41640  dvsinax  42077  dvnprodlem3  42113  itgsin0pilem1  42115  itgsbtaddcnst  42147  stoweidlem13  42179  stoweidlem26  42192  stoweidlem34  42200  stoweidlem38  42204  wallispilem2  42232  wallispilem4  42234  wallispi2lem1  42237  stirlinglem1  42240  stirlinglem5  42244  stirlinglem10  42249  dirkerper  42262  dirkertrigeqlem1  42264  dirkertrigeqlem3  42266  dirkertrigeq  42267  dirkercncflem4  42272  fourierdlem24  42297  sqwvfoura  42394  sqwvfourb  42395  fourierswlem  42396  1t10e1p1e11  43391  fmtnorec3  43557  fmtno5lem4  43565  fmtno5  43566  257prm  43570  fmtno4nprmfac193  43583  m3prm  43601  139prmALT  43606  127prm  43610  m7prm  43611  lighneallem3  43619  proththd  43626  3exp4mod41  43628  41prothprmlem2  43630  perfectALTVlem2  43734  perfectALTV  43735  11t31e341  43744  evengpop3  43810  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  bgoldbtbndlem1  43817  0nodd  43924  altgsumbcALT  44299  exple2lt6  44310  nn0sumshdiglemB  44578  line2ylem  44636  onetansqsecsq  44758  cotsqcscsq  44759  5m4e1  44796
  Copyright terms: Public domain W3C validator