Theorem zcn 12591

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℂcc 11093  ℤcz 12586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-neg 11439  df-z 12587

This theorem is referenced by:  zsscn  12594  zsubcl  12631  zrevaddcl  12634  nzadd  12637  zlem1lt  12641  zltlem1  12642  zdiv  12661  zdivadd  12662  zdivmul  12663  zextlt  12665  zneo  12674  zeo2  12678  peano5uzi  12680  zindd  12692  znnn0nn  12702  zriotaneg  12704  zmax  12964  rebtwnz  12966  qmulz  12970  zq  12973  qaddcl  12984  qnegcl  12985  qmulcl  12986  qreccl  12988  fzen  13564  uzsubsubfz  13570  fz01en  13576  fzmmmeqm  13581  fzsubel  13584  fztp  13604  fzsuc2  13606  fzrev2  13612  fzrev3  13614  elfzp1b  13625  fzrevral  13636  fzrevral2  13637  fzrevral3  13638  fzshftral  13639  fzo0addel  13743  fzo0addelr  13744  fzoaddel2  13745  fzosubel2  13750  eluzgtdifelfzo  13752  fzocatel  13754  elfzom1elp1fzo  13757  fzval3  13759  zpnn0elfzo1  13764  fzosplitprm1  13803  fzoshftral  13812  flzadd  13855  2tnp1ge0ge0  13858  ceilid  13880  quoremz  13884  intfracq  13888  mulmod0  13906  zmod10  13916  modcyc  13935  modcyc2  13936  muladdmodid  13942  mulp1mod1  13943  modmuladdnn0  13947  modmul1  13956  modmulmodr  13969  modaddmulmod  13970  uzrdgxfr  13999  fzen2  14001  seqshft2  14060  sermono  14066  m1expeven  14141  expsub  14142  zesq  14258  modexp  14270  sqoddm1div8  14275  bccmpl  14341  swrd00  14678  swrdswrd  14738  swrdpfx  14740  pfxccatin12lem4  14759  pfxccatin12lem1  14761  swrdccatin2  14762  pfxccatin12lem2  14764  pfxccatin12  14766  repswrevw  14820  cshwsublen  14829  cshwidxmodr  14837  cshwidx0mod  14838  2cshw  14846  2cshwid  14847  2cshwcom  14849  cshweqdif2  14852  cshweqrep  14854  cshw1  14855  2cshwcshw  14858  shftuz  15102  seqshft  15118  nn0abscl  15359  zabs0b  15361  nnabscl  15373  climshftlem  15621  climshft  15623  isershft  15711  mptfzshft  15825  fsumrev  15826  fsum0diag2  15830  efexp  16152  efzval  16153  demoivre  16251  sqrt2irr  16300  dvdsval2  16308  iddvds  16322  1dvds  16323  dvds0  16324  negdvdsb  16325  dvdsnegb  16326  0dvds  16329  dvdsmul1  16330  iddvdsexp  16332  muldvds1  16333  muldvds2  16334  dvdscmul  16335  dvdsmulc  16336  dvdscmulr  16337  dvdsmulcr  16338  summodnegmod  16339  difmod0  16340  modmulconst  16341  dvds2ln  16342  dvds2add  16343  dvds2sub  16344  dvdstr  16347  dvdssub2  16354  dvdsadd  16355  dvdsaddr  16356  dvdssub  16357  dvdssubr  16358  dvdsadd2b  16359  dvdsaddre2b  16360  dvdsabseq  16366  divconjdvds  16368  alzdvds  16373  addmodlteqALT  16378  dvdsexp2im  16380  odd2np1lem  16393  odd2np1  16394  even2n  16395  oddp1even  16397  mod2eq1n2dvds  16400  mulsucdiv2z  16406  zob  16412  ltoddhalfle  16414  halfleoddlt  16415  opoe  16416  omoe  16417  opeo  16418  omeo  16419  m1exp1  16429  divalglem0  16446  divalglem2  16448  divalglem4  16449  divalglem5  16450  divalglem9  16454  divalgb  16457  divalgmod  16459  modremain  16461  ndvdssub  16462  ndvdsadd  16463  flodddiv4  16468  flodddiv4t2lthalf  16471  bits0  16481  bitsp1e  16485  bitsp1o  16486  gcdneg  16575  gcdaddmlem  16577  gcdaddm  16578  gcdadd  16579  gcdid  16580  modgcd  16585  gcdmultiplez  16588  bezoutlem1  16592  bezoutlem2  16593  bezoutlem4  16595  dvdsgcd  16597  mulgcd  16601  absmulgcd  16602  mulgcdr  16603  gcddiv  16604  dvdssqim  16607  dvdsexpim  16608  zexpgcd  16618  dvdssq  16620  bezoutr1  16622  lcmcllem  16649  lcmneg  16656  lcmgcdlem  16659  lcmgcd  16660  lcmid  16662  lcm1  16663  coprmdvds  16706  coprmdvds2  16707  qredeq  16710  qredeu  16711  divgcdcoprmex  16719  cncongr1  16720  cncongr2  16721  prmdvdsexp  16769  rpexp1i  16777  divnumden  16802  zsqrtelqelz  16812  phiprmpw  16830  vfermltlALT  16857  nnnn0modprm0  16861  modprmn0modprm0  16862  coprimeprodsq2  16864  iserodd  16890  pclem  16893  pcprendvds2  16896  pcpremul  16898  pcmul  16906  pcneg  16929  fldivp1  16952  prmpwdvds  16959  zgz  16988  modxai  17123  mod2xnegi  17126  chnccat  18677  chnrev  18678  mulgfval  19130  mulgz  19163  mulgassr  19173  mulgmodid  19174  odmod  19611  odf1  19627  odf1o1  19637  gexdvds  19649  zaddablx  19937  ablfacrp  20133  pgpfac1lem3  20144  ablsimpgfindlem1  20174  zsubrg  21570  zsssubrg  21575  zringsub  21605  zringmulg  21606  zringinvg  21615  zringunit  21616  zringcyg  21619  prmirred  21624  mulgrhm2  21628  pzriprnglem6  21636  pzriprnglem8  21638  pzriprnglem10  21640  pzriprnglem12  21642  fermltlchr  21679  znunit  21713  degltp1le  26230  ef2kpi  26643  efper  26644  sinperlem  26645  sin2kpi  26648  cos2kpi  26649  abssinper  26686  sinkpi  26687  coskpi  26688  eflogeq  26767  cxpexpz  26832  root1eq1  26920  cxpeq  26922  zrtelqelz  26923  zrtdvds  26924  relogbexp  26945  sgmval2  27307  ppiprm  27315  ppinprm  27316  chtprm  27317  chtnprm  27318  lgslem3  27463  lgsneg  27485  lgsdir2lem2  27490  lgsdir2lem4  27492  lgsdir2  27494  lgssq  27501  lgsmulsqcoprm  27507  lgsdirnn0  27508  gausslemma2dlem3  27532  lgsquadlem1  27544  lgsquadlem2  27545  lgsquad2  27550  2lgslem1a2  27554  2lgsoddprmlem1  27572  2lgsoddprmlem2  27573  2sqlem2  27582  2sqlem7  27588  rplogsumlem2  27649  axlowdimlem13  29304  wlk1walk  29988  clwwisshclwwslemlem  30364  ipasslem5  31187  rearchi  33666  znfermltl  33681  knoppndvlem9  37129  poimirlem19  38310  itg2addnclem2  38343  gcdaddmzz2nncomi  42782  zdivgd  43118  ef11d  43120  cxp112d  43122  cxp111d  43123  cxpi11d  43124  dffltz  43386  lzenom  43521  rexzrexnn0  43551  pell1234qrne0  43600  pell1234qrreccl  43601  pell1234qrmulcl  43602  pell1234qrdich  43608  pell14qrdich  43616  reglogexp  43641  reglogexpbas  43644  rmxm1  43681  rmym1  43682  rmxdbl  43686  rmydbl  43687  jm2.24  43710  congtr  43712  congadd  43713  congmul  43714  congsym  43715  congneg  43716  congid  43718  congabseq  43721  acongsym  43723  acongneg2  43724  acongtr  43725  acongrep  43727  jm2.19lem3  43738  jm2.19lem4  43739  jm2.19  43740  jm2.25  43746  jm2.26a  43747  oddfl  46017  coskpi2  46600  cosknegpi  46603  dvdsn1add  46673  itgsinexp  46689  fourierdlem42  46883  fourierdlem97  46937  fourierswlem  46964  sinnpoly  47648  2elfz2melfz  48075  ceilbi  48094  flmrecm1  48100  submodaddmod  48104  submodneaddmod  48114  mod0mul  48119  m1modmmod  48121  modmkpkne  48124  modlt0b  48126  sfprmdvdsmersenne  48375  proththd  48386  ppivalnnprm  48397  ppivalnnnprmge6  48398  dfodd6  48422  dfeven4  48423  evenm1odd  48424  evenp1odd  48425  enege  48430  onego  48431  dfeven2  48434  bits0ALTV  48464  opoeALTV  48468  opeoALTV  48469  evensumeven  48492  fppr2odd  48516  sbgoldbwt  48562  nnsum3primesgbe  48577  gpgedgvtx0  48846  gpg5nbgrvtx03starlem2  48854  gpg5nbgrvtx13starlem2  48857  0nodd  48955  2nodd  48957  1neven  49023  2zlidl  49025  2zrngamgm  49030  2zrngasgrp  49031  2zrngagrp  49034  2zrngmmgm  49037  2zrngmsgrp  49038  2zrngnmrid  49041  zlmodzxzsub  49160  flsubz  49322  zofldiv2  49331  dignn0flhalflem1  49415  dignn0flhalflem2  49416