Theorem zcn 12615

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℂcc 11150  ℤcz 12610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-neg 11492  df-z 12611

This theorem is referenced by:  zsscn  12618  zsubcl  12656  zrevaddcl  12659  nzadd  12662  zlem1lt  12666  zltlem1  12667  zdiv  12685  zdivadd  12686  zdivmul  12687  zextlt  12689  zneo  12698  zeo2  12702  peano5uzi  12704  zindd  12716  znnn0nn  12726  zriotaneg  12728  zmax  12984  rebtwnz  12986  qmulz  12990  zq  12993  qaddcl  13004  qnegcl  13005  qmulcl  13006  qreccl  13008  fzen  13577  uzsubsubfz  13582  fz01en  13588  fzmmmeqm  13593  fzsubel  13596  fztp  13616  fzsuc2  13618  fzrev2  13624  fzrev3  13626  elfzp1b  13637  fzrevral  13648  fzrevral2  13649  fzrevral3  13650  fzshftral  13651  fzo0addel  13753  fzo0addelr  13754  fzoaddel2  13755  fzosubel2  13760  eluzgtdifelfzo  13762  fzocatel  13764  elfzom1elp1fzo  13767  fzval3  13769  zpnn0elfzo1  13774  fzosplitprm1  13812  fzoshftral  13819  flzadd  13862  2tnp1ge0ge0  13865  ceilid  13887  quoremz  13891  intfracq  13895  mulmod0  13913  zmod10  13923  modcyc  13942  modcyc2  13943  muladdmodid  13947  mulp1mod1  13948  modmuladdnn0  13952  modmul1  13961  modmulmodr  13974  modaddmulmod  13975  uzrdgxfr  14004  fzen2  14006  seqshft2  14065  sermono  14071  m1expeven  14146  expsub  14147  zesq  14261  modexp  14273  sqoddm1div8  14278  bccmpl  14344  swrd00  14678  addlenrevpfx  14724  swrdswrd  14739  swrdpfx  14741  pfxccatin12lem4  14760  pfxccatin12lem1  14762  swrdccatin2  14763  pfxccatin12lem2  14765  pfxccatin12  14767  repswrevw  14821  cshwsublen  14830  cshwidxmodr  14838  cshwidx0mod  14839  2cshw  14847  2cshwid  14848  2cshwcom  14850  cshweqdif2  14853  cshweqrep  14855  cshw1  14856  2cshwcshw  14860  shftuz  15104  seqshft  15120  nn0abscl  15347  nnabscl  15360  climshftlem  15606  climshft  15608  isershft  15696  mptfzshft  15810  fsumrev  15811  fsum0diag2  15815  efexp  16133  efzval  16134  demoivre  16232  sqrt2irr  16281  dvdsval2  16289  iddvds  16303  1dvds  16304  dvds0  16305  negdvdsb  16306  dvdsnegb  16307  0dvds  16310  dvdsmul1  16311  iddvdsexp  16313  muldvds1  16314  muldvds2  16315  dvdscmul  16316  dvdsmulc  16317  dvdscmulr  16318  dvdsmulcr  16319  summodnegmod  16320  modmulconst  16321  dvds2ln  16322  dvds2add  16323  dvds2sub  16324  dvdstr  16327  dvdssub2  16334  dvdsadd  16335  dvdsaddr  16336  dvdssub  16337  dvdssubr  16338  dvdsadd2b  16339  dvdsaddre2b  16340  dvdsabseq  16346  divconjdvds  16348  alzdvds  16353  addmodlteqALT  16358  dvdsexp2im  16360  odd2np1lem  16373  odd2np1  16374  even2n  16375  oddp1even  16377  mod2eq1n2dvds  16380  mulsucdiv2z  16386  zob  16392  ltoddhalfle  16394  halfleoddlt  16395  opoe  16396  omoe  16397  opeo  16398  omeo  16399  m1exp1  16409  divalglem0  16426  divalglem2  16428  divalglem4  16429  divalglem5  16430  divalglem9  16434  divalgb  16437  divalgmod  16439  modremain  16441  ndvdssub  16442  ndvdsadd  16443  flodddiv4  16448  flodddiv4t2lthalf  16451  bits0  16461  bitsp1e  16465  bitsp1o  16466  gcdneg  16555  gcdaddmlem  16557  gcdaddm  16558  gcdadd  16559  gcdid  16560  modgcd  16565  gcdmultiplez  16568  bezoutlem1  16572  bezoutlem2  16573  bezoutlem4  16575  dvdsgcd  16577  mulgcd  16581  absmulgcd  16582  mulgcdr  16583  gcddiv  16584  dvdssqim  16587  dvdsexpim  16588  zexpgcd  16598  dvdssq  16600  bezoutr1  16602  lcmcllem  16629  lcmneg  16636  lcmgcdlem  16639  lcmgcd  16640  lcmid  16642  lcm1  16643  coprmdvds  16686  coprmdvds2  16687  qredeq  16690  qredeu  16691  divgcdcoprmex  16699  cncongr1  16700  cncongr2  16701  prmdvdsexp  16748  rpexp1i  16756  divnumden  16781  zsqrtelqelz  16791  phiprmpw  16809  vfermltlALT  16835  nnnn0modprm0  16839  modprmn0modprm0  16840  coprimeprodsq2  16842  iserodd  16868  pclem  16871  pcprendvds2  16874  pcpremul  16876  pcmul  16884  pcneg  16907  fldivp1  16930  prmpwdvds  16937  zgz  16966  modxai  17101  mod2xnegi  17104  mulgfval  19099  mulgz  19132  mulgassr  19142  mulgmodid  19143  odmod  19578  odf1  19594  odf1o1  19604  gexdvds  19616  zaddablx  19904  ablfacrp  20100  pgpfac1lem3  20111  ablsimpgfindlem1  20141  zsubrg  21455  zsssubrg  21460  zringsub  21483  zringmulg  21484  zringinvg  21493  zringunit  21494  zringcyg  21497  prmirred  21502  mulgrhm2  21506  pzriprnglem6  21514  pzriprnglem8  21516  pzriprnglem10  21518  pzriprnglem12  21520  fermltlchr  21561  znunit  21599  degltp1le  26126  ef2kpi  26534  efper  26535  sinperlem  26536  sin2kpi  26539  cos2kpi  26540  abssinper  26577  sinkpi  26578  coskpi  26579  eflogeq  26658  cxpexpz  26723  root1eq1  26812  cxpeq  26814  zrtelqelz  26815  zrtdvds  26816  relogbexp  26837  sgmval2  27200  ppiprm  27208  ppinprm  27209  chtprm  27210  chtnprm  27211  lgslem3  27357  lgsneg  27379  lgsdir2lem2  27384  lgsdir2lem4  27386  lgsdir2  27388  lgssq  27395  lgsmulsqcoprm  27401  lgsdirnn0  27402  gausslemma2dlem3  27426  lgsquadlem1  27438  lgsquadlem2  27439  lgsquad2  27444  2lgslem1a2  27448  2lgsoddprmlem1  27466  2lgsoddprmlem2  27467  2sqlem2  27476  2sqlem7  27482  rplogsumlem2  27543  axlowdimlem13  28983  wlk1walk  29671  clwwisshclwwslemlem  30041  ipasslem5  30863  rearchi  33353  znfermltl  33373  knoppndvlem9  36502  poimirlem19  37625  itg2addnclem2  37658  gcdaddmzz2nncomi  41976  metakunt16  42201  zdivgd  42350  ef11d  42353  cxp112d  42355  cxp111d  42356  cxpi11d  42357  dffltz  42620  lzenom  42757  rexzrexnn0  42791  pell1234qrne0  42840  pell1234qrreccl  42841  pell1234qrmulcl  42842  pell1234qrdich  42848  pell14qrdich  42856  reglogexp  42881  reglogexpbas  42884  rmxm1  42922  rmym1  42923  rmxdbl  42927  rmydbl  42928  jm2.24  42951  congtr  42953  congadd  42954  congmul  42955  congsym  42956  congneg  42957  congid  42959  congabseq  42962  acongsym  42964  acongneg2  42965  acongtr  42966  acongrep  42968  jm2.19lem3  42979  jm2.19lem4  42980  jm2.19  42981  jm2.25  42987  jm2.26a  42988  oddfl  45227  coskpi2  45821  cosknegpi  45824  dvdsn1add  45894  itgsinexp  45910  fourierdlem42  46104  fourierdlem97  46158  fourierswlem  46185  2elfz2melfz  47267  submodaddmod  47280  submodneaddmod  47290  sfprmdvdsmersenne  47527  proththd  47538  dfodd6  47561  dfeven4  47562  evenm1odd  47563  evenp1odd  47564  enege  47569  onego  47570  dfeven2  47573  bits0ALTV  47603  opoeALTV  47607  opeoALTV  47608  evensumeven  47631  fppr2odd  47655  sbgoldbwt  47701  nnsum3primesgbe  47716  gpgedgvtx0  47953  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx13starlem2  47962  0nodd  48013  2nodd  48015  1neven  48081  2zlidl  48083  2zrngamgm  48088  2zrngasgrp  48089  2zrngagrp  48092  2zrngmmgm  48095  2zrngmsgrp  48096  2zrngnmrid  48099  zlmodzxzsub  48204  flsubz  48367  mod0mul  48368  m1modmmod  48370  zofldiv2  48380  dignn0flhalflem1  48464  dignn0flhalflem2  48465