Theorem zcn 9599

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 9598	. 2 |- ( N e. ZZ -> N e. RR )
2	1	recnd 8318	1 |- ( N e. ZZ -> N e. CC )

Syntax hints:   -> wi 4   e. wcel 2205   CCcc 8141   ZZcz 9594

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 8235

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 3218  df-in 3220  df-ss 3227  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061  df-neg 8463  df-z 9595

This theorem is referenced by:  zsscn  9602  zaddcllempos  9631  peano2zm  9632  zaddcllemneg  9633  zaddcl  9634  zsubcl  9635  zrevaddcl  9645  nzadd  9647  zlem1lt  9651  zltlem1  9652  zapne  9669  zdiv  9684  zdivadd  9685  zdivmul  9686  zextlt  9688  zneo  9697  zeo2  9702  peano5uzti  9704  zindd  9714  divfnzn  9971  qmulz  9973  zq  9976  qaddcl  9985  qnegcl  9986  qmulcl  9987  qreccl  9992  fzen  10397  uzsubsubfz  10401  fz01en  10408  fzmmmeqm  10413  fzsubel  10415  fztp  10434  fzsuc2  10435  fzrev2  10441  fzrev3  10443  elfzp1b  10453  fzrevral  10461  fzrevral2  10462  fzrevral3  10463  fzshftral  10464  fzo0addel  10555  fzo0addelr  10556  fzoaddel2  10557  fzosubel2  10562  eluzgtdifelfzo  10564  fzocatel  10566  elfzom1elp1fzo  10569  fzval3  10571  zpnn0elfzo1  10575  fzosplitprm1  10602  fzoshftral  10606  flqzadd  10682  2tnp1ge0ge0  10685  ceilid  10701  intfracq  10706  zmod10  10726  modqmuladdnn0  10754  addmodlteq  10784  frecfzen2  10813  seqshft2g  10868  ser3mono  10873  m1expeven  10972  expsubap  10973  zesq  11045  sqoddm1div8  11080  bccmpl  11141  swrd00g  11366  swrdswrd  11422  swrdpfx  11424  pfxccatin12lem4  11443  pfxccatin12lem1  11445  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12  11450  shftuz  11527  nnabscl  11810  climshftlemg  12012  climshft  12014  mptfzshft  12153  fsumrev  12154  fisum0diag2  12158  efexp  12393  efzval  12394  demoivre  12484  dvdsval2  12501  iddvds  12515  1dvds  12516  dvds0  12517  negdvdsb  12518  dvdsnegb  12519  0dvds  12522  dvdsmul1  12524  iddvdsexp  12526  muldvds1  12527  muldvds2  12528  dvdscmul  12529  dvdsmulc  12530  summodnegmod  12533  modmulconst  12534  dvds2ln  12535  dvds2add  12536  dvds2sub  12537  dvdstr  12539  dvdssub2  12546  dvdsadd  12547  dvdsaddr  12548  dvdssub  12549  dvdssubr  12550  dvdsadd2b  12551  dvdsabseq  12558  divconjdvds  12560  alzdvds  12565  addmodlteqALT  12570  zeo3  12579  odd2np1lem  12583  odd2np1  12584  even2n  12585  oddp1even  12587  mulsucdiv2z  12596  zob  12602  ltoddhalfle  12604  halfleoddlt  12605  opoe  12606  omoe  12607  opeo  12608  omeo  12609  m1exp1  12612  divalgb  12636  divalgmod  12638  modremain  12640  ndvdssub  12641  ndvdsadd  12642  flodddiv4  12647  flodddiv4t2lthalf  12650  bits0  12659  bitsp1e  12663  bitsp1o  12664  gcdneg  12703  gcdadd  12706  gcdid  12707  modgcd  12712  dvdsgcd  12733  mulgcd  12737  absmulgcd  12738  mulgcdr  12739  gcddiv  12740  gcdmultiplez  12742  dvdssqim  12745  dvdssq  12752  bezoutr1  12754  lcmneg  12796  lcmgcdlem  12799  lcmgcd  12800  lcmid  12802  lcm1  12803  coprmdvds  12814  coprmdvds2  12815  qredeq  12818  qredeu  12819  divgcdcoprmex  12824  cncongr1  12825  cncongr2  12826  prmdvdsexp  12870  rpexp1i  12876  sqrt2irr  12884  divnumden  12918  phiprmpw  12944  nnnn0modprm0  12978  modprmn0modprm0  12979  coprimeprodsq2  12981  pclemub  13010  pcprendvds2  13014  pcmul  13024  pcneg  13048  fldivp1  13071  prmpwdvds  13078  zgz  13096  4sqexercise1  13121  4sqexercise2  13122  modxai  13139  mulgz  13903  mulgassr  13913  mulgmodid  13914  gsumfzconst  14094  zsubrg  14855  zsssubrg  14859  zringmulg  14872  zringinvg  14878  mulgrhm2  14884  znunit  14933  ef2kpi  15797  efper  15798  sinperlem  15799  sin2kpi  15802  cos2kpi  15803  abssinper  15837  sinkpi  15838  coskpi  15839  cxpexprp  15886  sgmval2  15978  lgslem3  16001  lgsneg  16023  lgsdir2lem2  16028  lgsdir2lem4  16030  lgsdir2  16032  lgssq  16039  lgsmulsqcoprm  16045  lgsdirnn0  16046  gausslemma2dlem3  16062  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2  16082  2lgslem1a2  16086  2lgsoddprmlem1  16104  2lgsoddprmlem2  16105  2sqlem2  16114  2sqlem7  16120  wlk1walkdom  16480