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

Theorem zcn 10643
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 10642 . 2  |-  ( N  e.  ZZ  ->  N  e.  RR )
21recnd 9404 1  |-  ( N  e.  ZZ  ->  N  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   CCcc 9272   ZZcz 10638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-resscn 9331
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089  df-neg 9590  df-z 10639
This theorem is referenced by:  zsscn  10646  zsubcl  10679  zrevaddcl  10682  zlem1lt  10688  zltlem1  10689  zdiv  10704  zdivadd  10705  zdivmul  10706  zextlt  10708  zneo  10716  zeo2  10720  peano5uzi  10722  uzindOLD  10728  zindd  10735  zriotaneg  10746  zmax  10942  rebtwnz  10944  qmulz  10948  zq  10951  qaddcl  10961  qnegcl  10962  qmulcl  10963  qreccl  10965  fzen  11459  uzsubsubfz  11463  fz01en  11469  fzmmmeqm  11484  fzsubel  11486  fztp  11504  fzsuc2  11506  fzrev2  11512  fzrev3  11514  elfzp1b  11529  fzrevral  11536  fzrevral2  11537  fzrevral3  11538  fzshftral  11539  fzoaddel2  11590  fzosubel2  11592  fzocatel  11594  fzval3  11597  fzoshftral  11628  flzadd  11663  ceilid  11682  quoremz  11686  intfracq  11690  zmod10  11716  modcyc  11735  modcyc2  11736  modmul1  11744  modaddmulmod  11757  uzrdgxfr  11781  fzen2  11783  seqshft2  11824  sermono  11830  expsub  11903  zesq  11979  modexp  11991  bccmpl  12077  swrd00  12306  addlenrevswrd  12322  swrdswrd  12346  swrdswrd0  12348  swrdccatin12lem1  12367  swrdccatin12lem2b  12369  swrdccatin2  12370  swrdccatin12lem2  12372  swrdccatin12  12374  repswrevw  12416  cshwsublen  12425  cshwidx0mod  12433  2cshw  12439  2cshwid  12440  2cshwcom  12442  cshweqdif2  12445  cshweqrep  12447  cshw1  12448  shftuz  12550  seqshft  12566  nn0abscl  12793  nnabscl  12805  climshftlem  13044  climshft  13046  isershft  13133  mptfzshft  13237  fsumrev  13238  fsum0diag2  13242  efexp  13377  efzval  13378  demoivre  13476  znnenlem  13486  sqr2irr  13523  dvdsval2  13530  iddvds  13538  1dvds  13539  dvds0  13540  negdvdsb  13541  dvdsnegb  13542  0dvds  13545  dvdsmul1  13546  iddvdsexp  13548  muldvds1  13549  muldvds2  13550  dvdscmul  13551  dvdsmulc  13552  dvdscmulr  13553  dvdsmulcr  13554  dvds2ln  13555  dvds2add  13556  dvds2sub  13557  dvdstr  13558  dvdssub2  13562  dvdsadd  13563  dvdsaddr  13564  dvdssub  13565  dvdssubr  13566  dvdsadd2b  13567  alzdvds  13575  odd2np1lem  13583  odd2np1  13584  oddp1even  13586  divalglem0  13589  divalglem2  13591  divalglem4  13592  divalglem5  13593  divalglem9  13597  divalgb  13600  divalgmod  13602  ndvdssub  13603  ndvdsadd  13604  bits0  13616  bitsp1e  13620  bitsp1o  13621  gcdneg  13702  gcdaddmlem  13704  gcdaddm  13705  gcdadd  13706  gcdid  13707  modgcd  13712  bezoutlem1  13714  bezoutlem2  13715  bezoutlem4  13717  dvdsgcd  13719  mulgcd  13722  absmulgcd  13723  mulgcdr  13724  gcddiv  13725  gcdmultiplez  13727  dvdssqim  13729  dvdssq  13736  coprmdvds  13780  coprmdvds2  13781  qredeq  13784  qredeu  13785  prmdvdsexp  13792  rpexp1i  13799  divnumden  13818  zsqrelqelz  13828  phiprmpw  13843  nnnn0modprm0  13866  modprmn0modprm0  13867  coprimeprodsq2  13869  opoe  13870  omoe  13871  opeo  13872  omeo  13873  iserodd  13894  pclem  13897  pcprendvds2  13900  pcpremul  13902  pcmul  13910  pcneg  13932  fldivp1  13951  prmpwdvds  13957  zgz  13986  modxai  14089  mod2xnegi  14092  mulgz  15639  odmod  16040  odf1  16054  odf1o1  16062  gexdvds  16074  zaddablx  16341  cygabl  16358  ablfacrp  16555  pgpfac1lem3  16566  zsubrg  17841  zsssubrg  17846  zringmulg  17866  zrngmulg  17872  zringcyg  17882  zcyg  17887  zringinvg  17888  zringunit  17889  zrngunit  17890  prmirred  17894  prmirredOLD  17897  mulgrhm2  17902  mulgrhm2OLD  17905  znunit  17971  degltp1le  21519  ef2kpi  21915  efper  21916  sinperlem  21917  sin2kpi  21920  cos2kpi  21921  abssinper  21955  sinkpi  21956  coskpi  21957  eflogeq  22025  cxpexpz  22087  root1eq1  22168  cxpeq  22170  leibpilem1  22310  sgmval2  22456  ppiprm  22464  ppinprm  22465  chtprm  22466  chtnprm  22467  lgslem3  22612  lgsneg  22633  lgsdir2lem2  22638  lgsdir2lem4  22640  lgsdir2  22642  lgsdirnn0  22653  lgsquadlem1  22668  lgsquadlem2  22669  lgsquad2  22674  2sqlem2  22678  2sqlem7  22684  rplogsumlem2  22709  axlowdimlem13  23151  wlkdvspthlem  23457  gxneg  23704  gxsuc  23710  gxnn0add  23712  gxadd  23713  gxsub  23714  gxnn0mul  23715  gxmul  23716  zaddsubgo  23792  ipasslem5  24186  rearchi  26262  m1expevenALT  27059  pdivsq  27506  dvdspw  27507  itg2addnclem2  28397  lzenom  29061  rexzrexnn0  29095  pell1234qrne0  29147  pell1234qrreccl  29148  pell1234qrmulcl  29149  pell1234qrdich  29155  pell14qrdich  29163  reglogexp  29188  reglogexpbas  29191  rmxm1  29228  rmym1  29229  rmxdbl  29233  rmydbl  29234  jm2.24  29259  congtr  29261  congadd  29262  congmul  29263  congsym  29264  congneg  29265  congid  29267  congabseq  29270  acongsym  29272  acongneg2  29273  acongtr  29274  acongrep  29276  bezoutr1  29282  dvdsabsmod0  29288  jm2.19lem3  29293  jm2.19lem4  29294  jm2.19  29295  jm2.25  29301  jm2.26a  29302  itgsinexp  29748  2elfz2melfz  30155  eluzgtdifelfzo  30172  zpnn0elfzo1  30175  fzosplitprm1  30177  mulmoddvds  30199  clwwisshclwwlem1  30422  cshwlemma1  30442  zlmodzxzsub  30708
  Copyright terms: Public domain W3C validator