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

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 10139 . 2 class 1
2 cc 10136 . 2 class
31, 2wcel 2145 1 wff 1 ∈ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  10234  1ex  10237  mulid1  10239  mulid2  10240  1re  10241  1cnd  10258  muladd11  10408  peano2cn  10410  mul02lem2  10415  addid1  10418  cnegex2  10420  peano2cnm  10549  0reALT  10580  ine0  10667  mulm1  10673  0lt1  10752  ixi  10858  muleqadd  10873  reccl  10894  recne0  10900  recid  10901  recid2  10902  div1  10918  1div1e1  10919  diveq1  10920  recdiv  10933  divdiv1  10938  divdiv2  10939  recdiv2  10940  conjmul  10944  eqneg  10947  div2neg  10950  recp1lt1  11123  recreclt  11124  recgt0ii  11131  inelr  11212  ofnegsub  11220  peano5nni  11225  nn1m1nn  11242  nn1suc  11243  nnaddcl  11244  nnmulcl  11245  nnsub  11261  1m1e0  11291  neg1cn  11326  neg1ne0  11328  negneg1e1  11330  1pneg1e0  11331  1m0e1  11333  0p1e1  11334  1p0e1  11335  2m1e1  11337  3m1e2  11339  4m1e3  11340  5m1e4  11341  6m1e5  11342  7m1e6  11343  8m1e7  11344  9m1e8  11345  2p2e4  11346  1p2e3  11354  3p2e5  11362  3p3e6  11363  4p2e6  11364  4p3e7  11365  4p4e8  11366  5p2e7  11367  5p3e8  11368  5p4e9  11369  5p5e10OLD  11370  6p2e8  11371  6p3e9  11372  6p4e10OLD  11373  7p2e9  11374  7p3e10OLD  11375  8p2e10OLD  11376  1t1e1  11377  3t3e9  11382  neg1mulneg1e1  11447  1mhlfehlf  11453  8th4div3  11454  halfpm6th  11455  addltmul  11470  elnn0nn  11537  elz2  11596  zlem1lt  11631  zltlem1  11632  nnaddm1cl  11636  zextlt  11653  zeo  11665  peano5uzi  11668  numsuc  11713  numltc  11730  numsucc  11751  numaddc  11762  6p5lem  11796  5p5e10  11797  6p4e10  11799  7p3e10  11804  8p2e10  11811  10m1e9  11831  4t3lem  11832  7t4e28  11851  9t11e99  11872  9t11e99OLD  11873  decbin2  11884  halfthird  11886  5recm6rec  11887  uzp1  11923  peano2uzr  11945  uzaddcl  11946  rebtwnz  11990  qbtwnre  12235  iccf1o  12523  fz01en  12576  fztp  12604  fzsuc2  12605  fztpval  12609  fseq1m1p1  12622  elfzp1b  12624  fz0to4untppr  12650  predfz  12672  fzoss2  12704  fzval3  12745  fzosplitsnm1  12751  fzo0to42pr  12763  fzo1to4tp  12764  fldiv4p1lem1div2  12844  ceim1l  12854  fldiv  12867  uzrdgxfr  12974  fzen2  12976  nn0ennn  12986  seqm1  13025  seqshft2  13034  monoord2  13039  sermono  13040  seqf1olem1  13047  seqf1olem2  13048  seqz  13056  ser1const  13064  expcl  13085  m1expcl2  13089  expclzlem  13091  expm1t  13095  1exp  13096  mulexpz  13107  expadd  13109  expaddz  13111  expmul  13112  expubnd  13128  sqrecii  13153  neg1sqe1  13166  irec  13171  i4  13174  binom21  13187  sq01  13193  crreczi  13196  bernneq  13197  bernneq2  13198  nn0opthlem1  13259  facndiv  13279  faclbnd4lem1  13284  faclbnd6  13290  bcnp1n  13305  bcm1k  13306  bcp1nk  13308  bcn2  13310  bcp1m1  13311  bcpasc  13312  4bc3eq4  13319  hashgadd  13368  hashfz  13416  hashfzo  13418  hashxplem  13422  hashbclem  13438  hashf1  13443  seqcoll  13450  swrds1  13660  swrdlsw  13661  wrdind  13685  wrd2ind  13686  swrds2  13894  relexpaddg  14001  rei  14104  imi  14105  recan  14284  iserex  14595  isercoll2  14607  serf0  14619  iseraltlem2  14621  iseraltlem3  14622  iseralt  14623  sumrblem  14650  fsumm1  14688  fsump1  14695  telfsumo  14741  fsumparts  14745  hashiun  14761  binomlem  14768  binom  14769  binom1p  14770  binom11  14771  binom1dif  14772  bcxmas  14774  isumsplit  14779  isum1p  14780  climcndslem1  14788  supcvg  14795  harmonic  14798  arisum  14799  arisum2  14800  trireciplem  14801  geoserg  14805  geolim  14808  geolim2  14809  georeclim  14810  geo2sum  14811  geo2sum2  14812  geoisum1c  14818  0.999...  14819  0.999...OLD  14820  geoihalfsum  14821  cvgrat  14822  mertenslem1  14823  mertenslem2  14824  mertens  14825  prodf1  14830  prodfclim1  14832  prodrblem  14866  fprodcvg  14867  prodmolem2a  14871  zprod  14874  fprodntriv  14879  prodss  14884  fprodss  14885  fprodsplit  14903  fprodn0f  14928  fprodclf  14929  risefaccl  14952  fallfaccl  14953  risefacfac  14972  binomfallfac  14978  bpolycl  14989  bpolysum  14990  bpolydiflem  14991  fsumkthpow  14993  bpoly2  14994  bpoly3  14995  bpoly4  14996  fsumcube  14997  esum  15017  ege2le3  15026  efsub  15036  efexp  15037  efzval  15038  eftlub  15045  effsumlt  15047  ef4p  15049  tanval3  15070  efi4p  15073  tan0  15087  efival  15088  tanadd  15103  cos2t  15114  cos2tsin  15115  ef01bndlem  15120  cos1bnd  15123  cos2bnd  15124  demoivreALT  15137  eirrlem  15138  rpnnen2lem3  15151  rpnnen2lem11  15159  ruclem12  15176  3dvds  15261  3dvdsOLD  15262  3dvdsdec  15263  3dvdsdecOLD  15264  3dvds2dec  15265  odd2np1lem  15272  odd2np1  15273  opoe  15295  omoe  15296  opeo  15297  omeo  15298  m1exp1  15301  n2dvdsm1  15313  flodddiv4  15345  bitsfzo  15365  gcdmultiple  15477  sqgcd  15486  nn0seqcvgd  15491  prmind2  15605  hashdvds  15687  phiprmpw  15688  phiprm  15689  eulerthlem2  15694  iserodd  15747  sumhash  15807  fldivp1  15808  prmpwdvds  15815  pockthlem  15816  pockthi  15818  prmreclem4  15830  prmreclem6  15832  4sqlem11  15866  4sqlem19  15874  vdwapun  15885  vdwapid1  15886  vdwlem3  15894  vdwlem5  15896  vdwlem6  15897  vdwlem8  15899  vdwlem9  15900  vdwnnlem2  15907  ramub1lem1  15937  ramub1lem2  15938  ramcl  15940  prmo1  15948  dec5nprm  15977  decexp2  15986  prmlem0  16019  43prm  16036  83prm  16037  139prm  16038  163prm  16039  317prm  16040  631prm  16041  prmo4  16042  prmo5  16043  prmo6  16044  1259lem2  16046  1259lem3  16047  1259lem4  16048  1259lem5  16049  1259prm  16050  2503lem1  16051  2503lem2  16052  2503lem3  16053  2503prm  16054  4001lem1  16055  4001lem2  16056  4001lem3  16057  4001lem4  16058  4001prm  16059  gsumccat  17586  mulgnndir  17777  mulgnndirOLD  17778  mulgneg2  17783  m1expaddsub  18125  sylow1lem1  18220  sylow2a  18241  efgsval2  18353  efgsrel  18354  efgsres  18358  cnfld1  19986  zsssubrg  20019  cnmgpid  20023  zringcyg  20054  mulgrhm2  20062  cnmsgnsubg  20138  cnmsgnbas  20139  cnmsgngrp  20140  psgninv  20143  evpmodpmf1o  20158  blcvx  22821  iihalf2  22952  icopnfcnv  22961  iccpnfhmeo  22964  xrhmeo  22965  icccvx  22969  lebnumii  22985  reparphti  23016  pcoass  23043  pcorevlem  23045  pcorev2  23047  pi1xfrcnv  23076  cnstrcvs  23160  cncvs  23164  ncvsm1  23173  pjthlem1  23427  divcncf  23435  ovolunlem1a  23484  ovolunlem1  23485  ovolicc2lem4  23508  uniioombllem3  23573  uniioombllem4  23574  dyadovol  23581  vitalilem4  23599  mbf0  23622  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  24582  logdivlti  24587  logcnlem4  24612  dvlog2lem  24619  dvlog2  24620  advlog  24621  advlogexp  24622  logtayl  24627  logtayl2  24629  logccv  24630  cxpval  24631  1cxp  24639  cxpcl  24641  cxpp1  24647  cxpsqrt  24670  dvsqrt  24704  dvcnsqrt  24706  sqrtcn  24712  cxpaddlelem  24713  root1id  24716  root1cj  24718  logrec  24722  logb1  24728  logbmpt  24747  ang180lem1  24760  ang180lem2  24761  ang180lem3  24762  isosctrlem1  24769  isosctrlem2  24770  1cubrlem  24789  1cubr  24790  mcubic  24795  binom4  24798  dquartlem1  24799  quartlem1  24805  asinlem  24816  asinlem2  24817  asinlem3a  24818  asinlem3  24819  asinf  24820  atandm2  24825  atandm4  24827  atanf  24828  asinneg  24834  efiasin  24836  sinasin  24837  asinsin  24840  asin1  24842  acos1  24843  reasinsin  24844  asinbnd  24847  cosasin  24852  atanneg  24855  atancj  24858  efiatan  24860  atanlogaddlem  24861  atanlogadd  24862  atanlogsublem  24863  atanlogsub  24864  efiatan2  24865  2efiatan  24866  tanatan  24867  cosatan  24869  cosatanne0  24870  atantan  24871  atanbndlem  24873  bndatandm  24877  atans2  24879  dvatan  24883  atantayl  24885  atantayl2  24886  atantayl3  24887  leibpilem1  24888  leibpilem2  24889  leibpi  24890  log2cnv  24892  log2tlbnd  24893  log2ublem3  24896  log2ub  24897  birthdaylem2  24900  birthday  24902  efrlim  24917  dfef2  24918  cvxcl  24932  scvxcvx  24933  emcllem2  24944  emcllem4  24946  emcllem7  24949  harmonicbnd4  24958  fsumharmonic  24959  zetacvg  24962  lgamcvg2  25002  lgam1  25011  gam1  25012  wilthlem1  25015  wilthlem2  25016  wilthlem3  25017  basellem2  25029  basellem5  25032  basellem6  25033  basellem7  25034  basellem8  25035  basellem9  25036  0sgm  25091  mule1  25095  ppiprm  25098  ppinprm  25099  chtprm  25100  chtnprm  25101  chpp1  25102  mumullem2  25127  1sgmprm  25145  1sgm2ppw  25146  ppiublem2  25149  ppiub  25150  chtublem  25157  chtub  25158  logfaclbnd  25168  logfacbnd3  25169  logfacrlim  25170  logexprlim  25171  mersenne  25173  perfect1  25174  perfectlem1  25175  perfectlem2  25176  perfect  25177  dchrelbasd  25185  dchrmulid2  25198  dchrfi  25201  dchrsum2  25214  sumdchr2  25216  bcp1ctr  25225  bposlem8  25237  zabsle1  25242  lgslem1  25243  lgslem2  25244  lgsfcl2  25249  lgsvalmod  25262  lgsneg  25267  lgsdilem  25270  lgsdir2lem1  25271  lgsdir2lem2  25272  lgsdir2lem3  25273  lgsdir2lem5  25275  lgsdir2  25276  lgsdir  25278  lgsdi  25280  lgsne0  25281  lgseisenlem1  25321  lgseisenlem2  25322  lgseisen  25325  lgsquadlem1  25326  lgsquadlem2  25327  lgsquad2lem1  25330  lgsquad2  25332  m1lgs  25334  2lgslem3c  25344  2lgsoddprmlem3b  25357  2lgsoddprmlem3c  25358  2lgsoddprmlem3d  25359  2sqlem10  25374  2sqlem11  25375  2sqblem  25377  chtppilimlem2  25384  chebbnd2  25387  chto1lb  25388  rplogsumlem1  25394  rpvmasumlem  25397  dchrmusumlema  25403  dchrmusum2  25404  dchrisum0flblem1  25418  rpvmasum2  25422  mudivsum  25440  mulogsum  25442  vmalogdivsum2  25448  selberg2lem  25460  logdivbnd  25466  pntrmax  25474  pntrsumo1  25475  pntrsumbnd2  25477  pntrlog2bndlem5  25491  pntpbnd1a  25495  pntpbnd2  25497  pntibndlem2  25501  pntlemd  25504  pntlemc  25505  pntlemr  25512  brbtwn2  26006  colinearalglem4  26010  ax5seglem1  26029  ax5seglem2  26030  ax5seglem3  26032  ax5seglem5  26034  ax5seglem7  26036  ax5seglem9  26038  axbtwnid  26040  axpaschlem  26041  axlowdimlem13  26055  axlowdimlem14  26056  axlowdimlem16  26058  axeuclidlem  26063  axcontlem2  26066  axcontlem4  26068  axcontlem7  26071  axcontlem8  26072  crctcshwlkn0lem6  26943  wwlksnext  27037  clwwlkf1  27205  wwlksext2clwwlkOLD  27215  clwwlknonex2lem2  27284  ex-fl  27646  ex-ind-dvds  27660  vc2OLD  27763  vc0  27769  vcm  27771  nvm1  27860  nvmtri  27866  nvge0  27868  ipval2lem3  27900  ipidsq  27905  lnoadd  27953  ip1ilem  28021  ip1i  28022  ip2i  28023  ipdirilem  28024  ipasslem1  28026  ipasslem2  28027  ipasslem10  28034  minvecolem2  28071  hvsubid  28223  hv2times  28258  hisubcomi  28301  normlem9  28315  normlem7tALT  28316  norm-ii-i  28334  normsubi  28338  hhssnv  28461  pjhthlem1  28590  h1de2bi  28753  homulid2  28999  ho2times  29018  lnop0  29165  lnopaddi  29170  lnophmlem2  29216  lnfn0i  29241  lnfnaddi  29242  hst1h  29426  sto2i  29436  stadd3i  29447  addltmulALT  29645  dpmul4  29962  isarchi3  30081  archirngz  30083  psgnid  30187  lmatfvlem  30221  qqhval2lem  30365  dya2ub  30672  omssubadd  30702  eulerpartlemgs2  30782  fib5  30807  fib6  30808  ballotlem2  30890  sgnneg  30942  signswch  30978  signlem0  31004  itgexpif  31024  reprlt  31037  breprexp  31051  breprexpnat  31052  hgt750lem2  31070  subfacp1lem5  31504  subfacp1lem6  31505  subfacval2  31507  subfaclim  31508  subfacval3  31509  cvxsconn  31563  resconn  31566  cvmliftlem7  31611  cvmliftlem10  31614  problem4  31900  sinccvglem  31904  sqdivzi  31948  faclimlem1  31967  dnibndlem5  32809  dnibndlem10  32814  ltflcei  33730  sin2h  33732  cos2h  33733  tan2h  33734  pigt3  33735  poimirlem13  33755  poimirlem16  33758  poimirlem17  33759  poimirlem19  33761  poimirlem20  33762  poimirlem31  33773  mblfinlem2  33780  mblfinlem3  33781  dvtan  33792  itg2addnclem3  33795  dvasin  33828  dvacos  33829  areacirc  33837  fdc  33873  mettrifi  33885  heiborlem4  33945  heiborlem6  33947  eldioph2lem1  37849  lzenom  37859  irrapxlem1  37912  rmspecsqrtnq  37996  rmspecsqrtnqOLD  37997  rmxm1  38025  rmym1  38026  2nn0ind  38036  jm2.24nn  38052  jm2.17a  38053  jm2.17b  38054  jm2.17c  38055  jm2.24  38056  acongeq  38076  jm2.18  38081  jm2.27c  38100  jm3.1lem2  38111  rngunsnply  38269  flcidc  38270  inductionexd  38979  unitadd  39024  hashnzfzclim  39047  ofdivrec  39051  lhe4.4ex1a  39054  expgrowth  39060  dvradcnv2  39072  binomcxplemrat  39075  binomcxplemnotnn0  39081  isosctrlem1ALT  39692  monoord2xrv  40230  dvsinax  40645  dvnprodlem3  40681  itgsin0pilem1  40683  itgsbtaddcnst  40715  stoweidlem13  40747  stoweidlem26  40760  stoweidlem34  40768  stoweidlem38  40772  wallispilem2  40800  wallispilem4  40802  wallispi2lem1  40805  stirlinglem1  40808  stirlinglem5  40812  stirlinglem10  40817  dirkerper  40830  dirkertrigeqlem1  40832  dirkertrigeqlem3  40834  dirkertrigeq  40835  dirkercncflem4  40840  fourierdlem24  40865  sqwvfoura  40962  sqwvfourb  40963  fourierswlem  40964  1t10e1p1e11  41847  1t10e1p1e11OLD  41848  fmtnorec3  41988  fmtno5lem4  41996  fmtno5  41997  257prm  42001  fmtno4nprmfac193  42014  m3prm  42034  139prmALT  42039  127prm  42043  m7prm  42044  lighneallem3  42052  proththd  42059  3exp4mod41  42061  41prothprmlem2  42063  perfectALTVlem2  42159  perfectALTV  42160  evengpop3  42214  nnsum4primeseven  42216  nnsum4primesevenALTV  42217  bgoldbtbndlem1  42221  0nodd  42338  altgsumbcALT  42659  exple2lt6  42673  nn0sumshdiglemB  42942  onetansqsecsq  43033  cotsqcscsq  43034  5m4e1  43074
  Copyright terms: Public domain W3C validator