Theorem zcn 9052

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

Syntax hints:   -> wi 4   e. wcel 1480   CCcc 7611   ZZcz 9047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-resscn 7705

This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-rex 2420  df-rab 2423  df-v 2683  df-un 3070  df-in 3072  df-ss 3079  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-br 3925  df-iota 5083  df-fv 5126  df-ov 5770  df-neg 7929  df-z 9048

This theorem is referenced by:  zsscn  9055  zaddcllempos  9084  peano2zm  9085  zaddcllemneg  9086  zaddcl  9087  zsubcl  9088  zrevaddcl  9097  nzadd  9099  zlem1lt  9103  zltlem1  9104  zapne  9118  zdiv  9132  zdivadd  9133  zdivmul  9134  zextlt  9136  zneo  9145  zeo2  9150  peano5uzti  9152  zindd  9162  divfnzn  9406  qmulz  9408  zq  9411  qaddcl  9420  qnegcl  9421  qmulcl  9422  qreccl  9427  fzen  9816  uzsubsubfz  9820  fz01en  9826  fzmmmeqm  9831  fzsubel  9833  fztp  9851  fzsuc2  9852  fzrev2  9858  fzrev3  9860  elfzp1b  9870  fzrevral  9878  fzrevral2  9879  fzrevral3  9880  fzshftral  9881  fzoaddel2  9963  fzosubel2  9965  eluzgtdifelfzo  9967  fzocatel  9969  elfzom1elp1fzo  9972  fzval3  9974  zpnn0elfzo1  9978  fzosplitprm1  10004  fzoshftral  10008  flqzadd  10064  2tnp1ge0ge0  10067  ceilid  10081  intfracq  10086  zmod10  10106  modqmuladdnn0  10134  addmodlteq  10164  frecfzen2  10193  ser3mono  10244  m1expeven  10333  expsubap  10334  zesq  10403  sqoddm1div8  10437  bccmpl  10493  shftuz  10582  nnabscl  10865  climshftlemg  11064  climshft  11066  mptfzshft  11204  fsumrev  11205  fisum0diag2  11209  efexp  11377  efzval  11378  demoivre  11468  dvdsval2  11485  iddvds  11495  1dvds  11496  dvds0  11497  negdvdsb  11498  dvdsnegb  11499  0dvds  11502  dvdsmul1  11504  iddvdsexp  11506  muldvds1  11507  muldvds2  11508  dvdscmul  11509  dvdsmulc  11510  summodnegmod  11513  modmulconst  11514  dvds2ln  11515  dvds2add  11516  dvds2sub  11517  dvdstr  11519  dvdssub2  11524  dvdsadd  11525  dvdsaddr  11526  dvdssub  11527  dvdssubr  11528  dvdsadd2b  11529  dvdsabseq  11534  divconjdvds  11536  alzdvds  11541  addmodlteqALT  11546  zeo3  11554  odd2np1lem  11558  odd2np1  11559  even2n  11560  oddp1even  11562  mulsucdiv2z  11571  zob  11577  ltoddhalfle  11579  halfleoddlt  11580  opoe  11581  omoe  11582  opeo  11583  omeo  11584  m1exp1  11587  divalgb  11611  divalgmod  11613  modremain  11615  ndvdssub  11616  ndvdsadd  11617  flodddiv4  11620  flodddiv4t2lthalf  11623  gcdneg  11659  gcdadd  11662  gcdid  11663  modgcd  11668  dvdsgcd  11689  mulgcd  11693  absmulgcd  11694  mulgcdr  11695  gcddiv  11696  gcdmultiplez  11698  dvdssqim  11701  dvdssq  11708  bezoutr1  11710  lcmneg  11744  lcmgcdlem  11747  lcmgcd  11748  lcmid  11750  lcm1  11751  coprmdvds  11762  coprmdvds2  11763  qredeq  11766  qredeu  11767  divgcdcoprmex  11772  cncongr1  11773  cncongr2  11774  prmdvdsexp  11815  rpexp1i  11821  sqrt2irr  11829  divnumden  11863  phiprmpw  11887  ef2kpi  12876  efper  12877  sinperlem  12878  sin2kpi  12881  cos2kpi  12882  abssinper  12916  sinkpi  12917  coskpi  12918