Theorem zcn 9653

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8177   ZZcz 9648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8271

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-rab 2537  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088  df-neg 8501  df-z 9649

This theorem is used by:  zsscn  9656  zaddcllempos  9685  peano2zm  9686  zaddcllemneg  9687  zaddcl  9688  zsubcl  9689  zrevaddcl  9699  nzadd  9701  zlem1lt  9705  zltlem1  9706  zapne  9723  zdiv  9738  zdivadd  9739  zdivmul  9740  zextlt  9742  zneo  9751  zeo2  9756  peano5uzti  9758  zindd  9768  divfnzn  10030  qmulz  10032  zq  10035  qaddcl  10044  qnegcl  10045  qmulcl  10046  qreccl  10051  fzen  10457  uzsubsubfz  10462  fz01en  10469  fzmmmeqm  10474  fzsubel  10476  fztp  10495  fzsuc2  10496  fzrev2  10502  fzrev3  10504  elfzp1b  10514  fzrevral  10522  fzrevral2  10523  fzrevral3  10524  fzshftral  10525  fzo0addel  10616  fzo0addelr  10617  fzoaddel2  10618  fzosubel2  10623  eluzgtdifelfzo  10625  fzocatel  10627  elfzom1elp1fzo  10630  fzval3  10632  zpnn0elfzo1  10636  fzosplitprm1  10663  fzoshftral  10667  flqzadd  10746  2tnp1ge0ge0  10749  ceilid  10765  intfracq  10770  zmod10  10790  modqmuladdnn0  10818  addmodlteq  10848  frecfzen2  10877  seqshft2g  10932  ser3mono  10937  m1expeven  11036  expsubap  11037  zesq  11109  sqoddm1div8  11144  bccmpl  11206  swrd00g  11435  swrdswrd  11491  swrdpfx  11493  pfxccatin12lem4  11512  pfxccatin12lem1  11514  swrdccatin2  11515  pfxccatin12lem2  11517  pfxccatin12  11519  shftuz  11596  nnabscl  11881  climshftlemg  12084  climshft  12086  mptfzshft  12225  fsumrev  12226  fisum0diag2  12230  efexp  12465  efzval  12466  demoivre  12556  dvdsval2  12573  iddvds  12587  1dvds  12588  dvds0  12589  negdvdsb  12590  dvdsnegb  12591  0dvds  12594  dvdsmul1  12596  iddvdsexp  12598  muldvds1  12599  muldvds2  12600  dvdscmul  12601  dvdsmulc  12602  summodnegmod  12605  modmulconst  12606  dvds2ln  12607  dvds2add  12608  dvds2sub  12609  dvdstr  12611  dvdssub2  12618  dvdsadd  12619  dvdsaddr  12620  dvdssub  12621  dvdssubr  12622  dvdsadd2b  12623  dvdsabseq  12630  divconjdvds  12632  alzdvds  12637  addmodlteqALT  12642  zeo3  12651  odd2np1lem  12655  odd2np1  12656  even2n  12657  oddp1even  12659  mulsucdiv2z  12668  zob  12674  ltoddhalfle  12676  halfleoddlt  12677  opoe  12678  omoe  12679  opeo  12680  omeo  12681  m1exp1  12684  divalgb  12708  divalgmod  12710  modremain  12712  ndvdssub  12713  ndvdsadd  12714  flodddiv4  12719  flodddiv4t2lthalf  12722  bits0  12731  bitsp1e  12735  bitsp1o  12736  gcdneg  12775  gcdadd  12778  gcdid  12779  modgcd  12784  dvdsgcd  12805  mulgcd  12809  absmulgcd  12810  mulgcdr  12811  gcddiv  12812  gcdmultiplez  12814  dvdssqim  12817  dvdssq  12824  bezoutr1  12826  lcmneg  12868  lcmgcdlem  12871  lcmgcd  12872  lcmid  12874  lcm1  12875  coprmdvds  12886  coprmdvds2  12887  qredeq  12890  qredeu  12891  divgcdcoprmex  12896  cncongr1  12897  cncongr2  12898  prmdvdsexp  12943  rpexp1i  12949  sqrt2irr  12957  divnumden  12992  phiprmpw  13020  nnnn0modprm0  13054  modprmn0modprm0  13055  coprimeprodsq2  13057  pclemub  13086  pcprendvds2  13090  pcmul  13100  pcneg  13124  fldivp1  13147  prmpwdvds  13154  zgz  13172  4sqexercise1  13197  4sqexercise2  13198  modxai  13215  mod2xnegi  13218  mulgz  14002  mulgassr  14012  mulgmodid  14013  gzsumconst  14192  zsubrg  14967  zsssubrg  14971  zringmulg  14982  zringinvg  14988  mulgrhm2  14994  znunit  15043  ef2kpi  15957  efper  15958  sinperlem  15959  sin2kpi  15962  cos2kpi  15963  abssinper  15997  sinkpi  15998  coskpi  15999  cxpexprp  16050  sgmval2  16165  ppiprm  16170  ppinprm  16171  lgslem3  16219  lgsneg  16241  lgsdir2lem2  16246  lgsdir2lem4  16248  lgsdir2  16250  lgssq  16257  lgsmulsqcoprm  16263  lgsdirnn0  16264  gausslemma2dlem3  16280  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2  16300  2lgslem1a2  16304  2lgsoddprmlem1  16322  2lgsoddprmlem2  16323  2sqlem2  16332  2sqlem7  16338  wlk1walkdom  16698