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

Theorem zcn 10045
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 10044 . 2  |-  ( N  e.  ZZ  ->  N  e.  RR )
21recnd 8877 1  |-  ( N  e.  ZZ  ->  N  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   CCcc 8751   ZZcz 10040
This theorem is referenced by:  zsscn  10048  zsubcl  10077  zrevaddcl  10079  zlem1lt  10085  zltlem1  10086  zdiv  10098  zdivadd  10099  zdivmul  10100  zextlt  10102  zneo  10110  zeo2  10114  peano5uzi  10116  uzindOLD  10122  zindd  10129  zmax  10329  rebtwnz  10331  qmulz  10335  zq  10338  qaddcl  10348  qnegcl  10349  qmulcl  10350  qreccl  10352  fzen  10827  fz01en  10834  fzsubel  10843  fztp  10857  fzsuc2  10858  fzrev2  10863  fzrev3  10865  fzrevral  10882  fzrevral2  10883  fzrevral3  10884  fzshftral  10885  fzoaddel2  10923  fzosubel2  10925  fzval3  10927  flzadd  10967  quoremz  10975  intfracq  10979  zmod10  11003  modcyc  11015  modcyc2  11016  modmul1  11018  uzrdgxfr  11045  fzen2  11047  seqshft2  11088  sermono  11094  expsub  11165  zesq  11240  modexp  11252  bccmpl  11338  swrd00  11467  shftuz  11580  seqshft  11596  nn0abscl  11813  nnabscl  11825  climshftlem  12064  climshft  12066  isershft  12153  fsumrev  12257  fsumshft  12258  fsum0diag2  12261  efexp  12397  efzval  12398  demoivre  12496  znnenlem  12506  sqr2irr  12543  dvdsval2  12550  iddvds  12558  1dvds  12559  dvds0  12560  negdvdsb  12561  dvdsnegb  12562  0dvds  12565  dvdsmul1  12566  iddvdsexp  12568  muldvds1  12569  muldvds2  12570  dvdscmul  12571  dvdsmulc  12572  dvdscmulr  12573  dvdsmulcr  12574  dvds2ln  12575  dvds2add  12576  dvds2sub  12577  dvdstr  12578  dvdssub2  12582  dvdsadd  12583  dvdsaddr  12584  dvdssub  12585  dvdssubr  12586  dvdsadd2b  12587  alzdvds  12594  odd2np1lem  12602  odd2np1  12603  oddp1even  12605  divalglem0  12608  divalglem2  12610  divalglem4  12611  divalglem5  12612  divalglem9  12616  divalgb  12619  divalgmod  12621  ndvdssub  12622  ndvdsadd  12623  bits0  12635  bitsp1e  12639  bitsp1o  12640  gcdneg  12721  gcdaddmlem  12723  gcdaddm  12724  gcdadd  12725  gcdid  12726  modgcd  12731  bezoutlem1  12733  bezoutlem2  12734  bezoutlem4  12736  dvdsgcd  12738  mulgcd  12741  absmulgcd  12742  mulgcdr  12743  gcddiv  12744  gcdmultiplez  12746  dvdssqim  12748  dvdssq  12755  coprmdvds  12797  coprmdvds2  12798  qredeq  12801  qredeu  12802  prmdvdsexp  12809  rpexp1i  12816  divnumden  12835  zsqrelqelz  12845  phiprmpw  12860  coprimeprodsq2  12879  opoe  12880  omoe  12881  opeo  12882  omeo  12883  iserodd  12904  pclem  12907  pcprendvds2  12910  pcpremul  12912  pcmul  12920  pcneg  12942  fldivp1  12961  prmpwdvds  12967  zgz  12996  modxai  13099  mod2xnegi  13102  mulgz  14604  odmod  14877  odf1  14891  odf1o1  14899  gexdvds  14911  zaddablx  15176  cygabl  15193  ablfacrp  15317  pgpfac1lem3  15328  zsubrg  16441  zsssubrg  16446  zrngunit  16454  zcyg  16461  prmirred  16464  mulgrhm2  16477  znunit  16533  degltp1le  19475  ef2kpi  19862  efper  19863  sinperlem  19864  sin2kpi  19867  cos2kpi  19868  abssinper  19902  sinkpi  19903  coskpi  19904  eflogeq  19971  cxpexpz  20030  root1eq1  20111  cxpeq  20113  leibpilem1  20252  sgmval2  20397  ppiprm  20405  ppinprm  20406  chtprm  20407  chtnprm  20408  lgslem3  20553  lgsneg  20574  lgsdir2lem2  20579  lgsdir2lem4  20581  lgsdir2  20583  lgsdirnn0  20594  lgsquadlem1  20609  lgsquadlem2  20610  lgsquad2  20615  2sqlem2  20619  2sqlem7  20625  rplogsumlem2  20650  gxneg  20949  gxsuc  20955  gxnn0add  20957  gxadd  20958  gxsub  20959  gxnn0mul  20960  gxmul  20961  zaddsubgo  21037  ipasslem5  21429  elfzp1b  24027  pdivsq  24172  dvdspw  24173  axlowdimlem13  24653  itg2addnclem2  25003  lzenom  26951  rexzrexnn0  26987  pell1234qrne0  27040  pell1234qrreccl  27041  pell1234qrmulcl  27042  pell1234qrdich  27048  pell14qrdich  27056  reglogexp  27081  reglogexpbas  27084  rmxm1  27121  rmym1  27122  rmxdbl  27126  rmydbl  27127  jm2.24  27152  congtr  27154  congadd  27155  congmul  27156  congsym  27157  congneg  27158  congid  27160  congabseq  27163  acongsym  27165  acongneg2  27166  acongtr  27167  acongrep  27169  bezoutr1  27175  dvdsabsmod0  27181  jm2.19lem3  27186  jm2.19lem4  27187  jm2.19  27188  jm2.25  27194  jm2.26a  27195  fmul01lt1lem2  27817  itgsinexp  27851  stoweidlem26  27877  wlkdvspthlem  28364
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-resscn 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-neg 9056  df-z 10041
  Copyright terms: Public domain W3C validator