Theorem zcn 9584

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

Step	Hyp	Ref	Expression
1		zre 9583	. 2 |- ( N e. ZZ -> N e. RR )
2	1	recnd 8304	1 |- ( N e. ZZ -> N e. CC )

Syntax hints:   -> wi 4   e. wcel 2205   CCcc 8127   ZZcz 9579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8221

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-rab 2531  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362  df-ov 6055  df-neg 8449  df-z 9580

This theorem is referenced by:  zsscn  9587  zaddcllempos  9616  peano2zm  9617  zaddcllemneg  9618  zaddcl  9619  zsubcl  9620  zrevaddcl  9630  nzadd  9632  zlem1lt  9636  zltlem1  9637  zapne  9654  zdiv  9669  zdivadd  9670  zdivmul  9671  zextlt  9673  zneo  9682  zeo2  9687  peano5uzti  9689  zindd  9699  divfnzn  9956  qmulz  9958  zq  9961  qaddcl  9970  qnegcl  9971  qmulcl  9972  qreccl  9977  fzen  10380  uzsubsubfz  10384  fz01en  10390  fzmmmeqm  10395  fzsubel  10397  fztp  10416  fzsuc2  10417  fzrev2  10423  fzrev3  10425  elfzp1b  10435  fzrevral  10443  fzrevral2  10444  fzrevral3  10445  fzshftral  10446  fzo0addel  10537  fzo0addelr  10538  fzoaddel2  10539  fzosubel2  10544  eluzgtdifelfzo  10546  fzocatel  10548  elfzom1elp1fzo  10551  fzval3  10553  zpnn0elfzo1  10557  fzosplitprm1  10584  fzoshftral  10588  flqzadd  10662  2tnp1ge0ge0  10665  ceilid  10681  intfracq  10686  zmod10  10706  modqmuladdnn0  10734  addmodlteq  10764  frecfzen2  10793  seqshft2g  10848  ser3mono  10853  m1expeven  10952  expsubap  10953  zesq  11024  sqoddm1div8  11059  bccmpl  11120  swrd00g  11345  swrdswrd  11401  swrdpfx  11403  pfxccatin12lem4  11422  pfxccatin12lem1  11424  swrdccatin2  11425  pfxccatin12lem2  11427  pfxccatin12  11429  shftuz  11506  nnabscl  11789  climshftlemg  11991  climshft  11993  mptfzshft  12132  fsumrev  12133  fisum0diag2  12137  efexp  12372  efzval  12373  demoivre  12463  dvdsval2  12480  iddvds  12494  1dvds  12495  dvds0  12496  negdvdsb  12497  dvdsnegb  12498  0dvds  12501  dvdsmul1  12503  iddvdsexp  12505  muldvds1  12506  muldvds2  12507  dvdscmul  12508  dvdsmulc  12509  summodnegmod  12512  modmulconst  12513  dvds2ln  12514  dvds2add  12515  dvds2sub  12516  dvdstr  12518  dvdssub2  12525  dvdsadd  12526  dvdsaddr  12527  dvdssub  12528  dvdssubr  12529  dvdsadd2b  12530  dvdsabseq  12537  divconjdvds  12539  alzdvds  12544  addmodlteqALT  12549  zeo3  12558  odd2np1lem  12562  odd2np1  12563  even2n  12564  oddp1even  12566  mulsucdiv2z  12575  zob  12581  ltoddhalfle  12583  halfleoddlt  12584  opoe  12585  omoe  12586  opeo  12587  omeo  12588  m1exp1  12591  divalgb  12615  divalgmod  12617  modremain  12619  ndvdssub  12620  ndvdsadd  12621  flodddiv4  12626  flodddiv4t2lthalf  12629  bits0  12638  bitsp1e  12642  bitsp1o  12643  gcdneg  12682  gcdadd  12685  gcdid  12686  modgcd  12691  dvdsgcd  12712  mulgcd  12716  absmulgcd  12717  mulgcdr  12718  gcddiv  12719  gcdmultiplez  12721  dvdssqim  12724  dvdssq  12731  bezoutr1  12733  lcmneg  12775  lcmgcdlem  12778  lcmgcd  12779  lcmid  12781  lcm1  12782  coprmdvds  12793  coprmdvds2  12794  qredeq  12797  qredeu  12798  divgcdcoprmex  12803  cncongr1  12804  cncongr2  12805  prmdvdsexp  12849  rpexp1i  12855  sqrt2irr  12863  divnumden  12897  phiprmpw  12923  nnnn0modprm0  12957  modprmn0modprm0  12958  coprimeprodsq2  12960  pclemub  12989  pcprendvds2  12993  pcmul  13003  pcneg  13027  fldivp1  13050  prmpwdvds  13057  zgz  13075  4sqexercise1  13100  4sqexercise2  13101  modxai  13118  mulgz  13884  mulgassr  13894  mulgmodid  13895  gsumfzconst  14075  zsubrg  14746  zsssubrg  14750  zringmulg  14763  zringinvg  14769  mulgrhm2  14775  znunit  14824  ef2kpi  15688  efper  15689  sinperlem  15690  sin2kpi  15693  cos2kpi  15694  abssinper  15728  sinkpi  15729  coskpi  15730  cxpexprp  15777  sgmval2  15869  lgslem3  15892  lgsneg  15914  lgsdir2lem2  15919  lgsdir2lem4  15921  lgsdir2  15923  lgssq  15930  lgsmulsqcoprm  15936  lgsdirnn0  15937  gausslemma2dlem3  15953  lgsquadlem1  15967  lgsquadlem2  15968  lgsquad2  15973  2lgslem1a2  15977  2lgsoddprmlem1  15995  2lgsoddprmlem2  15996  2sqlem2  16005  2sqlem7  16011  wlk1walkdom  16371