Theorem zcn 9660

Description: An integer is a complex number. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
zcn	⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

Proof of Theorem zcn

Step	Hyp	Ref	Expression
1		zre 9659	. 2 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
2	1	recnd 8360	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℂcc 8183  ℤcz 9655

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 8277

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 4132  df-iota 5340  df-fv 5388  df-ov 6091  df-neg 8507  df-z 9656

This theorem is used by:  zsscn  9663  zaddcllempos  9692  peano2zm  9693  zaddcllemneg  9694  zaddcl  9695  zsubcl  9696  zrevaddcl  9706  nzadd  9708  zlem1lt  9712  zltlem1  9713  zapne  9730  zdiv  9745  zdivadd  9746  zdivmul  9747  zextlt  9749  zneo  9758  zeo2  9763  peano5uzti  9765  zindd  9775  divfnzn  10037  qmulz  10039  zq  10042  qaddcl  10051  qnegcl  10052  qmulcl  10053  qreccl  10058  fzen  10464  uzsubsubfz  10469  fz01en  10476  fzmmmeqm  10481  fzsubel  10483  fztp  10502  fzsuc2  10503  fzrev2  10509  fzrev3  10511  elfzp1b  10521  fzrevral  10529  fzrevral2  10530  fzrevral3  10531  fzshftral  10532  fzo0addel  10623  fzo0addelr  10624  fzoaddel2  10625  fzosubel2  10630  eluzgtdifelfzo  10632  fzocatel  10634  elfzom1elp1fzo  10637  fzval3  10639  zpnn0elfzo1  10643  fzosplitprm1  10670  fzoshftral  10674  flqzadd  10754  2tnp1ge0ge0  10757  ceilid  10773  intfracq  10778  zmod10  10798  modqmuladdnn0  10826  addmodlteq  10856  frecfzen2  10885  seqshft2g  10940  ser3mono  10945  m1expeven  11044  expsubap  11045  zesq  11117  sqoddm1div8  11152  bccmpl  11214  swrd00g  11443  swrdswrd  11499  swrdpfx  11501  pfxccatin12lem4  11520  pfxccatin12lem1  11522  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccatin12  11527  shftuz  11604  nnabscl  11889  climshftlemg  12093  climshft  12095  mptfzshft  12234  fsumrev  12235  fisum0diag2  12239  efexp  12474  efzval  12475  demoivre  12565  dvdsval2  12582  iddvds  12596  1dvds  12597  dvds0  12598  negdvdsb  12599  dvdsnegb  12600  0dvds  12603  dvdsmul1  12605  iddvdsexp  12607  muldvds1  12608  muldvds2  12609  dvdscmul  12610  dvdsmulc  12611  summodnegmod  12614  modmulconst  12615  dvds2ln  12616  dvds2add  12617  dvds2sub  12618  dvdstr  12620  dvdssub2  12627  dvdsadd  12628  dvdsaddr  12629  dvdssub  12630  dvdssubr  12631  dvdsadd2b  12632  dvdsabseq  12639  divconjdvds  12641  alzdvds  12646  addmodlteqALT  12651  zeo3  12660  odd2np1lem  12664  odd2np1  12665  even2n  12666  oddp1even  12668  mulsucdiv2z  12677  zob  12683  ltoddhalfle  12685  halfleoddlt  12686  opoe  12687  omoe  12688  opeo  12689  omeo  12690  m1exp1  12693  divalgb  12717  divalgmod  12719  modremain  12721  ndvdssub  12722  ndvdsadd  12723  flodddiv4  12728  flodddiv4t2lthalf  12731  bits0  12740  bitsp1e  12744  bitsp1o  12745  gcdneg  12784  gcdadd  12787  gcdid  12788  modgcd  12793  dvdsgcd  12814  mulgcd  12818  absmulgcd  12819  mulgcdr  12820  gcddiv  12821  gcdmultiplez  12823  dvdssqim  12826  dvdssq  12833  bezoutr1  12835  lcmneg  12877  lcmgcdlem  12880  lcmgcd  12881  lcmid  12883  lcm1  12884  coprmdvds  12895  coprmdvds2  12896  qredeq  12899  qredeu  12900  divgcdcoprmex  12905  cncongr1  12906  cncongr2  12907  prmdvdsexp  12952  rpexp1i  12958  sqrt2irr  12966  divnumden  13001  phiprmpw  13029  nnnn0modprm0  13063  modprmn0modprm0  13064  coprimeprodsq2  13066  pclemub  13095  pcprendvds2  13099  pcmul  13109  pcneg  13133  fldivp1  13156  prmpwdvds  13163  zgz  13181  4sqexercise1  13206  4sqexercise2  13207  modxai  13224  mod2xnegi  13227  mulgz  14012  mulgassr  14022  mulgmodid  14023  gzsumconst  14233  zsubrg  15027  zsssubrg  15031  zringmulg  15042  zringinvg  15048  mulgrhm2  15054  znunit  15103  ef2kpi  16033  efper  16034  sinperlem  16035  sin2kpi  16038  cos2kpi  16039  abssinper  16073  sinkpi  16074  coskpi  16075  cxpexprp  16128  sgmval2  16253  ppiprm  16259  ppinprm  16260  chtprm  16261  chtnprm  16262  lgslem3  16326  lgsneg  16348  lgsdir2lem2  16353  lgsdir2lem4  16355  lgsdir2  16357  lgssq  16364  lgsmulsqcoprm  16370  lgsdirnn0  16371  gausslemma2dlem3  16387  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2  16407  2lgslem1a2  16411  2lgsoddprmlem1  16429  2lgsoddprmlem2  16430  2sqlem2  16439  2sqlem7  16445  wlk1walkdom  16805