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 9611 1  |-  ( N  e.  ZZ  ->  N  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823   CCcc 9479   ZZcz 10860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-resscn 9538
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273  df-neg 9799  df-z 10861
This theorem is referenced by:  zsscn  10868  zsubcl  10902  zrevaddcl  10905  zlem1lt  10911  zltlem1  10912  zdiv  10929  zdivadd  10930  zdivmul  10931  zextlt  10933  zneo  10941  zeo2  10945  peano5uzi  10947  uzindOLD  10953  zindd  10961  znnn0nn  10972  zriotaneg  10974  zmax  11180  rebtwnz  11182  qmulz  11186  zq  11189  qaddcl  11199  qnegcl  11200  qmulcl  11201  qreccl  11203  fzen  11706  uzsubsubfz  11710  fz01en  11716  fzmmmeqm  11721  fzsubel  11723  fztp  11740  fzsuc2  11741  fzrev2  11747  fzrev3  11749  elfzp1b  11759  fzrevral  11767  fzrevral2  11768  fzrevral3  11769  fzshftral  11770  fzo0addel  11851  fzo0addelr  11852  fzoaddel2  11853  elfzoext  11854  fzosubel2  11857  eluzgtdifelfzo  11859  fzocatel  11861  elfzom1elp1fzo  11864  fzval3  11866  zpnn0elfzo1  11870  fzosplitprm1  11900  fzoshftral  11904  flzadd  11941  ceilid  11960  quoremz  11964  intfracq  11968  zmod10  11994  modcyc  12013  modcyc2  12014  modmul1  12022  modaddmulmod  12035  uzrdgxfr  12059  fzen2  12061  seqshft2  12115  sermono  12121  expsub  12195  zesq  12271  modexp  12283  bccmpl  12369  swrd00  12634  addlenrevswrd  12653  swrdswrd  12676  swrdswrd0  12678  swrdccatin12lem1  12700  swrdccatin12lem2b  12702  swrdccatin2  12703  swrdccatin12lem2  12705  swrdccatin12  12707  repswrevw  12749  cshwsublen  12758  cshwidx0mod  12766  2cshw  12772  2cshwid  12773  2cshwcom  12775  cshweqdif2  12778  cshweqrep  12780  cshw1  12781  2cshwcshw  12784  shftuz  12984  seqshft  13000  nn0abscl  13227  nnabscl  13240  climshftlem  13479  climshft  13481  isershft  13568  mptfzshft  13675  fsumrev  13676  fsum0diag2  13680  efexp  13918  efzval  13919  demoivre  14017  znnenlem  14029  sqrt2irr  14066  dvdsval2  14073  iddvds  14081  1dvds  14082  dvds0  14083  negdvdsb  14084  dvdsnegb  14085  0dvds  14088  dvdsmul1  14089  iddvdsexp  14091  muldvds1  14092  muldvds2  14093  dvdscmul  14094  dvdsmulc  14095  dvdscmulr  14096  dvdsmulcr  14097  dvds2ln  14098  dvds2add  14099  dvds2sub  14100  dvdstr  14102  dvdssub2  14107  dvdsadd  14108  dvdsaddr  14109  dvdssub  14110  dvdssubr  14111  dvdsadd2b  14112  alzdvds  14120  mulmoddvds  14128  odd2np1lem  14129  odd2np1  14130  oddp1even  14132  divalglem0  14135  divalglem2  14137  divalglem4  14138  divalglem5  14139  divalglem9  14143  divalgb  14146  divalgmod  14148  ndvdssub  14149  ndvdsadd  14150  bits0  14162  bitsp1e  14166  bitsp1o  14167  gcdneg  14248  gcdaddmlem  14250  gcdaddm  14251  gcdadd  14252  gcdid  14253  modgcd  14258  bezoutlem1  14260  bezoutlem2  14261  bezoutlem4  14263  dvdsgcd  14265  mulgcd  14268  absmulgcd  14269  mulgcdr  14270  gcddiv  14271  gcdmultiplez  14273  dvdssqim  14275  dvdssq  14282  coprmdvds  14327  coprmdvds2  14328  qredeq  14331  qredeu  14332  prmdvdsexp  14339  rpexp1i  14346  divnumden  14365  zsqrtelqelz  14375  phiprmpw  14390  nnnn0modprm0  14415  modprmn0modprm0  14416  coprimeprodsq2  14418  opoe  14419  omoe  14420  opeo  14421  omeo  14422  iserodd  14443  pclem  14446  pcprendvds2  14449  pcpremul  14451  pcmul  14459  pcneg  14481  fldivp1  14500  prmpwdvds  14506  zgz  14535  modxai  14638  mod2xnegi  14641  mulgz  16362  odmod  16769  odf1  16783  odf1o1  16791  gexdvds  16803  zaddablx  17075  cygabl  17092  ablfacrp  17312  pgpfac1lem3  17323  zsubrg  18666  zsssubrg  18671  zringmulg  18691  zringcyg  18701  zringinvg  18702  zringunit  18703  prmirred  18707  mulgrhm2  18711  znunit  18775  degltp1le  22639  ef2kpi  23037  efper  23038  sinperlem  23039  sin2kpi  23042  cos2kpi  23043  abssinper  23077  sinkpi  23078  coskpi  23079  eflogeq  23155  cxpexpz  23216  root1eq1  23297  cxpeq  23299  relogbexp  23319  leibpilem1  23468  sgmval2  23615  ppiprm  23623  ppinprm  23624  chtprm  23625  chtnprm  23626  lgslem3  23771  lgsneg  23792  lgsdir2lem2  23797  lgsdir2lem4  23799  lgsdir2  23801  lgsdirnn0  23812  lgsquadlem1  23827  lgsquadlem2  23828  lgsquad2  23833  2sqlem2  23837  2sqlem7  23843  rplogsumlem2  23868  axlowdimlem13  24459  wlkdvspthlem  24811  clwwisshclwwlem1  25007  gxneg  25466  gxsuc  25472  gxnn0add  25474  gxadd  25475  gxsub  25476  gxnn0mul  25477  gxmul  25478  zaddsubgo  25554  ipasslem5  25948  rearchi  28067  m1expevenALT  28927  pdivsq  29415  dvdspw  29416  itg2addnclem2  30307  lzenom  30942  rexzrexnn0  30977  pell1234qrne0  31028  pell1234qrreccl  31029  pell1234qrmulcl  31030  pell1234qrdich  31036  pell14qrdich  31044  reglogexp  31069  reglogexpbas  31072  rmxm1  31109  rmym1  31110  rmxdbl  31114  rmydbl  31115  jm2.24  31140  congtr  31142  congadd  31143  congmul  31144  congsym  31145  congneg  31146  congid  31148  congabseq  31151  acongsym  31153  acongneg2  31154  acongtr  31155  acongrep  31157  bezoutr1  31163  dvdsabsmod0  31167  jm2.19lem3  31172  jm2.19lem4  31173  jm2.19  31174  jm2.25  31180  jm2.26a  31181  lcmcllem  31443  lcmneg  31450  lcmgcdlem  31453  lcmgcd  31454  lcmid  31456  oddfl  31699  coskpi2  31905  cosknegpi  31908  dvdsn1add  31975  itgsinexp  31992  fourierdlem42  32170  fourierdlem97  32225  fourierswlem  32252  mod2eq1n2dvds  32534  elmod2  32535  zob  32548  dfodd6  32552  dfeven4  32553  evenm1odd  32554  evenp1odd  32555  enege  32559  onego  32560  dfeven2  32561  bits0ALTV  32585  opoeALTV  32589  opeoALTV  32590  addlenrevpfx  32625  pfxccatin12lem1  32651  pfxccatin12lem2  32652  pfxccatin12  32653  2elfz2melfz  32708  0nodd  32870  2nodd  32872  1neven  32992  2zlidl  32994  2zrngamgm  32999  2zrngasgrp  33000  2zrngagrp  33003  2zrngmmgm  33006  2zrngmsgrp  33007  2zrngnmrid  33010  zlmodzxzsub  33203  flsubz  33384  mod0mul  33386  m1modmmod  33388  zofldiv2  33402  dignn0flhalflem1  33490  dignn0flhalflem2  33491
  Copyright terms: Public domain W3C validator