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

Theorem zcn 10212
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 10211 . 2  |-  ( N  e.  ZZ  ->  N  e.  RR )
21recnd 9040 1  |-  ( N  e.  ZZ  ->  N  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   CCcc 8914   ZZcz 10207
This theorem is referenced by:  zsscn  10215  zsubcl  10244  zrevaddcl  10246  zlem1lt  10252  zltlem1  10253  zdiv  10265  zdivadd  10266  zdivmul  10267  zextlt  10269  zneo  10277  zeo2  10281  peano5uzi  10283  uzindOLD  10289  zindd  10296  zmax  10496  rebtwnz  10498  qmulz  10502  zq  10505  qaddcl  10515  qnegcl  10516  qmulcl  10517  qreccl  10519  fzen  10997  fz01en  11004  fzsubel  11013  fztp  11027  fzsuc2  11028  fzrev2  11033  fzrev3  11035  fzrevral  11054  fzrevral2  11055  fzrevral3  11056  fzshftral  11057  fzoaddel2  11097  fzosubel2  11099  fzval3  11101  flzadd  11148  quoremz  11156  intfracq  11160  zmod10  11184  modcyc  11196  modcyc2  11197  modmul1  11199  uzrdgxfr  11226  fzen2  11228  seqshft2  11269  sermono  11275  expsub  11347  zesq  11422  modexp  11434  bccmpl  11520  swrd00  11685  shftuz  11804  seqshft  11820  nn0abscl  12037  nnabscl  12049  climshftlem  12288  climshft  12290  isershft  12377  fsumrev  12482  fsumshft  12483  fsum0diag2  12486  efexp  12622  efzval  12623  demoivre  12721  znnenlem  12731  sqr2irr  12768  dvdsval2  12775  iddvds  12783  1dvds  12784  dvds0  12785  negdvdsb  12786  dvdsnegb  12787  0dvds  12790  dvdsmul1  12791  iddvdsexp  12793  muldvds1  12794  muldvds2  12795  dvdscmul  12796  dvdsmulc  12797  dvdscmulr  12798  dvdsmulcr  12799  dvds2ln  12800  dvds2add  12801  dvds2sub  12802  dvdstr  12803  dvdssub2  12807  dvdsadd  12808  dvdsaddr  12809  dvdssub  12810  dvdssubr  12811  dvdsadd2b  12812  alzdvds  12819  odd2np1lem  12827  odd2np1  12828  oddp1even  12830  divalglem0  12833  divalglem2  12835  divalglem4  12836  divalglem5  12837  divalglem9  12841  divalgb  12844  divalgmod  12846  ndvdssub  12847  ndvdsadd  12848  bits0  12860  bitsp1e  12864  bitsp1o  12865  gcdneg  12946  gcdaddmlem  12948  gcdaddm  12949  gcdadd  12950  gcdid  12951  modgcd  12956  bezoutlem1  12958  bezoutlem2  12959  bezoutlem4  12961  dvdsgcd  12963  mulgcd  12966  absmulgcd  12967  mulgcdr  12968  gcddiv  12969  gcdmultiplez  12971  dvdssqim  12973  dvdssq  12980  coprmdvds  13022  coprmdvds2  13023  qredeq  13026  qredeu  13027  prmdvdsexp  13034  rpexp1i  13041  divnumden  13060  zsqrelqelz  13070  phiprmpw  13085  coprimeprodsq2  13104  opoe  13105  omoe  13106  opeo  13107  omeo  13108  iserodd  13129  pclem  13132  pcprendvds2  13135  pcpremul  13137  pcmul  13145  pcneg  13167  fldivp1  13186  prmpwdvds  13192  zgz  13221  modxai  13324  mod2xnegi  13327  mulgz  14831  odmod  15104  odf1  15118  odf1o1  15126  gexdvds  15138  zaddablx  15403  cygabl  15420  ablfacrp  15544  pgpfac1lem3  15555  zsubrg  16668  zsssubrg  16673  zrngunit  16681  zcyg  16688  prmirred  16691  mulgrhm2  16704  znunit  16760  degltp1le  19856  ef2kpi  20246  efper  20247  sinperlem  20248  sin2kpi  20251  cos2kpi  20252  abssinper  20286  sinkpi  20287  coskpi  20288  eflogeq  20356  cxpexpz  20418  root1eq1  20499  cxpeq  20501  leibpilem1  20640  sgmval2  20786  ppiprm  20794  ppinprm  20795  chtprm  20796  chtnprm  20797  lgslem3  20942  lgsneg  20963  lgsdir2lem2  20968  lgsdir2lem4  20970  lgsdir2  20972  lgsdirnn0  20983  lgsquadlem1  20998  lgsquadlem2  20999  lgsquad2  21004  2sqlem2  21008  2sqlem7  21014  rplogsumlem2  21039  wlkdvspthlem  21448  gxneg  21695  gxsuc  21701  gxnn0add  21703  gxadd  21704  gxsub  21705  gxnn0mul  21706  gxmul  21707  zaddsubgo  21783  ipasslem5  22177  zzsmulg  24074  m1expevenALT  24677  elfzp1b  24888  pdivsq  25119  dvdspw  25120  axlowdimlem13  25600  itg2addnclem2  25951  lzenom  26512  rexzrexnn0  26548  pell1234qrne0  26600  pell1234qrreccl  26601  pell1234qrmulcl  26602  pell1234qrdich  26608  pell14qrdich  26616  reglogexp  26641  reglogexpbas  26644  rmxm1  26681  rmym1  26682  rmxdbl  26686  rmydbl  26687  jm2.24  26712  congtr  26714  congadd  26715  congmul  26716  congsym  26717  congneg  26718  congid  26720  congabseq  26723  acongsym  26725  acongneg2  26726  acongtr  26727  acongrep  26729  bezoutr1  26735  dvdsabsmod0  26741  jm2.19lem3  26746  jm2.19lem4  26747  jm2.19  26748  jm2.25  26754  jm2.26a  26755  itgsinexp  27410
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 2361  ax-resscn 8973
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 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-rex 2648  df-rab 2651  df-v 2894  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-sn 3756  df-pr 3757  df-op 3759  df-uni 3951  df-br 4147  df-iota 5351  df-fv 5395  df-ov 6016  df-neg 9219  df-z 10208
  Copyright terms: Public domain W3C validator