Theorem zcn 12705

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℂcc 11205  ℤcz 12700

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-resscn 11264

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427  df-neg 11551  df-z 12701

This theorem is used by:  zsscn  12708  zsubcl  12745  zrevaddcl  12748  nzadd  12751  zlem1lt  12755  zltlem1  12756  zdiv  12776  zdivadd  12777  zdivmul  12778  zextlt  12780  zneo  12789  zeo2  12793  peano5uzi  12795  zindd  12807  znnn0nn  12817  zriotaneg  12819  zmax  13079  rebtwnz  13081  qmulz  13085  zq  13088  qaddcl  13100  qnegcl  13101  qmulcl  13102  qreccl  13104  fzen  13681  uzsubsubfz  13687  fz01en  13693  fzmmmeqm  13698  fzsubel  13701  fztp  13721  fzsuc2  13723  fzrev2  13729  fzrev3  13731  elfzp1b  13742  fzrevral  13753  fzrevral2  13754  fzrevral3  13755  fzshftral  13756  fzo0addel  13860  fzo0addelr  13861  fzoaddel2  13862  fzosubel2  13867  eluzgtdifelfzo  13869  fzocatel  13871  elfzom1elp1fzo  13874  fzval3  13876  zpnn0elfzo1  13881  fzosplitprm1  13920  fzoshftral  13929  flzadd  13973  2tnp1ge0ge0  13976  ceilid  13998  quoremz  14002  intfracq  14006  mulmod0  14024  zmod10  14034  modcyc  14053  modcyc2  14054  muladdmodid  14060  mulp1mod1  14061  modmuladdnn0  14065  modmul1  14074  modmulmodr  14087  modaddmulmod  14088  uzrdgxfr  14117  fzen2  14119  seqshft2  14178  sermono  14184  m1expeven  14259  expsub  14260  zesq  14377  modexp  14389  sqoddm1div8  14394  bccmpl  14460  swrd00  14800  swrdswrd  14862  swrdpfx  14864  pfxccatin12lem4  14883  pfxccatin12lem1  14885  swrdccatin2  14886  pfxccatin12lem2  14888  pfxccatin12  14890  repswrevw  14946  cshwsublen  14955  cshwidxmodr  14963  cshwidx0mod  14964  2cshw  14972  2cshwid  14973  2cshwcom  14975  cshweqdif2  14978  cshweqrep  14980  cshw1  14981  2cshwcshw  14984  shftuz  15231  seqshft  15247  nn0abscl  15488  zabs0b  15490  nnabscl  15502  climshftlem  15750  climshft  15752  isershft  15840  mptfzshft  15953  fsumrev  15954  fsum0diag2  15958  efexp  16278  efzval  16279  demoivre  16377  sqrt2irr  16426  dvdsval2  16434  iddvds  16448  1dvds  16449  dvds0  16450  negdvdsb  16451  dvdsnegb  16452  0dvds  16455  dvdsmul1  16456  iddvdsexp  16458  muldvds1  16459  muldvds2  16460  dvdscmul  16461  dvdsmulc  16462  dvdscmulr  16463  dvdsmulcr  16464  summodnegmod  16465  difmod0  16466  modmulconst  16467  dvds2ln  16468  dvds2add  16469  dvds2sub  16470  dvdstr  16473  dvdssub2  16480  dvdsadd  16481  dvdsaddr  16482  dvdssub  16483  dvdssubr  16484  dvdsadd2b  16485  dvdsaddre2b  16486  dvdsabseq  16492  divconjdvds  16494  alzdvds  16499  addmodlteqALT  16504  dvdsexp2im  16506  odd2np1lem  16519  odd2np1  16520  even2n  16521  oddp1even  16523  mod2eq1n2dvds  16526  mulsucdiv2z  16532  zob  16538  ltoddhalfle  16540  halfleoddlt  16541  opoe  16542  omoe  16543  opeo  16544  omeo  16545  m1exp1  16555  divalglem0  16572  divalglem2  16574  divalglem4  16575  divalglem5  16576  divalglem9  16580  divalgb  16583  divalgmod  16585  modremain  16587  ndvdssub  16588  ndvdsadd  16589  flodddiv4  16594  flodddiv4t2lthalf  16597  bits0  16607  bitsp1e  16611  bitsp1o  16612  gcdneg  16703  gcdaddmlem  16705  gcdaddm  16706  gcdadd  16707  gcdid  16708  modgcd  16714  gcdmultiplez  16717  bezoutlem1  16721  bezoutlem2  16722  bezoutlem4  16724  dvdsgcd  16726  mulgcd  16730  absmulgcd  16731  mulgcdr  16732  gcddiv  16733  dvdssqim  16736  dvdsexpim  16737  zexpgcd  16748  dvdssq  16751  bezoutr1  16753  lcmcllem  16780  lcmneg  16787  lcmgcdlem  16790  lcmgcd  16791  lcmid  16793  lcm1  16794  coprmdvds  16837  coprmdvds2  16838  qredeq  16841  qredeu  16842  divgcdcoprmex  16850  cncongr1  16851  cncongr2  16852  prmdvdsexp  16900  rpexp1i  16908  divnumden  16933  zsqrtelqelz  16943  phiprmpw  16962  vfermltlALT  16989  nnnn0modprm0  16993  modprmn0modprm0  16994  coprimeprodsq2  16996  iserodd  17022  pclem  17025  pcprendvds2  17028  pcpremul  17030  pcmul  17038  pcneg  17061  fldivp1  17084  prmpwdvds  17091  zgz  17120  modxai  17255  mod2xnegi  17258  chnccat  18809  chnrev  18810  mulgfval  19288  mulgz  19321  mulgassr  19331  mulgmodid  19332  odmod  19769  odf1  19785  odf1o1  19795  gexdvds  19807  zaddablx  20095  ablfacrp  20291  pgpfac1lem3  20302  ablsimpgfindlem1  20332  zsubrg  21735  zsssubrg  21740  zringsub  21770  zringmulg  21771  zringinvg  21780  zringunit  21781  zringcyg  21784  prmirred  21789  mulgrhm2  21793  pzriprnglem6  21801  pzriprnglem8  21803  pzriprnglem10  21805  pzriprnglem12  21807  fermltlchr  21844  znunit  21878  degltp1le  26400  ef2kpi  26816  efper  26817  sinperlem  26818  sin2kpi  26821  cos2kpi  26822  abssinper  26858  sinkpi  26859  coskpi  26860  eflogeq  26939  cxpexpz  27004  root1eq1  27092  cxpeq  27094  zrtelqelz  27095  zrtdvds  27096  relogbexp  27117  sgmval2  27479  ppiprm  27487  ppinprm  27488  chtprm  27489  chtnprm  27490  lgslem3  27635  lgsneg  27657  lgsdir2lem2  27662  lgsdir2lem4  27664  lgsdir2  27666  lgssq  27673  lgsmulsqcoprm  27679  lgsdirnn0  27680  gausslemma2dlem3  27704  lgsquadlem1  27716  lgsquadlem2  27717  lgsquad2  27722  2lgslem1a2  27726  2lgsoddprmlem1  27744  2lgsoddprmlem2  27745  2sqlem2  27754  2sqlem7  27760  rplogsumlem2  27821  axlowdimlem13  29541  wlk1walk  30228  clwwisshclwwslemlem  30613  ipasslem5  31446  rearchi  33957  znfermltl  33972  knoppndvlem9  37510  poimirlem19  38694  itg2addnclem2  38727  gcdaddmzz2nncomi  43182  zdivgd  43525  ef11d  43527  cxp112d  43529  cxp111d  43530  cxpi11d  43531  dffltz  43807  lzenom  43918  rexzrexnn0  43948  pell1234qrne0  43997  pell1234qrreccl  43998  pell1234qrmulcl  43999  pell1234qrdich  44005  pell14qrdich  44013  reglogexp  44038  reglogexpbas  44041  rmxm1  44078  rmym1  44079  rmxdbl  44083  rmydbl  44084  jm2.24  44107  congtr  44109  congadd  44110  congmul  44111  congsym  44112  congneg  44113  congid  44115  congabseq  44118  acongsym  44120  acongneg2  44121  acongtr  44122  acongrep  44124  jm2.19lem3  44135  jm2.19lem4  44136  jm2.19  44137  jm2.25  44143  jm2.26a  44144  oddfl  46430  coskpi2  47012  cosknegpi  47015  dvdsn1add  47085  itgsinexp  47101  fourierdlem42  47295  fourierdlem97  47349  fourierswlem  47376  sinnpoly  48077  2elfz2melfz  48524  ceilbi  48543  flmrecm1  48549  submodaddmod  48553  submodneaddmod  48563  mod0mul  48568  m1modmmod  48570  modmkpkne  48573  modlt0b  48575  sfprmdvdsmersenne  48824  proththd  48835  ppivalnnprm  48846  ppivalnnnprmge6  48847  dfodd6  48871  dfeven4  48872  evenm1odd  48873  evenp1odd  48874  enege  48879  onego  48880  dfeven2  48883  bits0ALTV  48913  opoeALTV  48917  opeoALTV  48918  evensumeven  48941  fppr2odd  48965  sbgoldbwt  49011  nnsum3primesgbe  49026  gpgedgvtx0  49295  gpg5nbgrvtx03starlem2  49303  gpg5nbgrvtx13starlem2  49306  0nodd  49403  2nodd  49405  1neven  49471  2zlidl  49473  2zrngamgm  49478  2zrngasgrp  49479  2zrngagrp  49482  2zrngmmgm  49485  2zrngmsgrp  49486  2zrngnmrid  49489  zlmodzxzsub  49608  flsubz  49770  zofldiv2  49779  dignn0flhalflem1  49863  dignn0flhalflem2  49864