Theorem zcn 12698

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11198  ℤcz 12693

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-resscn 11257

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-neg 11544  df-z 12694

This theorem is used by:  zsscn  12701  zsubcl  12738  zrevaddcl  12741  nzadd  12744  zlem1lt  12748  zltlem1  12749  zdiv  12769  zdivadd  12770  zdivmul  12771  zextlt  12773  zneo  12782  zeo2  12786  peano5uzi  12788  zindd  12800  znnn0nn  12810  zriotaneg  12812  zmax  13072  rebtwnz  13074  qmulz  13078  zq  13081  qaddcl  13093  qnegcl  13094  qmulcl  13095  qreccl  13097  fzen  13674  uzsubsubfz  13680  fz01en  13686  fzmmmeqm  13691  fzsubel  13694  fztp  13714  fzsuc2  13716  fzrev2  13722  fzrev3  13724  elfzp1b  13735  fzrevral  13746  fzrevral2  13747  fzrevral3  13748  fzshftral  13749  fzo0addel  13853  fzo0addelr  13854  fzoaddel2  13855  fzosubel2  13860  eluzgtdifelfzo  13862  fzocatel  13864  elfzom1elp1fzo  13867  fzval3  13869  zpnn0elfzo1  13874  fzosplitprm1  13913  fzoshftral  13922  flzadd  13966  2tnp1ge0ge0  13969  ceilid  13991  quoremz  13995  intfracq  13999  mulmod0  14017  zmod10  14027  modcyc  14046  modcyc2  14047  muladdmodid  14053  mulp1mod1  14054  modmuladdnn0  14058  modmul1  14067  modmulmodr  14080  modaddmulmod  14081  uzrdgxfr  14110  fzen2  14112  seqshft2  14171  sermono  14177  m1expeven  14252  expsub  14253  zesq  14370  modexp  14382  sqoddm1div8  14387  bccmpl  14453  swrd00  14792  swrdswrd  14854  swrdpfx  14856  pfxccatin12lem4  14875  pfxccatin12lem1  14877  swrdccatin2  14878  pfxccatin12lem2  14880  pfxccatin12  14882  repswrevw  14938  cshwsublen  14947  cshwidxmodr  14955  cshwidx0mod  14956  2cshw  14964  2cshwid  14965  2cshwcom  14967  cshweqdif2  14970  cshweqrep  14972  cshw1  14973  2cshwcshw  14976  shftuz  15222  seqshft  15238  nn0abscl  15479  zabs0b  15481  nnabscl  15493  climshftlem  15741  climshft  15743  isershft  15831  mptfzshft  15944  fsumrev  15945  fsum0diag2  15949  efexp  16269  efzval  16270  demoivre  16368  sqrt2irr  16417  dvdsval2  16425  iddvds  16439  1dvds  16440  dvds0  16441  negdvdsb  16442  dvdsnegb  16443  0dvds  16446  dvdsmul1  16447  iddvdsexp  16449  muldvds1  16450  muldvds2  16451  dvdscmul  16452  dvdsmulc  16453  dvdscmulr  16454  dvdsmulcr  16455  summodnegmod  16456  difmod0  16457  modmulconst  16458  dvds2ln  16459  dvds2add  16460  dvds2sub  16461  dvdstr  16464  dvdssub2  16471  dvdsadd  16472  dvdsaddr  16473  dvdssub  16474  dvdssubr  16475  dvdsadd2b  16476  dvdsaddre2b  16477  dvdsabseq  16483  divconjdvds  16485  alzdvds  16490  addmodlteqALT  16495  dvdsexp2im  16497  odd2np1lem  16510  odd2np1  16511  even2n  16512  oddp1even  16514  mod2eq1n2dvds  16517  mulsucdiv2z  16523  zob  16529  ltoddhalfle  16531  halfleoddlt  16532  opoe  16533  omoe  16534  opeo  16535  omeo  16536  m1exp1  16546  divalglem0  16563  divalglem2  16565  divalglem4  16566  divalglem5  16567  divalglem9  16571  divalgb  16574  divalgmod  16576  modremain  16578  ndvdssub  16579  ndvdsadd  16580  flodddiv4  16585  flodddiv4t2lthalf  16588  bits0  16598  bitsp1e  16602  bitsp1o  16603  gcdneg  16694  gcdaddmlem  16696  gcdaddm  16697  gcdadd  16698  gcdid  16699  modgcd  16705  gcdmultiplez  16708  bezoutlem1  16712  bezoutlem2  16713  bezoutlem4  16715  dvdsgcd  16717  mulgcd  16721  absmulgcd  16722  mulgcdr  16723  gcddiv  16724  dvdssqim  16727  dvdsexpim  16728  zexpgcd  16739  dvdssq  16742  bezoutr1  16744  lcmcllem  16771  lcmneg  16778  lcmgcdlem  16781  lcmgcd  16782  lcmid  16784  lcm1  16785  coprmdvds  16828  coprmdvds2  16829  qredeq  16832  qredeu  16833  divgcdcoprmex  16841  cncongr1  16842  cncongr2  16843  prmdvdsexp  16891  rpexp1i  16899  divnumden  16924  zsqrtelqelz  16934  phiprmpw  16953  vfermltlALT  16980  nnnn0modprm0  16984  modprmn0modprm0  16985  coprimeprodsq2  16987  iserodd  17013  pclem  17016  pcprendvds2  17019  pcpremul  17021  pcmul  17029  pcneg  17052  fldivp1  17075  prmpwdvds  17082  zgz  17111  modxai  17246  mod2xnegi  17249  chnccat  18800  chnrev  18801  mulgfval  19279  mulgz  19312  mulgassr  19322  mulgmodid  19323  odmod  19760  odf1  19776  odf1o1  19786  gexdvds  19798  zaddablx  20086  ablfacrp  20282  pgpfac1lem3  20293  ablsimpgfindlem1  20323  zsubrg  21726  zsssubrg  21731  zringsub  21761  zringmulg  21762  zringinvg  21771  zringunit  21772  zringcyg  21775  prmirred  21780  mulgrhm2  21784  pzriprnglem6  21792  pzriprnglem8  21794  pzriprnglem10  21796  pzriprnglem12  21798  fermltlchr  21835  znunit  21869  degltp1le  26391  ef2kpi  26807  efper  26808  sinperlem  26809  sin2kpi  26812  cos2kpi  26813  abssinper  26849  sinkpi  26850  coskpi  26851  eflogeq  26930  cxpexpz  26995  root1eq1  27083  cxpeq  27085  zrtelqelz  27086  zrtdvds  27087  relogbexp  27108  sgmval2  27470  ppiprm  27478  ppinprm  27479  chtprm  27480  chtnprm  27481  lgslem3  27626  lgsneg  27648  lgsdir2lem2  27653  lgsdir2lem4  27655  lgsdir2  27657  lgssq  27664  lgsmulsqcoprm  27670  lgsdirnn0  27671  gausslemma2dlem3  27695  lgsquadlem1  27707  lgsquadlem2  27708  lgsquad2  27713  2lgslem1a2  27717  2lgsoddprmlem1  27735  2lgsoddprmlem2  27736  2sqlem2  27745  2sqlem7  27751  rplogsumlem2  27812  axlowdimlem13  29532  wlk1walk  30219  clwwisshclwwslemlem  30604  ipasslem5  31437  rearchi  33907  znfermltl  33922  knoppndvlem9  37386  poimirlem19  38557  itg2addnclem2  38590  gcdaddmzz2nncomi  43045  zdivgd  43388  ef11d  43390  cxp112d  43392  cxp111d  43393  cxpi11d  43394  dffltz  43670  lzenom  43780  rexzrexnn0  43810  pell1234qrne0  43859  pell1234qrreccl  43860  pell1234qrmulcl  43861  pell1234qrdich  43867  pell14qrdich  43875  reglogexp  43900  reglogexpbas  43903  rmxm1  43940  rmym1  43941  rmxdbl  43945  rmydbl  43946  jm2.24  43969  congtr  43971  congadd  43972  congmul  43973  congsym  43974  congneg  43975  congid  43977  congabseq  43980  acongsym  43982  acongneg2  43983  acongtr  43984  acongrep  43986  jm2.19lem3  43997  jm2.19lem4  43998  jm2.19  43999  jm2.25  44005  jm2.26a  44006  oddfl  46293  coskpi2  46875  cosknegpi  46878  dvdsn1add  46948  itgsinexp  46964  fourierdlem42  47158  fourierdlem97  47212  fourierswlem  47239  sinnpoly  47940  2elfz2melfz  48387  ceilbi  48406  flmrecm1  48412  submodaddmod  48416  submodneaddmod  48426  mod0mul  48431  m1modmmod  48433  modmkpkne  48436  modlt0b  48438  sfprmdvdsmersenne  48687  proththd  48698  ppivalnnprm  48709  ppivalnnnprmge6  48710  dfodd6  48734  dfeven4  48735  evenm1odd  48736  evenp1odd  48737  enege  48742  onego  48743  dfeven2  48746  bits0ALTV  48776  opoeALTV  48780  opeoALTV  48781  evensumeven  48804  fppr2odd  48828  sbgoldbwt  48874  nnsum3primesgbe  48889  gpgedgvtx0  49158  gpg5nbgrvtx03starlem2  49166  gpg5nbgrvtx13starlem2  49169  0nodd  49266  2nodd  49268  1neven  49334  2zlidl  49336  2zrngamgm  49341  2zrngasgrp  49342  2zrngagrp  49345  2zrngmmgm  49348  2zrngmsgrp  49349  2zrngnmrid  49352  zlmodzxzsub  49471  flsubz  49633  zofldiv2  49642  dignn0flhalflem1  49726  dignn0flhalflem2  49727