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

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 10225 . 2 class 1
2 cc 10222 . 2 class
31, 2wcel 2157 1 wff 1 ∈ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  10320  1cnd  10323  1ex  10324  mulid1  10326  mulid2  10327  1re  10328  muladd11  10494  peano2cn  10496  mul02lem2  10501  addid1  10504  cnegex2  10506  peano2cnm  10635  0reALT  10666  ine0  10753  mulm1  10759  0lt1  10838  ixi  10944  muleqadd  10959  reccl  10980  recne0  10986  recid  10987  recid2  10988  div1  11004  1div1e1  11005  diveq1  11006  recdiv  11019  divdiv1  11024  divdiv2  11025  recdiv2  11026  conjmul  11030  eqneg  11033  div2neg  11036  recp1lt1  11209  recreclt  11210  recgt0ii  11217  inelr  11298  ofnegsub  11306  peano5nni  11311  nn1m1nn  11328  nn1suc  11329  nnaddcl  11330  nnmulcl  11331  nnmulclOLD  11332  nnsub  11348  1m1e0  11376  neg1cn  11409  neg1ne0  11411  negneg1e1  11413  1pneg1e0  11414  1m0e1  11416  0p1e1  11417  1p0e1  11419  2m1e1  11421  3m1e2  11423  4m1e3  11424  5m1e4  11425  6m1e5  11426  7m1e6  11427  8m1e7  11428  9m1e8  11429  2p2e4  11430  1p2e3  11438  3p2e5  11445  3p3e6  11446  4p2e6  11447  4p3e7  11448  4p4e8  11449  5p2e7  11450  5p3e8  11451  5p4e9  11452  6p2e8  11453  6p3e9  11454  7p2e9  11455  1t1e1  11456  3t3e9  11461  neg1mulneg1e1  11515  1mhlfehlf  11521  8th4div3  11522  halfpm6th  11523  addltmul  11538  elnn0nn  11604  elz2  11663  zlem1lt  11698  zltlem1  11699  nnaddm1cl  11703  zextlt  11720  zeo  11732  peano5uzi  11735  numsuc  11776  numltc  11788  numsucc  11802  numaddc  11810  6p5lem  11832  5p5e10  11833  6p4e10  11834  7p3e10  11837  8p2e10  11842  10m1e9  11858  4t3lem  11859  7t4e28  11873  9t11e99  11892  decbin2  11903  halfthird  11905  5recm6rec  11906  uzp1  11942  peano2uzr  11964  uzaddcl  11965  rebtwnz  12009  qbtwnre  12251  iccf1o  12542  fz01en  12595  fztp  12623  fzsuc2  12624  fztpval  12628  fseq1m1p1  12641  elfzp1b  12643  fz0to4untppr  12669  predfz  12691  fzoss2  12723  fzval3  12764  fzosplitsnm1  12770  fzo0to42pr  12782  fzo1to4tp  12783  fldiv4p1lem1div2  12863  ceim1l  12873  fldiv  12886  uzrdgxfr  12993  fzen2  12995  nn0ennn  13005  seqm1  13044  seqshft2  13053  monoord2  13058  sermono  13059  seqf1olem1  13066  seqf1olem2  13067  seqz  13075  ser1const  13083  expcl  13104  m1expcl2  13108  expclzlem  13110  expm1t  13114  1exp  13115  mulexpz  13126  expadd  13128  expaddz  13130  expmul  13131  expubnd  13147  sqrecii  13172  neg1sqe1  13185  irec  13190  i4  13193  binom21  13206  sq01  13212  crreczi  13215  bernneq  13216  bernneq2  13217  nn0opthlem1  13278  facndiv  13298  faclbnd4lem1  13303  faclbnd6  13309  bcnp1n  13324  bcm1k  13325  bcp1nk  13327  bcn2  13329  bcp1m1  13330  bcpasc  13331  4bc3eq4  13338  hashgadd  13387  hashfz  13434  hashfzo  13436  hashxplem  13440  hashbclem  13456  hashf1  13461  seqcoll  13468  swrds1  13678  swrdlsw  13679  wrdind  13703  wrd2ind  13704  swrds2  13912  relexpaddg  14019  rei  14122  imi  14123  recan  14302  iserex  14613  isercoll2  14625  serf0  14637  iseraltlem2  14639  iseraltlem3  14640  iseralt  14641  sumrblem  14668  fsumm1  14706  fsump1  14713  telfsumo  14759  fsumparts  14763  hashiun  14779  binomlem  14786  binom  14787  binom1p  14788  binom11  14789  binom1dif  14790  bcxmas  14792  isumsplit  14797  isum1p  14798  climcndslem1  14806  supcvg  14813  harmonic  14816  arisum  14817  arisum2  14818  trireciplem  14819  geoserg  14823  geolim  14826  geolim2  14827  georeclim  14828  geo2sum  14829  geo2sum2  14830  geoisum1c  14836  0.999...  14837  geoihalfsum  14838  cvgrat  14839  mertenslem1  14840  mertenslem2  14841  mertens  14842  prodf1  14847  prodfclim1  14849  prodrblem  14883  fprodcvg  14884  prodmolem2a  14888  zprod  14891  fprodntriv  14896  prodss  14901  fprodss  14902  fprodsplit  14920  fprodn0f  14945  fprodclf  14946  risefaccl  14969  fallfaccl  14970  risefacfac  14989  binomfallfac  14995  bpolycl  15006  bpolysum  15007  bpolydiflem  15008  fsumkthpow  15010  bpoly2  15011  bpoly3  15012  bpoly4  15013  fsumcube  15014  esum  15034  ege2le3  15043  efsub  15053  efexp  15054  efzval  15055  eftlub  15062  effsumlt  15064  ef4p  15066  tanval3  15087  efi4p  15090  tan0  15104  efival  15105  tanadd  15120  cos2t  15131  cos2tsin  15132  ef01bndlem  15137  cos1bnd  15140  cos2bnd  15141  demoivreALT  15154  eirrlem  15155  rpnnen2lem3  15168  rpnnen2lem11  15176  ruclem12  15193  3dvds  15278  3dvdsdec  15279  3dvds2dec  15280  odd2np1lem  15287  odd2np1  15288  opoe  15310  omoe  15311  opeo  15312  omeo  15313  m1exp1  15316  n2dvdsm1  15328  flodddiv4  15359  bitsfzo  15379  gcdmultiple  15491  sqgcd  15500  nn0seqcvgd  15505  prmind2  15619  hashdvds  15700  phiprmpw  15701  phiprm  15702  eulerthlem2  15707  iserodd  15760  sumhash  15820  fldivp1  15821  prmpwdvds  15828  pockthlem  15829  pockthi  15831  prmreclem4  15843  prmreclem6  15845  4sqlem11  15879  4sqlem19  15887  vdwapun  15898  vdwapid1  15899  vdwlem3  15907  vdwlem5  15909  vdwlem6  15910  vdwlem8  15912  vdwlem9  15913  vdwnnlem2  15920  ramub1lem1  15950  ramub1lem2  15951  ramcl  15953  prmo1  15961  dec5nprm  15990  decexp2  15999  prmlem0  16027  43prm  16043  83prm  16044  139prm  16045  163prm  16046  317prm  16047  631prm  16048  prmo4  16049  prmo5  16050  prmo6  16051  1259lem2  16053  1259lem3  16054  1259lem4  16055  1259lem5  16056  1259prm  16057  2503lem1  16058  2503lem2  16059  2503lem3  16060  2503prm  16061  4001lem1  16062  4001lem2  16063  4001lem3  16064  4001lem4  16065  4001prm  16066  gsumccat  17586  mulgnndir  17776  mulgneg2  17781  m1expaddsub  18122  sylow1lem1  18217  sylow2a  18238  efgsval2  18350  efgsrel  18351  efgsres  18355  cnfld1  19982  zsssubrg  20015  cnmgpid  20019  zringcyg  20050  mulgrhm2  20058  cnmsgnsubg  20133  cnmsgnbas  20134  cnmsgngrp  20135  psgninv  20138  evpmodpmf1o  20153  blcvx  22818  iihalf2  22949  icopnfcnv  22958  iccpnfhmeo  22961  xrhmeo  22962  icccvx  22966  lebnumii  22982  reparphti  23013  pcoass  23040  pcorevlem  23042  pcorev2  23044  pi1xfrcnv  23073  cnstrcvs  23157  cncvs  23161  ncvsm1  23170  pjthlem1  23426  divcncf  23434  ovolunlem1a  23483  ovolunlem1  23484  ovolicc2lem4  23507  uniioombllem3  23572  uniioombllem4  23573  dyadovol  23580  vitalilem4  23598  mbf0  23621  iblitg  23755  iblcnlem1  23774  itgcnlem  23776  dvid  23901  dvexp  23936  dvexp2  23937  dvexp3  23961  dveflem  23962  dvef  23963  dvlipcn  23977  dvcvx  24003  dvfsumle  24004  dvfsumlem1  24009  degltp1le  24053  ply1divex  24116  fta1glem1  24145  plyaddlem1  24189  plymullem1  24190  coeidp  24239  dgrid  24240  dvply1  24259  dvply2g  24260  plyremlem  24279  fta1lem  24282  vieta1lem1  24285  vieta1lem2  24286  qaa  24298  iaa  24300  aalioulem3  24309  geolim3  24314  aaliou3lem2  24318  aaliou3lem7  24324  taylply2  24342  dvradcnv  24395  pserdvlem2  24402  pserdv2  24404  abelthlem1  24405  abelthlem2  24406  abelthlem6  24410  abelthlem7  24412  abelth  24415  reeff1olem  24420  reeff1o  24421  efcvx  24423  sinhalfpilem  24436  eulerid  24447  cos2pi  24449  sincosq3sgn  24473  sincosq4sgn  24474  tangtx  24478  sincos4thpi  24486  sincos6thpi  24488  pige3  24490  abssinper  24491  coskpi  24493  coseq1  24495  efeq1  24496  tanregt0  24506  logneg2  24581  logdivlti  24586  logcnlem4  24611  dvlog2lem  24618  dvlog2  24619  advlog  24620  advlogexp  24621  logtayl  24626  logtayl2  24628  logccv  24629  cxpval  24630  1cxp  24638  cxpcl  24640  cxpp1  24646  cxpsqrt  24669  dvsqrt  24703  dvcnsqrt  24705  sqrtcn  24711  cxpaddlelem  24712  root1id  24715  root1cj  24717  logrec  24721  logb1  24727  logbmpt  24746  ang180lem1  24759  ang180lem2  24760  ang180lem3  24761  isosctrlem1  24768  isosctrlem2  24769  1cubrlem  24788  1cubr  24789  mcubic  24794  binom4  24797  dquartlem1  24798  quartlem1  24804  asinlem  24815  asinlem2  24816  asinlem3a  24817  asinlem3  24818  asinf  24819  atandm2  24824  atandm4  24826  atanf  24827  asinneg  24833  efiasin  24835  sinasin  24836  asinsin  24839  asin1  24841  acos1  24842  reasinsin  24843  asinbnd  24846  cosasin  24851  atanneg  24854  atancj  24857  efiatan  24859  atanlogaddlem  24860  atanlogadd  24861  atanlogsublem  24862  atanlogsub  24863  efiatan2  24864  2efiatan  24865  tanatan  24866  cosatan  24868  cosatanne0  24869  atantan  24870  atanbndlem  24872  bndatandm  24876  atans2  24878  dvatan  24882  atantayl  24884  atantayl2  24885  atantayl3  24886  leibpilem1  24887  leibpilem2  24888  leibpi  24889  log2cnv  24891  log2tlbnd  24892  log2ublem3  24895  log2ub  24896  birthdaylem2  24899  birthday  24901  efrlim  24916  dfef2  24917  cvxcl  24931  scvxcvx  24932  emcllem2  24943  emcllem4  24945  emcllem7  24948  harmonicbnd4  24957  fsumharmonic  24958  zetacvg  24961  lgamcvg2  25001  lgam1  25010  gam1  25011  wilthlem1  25014  wilthlem2  25015  wilthlem3  25016  basellem2  25028  basellem5  25031  basellem6  25032  basellem7  25033  basellem8  25034  basellem9  25035  0sgm  25090  mule1  25094  ppiprm  25097  ppinprm  25098  chtprm  25099  chtnprm  25100  chpp1  25101  mumullem2  25126  1sgmprm  25144  1sgm2ppw  25145  ppiublem2  25148  ppiub  25149  chtublem  25156  chtub  25157  logfaclbnd  25167  logfacbnd3  25168  logfacrlim  25169  logexprlim  25170  mersenne  25172  perfect1  25173  perfectlem1  25174  perfectlem2  25175  perfect  25176  dchrelbasd  25184  dchrmulid2  25197  dchrfi  25200  dchrsum2  25213  sumdchr2  25215  bcp1ctr  25224  bposlem8  25236  zabsle1  25241  lgslem1  25242  lgslem2  25243  lgsfcl2  25248  lgsvalmod  25261  lgsneg  25266  lgsdilem  25269  lgsdir2lem1  25270  lgsdir2lem2  25271  lgsdir2lem3  25272  lgsdir2lem5  25274  lgsdir2  25275  lgsdir  25277  lgsdi  25279  lgsne0  25280  lgseisenlem1  25320  lgseisenlem2  25321  lgseisen  25324  lgsquadlem1  25325  lgsquadlem2  25326  lgsquad2lem1  25329  lgsquad2  25331  m1lgs  25333  2lgslem3c  25343  2lgsoddprmlem3b  25356  2lgsoddprmlem3c  25357  2lgsoddprmlem3d  25358  2sqlem10  25373  2sqlem11  25374  2sqblem  25376  chtppilimlem2  25383  chebbnd2  25386  chto1lb  25387  rplogsumlem1  25393  rpvmasumlem  25396  dchrmusumlema  25402  dchrmusum2  25403  dchrisum0flblem1  25417  rpvmasum2  25421  mudivsum  25439  mulogsum  25441  vmalogdivsum2  25447  selberg2lem  25459  logdivbnd  25465  pntrmax  25473  pntrsumo1  25474  pntrsumbnd2  25476  pntrlog2bndlem5  25490  pntpbnd1a  25494  pntpbnd2  25496  pntibndlem2  25500  pntlemd  25503  pntlemc  25504  pntlemr  25511  brbtwn2  26005  colinearalglem4  26009  ax5seglem1  26028  ax5seglem2  26029  ax5seglem3  26031  ax5seglem5  26033  ax5seglem7  26035  ax5seglem9  26037  axbtwnid  26039  axpaschlem  26040  axlowdimlem13  26054  axlowdimlem14  26055  axlowdimlem16  26057  axeuclidlem  26062  axcontlem2  26065  axcontlem4  26067  axcontlem7  26070  axcontlem8  26071  crctcshwlkn0lem6  26942  wwlksnext  27036  clwwlkf1  27204  wwlksext2clwwlkOLD  27214  clwwlknonex2lem2  27283  ex-fl  27641  ex-ind-dvds  27655  vc2OLD  27757  vc0  27763  vcm  27765  nvm1  27854  nvmtri  27860  nvge0  27862  ipval2lem3  27894  ipidsq  27899  lnoadd  27947  ip1ilem  28015  ip1i  28016  ip2i  28017  ipdirilem  28018  ipasslem1  28020  ipasslem2  28021  ipasslem10  28028  minvecolem2  28065  hvsubid  28217  hv2times  28252  hisubcomi  28295  normlem9  28309  normlem7tALT  28310  norm-ii-i  28328  normsubi  28332  hhssnv  28455  pjhthlem1  28584  h1de2bi  28747  homulid2  28993  ho2times  29012  lnop0  29159  lnopaddi  29164  lnophmlem2  29210  lnfn0i  29235  lnfnaddi  29236  hst1h  29420  sto2i  29430  stadd3i  29441  addltmulALT  29639  dpmul4  29953  isarchi3  30072  archirngz  30074  psgnid  30178  lmatfvlem  30212  qqhval2lem  30356  dya2ub  30663  omssubadd  30693  eulerpartlemgs2  30773  fib5  30798  fib6  30799  ballotlem2  30881  sgnneg  30933  signswch  30969  signlem0  30995  itgexpif  31015  reprlt  31028  breprexp  31042  breprexpnat  31043  hgt750lem2  31061  subfacp1lem5  31494  subfacp1lem6  31495  subfacval2  31497  subfaclim  31498  subfacval3  31499  cvxsconn  31553  resconn  31556  cvmliftlem7  31601  cvmliftlem10  31604  problem4  31889  sinccvglem  31893  sqdivzi  31937  faclimlem1  31956  dnibndlem5  32794  dnibndlem10  32799  ltflcei  33712  sin2h  33714  cos2h  33715  tan2h  33716  pigt3  33717  poimirlem13  33737  poimirlem16  33740  poimirlem17  33741  poimirlem19  33743  poimirlem20  33744  poimirlem31  33755  mblfinlem2  33762  mblfinlem3  33763  dvtan  33774  itg2addnclem3  33777  dvasin  33810  dvacos  33811  areacirc  33819  fdc  33854  mettrifi  33866  heiborlem4  33926  heiborlem6  33928  eldioph2lem1  37826  lzenom  37836  irrapxlem1  37889  rmspecsqrtnq  37973  rmxm1  38001  rmym1  38002  2nn0ind  38012  jm2.24nn  38028  jm2.17a  38029  jm2.17b  38030  jm2.17c  38031  jm2.24  38032  acongeq  38052  jm2.18  38057  jm2.27c  38076  jm3.1lem2  38087  rngunsnply  38245  flcidc  38246  inductionexd  38954  unitadd  38999  hashnzfzclim  39022  ofdivrec  39026  lhe4.4ex1a  39029  expgrowth  39035  dvradcnv2  39047  binomcxplemrat  39050  binomcxplemnotnn0  39056  isosctrlem1ALT  39665  monoord2xrv  40194  dvsinax  40608  dvnprodlem3  40644  itgsin0pilem1  40646  itgsbtaddcnst  40678  stoweidlem13  40710  stoweidlem26  40723  stoweidlem34  40731  stoweidlem38  40735  wallispilem2  40763  wallispilem4  40765  wallispi2lem1  40768  stirlinglem1  40771  stirlinglem5  40775  stirlinglem10  40780  dirkerper  40793  dirkertrigeqlem1  40795  dirkertrigeqlem3  40797  dirkertrigeq  40798  dirkercncflem4  40803  fourierdlem24  40828  sqwvfoura  40925  sqwvfourb  40926  fourierswlem  40927  1t10e1p1e11  41896  fmtnorec3  42036  fmtno5lem4  42044  fmtno5  42045  257prm  42049  fmtno4nprmfac193  42062  m3prm  42082  139prmALT  42087  127prm  42091  m7prm  42092  lighneallem3  42100  proththd  42107  3exp4mod41  42109  41prothprmlem2  42111  perfectALTVlem2  42207  perfectALTV  42208  evengpop3  42262  nnsum4primeseven  42264  nnsum4primesevenALTV  42265  bgoldbtbndlem1  42269  0nodd  42379  altgsumbcALT  42700  exple2lt6  42714  nn0sumshdiglemB  42983  onetansqsecsq  43074  cotsqcscsq  43075  5m4e1  43115
  Copyright terms: Public domain W3C validator