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

Theorem zcn 10865
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 10864 . 2  |-  ( N  e.  ZZ  ->  N  e.  RR )
21recnd 9618 1  |-  ( N  e.  ZZ  ->  N  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   CCcc 9486   ZZcz 10860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-resscn 9545
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5549  df-fv 5594  df-ov 6285  df-neg 9804  df-z 10861
This theorem is referenced by:  zsscn  10868  zsubcl  10901  zrevaddcl  10904  zlem1lt  10910  zltlem1  10911  zdiv  10927  zdivadd  10928  zdivmul  10929  zextlt  10931  zneo  10939  zeo2  10943  peano5uzi  10945  uzindOLD  10951  zindd  10958  zriotaneg  10970  zmax  11175  rebtwnz  11177  qmulz  11181  zq  11184  qaddcl  11194  qnegcl  11195  qmulcl  11196  qreccl  11198  fzen  11699  uzsubsubfz  11703  fz01en  11709  fzmmmeqm  11713  fzsubel  11715  fztp  11732  fzsuc2  11733  fzrev2  11739  fzrev3  11741  elfzp1b  11751  fzrevral  11758  fzrevral2  11759  fzrevral3  11760  fzshftral  11761  fzoaddel2  11838  fzosubel2  11840  eluzgtdifelfzo  11842  fzocatel  11844  elfzom1elp1fzo  11847  fzval3  11849  zpnn0elfzo1  11853  fzosplitprm1  11883  fzoshftral  11887  flzadd  11923  ceilid  11942  quoremz  11946  intfracq  11950  zmod10  11976  modcyc  11995  modcyc2  11996  modmul1  12004  modaddmulmod  12017  uzrdgxfr  12041  fzen2  12043  seqshft2  12097  sermono  12103  expsub  12177  zesq  12253  modexp  12265  bccmpl  12351  swrd00  12604  addlenrevswrd  12620  swrdswrd  12644  swrdswrd0  12646  swrdccatin12lem1  12668  swrdccatin12lem2b  12670  swrdccatin2  12671  swrdccatin12lem2  12673  swrdccatin12  12675  repswrevw  12717  cshwsublen  12726  cshwidx0mod  12734  2cshw  12740  2cshwid  12741  2cshwcom  12743  cshweqdif2  12746  cshweqrep  12748  cshw1  12749  2cshwcshw  12752  shftuz  12861  seqshft  12877  nn0abscl  13104  nnabscl  13117  climshftlem  13356  climshft  13358  isershft  13445  mptfzshft  13552  fsumrev  13553  fsum0diag2  13557  efexp  13693  efzval  13694  demoivre  13792  znnenlem  13802  sqrt2irr  13839  dvdsval2  13846  iddvds  13854  1dvds  13855  dvds0  13856  negdvdsb  13857  dvdsnegb  13858  0dvds  13861  dvdsmul1  13862  iddvdsexp  13864  muldvds1  13865  muldvds2  13866  dvdscmul  13867  dvdsmulc  13868  dvdscmulr  13869  dvdsmulcr  13870  dvds2ln  13871  dvds2add  13872  dvds2sub  13873  dvdstr  13874  dvdssub2  13878  dvdsadd  13879  dvdsaddr  13880  dvdssub  13881  dvdssubr  13882  dvdsadd2b  13883  alzdvds  13891  mulmoddvds  13899  odd2np1lem  13900  odd2np1  13901  oddp1even  13903  divalglem0  13906  divalglem2  13908  divalglem4  13909  divalglem5  13910  divalglem9  13914  divalgb  13917  divalgmod  13919  ndvdssub  13920  ndvdsadd  13921  bits0  13933  bitsp1e  13937  bitsp1o  13938  gcdneg  14019  gcdaddmlem  14021  gcdaddm  14022  gcdadd  14023  gcdid  14024  modgcd  14029  bezoutlem1  14031  bezoutlem2  14032  bezoutlem4  14034  dvdsgcd  14036  mulgcd  14039  absmulgcd  14040  mulgcdr  14041  gcddiv  14042  gcdmultiplez  14044  dvdssqim  14046  dvdssq  14053  coprmdvds  14098  coprmdvds2  14099  qredeq  14102  qredeu  14103  prmdvdsexp  14110  rpexp1i  14117  divnumden  14136  zsqrtelqelz  14146  phiprmpw  14161  nnnn0modprm0  14186  modprmn0modprm0  14187  coprimeprodsq2  14189  opoe  14190  omoe  14191  opeo  14192  omeo  14193  iserodd  14214  pclem  14217  pcprendvds2  14220  pcpremul  14222  pcmul  14230  pcneg  14252  fldivp1  14271  prmpwdvds  14277  zgz  14306  modxai  14409  mod2xnegi  14412  mulgz  15963  odmod  16366  odf1  16380  odf1o1  16388  gexdvds  16400  zaddablx  16667  cygabl  16684  ablfacrp  16907  pgpfac1lem3  16918  zsubrg  18239  zsssubrg  18244  zringmulg  18264  zrngmulg  18270  zringcyg  18280  zcyg  18285  zringinvg  18286  zringunit  18287  zrngunit  18288  prmirred  18292  prmirredOLD  18295  mulgrhm2  18300  mulgrhm2OLD  18303  znunit  18369  degltp1le  22208  ef2kpi  22604  efper  22605  sinperlem  22606  sin2kpi  22609  cos2kpi  22610  abssinper  22644  sinkpi  22645  coskpi  22646  eflogeq  22714  cxpexpz  22776  root1eq1  22857  cxpeq  22859  leibpilem1  22999  sgmval2  23145  ppiprm  23153  ppinprm  23154  chtprm  23155  chtnprm  23156  lgslem3  23301  lgsneg  23322  lgsdir2lem2  23327  lgsdir2lem4  23329  lgsdir2  23331  lgsdirnn0  23342  lgsquadlem1  23357  lgsquadlem2  23358  lgsquad2  23363  2sqlem2  23367  2sqlem7  23373  rplogsumlem2  23398  axlowdimlem13  23933  wlkdvspthlem  24285  clwwisshclwwlem1  24481  gxneg  24944  gxsuc  24950  gxnn0add  24952  gxadd  24953  gxsub  24954  gxnn0mul  24955  gxmul  24956  zaddsubgo  25032  ipasslem5  25426  rearchi  27495  m1expevenALT  28303  pdivsq  28751  dvdspw  28752  itg2addnclem2  29644  lzenom  30307  rexzrexnn0  30341  pell1234qrne0  30393  pell1234qrreccl  30394  pell1234qrmulcl  30395  pell1234qrdich  30401  pell14qrdich  30409  reglogexp  30434  reglogexpbas  30437  rmxm1  30474  rmym1  30475  rmxdbl  30479  rmydbl  30480  jm2.24  30505  congtr  30507  congadd  30508  congmul  30509  congsym  30510  congneg  30511  congid  30513  congabseq  30516  acongsym  30518  acongneg2  30519  acongtr  30520  acongrep  30522  bezoutr1  30528  dvdsabsmod0  30532  jm2.19lem3  30537  jm2.19lem4  30538  jm2.19  30539  jm2.25  30545  jm2.26a  30546  lcmcllem  30802  lcmneg  30809  lcmgcdlem  30812  lcmgcd  30813  lcmid  30815  znnn0nn  31066  coskpi2  31202  cosknegpi  31205  itgsinexp  31272  dirkertrigeq  31401  fourierswlem  31531  2elfz2melfz  31803  zlmodzxzsub  32013
  Copyright terms: Public domain W3C validator