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

Theorem zcn 10955
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 10954 . 2  |-  ( N  e.  ZZ  ->  N  e.  RR )
21recnd 9682 1  |-  ( N  e.  ZZ  ->  N  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1873   CCcc 9550   ZZcz 10950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402  ax-resscn 9609
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rex 2782  df-rab 2785  df-v 3087  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3918  df-sn 4005  df-pr 4007  df-op 4011  df-uni 4226  df-br 4430  df-iota 5571  df-fv 5615  df-ov 6314  df-neg 9876  df-z 10951
This theorem is referenced by:  zsscn  10958  zsubcl  10992  zrevaddcl  10995  zlem1lt  11001  zltlem1  11002  zdiv  11019  zdivadd  11020  zdivmul  11021  zextlt  11023  zneo  11031  zeo2  11035  peano5uzi  11037  zindd  11049  znnn0nn  11060  zriotaneg  11062  zmax  11274  rebtwnz  11276  qmulz  11280  zq  11283  qaddcl  11293  qnegcl  11294  qmulcl  11295  qreccl  11297  fzen  11829  uzsubsubfz  11834  fz01en  11840  fzmmmeqm  11845  fzsubel  11847  fztp  11865  fzsuc2  11866  fzrev2  11872  fzrev3  11874  elfzp1b  11884  fzrevral  11892  fzrevral2  11893  fzrevral3  11894  fzshftral  11895  fzo0addel  11980  fzo0addelr  11981  fzoaddel2  11982  elfzoext  11983  fzosubel2  11986  eluzgtdifelfzo  11988  fzocatel  11990  elfzom1elp1fzo  11993  fzval3  11995  zpnn0elfzo1  11999  fzosplitprm1  12030  fzoshftral  12034  flzadd  12071  ceilid  12090  quoremz  12094  intfracq  12098  mulmod0  12116  zmod10  12125  modcyc  12144  modcyc2  12145  muladdmodid  12149  modmul1  12155  modaddmulmod  12168  uzrdgxfr  12192  fzen2  12194  seqshft2  12251  sermono  12257  m1expeven  12331  expsub  12332  zesq  12407  modexp  12419  bccmpl  12506  swrd00  12782  addlenrevswrd  12801  swrdswrd  12824  swrdswrd0  12826  swrdccatin12lem1  12848  swrdccatin12lem2b  12850  swrdccatin2  12851  swrdccatin12lem2  12853  swrdccatin12  12855  repswrevw  12897  cshwsublen  12906  cshwidx0mod  12914  2cshw  12920  2cshwid  12921  2cshwcom  12923  cshweqdif2  12926  cshweqrep  12928  cshw1  12929  2cshwcshw  12932  shftuz  13138  seqshft  13154  nn0abscl  13381  nnabscl  13394  climshftlem  13643  climshft  13645  isershft  13732  mptfzshft  13844  fsumrev  13845  fsum0diag2  13849  efexp  14160  efzval  14161  demoivre  14259  znnenlem  14269  sqrt2irr  14306  dvdsval2  14313  iddvds  14321  1dvds  14322  dvds0  14323  negdvdsb  14324  dvdsnegb  14325  0dvds  14328  dvdsmul1  14329  iddvdsexp  14331  muldvds1  14332  muldvds2  14333  dvdscmul  14334  dvdsmulc  14335  dvdscmulr  14336  dvdsmulcr  14337  dvds2ln  14338  dvds2add  14339  dvds2sub  14340  dvdstr  14342  dvdssub2  14347  dvdsadd  14348  dvdsaddr  14349  dvdssub  14350  dvdssubr  14351  dvdsadd2b  14352  alzdvds  14360  mulmoddvds  14368  odd2np1lem  14369  odd2np1  14370  oddp1even  14372  fproddvdsd  14375  divalglem0  14376  divalglem2  14378  divalglem2OLD  14379  divalglem4  14380  divalglem5OLD  14381  divalglem5  14382  divalglem9  14386  divalglem9OLD  14387  divalgb  14390  divalgmod  14392  ndvdssub  14393  ndvdsadd  14394  bits0  14406  bitsp1e  14410  bitsp1o  14411  gcdneg  14495  gcdaddmlem  14497  gcdaddm  14498  gcdadd  14499  gcdid  14500  modgcd  14505  bezoutlem1  14508  bezoutlem2OLD  14509  bezoutlem4OLD  14511  bezoutlem2  14512  bezoutlem4  14514  dvdsgcd  14516  mulgcd  14519  absmulgcd  14520  mulgcdr  14521  gcddiv  14522  gcdmultiplez  14524  dvdssqim  14526  dvdssq  14533  lcmcllem  14566  lcmneg  14573  lcmgcdlem  14576  lcmgcd  14577  lcmid  14579  lcm1  14580  coprmdvds  14664  coprmdvds2  14665  qredeq  14668  qredeu  14669  prmdvdsexp  14672  rpexp1i  14678  divnumden  14702  zsqrtelqelz  14712  phiprmpw  14729  vfermltlALT  14758  nnnn0modprm0  14762  modprmn0modprm0  14763  coprimeprodsq2  14765  opoe  14766  omoe  14767  opeo  14768  omeo  14769  iserodd  14790  pclem  14793  pcprendvds2  14796  pcpremul  14798  pcmul  14806  pcneg  14828  fldivp1  14847  prmpwdvds  14853  zgz  14882  modxai  15045  mod2xnegi  15048  mulgz  16784  odmod  17200  odf1  17218  odf1o1  17226  gexdvds  17240  zaddablx  17513  cygabl  17530  ablfacrp  17704  pgpfac1lem3  17715  zsubrg  19026  zsssubrg  19031  zringmulg  19051  zringcyg  19064  zringinvg  19065  zringunit  19066  prmirred  19070  mulgrhm2  19074  znunit  19138  degltp1le  23026  ef2kpi  23437  efper  23438  sinperlem  23439  sin2kpi  23442  cos2kpi  23443  abssinper  23477  sinkpi  23478  coskpi  23479  eflogeq  23555  cxpexpz  23616  root1eq1  23699  cxpeq  23701  relogbexp  23721  leibpilem1  23870  sgmval2  24074  ppiprm  24082  ppinprm  24083  chtprm  24084  chtnprm  24085  lgslem3  24230  lgsneg  24251  lgsdir2lem2  24256  lgsdir2lem4  24258  lgsdir2  24260  lgsdirnn0  24271  lgsquadlem1  24286  lgsquadlem2  24287  lgsquad2  24292  2sqlem2  24296  2sqlem7  24302  rplogsumlem2  24327  axlowdimlem13  24988  wlkdvspthlem  25341  clwwisshclwwlem1  25537  gxneg  25998  gxsuc  26004  gxnn0add  26006  gxadd  26007  gxsub  26008  gxnn0mul  26009  gxmul  26010  zaddsubgo  26086  ipasslem5  26480  rearchi  28619  pdivsq  30398  dvdspw  30399  poimirlem19  31929  itg2addnclem2  31964  lzenom  35587  rexzrexnn0  35622  pell1234qrne0  35675  pell1234qrreccl  35676  pell1234qrmulcl  35677  pell1234qrdich  35683  pell14qrdich  35691  reglogexp  35718  reglogexpbas  35721  rmxm1  35758  rmym1  35759  rmxdbl  35763  rmydbl  35764  jm2.24  35789  congtr  35791  congadd  35792  congmul  35793  congsym  35794  congneg  35795  congid  35797  congabseq  35800  acongsym  35802  acongneg2  35803  acongtr  35804  acongrep  35806  bezoutr1  35812  dvdsabsmod0OLD  35817  jm2.19lem3  35822  jm2.19lem4  35823  jm2.19  35824  jm2.25  35830  jm2.26a  35831  oddfl  37447  coskpi2  37687  cosknegpi  37690  dvdsn1add  37760  itgsinexp  37777  fourierdlem42  37958  fourierdlem42OLD  37959  fourierdlem97  38013  fourierswlem  38040  mod2eq1n2dvds  38601  elmod2OLD  38602  zob  38639  dfodd6  38643  dfeven4  38644  evenm1odd  38645  evenp1odd  38646  enege  38651  onego  38652  dfeven2  38655  bits0ALTV  38684  opoeALTV  38688  opeoALTV  38689  evensumeven  38710  bgoldbwt  38754  nnsum3primesgbe  38763  proththd  38790  addlenrevpfx  38814  pfxccatin12lem1  38840  pfxccatin12lem2  38841  pfxccatin12  38842  2elfz2melfz  38917  0nodd  39427  2nodd  39429  1neven  39549  2zlidl  39551  2zrngamgm  39556  2zrngasgrp  39557  2zrngagrp  39560  2zrngmmgm  39563  2zrngmsgrp  39564  2zrngnmrid  39567  zlmodzxzsub  39760  flsubz  39939  mod0mul  39941  m1modmmod  39943  zofldiv2  39957  dignn0flhalflem1  40045  dignn0flhalflem2  40046
  Copyright terms: Public domain W3C validator