Theorem zcn 9658

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 9657	. 2 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
2	1	recnd 8360	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

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

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 9654

This theorem is used by:  zsscn  9661  zaddcllempos  9690  peano2zm  9691  zaddcllemneg  9692  zaddcl  9693  zsubcl  9694  zrevaddcl  9704  nzadd  9706  zlem1lt  9710  zltlem1  9711  zapne  9728  zdiv  9744  zdivadd  9745  zdivmul  9746  zextlt  9748  zneo  9757  zeo2  9762  peano5uzti  9764  zindd  9774  divfnzn  10036  qmulz  10038  zq  10041  qaddcl  10050  qnegcl  10051  qmulcl  10052  qreccl  10057  fzen  10463  uzsubsubfz  10468  fz01en  10475  fzmmmeqm  10480  fzsubel  10482  fztp  10501  fzsuc2  10502  fzrev2  10508  fzrev3  10510  elfzp1b  10520  fzrevral  10528  fzrevral2  10529  fzrevral3  10530  fzshftral  10531  fzo0addel  10622  fzo0addelr  10623  fzoaddel2  10624  fzosubel2  10629  eluzgtdifelfzo  10631  fzocatel  10633  elfzom1elp1fzo  10636  fzval3  10638  zpnn0elfzo1  10642  fzosplitprm1  10669  fzoshftral  10673  flqzadd  10753  2tnp1ge0ge0  10756  ceilid  10772  intfracq  10777  zmod10  10797  modqmuladdnn0  10825  addmodlteq  10855  frecfzen2  10884  seqshft2g  10939  ser3mono  10944  m1expeven  11043  expsubap  11044  zesq  11116  sqoddm1div8  11151  bccmpl  11213  swrd00g  11442  swrdswrd  11498  swrdpfx  11500  pfxccatin12lem4  11519  pfxccatin12lem1  11521  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatin12  11526  shftuz  11603  nnabscl  11888  climshftlemg  12092  climshft  12094  mptfzshft  12233  fsumrev  12234  fisum0diag2  12238  efexp  12473  efzval  12474  demoivre  12564  dvdsval2  12581  iddvds  12595  1dvds  12596  dvds0  12597  negdvdsb  12598  dvdsnegb  12599  0dvds  12602  dvdsmul1  12604  iddvdsexp  12606  muldvds1  12607  muldvds2  12608  dvdscmul  12609  dvdsmulc  12610  summodnegmod  12613  modmulconst  12614  dvds2ln  12615  dvds2add  12616  dvds2sub  12617  dvdstr  12619  dvdssub2  12626  dvdsadd  12627  dvdsaddr  12628  dvdssub  12629  dvdssubr  12630  dvdsadd2b  12631  dvdsabseq  12638  divconjdvds  12640  alzdvds  12645  addmodlteqALT  12650  zeo3  12659  odd2np1lem  12663  odd2np1  12664  even2n  12665  oddp1even  12667  mulsucdiv2z  12676  zob  12682  ltoddhalfle  12684  halfleoddlt  12685  opoe  12686  omoe  12687  opeo  12688  omeo  12689  m1exp1  12692  divalgb  12716  divalgmod  12718  modremain  12720  ndvdssub  12721  ndvdsadd  12722  flodddiv4  12727  flodddiv4t2lthalf  12730  bits0  12739  bitsp1e  12743  bitsp1o  12744  gcdneg  12783  gcdadd  12786  gcdid  12787  modgcd  12792  dvdsgcd  12813  mulgcd  12817  absmulgcd  12818  mulgcdr  12819  gcddiv  12820  gcdmultiplez  12822  dvdssqim  12825  dvdssq  12832  bezoutr1  12834  lcmneg  12876  lcmgcdlem  12879  lcmgcd  12880  lcmid  12882  lcm1  12883  coprmdvds  12894  coprmdvds2  12895  qredeq  12898  qredeu  12899  divgcdcoprmex  12904  cncongr1  12905  cncongr2  12906  prmdvdsexp  12951  rpexp1i  12957  sqrt2irr  12965  divnumden  13000  phiprmpw  13028  nnnn0modprm0  13062  modprmn0modprm0  13063  coprimeprodsq2  13065  pclemub  13094  pcprendvds2  13098  pcmul  13108  pcneg  13132  fldivp1  13155  prmpwdvds  13162  zgz  13180  4sqexercise1  13205  4sqexercise2  13206  modxai  13223  mod2xnegi  13226  mulgz  14011  mulgassr  14021  mulgmodid  14022  gzsumconst  14232  zsubrg  15026  zsssubrg  15030  zringmulg  15041  zringinvg  15047  mulgrhm2  15053  znunit  15102  ef2kpi  16050  efper  16051  sinperlem  16052  sin2kpi  16055  cos2kpi  16056  abssinper  16090  sinkpi  16091  coskpi  16092  cxpexprp  16145  sgmval2  16270  ppiprm  16276  ppinprm  16277  chtprm  16278  chtnprm  16279  lgslem3  16343  lgsneg  16365  lgsdir2lem2  16370  lgsdir2lem4  16372  lgsdir2  16374  lgssq  16381  lgsmulsqcoprm  16387  lgsdirnn0  16388  gausslemma2dlem3  16404  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2  16424  2lgslem1a2  16428  2lgsoddprmlem1  16446  2lgsoddprmlem2  16447  2sqlem2  16456  2sqlem7  16462  wlk1walkdom  16822