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

Theorem zcn 10220
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 10219 . 2  |-  ( N  e.  ZZ  ->  N  e.  RR )
21recnd 9048 1  |-  ( N  e.  ZZ  ->  N  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   CCcc 8922   ZZcz 10215
This theorem is referenced by:  zsscn  10223  zsubcl  10252  zrevaddcl  10254  zlem1lt  10260  zltlem1  10261  zdiv  10273  zdivadd  10274  zdivmul  10275  zextlt  10277  zneo  10285  zeo2  10289  peano5uzi  10291  uzindOLD  10297  zindd  10304  zmax  10504  rebtwnz  10506  qmulz  10510  zq  10513  qaddcl  10523  qnegcl  10524  qmulcl  10525  qreccl  10527  fzen  11005  fz01en  11012  fzsubel  11021  fztp  11035  fzsuc2  11036  fzrev2  11041  fzrev3  11043  fzrevral  11062  fzrevral2  11063  fzrevral3  11064  fzshftral  11065  fzoaddel2  11105  fzosubel2  11107  fzval3  11109  flzadd  11156  quoremz  11164  intfracq  11168  zmod10  11192  modcyc  11204  modcyc2  11205  modmul1  11207  uzrdgxfr  11234  fzen2  11236  seqshft2  11277  sermono  11283  expsub  11355  zesq  11430  modexp  11442  bccmpl  11528  swrd00  11693  shftuz  11812  seqshft  11828  nn0abscl  12045  nnabscl  12057  climshftlem  12296  climshft  12298  isershft  12385  fsumrev  12490  fsumshft  12491  fsum0diag2  12494  efexp  12630  efzval  12631  demoivre  12729  znnenlem  12739  sqr2irr  12776  dvdsval2  12783  iddvds  12791  1dvds  12792  dvds0  12793  negdvdsb  12794  dvdsnegb  12795  0dvds  12798  dvdsmul1  12799  iddvdsexp  12801  muldvds1  12802  muldvds2  12803  dvdscmul  12804  dvdsmulc  12805  dvdscmulr  12806  dvdsmulcr  12807  dvds2ln  12808  dvds2add  12809  dvds2sub  12810  dvdstr  12811  dvdssub2  12815  dvdsadd  12816  dvdsaddr  12817  dvdssub  12818  dvdssubr  12819  dvdsadd2b  12820  alzdvds  12827  odd2np1lem  12835  odd2np1  12836  oddp1even  12838  divalglem0  12841  divalglem2  12843  divalglem4  12844  divalglem5  12845  divalglem9  12849  divalgb  12852  divalgmod  12854  ndvdssub  12855  ndvdsadd  12856  bits0  12868  bitsp1e  12872  bitsp1o  12873  gcdneg  12954  gcdaddmlem  12956  gcdaddm  12957  gcdadd  12958  gcdid  12959  modgcd  12964  bezoutlem1  12966  bezoutlem2  12967  bezoutlem4  12969  dvdsgcd  12971  mulgcd  12974  absmulgcd  12975  mulgcdr  12976  gcddiv  12977  gcdmultiplez  12979  dvdssqim  12981  dvdssq  12988  coprmdvds  13030  coprmdvds2  13031  qredeq  13034  qredeu  13035  prmdvdsexp  13042  rpexp1i  13049  divnumden  13068  zsqrelqelz  13078  phiprmpw  13093  coprimeprodsq2  13112  opoe  13113  omoe  13114  opeo  13115  omeo  13116  iserodd  13137  pclem  13140  pcprendvds2  13143  pcpremul  13145  pcmul  13153  pcneg  13175  fldivp1  13194  prmpwdvds  13200  zgz  13229  modxai  13332  mod2xnegi  13335  mulgz  14839  odmod  15112  odf1  15126  odf1o1  15134  gexdvds  15146  zaddablx  15411  cygabl  15428  ablfacrp  15552  pgpfac1lem3  15563  zsubrg  16676  zsssubrg  16681  zrngunit  16689  zcyg  16696  prmirred  16699  mulgrhm2  16712  znunit  16768  degltp1le  19864  ef2kpi  20254  efper  20255  sinperlem  20256  sin2kpi  20259  cos2kpi  20260  abssinper  20294  sinkpi  20295  coskpi  20296  eflogeq  20364  cxpexpz  20426  root1eq1  20507  cxpeq  20509  leibpilem1  20648  sgmval2  20794  ppiprm  20802  ppinprm  20803  chtprm  20804  chtnprm  20805  lgslem3  20950  lgsneg  20971  lgsdir2lem2  20976  lgsdir2lem4  20978  lgsdir2  20980  lgsdirnn0  20991  lgsquadlem1  21006  lgsquadlem2  21007  lgsquad2  21012  2sqlem2  21016  2sqlem7  21022  rplogsumlem2  21047  wlkdvspthlem  21456  gxneg  21703  gxsuc  21709  gxnn0add  21711  gxadd  21712  gxsub  21713  gxnn0mul  21714  gxmul  21715  zaddsubgo  21791  ipasslem5  22185  zzsmulg  24082  m1expevenALT  24685  elfzp1b  24896  pdivsq  25127  dvdspw  25128  axlowdimlem13  25608  itg2addnclem2  25959  lzenom  26520  rexzrexnn0  26556  pell1234qrne0  26608  pell1234qrreccl  26609  pell1234qrmulcl  26610  pell1234qrdich  26616  pell14qrdich  26624  reglogexp  26649  reglogexpbas  26652  rmxm1  26689  rmym1  26690  rmxdbl  26694  rmydbl  26695  jm2.24  26720  congtr  26722  congadd  26723  congmul  26724  congsym  26725  congneg  26726  congid  26728  congabseq  26731  acongsym  26733  acongneg2  26734  acongtr  26735  acongrep  26737  bezoutr1  26743  dvdsabsmod0  26749  jm2.19lem3  26754  jm2.19lem4  26755  jm2.19  26756  jm2.25  26762  jm2.26a  26763  itgsinexp  27418
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-resscn 8981
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 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-rex 2656  df-rab 2659  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-br 4155  df-iota 5359  df-fv 5403  df-ov 6024  df-neg 9227  df-z 10216
  Copyright terms: Public domain W3C validator