Theorem zcn 9287

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

Syntax hints:   -> wi 4   e. wcel 2160   CCcc 7838   ZZcz 9282

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-resscn 7932

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-rab 2477  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-iota 5196  df-fv 5243  df-ov 5898  df-neg 8160  df-z 9283

This theorem is referenced by:  zsscn  9290  zaddcllempos  9319  peano2zm  9320  zaddcllemneg  9321  zaddcl  9322  zsubcl  9323  zrevaddcl  9332  nzadd  9334  zlem1lt  9338  zltlem1  9339  zapne  9356  zdiv  9370  zdivadd  9371  zdivmul  9372  zextlt  9374  zneo  9383  zeo2  9388  peano5uzti  9390  zindd  9400  divfnzn  9650  qmulz  9652  zq  9655  qaddcl  9664  qnegcl  9665  qmulcl  9666  qreccl  9671  fzen  10072  uzsubsubfz  10076  fz01en  10082  fzmmmeqm  10087  fzsubel  10089  fztp  10107  fzsuc2  10108  fzrev2  10114  fzrev3  10116  elfzp1b  10126  fzrevral  10134  fzrevral2  10135  fzrevral3  10136  fzshftral  10137  fzoaddel2  10222  fzosubel2  10224  eluzgtdifelfzo  10226  fzocatel  10228  elfzom1elp1fzo  10231  fzval3  10233  zpnn0elfzo1  10237  fzosplitprm1  10263  fzoshftral  10267  flqzadd  10328  2tnp1ge0ge0  10331  ceilid  10345  intfracq  10350  zmod10  10370  modqmuladdnn0  10398  addmodlteq  10428  frecfzen2  10457  ser3mono  10508  m1expeven  10597  expsubap  10598  zesq  10669  sqoddm1div8  10704  bccmpl  10765  shftuz  10857  nnabscl  11140  climshftlemg  11341  climshft  11343  mptfzshft  11481  fsumrev  11482  fisum0diag2  11486  efexp  11721  efzval  11722  demoivre  11811  dvdsval2  11828  iddvds  11842  1dvds  11843  dvds0  11844  negdvdsb  11845  dvdsnegb  11846  0dvds  11849  dvdsmul1  11851  iddvdsexp  11853  muldvds1  11854  muldvds2  11855  dvdscmul  11856  dvdsmulc  11857  summodnegmod  11860  modmulconst  11861  dvds2ln  11862  dvds2add  11863  dvds2sub  11864  dvdstr  11866  dvdssub2  11873  dvdsadd  11874  dvdsaddr  11875  dvdssub  11876  dvdssubr  11877  dvdsadd2b  11878  dvdsabseq  11884  divconjdvds  11886  alzdvds  11891  addmodlteqALT  11896  zeo3  11904  odd2np1lem  11908  odd2np1  11909  even2n  11910  oddp1even  11912  mulsucdiv2z  11921  zob  11927  ltoddhalfle  11929  halfleoddlt  11930  opoe  11931  omoe  11932  opeo  11933  omeo  11934  m1exp1  11937  divalgb  11961  divalgmod  11963  modremain  11965  ndvdssub  11966  ndvdsadd  11967  flodddiv4  11970  flodddiv4t2lthalf  11973  gcdneg  12014  gcdadd  12017  gcdid  12018  modgcd  12023  dvdsgcd  12044  mulgcd  12048  absmulgcd  12049  mulgcdr  12050  gcddiv  12051  gcdmultiplez  12053  dvdssqim  12056  dvdssq  12063  bezoutr1  12065  lcmneg  12105  lcmgcdlem  12108  lcmgcd  12109  lcmid  12111  lcm1  12112  coprmdvds  12123  coprmdvds2  12124  qredeq  12127  qredeu  12128  divgcdcoprmex  12133  cncongr1  12134  cncongr2  12135  prmdvdsexp  12179  rpexp1i  12185  sqrt2irr  12193  divnumden  12227  phiprmpw  12253  nnnn0modprm0  12286  modprmn0modprm0  12287  coprimeprodsq2  12289  pclemub  12318  pcprendvds2  12322  pcmul  12332  pcneg  12356  fldivp1  12379  prmpwdvds  12386  zgz  12404  4sqexercise1  12429  4sqexercise2  12430  mulgz  13087  mulgassr  13097  mulgmodid  13098  zsubrg  13881  zsssubrg  13885  zringmulg  13894  zringinvg  13900  mulgrhm2  13905  ef2kpi  14679  efper  14680  sinperlem  14681  sin2kpi  14684  cos2kpi  14685  abssinper  14719  sinkpi  14720  coskpi  14721  cxpexprp  14768  lgslem3  14856  lgsneg  14878  lgsdir2lem2  14883  lgsdir2lem4  14885  lgsdir2  14887  lgssq  14894  lgsmulsqcoprm  14900  lgsdirnn0  14901  2lgsoddprmlem1  14906  2lgsoddprmlem2  14907  2sqlem2  14915  2sqlem7  14921