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

Theorem zcn 10243
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 10242 . 2  |-  ( N  e.  ZZ  ->  N  e.  RR )
21recnd 9070 1  |-  ( N  e.  ZZ  ->  N  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   CCcc 8944   ZZcz 10238
This theorem is referenced by:  zsscn  10246  zsubcl  10275  zrevaddcl  10277  zlem1lt  10283  zltlem1  10284  zdiv  10296  zdivadd  10297  zdivmul  10298  zextlt  10300  zneo  10308  zeo2  10312  peano5uzi  10314  uzindOLD  10320  zindd  10327  zmax  10527  rebtwnz  10529  qmulz  10533  zq  10536  qaddcl  10546  qnegcl  10547  qmulcl  10548  qreccl  10550  fzen  11028  fz01en  11035  fzsubel  11044  fztp  11058  fzsuc2  11060  fzrev2  11065  fzrev3  11067  fzrevral  11086  fzrevral2  11087  fzrevral3  11088  fzshftral  11089  fzoaddel2  11131  fzosubel2  11133  fzval3  11135  flzadd  11183  quoremz  11191  intfracq  11195  zmod10  11219  modcyc  11231  modcyc2  11232  modmul1  11234  uzrdgxfr  11261  fzen2  11263  seqshft2  11304  sermono  11310  expsub  11382  zesq  11457  modexp  11469  bccmpl  11555  swrd00  11720  shftuz  11839  seqshft  11855  nn0abscl  12072  nnabscl  12084  climshftlem  12323  climshft  12325  isershft  12412  fsumrev  12517  fsumshft  12518  fsum0diag2  12521  efexp  12657  efzval  12658  demoivre  12756  znnenlem  12766  sqr2irr  12803  dvdsval2  12810  iddvds  12818  1dvds  12819  dvds0  12820  negdvdsb  12821  dvdsnegb  12822  0dvds  12825  dvdsmul1  12826  iddvdsexp  12828  muldvds1  12829  muldvds2  12830  dvdscmul  12831  dvdsmulc  12832  dvdscmulr  12833  dvdsmulcr  12834  dvds2ln  12835  dvds2add  12836  dvds2sub  12837  dvdstr  12838  dvdssub2  12842  dvdsadd  12843  dvdsaddr  12844  dvdssub  12845  dvdssubr  12846  dvdsadd2b  12847  alzdvds  12854  odd2np1lem  12862  odd2np1  12863  oddp1even  12865  divalglem0  12868  divalglem2  12870  divalglem4  12871  divalglem5  12872  divalglem9  12876  divalgb  12879  divalgmod  12881  ndvdssub  12882  ndvdsadd  12883  bits0  12895  bitsp1e  12899  bitsp1o  12900  gcdneg  12981  gcdaddmlem  12983  gcdaddm  12984  gcdadd  12985  gcdid  12986  modgcd  12991  bezoutlem1  12993  bezoutlem2  12994  bezoutlem4  12996  dvdsgcd  12998  mulgcd  13001  absmulgcd  13002  mulgcdr  13003  gcddiv  13004  gcdmultiplez  13006  dvdssqim  13008  dvdssq  13015  coprmdvds  13057  coprmdvds2  13058  qredeq  13061  qredeu  13062  prmdvdsexp  13069  rpexp1i  13076  divnumden  13095  zsqrelqelz  13105  phiprmpw  13120  coprimeprodsq2  13139  opoe  13140  omoe  13141  opeo  13142  omeo  13143  iserodd  13164  pclem  13167  pcprendvds2  13170  pcpremul  13172  pcmul  13180  pcneg  13202  fldivp1  13221  prmpwdvds  13227  zgz  13256  modxai  13359  mod2xnegi  13362  mulgz  14866  odmod  15139  odf1  15153  odf1o1  15161  gexdvds  15173  zaddablx  15438  cygabl  15455  ablfacrp  15579  pgpfac1lem3  15590  zsubrg  16707  zsssubrg  16712  zrngunit  16720  zcyg  16727  prmirred  16730  mulgrhm2  16743  znunit  16799  degltp1le  19949  ef2kpi  20339  efper  20340  sinperlem  20341  sin2kpi  20344  cos2kpi  20345  abssinper  20379  sinkpi  20380  coskpi  20381  eflogeq  20449  cxpexpz  20511  root1eq1  20592  cxpeq  20594  leibpilem1  20733  sgmval2  20879  ppiprm  20887  ppinprm  20888  chtprm  20889  chtnprm  20890  lgslem3  21035  lgsneg  21056  lgsdir2lem2  21061  lgsdir2lem4  21063  lgsdir2  21065  lgsdirnn0  21076  lgsquadlem1  21091  lgsquadlem2  21092  lgsquad2  21097  2sqlem2  21101  2sqlem7  21107  rplogsumlem2  21132  wlkdvspthlem  21560  gxneg  21807  gxsuc  21813  gxnn0add  21815  gxadd  21816  gxsub  21817  gxnn0mul  21818  gxmul  21819  zaddsubgo  21895  ipasslem5  22289  zzsmulg  24218  m1expevenALT  24858  elfzp1b  25069  pdivsq  25316  dvdspw  25317  axlowdimlem13  25797  itg2addnclem2  26156  lzenom  26718  rexzrexnn0  26754  pell1234qrne0  26806  pell1234qrreccl  26807  pell1234qrmulcl  26808  pell1234qrdich  26814  pell14qrdich  26822  reglogexp  26847  reglogexpbas  26850  rmxm1  26887  rmym1  26888  rmxdbl  26892  rmydbl  26893  jm2.24  26918  congtr  26920  congadd  26921  congmul  26922  congsym  26923  congneg  26924  congid  26926  congabseq  26929  acongsym  26931  acongneg2  26932  acongtr  26933  acongrep  26935  bezoutr1  26941  dvdsabsmod0  26947  jm2.19lem3  26952  jm2.19lem4  26953  jm2.19  26954  jm2.25  26960  jm2.26a  26961  itgsinexp  27616  ubmelfzo  27986  ubmelm1fzo  27987  addlenrevswrd  28004  swrd0swrd  28009  swrdswrd  28011  swrd0swrdid  28012  swrdswrd0  28013  swrdccatin2  28018  swrdccatin12lem2  28020  swrdccatin12lem3b  28022  swrdccatin12lem3  28024  swrdccatin12  28026  swrdccatin12b  28027  swrdccat3b  28031
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-resscn 9003
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-neg 9250  df-z 10239
  Copyright terms: Public domain W3C validator