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

Theorem zcn 10763
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 10762 . 2  |-  ( N  e.  ZZ  ->  N  e.  RR )
21recnd 9524 1  |-  ( N  e.  ZZ  ->  N  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   CCcc 9392   ZZcz 10758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-resscn 9451
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2805  df-rab 2808  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-uni 4201  df-br 4402  df-iota 5490  df-fv 5535  df-ov 6204  df-neg 9710  df-z 10759
This theorem is referenced by:  zsscn  10766  zsubcl  10799  zrevaddcl  10802  zlem1lt  10808  zltlem1  10809  zdiv  10824  zdivadd  10825  zdivmul  10826  zextlt  10828  zneo  10836  zeo2  10840  peano5uzi  10842  uzindOLD  10848  zindd  10855  zriotaneg  10866  zmax  11062  rebtwnz  11064  qmulz  11068  zq  11071  qaddcl  11081  qnegcl  11082  qmulcl  11083  qreccl  11085  fzen  11585  uzsubsubfz  11589  fz01en  11595  fzmmmeqm  11610  fzsubel  11612  fztp  11630  fzsuc2  11632  fzrev2  11638  fzrev3  11640  elfzp1b  11655  fzrevral  11662  fzrevral2  11663  fzrevral3  11664  fzshftral  11665  fzoaddel2  11716  fzosubel2  11718  fzocatel  11720  fzval3  11723  fzoshftral  11754  flzadd  11789  ceilid  11808  quoremz  11812  intfracq  11816  zmod10  11842  modcyc  11861  modcyc2  11862  modmul1  11870  modaddmulmod  11883  uzrdgxfr  11907  fzen2  11909  seqshft2  11950  sermono  11956  expsub  12029  zesq  12105  modexp  12117  bccmpl  12203  swrd00  12433  addlenrevswrd  12449  swrdswrd  12473  swrdswrd0  12475  swrdccatin12lem1  12494  swrdccatin12lem2b  12496  swrdccatin2  12497  swrdccatin12lem2  12499  swrdccatin12  12501  repswrevw  12543  cshwsublen  12552  cshwidx0mod  12560  2cshw  12566  2cshwid  12567  2cshwcom  12569  cshweqdif2  12572  cshweqrep  12574  cshw1  12575  shftuz  12677  seqshft  12693  nn0abscl  12920  nnabscl  12932  climshftlem  13171  climshft  13173  isershft  13260  mptfzshft  13364  fsumrev  13365  fsum0diag2  13369  efexp  13504  efzval  13505  demoivre  13603  znnenlem  13613  sqr2irr  13650  dvdsval2  13657  iddvds  13665  1dvds  13666  dvds0  13667  negdvdsb  13668  dvdsnegb  13669  0dvds  13672  dvdsmul1  13673  iddvdsexp  13675  muldvds1  13676  muldvds2  13677  dvdscmul  13678  dvdsmulc  13679  dvdscmulr  13680  dvdsmulcr  13681  dvds2ln  13682  dvds2add  13683  dvds2sub  13684  dvdstr  13685  dvdssub2  13689  dvdsadd  13690  dvdsaddr  13691  dvdssub  13692  dvdssubr  13693  dvdsadd2b  13694  alzdvds  13702  odd2np1lem  13710  odd2np1  13711  oddp1even  13713  divalglem0  13716  divalglem2  13718  divalglem4  13719  divalglem5  13720  divalglem9  13724  divalgb  13727  divalgmod  13729  ndvdssub  13730  ndvdsadd  13731  bits0  13743  bitsp1e  13747  bitsp1o  13748  gcdneg  13829  gcdaddmlem  13831  gcdaddm  13832  gcdadd  13833  gcdid  13834  modgcd  13839  bezoutlem1  13841  bezoutlem2  13842  bezoutlem4  13844  dvdsgcd  13846  mulgcd  13849  absmulgcd  13850  mulgcdr  13851  gcddiv  13852  gcdmultiplez  13854  dvdssqim  13856  dvdssq  13863  coprmdvds  13907  coprmdvds2  13908  qredeq  13911  qredeu  13912  prmdvdsexp  13919  rpexp1i  13926  divnumden  13945  zsqrelqelz  13955  phiprmpw  13970  nnnn0modprm0  13993  modprmn0modprm0  13994  coprimeprodsq2  13996  opoe  13997  omoe  13998  opeo  13999  omeo  14000  iserodd  14021  pclem  14024  pcprendvds2  14027  pcpremul  14029  pcmul  14037  pcneg  14059  fldivp1  14078  prmpwdvds  14084  zgz  14113  modxai  14216  mod2xnegi  14219  mulgz  15768  odmod  16171  odf1  16185  odf1o1  16193  gexdvds  16205  zaddablx  16472  cygabl  16489  ablfacrp  16690  pgpfac1lem3  16701  zsubrg  17992  zsssubrg  17997  zringmulg  18017  zrngmulg  18023  zringcyg  18033  zcyg  18038  zringinvg  18039  zringunit  18040  zrngunit  18041  prmirred  18045  prmirredOLD  18048  mulgrhm2  18053  mulgrhm2OLD  18056  znunit  18122  degltp1le  21678  ef2kpi  22074  efper  22075  sinperlem  22076  sin2kpi  22079  cos2kpi  22080  abssinper  22114  sinkpi  22115  coskpi  22116  eflogeq  22184  cxpexpz  22246  root1eq1  22327  cxpeq  22329  leibpilem1  22469  sgmval2  22615  ppiprm  22623  ppinprm  22624  chtprm  22625  chtnprm  22626  lgslem3  22771  lgsneg  22792  lgsdir2lem2  22797  lgsdir2lem4  22799  lgsdir2  22801  lgsdirnn0  22812  lgsquadlem1  22827  lgsquadlem2  22828  lgsquad2  22833  2sqlem2  22837  2sqlem7  22843  rplogsumlem2  22868  axlowdimlem13  23353  wlkdvspthlem  23659  gxneg  23906  gxsuc  23912  gxnn0add  23914  gxadd  23915  gxsub  23916  gxnn0mul  23917  gxmul  23918  zaddsubgo  23994  ipasslem5  24388  rearchi  26456  m1expevenALT  27252  pdivsq  27700  dvdspw  27701  itg2addnclem2  28593  lzenom  29257  rexzrexnn0  29291  pell1234qrne0  29343  pell1234qrreccl  29344  pell1234qrmulcl  29345  pell1234qrdich  29351  pell14qrdich  29359  reglogexp  29384  reglogexpbas  29387  rmxm1  29424  rmym1  29425  rmxdbl  29429  rmydbl  29430  jm2.24  29455  congtr  29457  congadd  29458  congmul  29459  congsym  29460  congneg  29461  congid  29463  congabseq  29466  acongsym  29468  acongneg2  29469  acongtr  29470  acongrep  29472  bezoutr1  29478  dvdsabsmod0  29484  jm2.19lem3  29489  jm2.19lem4  29490  jm2.19  29491  jm2.25  29497  jm2.26a  29498  itgsinexp  29944  2elfz2melfz  30351  eluzgtdifelfzo  30368  zpnn0elfzo1  30371  fzosplitprm1  30373  mulmoddvds  30395  clwwisshclwwlem1  30618  cshwlemma1  30638  zlmodzxzsub  30906
  Copyright terms: Public domain W3C validator