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

Theorem zcn 10639
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 10638 . 2  |-  ( N  e.  ZZ  ->  N  e.  RR )
21recnd 9400 1  |-  ( N  e.  ZZ  ->  N  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   CCcc 9268   ZZcz 10634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-resscn 9327
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083  df-neg 9586  df-z 10635
This theorem is referenced by:  zsscn  10642  zsubcl  10675  zrevaddcl  10678  zlem1lt  10684  zltlem1  10685  zdiv  10700  zdivadd  10701  zdivmul  10702  zextlt  10704  zneo  10712  zeo2  10716  peano5uzi  10718  uzindOLD  10724  zindd  10731  zriotaneg  10742  zmax  10938  rebtwnz  10940  qmulz  10944  zq  10947  qaddcl  10957  qnegcl  10958  qmulcl  10959  qreccl  10961  fzen  11454  uzsubsubfz  11458  fz01en  11464  fzmmmeqm  11479  fzsubel  11481  fztp  11497  fzsuc2  11499  fzrev2  11504  fzrev3  11506  elfzp1b  11521  fzrevral  11528  fzrevral2  11529  fzrevral3  11530  fzshftral  11531  fzoaddel2  11582  fzosubel2  11584  fzocatel  11586  fzval3  11589  fzoshftral  11620  flzadd  11655  ceilid  11674  quoremz  11678  intfracq  11682  zmod10  11708  modcyc  11727  modcyc2  11728  modmul1  11736  modaddmulmod  11749  uzrdgxfr  11773  fzen2  11775  seqshft2  11816  sermono  11822  expsub  11895  zesq  11971  modexp  11983  bccmpl  12069  swrd00  12298  addlenrevswrd  12314  swrdswrd  12338  swrdswrd0  12340  swrdccatin12lem1  12359  swrdccatin12lem2b  12361  swrdccatin2  12362  swrdccatin12lem2  12364  swrdccatin12  12366  repswrevw  12408  cshwsublen  12417  cshwidx0mod  12425  2cshw  12431  2cshwid  12432  2cshwcom  12434  cshweqdif2  12437  cshweqrep  12439  cshw1  12440  shftuz  12542  seqshft  12558  nn0abscl  12785  nnabscl  12797  climshftlem  13036  climshft  13038  isershft  13125  fsumrev  13229  fsumshft  13230  fsum0diag2  13233  efexp  13368  efzval  13369  demoivre  13467  znnenlem  13477  sqr2irr  13514  dvdsval2  13521  iddvds  13529  1dvds  13530  dvds0  13531  negdvdsb  13532  dvdsnegb  13533  0dvds  13536  dvdsmul1  13537  iddvdsexp  13539  muldvds1  13540  muldvds2  13541  dvdscmul  13542  dvdsmulc  13543  dvdscmulr  13544  dvdsmulcr  13545  dvds2ln  13546  dvds2add  13547  dvds2sub  13548  dvdstr  13549  dvdssub2  13553  dvdsadd  13554  dvdsaddr  13555  dvdssub  13556  dvdssubr  13557  dvdsadd2b  13558  alzdvds  13566  odd2np1lem  13574  odd2np1  13575  oddp1even  13577  divalglem0  13580  divalglem2  13582  divalglem4  13583  divalglem5  13584  divalglem9  13588  divalgb  13591  divalgmod  13593  ndvdssub  13594  ndvdsadd  13595  bits0  13607  bitsp1e  13611  bitsp1o  13612  gcdneg  13693  gcdaddmlem  13695  gcdaddm  13696  gcdadd  13697  gcdid  13698  modgcd  13703  bezoutlem1  13705  bezoutlem2  13706  bezoutlem4  13708  dvdsgcd  13710  mulgcd  13713  absmulgcd  13714  mulgcdr  13715  gcddiv  13716  gcdmultiplez  13718  dvdssqim  13720  dvdssq  13727  coprmdvds  13771  coprmdvds2  13772  qredeq  13775  qredeu  13776  prmdvdsexp  13783  rpexp1i  13790  divnumden  13809  zsqrelqelz  13819  phiprmpw  13834  nnnn0modprm0  13857  modprmn0modprm0  13858  coprimeprodsq2  13860  opoe  13861  omoe  13862  opeo  13863  omeo  13864  iserodd  13885  pclem  13888  pcprendvds2  13891  pcpremul  13893  pcmul  13901  pcneg  13923  fldivp1  13942  prmpwdvds  13948  zgz  13977  modxai  14080  mod2xnegi  14083  mulgz  15628  odmod  16029  odf1  16043  odf1o1  16051  gexdvds  16063  zaddablx  16330  cygabl  16347  ablfacrp  16541  pgpfac1lem3  16552  zsubrg  17710  zsssubrg  17715  zringmulg  17733  zrngmulg  17739  zringcyg  17749  zcyg  17754  zringinvg  17755  zringunit  17756  zrngunit  17757  prmirred  17761  prmirredOLD  17764  mulgrhm2  17769  mulgrhm2OLD  17772  znunit  17838  degltp1le  21429  ef2kpi  21825  efper  21826  sinperlem  21827  sin2kpi  21830  cos2kpi  21831  abssinper  21865  sinkpi  21866  coskpi  21867  eflogeq  21935  cxpexpz  21997  root1eq1  22078  cxpeq  22080  leibpilem1  22220  sgmval2  22366  ppiprm  22374  ppinprm  22375  chtprm  22376  chtnprm  22377  lgslem3  22522  lgsneg  22543  lgsdir2lem2  22548  lgsdir2lem4  22550  lgsdir2  22552  lgsdirnn0  22563  lgsquadlem1  22578  lgsquadlem2  22579  lgsquad2  22584  2sqlem2  22588  2sqlem7  22594  rplogsumlem2  22619  axlowdimlem13  23023  wlkdvspthlem  23329  gxneg  23576  gxsuc  23582  gxnn0add  23584  gxadd  23585  gxsub  23586  gxnn0mul  23587  gxmul  23588  zaddsubgo  23664  ipasslem5  24058  rearchi  26164  m1expevenALT  26955  pdivsq  27402  dvdspw  27403  itg2addnclem2  28288  lzenom  28953  rexzrexnn0  28987  pell1234qrne0  29039  pell1234qrreccl  29040  pell1234qrmulcl  29041  pell1234qrdich  29047  pell14qrdich  29055  reglogexp  29080  reglogexpbas  29083  rmxm1  29120  rmym1  29121  rmxdbl  29125  rmydbl  29126  jm2.24  29151  congtr  29153  congadd  29154  congmul  29155  congsym  29156  congneg  29157  congid  29159  congabseq  29162  acongsym  29164  acongneg2  29165  acongtr  29166  acongrep  29168  bezoutr1  29174  dvdsabsmod0  29180  jm2.19lem3  29185  jm2.19lem4  29186  jm2.19  29187  jm2.25  29193  jm2.26a  29194  itgsinexp  29641  2elfz2melfz  30048  eluzgtdifelfzo  30065  zpnn0elfzo1  30068  fzosplitprm1  30070  mulmoddvds  30092  clwwisshclwwlem1  30315  cshwlemma1  30335  zlmodzxzsub  30591
  Copyright terms: Public domain W3C validator