MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zcn Structured version   Unicode version

Theorem zcn 10942
Description: An integer is a complex number. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
zcn  |-  ( N  e.  ZZ  ->  N  e.  CC )

Proof of Theorem zcn
StepHypRef Expression
1 zre 10941 . 2  |-  ( N  e.  ZZ  ->  N  e.  RR )
21recnd 9668 1  |-  ( N  e.  ZZ  ->  N  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   CCcc 9536   ZZcz 10937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-resscn 9595
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308  df-neg 9862  df-z 10938
This theorem is referenced by:  zsscn  10945  zsubcl  10979  zrevaddcl  10982  zlem1lt  10988  zltlem1  10989  zdiv  11006  zdivadd  11007  zdivmul  11008  zextlt  11010  zneo  11018  zeo2  11022  peano5uzi  11024  zindd  11036  znnn0nn  11047  zriotaneg  11049  zmax  11261  rebtwnz  11263  qmulz  11267  zq  11270  qaddcl  11280  qnegcl  11281  qmulcl  11282  qreccl  11284  fzen  11814  uzsubsubfz  11819  fz01en  11825  fzmmmeqm  11830  fzsubel  11832  fztp  11850  fzsuc2  11851  fzrev2  11857  fzrev3  11859  elfzp1b  11869  fzrevral  11877  fzrevral2  11878  fzrevral3  11879  fzshftral  11880  fzo0addel  11965  fzo0addelr  11966  fzoaddel2  11967  elfzoext  11968  fzosubel2  11971  eluzgtdifelfzo  11973  fzocatel  11975  elfzom1elp1fzo  11978  fzval3  11980  zpnn0elfzo1  11984  fzosplitprm1  12015  fzoshftral  12019  flzadd  12056  ceilid  12075  quoremz  12079  intfracq  12083  mulmod0  12101  zmod10  12110  modcyc  12129  modcyc2  12130  muladdmodid  12134  modmul1  12140  modaddmulmod  12153  uzrdgxfr  12177  fzen2  12179  seqshft2  12236  sermono  12242  m1expeven  12316  expsub  12317  zesq  12392  modexp  12404  bccmpl  12491  swrd00  12759  addlenrevswrd  12778  swrdswrd  12801  swrdswrd0  12803  swrdccatin12lem1  12825  swrdccatin12lem2b  12827  swrdccatin2  12828  swrdccatin12lem2  12830  swrdccatin12  12832  repswrevw  12874  cshwsublen  12883  cshwidx0mod  12891  2cshw  12897  2cshwid  12898  2cshwcom  12900  cshweqdif2  12903  cshweqrep  12905  cshw1  12906  2cshwcshw  12909  shftuz  13111  seqshft  13127  nn0abscl  13354  nnabscl  13367  climshftlem  13616  climshft  13618  isershft  13705  mptfzshft  13817  fsumrev  13818  fsum0diag2  13822  efexp  14133  efzval  14134  demoivre  14232  znnenlem  14242  sqrt2irr  14279  dvdsval2  14286  iddvds  14294  1dvds  14295  dvds0  14296  negdvdsb  14297  dvdsnegb  14298  0dvds  14301  dvdsmul1  14302  iddvdsexp  14304  muldvds1  14305  muldvds2  14306  dvdscmul  14307  dvdsmulc  14308  dvdscmulr  14309  dvdsmulcr  14310  dvds2ln  14311  dvds2add  14312  dvds2sub  14313  dvdstr  14315  dvdssub2  14320  dvdsadd  14321  dvdsaddr  14322  dvdssub  14323  dvdssubr  14324  dvdsadd2b  14325  alzdvds  14333  mulmoddvds  14341  odd2np1lem  14342  odd2np1  14343  oddp1even  14345  fproddvdsd  14348  divalglem0  14349  divalglem2  14351  divalglem4  14352  divalglem5  14353  divalglem9  14357  divalgb  14360  divalgmod  14362  ndvdssub  14363  ndvdsadd  14364  bits0  14376  bitsp1e  14380  bitsp1o  14381  gcdneg  14464  gcdaddmlem  14466  gcdaddm  14467  gcdadd  14468  gcdid  14469  modgcd  14474  bezoutlem1  14477  bezoutlem2  14478  bezoutlem4  14480  dvdsgcd  14482  mulgcd  14485  absmulgcd  14486  mulgcdr  14487  gcddiv  14488  gcdmultiplez  14490  dvdssqim  14492  dvdssq  14499  lcmcllem  14532  lcmneg  14539  lcmgcdlem  14542  lcmgcd  14543  lcmid  14545  lcm1  14546  coprmdvds  14630  coprmdvds2  14631  qredeq  14634  qredeu  14635  prmdvdsexp  14638  rpexp1i  14644  divnumden  14668  zsqrtelqelz  14678  phiprmpw  14693  vfermltlALT  14716  nnnn0modprm0  14720  modprmn0modprm0  14721  coprimeprodsq2  14723  opoe  14724  omoe  14725  opeo  14726  omeo  14727  iserodd  14748  pclem  14751  pcprendvds2  14754  pcpremul  14756  pcmul  14764  pcneg  14786  fldivp1  14805  prmpwdvds  14811  zgz  14840  modxai  15003  mod2xnegi  15006  mulgz  16730  odmod  17137  odf1  17151  odf1o1  17159  gexdvds  17171  zaddablx  17443  cygabl  17460  ablfacrp  17634  pgpfac1lem3  17645  zsubrg  18956  zsssubrg  18961  zringmulg  18981  zringcyg  18991  zringinvg  18992  zringunit  18993  prmirred  18997  mulgrhm2  19001  znunit  19065  degltp1le  22899  ef2kpi  23298  efper  23299  sinperlem  23300  sin2kpi  23303  cos2kpi  23304  abssinper  23338  sinkpi  23339  coskpi  23340  eflogeq  23416  cxpexpz  23477  root1eq1  23560  cxpeq  23562  relogbexp  23582  leibpilem1  23731  sgmval2  23933  ppiprm  23941  ppinprm  23942  chtprm  23943  chtnprm  23944  lgslem3  24089  lgsneg  24110  lgsdir2lem2  24115  lgsdir2lem4  24117  lgsdir2  24119  lgsdirnn0  24130  lgsquadlem1  24145  lgsquadlem2  24146  lgsquad2  24151  2sqlem2  24155  2sqlem7  24161  rplogsumlem2  24186  axlowdimlem13  24830  wlkdvspthlem  25182  clwwisshclwwlem1  25378  gxneg  25839  gxsuc  25845  gxnn0add  25847  gxadd  25848  gxsub  25849  gxnn0mul  25850  gxmul  25851  zaddsubgo  25927  ipasslem5  26321  rearchi  28444  pdivsq  30172  dvdspw  30173  poimirlem19  31663  itg2addnclem2  31698  lzenom  35321  rexzrexnn0  35356  pell1234qrne0  35407  pell1234qrreccl  35408  pell1234qrmulcl  35409  pell1234qrdich  35415  pell14qrdich  35423  reglogexp  35448  reglogexpbas  35451  rmxm1  35488  rmym1  35489  rmxdbl  35493  rmydbl  35494  jm2.24  35519  congtr  35521  congadd  35522  congmul  35523  congsym  35524  congneg  35525  congid  35527  congabseq  35530  acongsym  35532  acongneg2  35533  acongtr  35534  acongrep  35536  bezoutr1  35542  dvdsabsmod0OLD  35547  jm2.19lem3  35552  jm2.19lem4  35553  jm2.19  35554  jm2.25  35560  jm2.26a  35561  oddfl  37096  coskpi2  37313  cosknegpi  37316  dvdsn1add  37383  itgsinexp  37400  fourierdlem42  37580  fourierdlem97  37635  fourierswlem  37662  mod2eq1n2dvds  38124  elmod2OLD  38125  zob  38162  dfodd6  38166  dfeven4  38167  evenm1odd  38168  evenp1odd  38169  enege  38174  onego  38175  dfeven2  38178  bits0ALTV  38207  opoeALTV  38211  opeoALTV  38212  evensumeven  38233  bgoldbwt  38277  nnsum3primesgbe  38286  proththd  38313  addlenrevpfx  38337  pfxccatin12lem1  38363  pfxccatin12lem2  38364  pfxccatin12  38365  2elfz2melfz  38416  0nodd  38577  2nodd  38579  1neven  38699  2zlidl  38701  2zrngamgm  38706  2zrngasgrp  38707  2zrngagrp  38710  2zrngmmgm  38713  2zrngmsgrp  38714  2zrngnmrid  38717  zlmodzxzsub  38910  flsubz  39090  mod0mul  39092  m1modmmod  39094  zofldiv2  39108  dignn0flhalflem1  39196  dignn0flhalflem2  39197
  Copyright terms: Public domain W3C validator