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

Theorem zcn 10277
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 10276 . 2  |-  ( N  e.  ZZ  ->  N  e.  RR )
21recnd 9104 1  |-  ( N  e.  ZZ  ->  N  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   CCcc 8978   ZZcz 10272
This theorem is referenced by:  zsscn  10280  zsubcl  10309  zrevaddcl  10311  zlem1lt  10317  zltlem1  10318  zdiv  10330  zdivadd  10331  zdivmul  10332  zextlt  10334  zneo  10342  zeo2  10346  peano5uzi  10348  uzindOLD  10354  zindd  10361  zmax  10561  rebtwnz  10563  qmulz  10567  zq  10570  qaddcl  10580  qnegcl  10581  qmulcl  10582  qreccl  10584  fzen  11062  fz01en  11069  fzsubel  11078  fztp  11092  fzsuc2  11094  fzrev2  11099  fzrev3  11101  fzrevral  11121  fzrevral2  11122  fzrevral3  11123  fzshftral  11124  fzoaddel2  11166  fzosubel2  11168  fzval3  11170  flzadd  11218  quoremz  11226  intfracq  11230  zmod10  11254  modcyc  11266  modcyc2  11267  modmul1  11269  uzrdgxfr  11296  fzen2  11298  seqshft2  11339  sermono  11345  expsub  11417  zesq  11492  modexp  11504  bccmpl  11590  swrd00  11755  shftuz  11874  seqshft  11890  nn0abscl  12107  nnabscl  12119  climshftlem  12358  climshft  12360  isershft  12447  fsumrev  12552  fsumshft  12553  fsum0diag2  12556  efexp  12692  efzval  12693  demoivre  12791  znnenlem  12801  sqr2irr  12838  dvdsval2  12845  iddvds  12853  1dvds  12854  dvds0  12855  negdvdsb  12856  dvdsnegb  12857  0dvds  12860  dvdsmul1  12861  iddvdsexp  12863  muldvds1  12864  muldvds2  12865  dvdscmul  12866  dvdsmulc  12867  dvdscmulr  12868  dvdsmulcr  12869  dvds2ln  12870  dvds2add  12871  dvds2sub  12872  dvdstr  12873  dvdssub2  12877  dvdsadd  12878  dvdsaddr  12879  dvdssub  12880  dvdssubr  12881  dvdsadd2b  12882  alzdvds  12889  odd2np1lem  12897  odd2np1  12898  oddp1even  12900  divalglem0  12903  divalglem2  12905  divalglem4  12906  divalglem5  12907  divalglem9  12911  divalgb  12914  divalgmod  12916  ndvdssub  12917  ndvdsadd  12918  bits0  12930  bitsp1e  12934  bitsp1o  12935  gcdneg  13016  gcdaddmlem  13018  gcdaddm  13019  gcdadd  13020  gcdid  13021  modgcd  13026  bezoutlem1  13028  bezoutlem2  13029  bezoutlem4  13031  dvdsgcd  13033  mulgcd  13036  absmulgcd  13037  mulgcdr  13038  gcddiv  13039  gcdmultiplez  13041  dvdssqim  13043  dvdssq  13050  coprmdvds  13092  coprmdvds2  13093  qredeq  13096  qredeu  13097  prmdvdsexp  13104  rpexp1i  13111  divnumden  13130  zsqrelqelz  13140  phiprmpw  13155  coprimeprodsq2  13174  opoe  13175  omoe  13176  opeo  13177  omeo  13178  iserodd  13199  pclem  13202  pcprendvds2  13205  pcpremul  13207  pcmul  13215  pcneg  13237  fldivp1  13256  prmpwdvds  13262  zgz  13291  modxai  13394  mod2xnegi  13397  mulgz  14901  odmod  15174  odf1  15188  odf1o1  15196  gexdvds  15208  zaddablx  15473  cygabl  15490  ablfacrp  15614  pgpfac1lem3  15625  zsubrg  16742  zsssubrg  16747  zrngunit  16755  zcyg  16762  prmirred  16765  mulgrhm2  16778  znunit  16834  degltp1le  19986  ef2kpi  20376  efper  20377  sinperlem  20378  sin2kpi  20381  cos2kpi  20382  abssinper  20416  sinkpi  20417  coskpi  20418  eflogeq  20486  cxpexpz  20548  root1eq1  20629  cxpeq  20631  leibpilem1  20770  sgmval2  20916  ppiprm  20924  ppinprm  20925  chtprm  20926  chtnprm  20927  lgslem3  21072  lgsneg  21093  lgsdir2lem2  21098  lgsdir2lem4  21100  lgsdir2  21102  lgsdirnn0  21113  lgsquadlem1  21128  lgsquadlem2  21129  lgsquad2  21134  2sqlem2  21138  2sqlem7  21144  rplogsumlem2  21169  wlkdvspthlem  21597  gxneg  21844  gxsuc  21850  gxnn0add  21852  gxadd  21853  gxsub  21854  gxnn0mul  21855  gxmul  21856  zaddsubgo  21932  ipasslem5  22326  zzsmulg  24255  m1expevenALT  24895  elfzp1b  25106  pdivsq  25358  dvdspw  25359  axlowdimlem13  25858  itg2addnclem2  26220  lzenom  26782  rexzrexnn0  26818  pell1234qrne0  26870  pell1234qrreccl  26871  pell1234qrmulcl  26872  pell1234qrdich  26878  pell14qrdich  26886  reglogexp  26911  reglogexpbas  26914  rmxm1  26951  rmym1  26952  rmxdbl  26956  rmydbl  26957  jm2.24  26982  congtr  26984  congadd  26985  congmul  26986  congsym  26987  congneg  26988  congid  26990  congabseq  26993  acongsym  26995  acongneg2  26996  acongtr  26997  acongrep  26999  bezoutr1  27005  dvdsabsmod0  27011  jm2.19lem3  27016  jm2.19lem4  27017  jm2.19  27018  jm2.25  27024  jm2.26a  27025  itgsinexp  27680  fzmmmeqm  28063  2elfz2melfz  28065  ubmelfzo  28073  ubmelm1fzo  28074  modaddmulmod  28100  addlenrevswrd  28121  swrd0swrd  28127  swrdswrd  28129  swrd0swrdid  28130  swrdswrd0  28131  swrdccatin12lem2  28137  swrdccatin12lem3b  28139  swrdccatin2  28140  swrdccatin12lem3  28142  swrdccatin12  28144  2cshw1lem1  28178  2cshw2lem1  28182  cshweqdif2  28197
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-resscn 9037
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076  df-neg 9284  df-z 10273
  Copyright terms: Public domain W3C validator