Theorem zcn 9545

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8090   ZZcz 9540

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 2213  ax-resscn 8184

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-rab 2520  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031  df-neg 8412  df-z 9541

This theorem is referenced by:  zsscn  9548  zaddcllempos  9577  peano2zm  9578  zaddcllemneg  9579  zaddcl  9580  zsubcl  9581  zrevaddcl  9591  nzadd  9593  zlem1lt  9597  zltlem1  9598  zapne  9615  zdiv  9629  zdivadd  9630  zdivmul  9631  zextlt  9633  zneo  9642  zeo2  9647  peano5uzti  9649  zindd  9659  divfnzn  9916  qmulz  9918  zq  9921  qaddcl  9930  qnegcl  9931  qmulcl  9932  qreccl  9937  fzen  10340  uzsubsubfz  10344  fz01en  10350  fzmmmeqm  10355  fzsubel  10357  fztp  10375  fzsuc2  10376  fzrev2  10382  fzrev3  10384  elfzp1b  10394  fzrevral  10402  fzrevral2  10403  fzrevral3  10404  fzshftral  10405  fzo0addel  10496  fzo0addelr  10497  fzoaddel2  10498  fzosubel2  10503  eluzgtdifelfzo  10505  fzocatel  10507  elfzom1elp1fzo  10510  fzval3  10512  zpnn0elfzo1  10516  fzosplitprm1  10543  fzoshftral  10547  flqzadd  10621  2tnp1ge0ge0  10624  ceilid  10640  intfracq  10645  zmod10  10665  modqmuladdnn0  10693  addmodlteq  10723  frecfzen2  10752  seqshft2g  10807  ser3mono  10812  m1expeven  10911  expsubap  10912  zesq  10983  sqoddm1div8  11018  bccmpl  11079  swrd00g  11296  swrdswrd  11352  swrdpfx  11354  pfxccatin12lem4  11373  pfxccatin12lem1  11375  swrdccatin2  11376  pfxccatin12lem2  11378  pfxccatin12  11380  shftuz  11457  nnabscl  11740  climshftlemg  11942  climshft  11944  mptfzshft  12083  fsumrev  12084  fisum0diag2  12088  efexp  12323  efzval  12324  demoivre  12414  dvdsval2  12431  iddvds  12445  1dvds  12446  dvds0  12447  negdvdsb  12448  dvdsnegb  12449  0dvds  12452  dvdsmul1  12454  iddvdsexp  12456  muldvds1  12457  muldvds2  12458  dvdscmul  12459  dvdsmulc  12460  summodnegmod  12463  modmulconst  12464  dvds2ln  12465  dvds2add  12466  dvds2sub  12467  dvdstr  12469  dvdssub2  12476  dvdsadd  12477  dvdsaddr  12478  dvdssub  12479  dvdssubr  12480  dvdsadd2b  12481  dvdsabseq  12488  divconjdvds  12490  alzdvds  12495  addmodlteqALT  12500  zeo3  12509  odd2np1lem  12513  odd2np1  12514  even2n  12515  oddp1even  12517  mulsucdiv2z  12526  zob  12532  ltoddhalfle  12534  halfleoddlt  12535  opoe  12536  omoe  12537  opeo  12538  omeo  12539  m1exp1  12542  divalgb  12566  divalgmod  12568  modremain  12570  ndvdssub  12571  ndvdsadd  12572  flodddiv4  12577  flodddiv4t2lthalf  12580  bits0  12589  bitsp1e  12593  bitsp1o  12594  gcdneg  12633  gcdadd  12636  gcdid  12637  modgcd  12642  dvdsgcd  12663  mulgcd  12667  absmulgcd  12668  mulgcdr  12669  gcddiv  12670  gcdmultiplez  12672  dvdssqim  12675  dvdssq  12682  bezoutr1  12684  lcmneg  12726  lcmgcdlem  12729  lcmgcd  12730  lcmid  12732  lcm1  12733  coprmdvds  12744  coprmdvds2  12745  qredeq  12748  qredeu  12749  divgcdcoprmex  12754  cncongr1  12755  cncongr2  12756  prmdvdsexp  12800  rpexp1i  12806  sqrt2irr  12814  divnumden  12848  phiprmpw  12874  nnnn0modprm0  12908  modprmn0modprm0  12909  coprimeprodsq2  12911  pclemub  12940  pcprendvds2  12944  pcmul  12954  pcneg  12978  fldivp1  13001  prmpwdvds  13008  zgz  13026  4sqexercise1  13051  4sqexercise2  13052  modxai  13069  mulgz  13817  mulgassr  13827  mulgmodid  13828  gsumfzconst  14008  zsubrg  14677  zsssubrg  14681  zringmulg  14694  zringinvg  14700  mulgrhm2  14706  znunit  14755  ef2kpi  15617  efper  15618  sinperlem  15619  sin2kpi  15622  cos2kpi  15623  abssinper  15657  sinkpi  15658  coskpi  15659  cxpexprp  15706  sgmval2  15798  lgslem3  15821  lgsneg  15843  lgsdir2lem2  15848  lgsdir2lem4  15850  lgsdir2  15852  lgssq  15859  lgsmulsqcoprm  15865  lgsdirnn0  15866  gausslemma2dlem3  15882  lgsquadlem1  15896  lgsquadlem2  15897  lgsquad2  15902  2lgslem1a2  15906  2lgsoddprmlem1  15924  2lgsoddprmlem2  15925  2sqlem2  15934  2sqlem7  15940  wlk1walkdom  16300