Theorem zcn 12491

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11022  ℤcz 12486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-resscn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-neg 11365  df-z 12487

This theorem is referenced by:  zsscn  12494  zsubcl  12531  zrevaddcl  12534  nzadd  12537  zlem1lt  12541  zltlem1  12542  zdiv  12560  zdivadd  12561  zdivmul  12562  zextlt  12564  zneo  12573  zeo2  12577  peano5uzi  12579  zindd  12591  znnn0nn  12601  zriotaneg  12603  zmax  12856  rebtwnz  12858  qmulz  12862  zq  12865  qaddcl  12876  qnegcl  12877  qmulcl  12878  qreccl  12880  fzen  13455  uzsubsubfz  13460  fz01en  13466  fzmmmeqm  13471  fzsubel  13474  fztp  13494  fzsuc2  13496  fzrev2  13502  fzrev3  13504  elfzp1b  13515  fzrevral  13526  fzrevral2  13527  fzrevral3  13528  fzshftral  13529  fzo0addel  13632  fzo0addelr  13633  fzoaddel2  13634  fzosubel2  13639  eluzgtdifelfzo  13641  fzocatel  13643  elfzom1elp1fzo  13646  fzval3  13648  zpnn0elfzo1  13653  fzosplitprm1  13692  fzoshftral  13701  flzadd  13744  2tnp1ge0ge0  13747  ceilid  13769  quoremz  13773  intfracq  13777  mulmod0  13795  zmod10  13805  modcyc  13824  modcyc2  13825  muladdmodid  13831  mulp1mod1  13832  modmuladdnn0  13836  modmul1  13845  modmulmodr  13858  modaddmulmod  13859  uzrdgxfr  13888  fzen2  13890  seqshft2  13949  sermono  13955  m1expeven  14030  expsub  14031  zesq  14147  modexp  14159  sqoddm1div8  14164  bccmpl  14230  swrd00  14566  swrdswrd  14626  swrdpfx  14628  pfxccatin12lem4  14647  pfxccatin12lem1  14649  swrdccatin2  14650  pfxccatin12lem2  14652  pfxccatin12  14654  repswrevw  14708  cshwsublen  14717  cshwidxmodr  14725  cshwidx0mod  14726  2cshw  14734  2cshwid  14735  2cshwcom  14737  cshweqdif2  14740  cshweqrep  14742  cshw1  14743  2cshwcshw  14746  shftuz  14990  seqshft  15006  nn0abscl  15233  zabs0b  15235  nnabscl  15247  climshftlem  15495  climshft  15497  isershft  15585  mptfzshft  15699  fsumrev  15700  fsum0diag2  15704  efexp  16024  efzval  16025  demoivre  16123  sqrt2irr  16172  dvdsval2  16180  iddvds  16194  1dvds  16195  dvds0  16196  negdvdsb  16197  dvdsnegb  16198  0dvds  16201  dvdsmul1  16202  iddvdsexp  16204  muldvds1  16205  muldvds2  16206  dvdscmul  16207  dvdsmulc  16208  dvdscmulr  16209  dvdsmulcr  16210  summodnegmod  16211  difmod0  16212  modmulconst  16213  dvds2ln  16214  dvds2add  16215  dvds2sub  16216  dvdstr  16219  dvdssub2  16226  dvdsadd  16227  dvdsaddr  16228  dvdssub  16229  dvdssubr  16230  dvdsadd2b  16231  dvdsaddre2b  16232  dvdsabseq  16238  divconjdvds  16240  alzdvds  16245  addmodlteqALT  16250  dvdsexp2im  16252  odd2np1lem  16265  odd2np1  16266  even2n  16267  oddp1even  16269  mod2eq1n2dvds  16272  mulsucdiv2z  16278  zob  16284  ltoddhalfle  16286  halfleoddlt  16287  opoe  16288  omoe  16289  opeo  16290  omeo  16291  m1exp1  16301  divalglem0  16318  divalglem2  16320  divalglem4  16321  divalglem5  16322  divalglem9  16326  divalgb  16329  divalgmod  16331  modremain  16333  ndvdssub  16334  ndvdsadd  16335  flodddiv4  16340  flodddiv4t2lthalf  16343  bits0  16353  bitsp1e  16357  bitsp1o  16358  gcdneg  16447  gcdaddmlem  16449  gcdaddm  16450  gcdadd  16451  gcdid  16452  modgcd  16457  gcdmultiplez  16460  bezoutlem1  16464  bezoutlem2  16465  bezoutlem4  16467  dvdsgcd  16469  mulgcd  16473  absmulgcd  16474  mulgcdr  16475  gcddiv  16476  dvdssqim  16479  dvdsexpim  16480  zexpgcd  16490  dvdssq  16492  bezoutr1  16494  lcmcllem  16521  lcmneg  16528  lcmgcdlem  16531  lcmgcd  16532  lcmid  16534  lcm1  16535  coprmdvds  16578  coprmdvds2  16579  qredeq  16582  qredeu  16583  divgcdcoprmex  16591  cncongr1  16592  cncongr2  16593  prmdvdsexp  16640  rpexp1i  16648  divnumden  16673  zsqrtelqelz  16683  phiprmpw  16701  vfermltlALT  16728  nnnn0modprm0  16732  modprmn0modprm0  16733  coprimeprodsq2  16735  iserodd  16761  pclem  16764  pcprendvds2  16767  pcpremul  16769  pcmul  16777  pcneg  16800  fldivp1  16823  prmpwdvds  16830  zgz  16859  modxai  16994  mod2xnegi  16997  chnccat  18547  chnrev  18548  mulgfval  18997  mulgz  19030  mulgassr  19040  mulgmodid  19041  odmod  19473  odf1  19489  odf1o1  19499  gexdvds  19511  zaddablx  19799  ablfacrp  19995  pgpfac1lem3  20006  ablsimpgfindlem1  20036  zsubrg  21373  zsssubrg  21378  zringsub  21408  zringmulg  21409  zringinvg  21418  zringunit  21419  zringcyg  21422  prmirred  21427  mulgrhm2  21431  pzriprnglem6  21439  pzriprnglem8  21441  pzriprnglem10  21443  pzriprnglem12  21445  fermltlchr  21482  znunit  21516  degltp1le  26032  ef2kpi  26441  efper  26442  sinperlem  26443  sin2kpi  26446  cos2kpi  26447  abssinper  26484  sinkpi  26485  coskpi  26486  eflogeq  26565  cxpexpz  26630  root1eq1  26719  cxpeq  26721  zrtelqelz  26722  zrtdvds  26723  relogbexp  26744  sgmval2  27107  ppiprm  27115  ppinprm  27116  chtprm  27117  chtnprm  27118  lgslem3  27264  lgsneg  27286  lgsdir2lem2  27291  lgsdir2lem4  27293  lgsdir2  27295  lgssq  27302  lgsmulsqcoprm  27308  lgsdirnn0  27309  gausslemma2dlem3  27333  lgsquadlem1  27345  lgsquadlem2  27346  lgsquad2  27351  2lgslem1a2  27355  2lgsoddprmlem1  27373  2lgsoddprmlem2  27374  2sqlem2  27383  2sqlem7  27389  rplogsumlem2  27450  axlowdimlem13  28976  wlk1walk  29661  clwwisshclwwslemlem  30037  ipasslem5  30859  rearchi  33376  znfermltl  33396  knoppndvlem9  36663  poimirlem19  37779  itg2addnclem2  37812  gcdaddmzz2nncomi  42188  zdivgd  42534  ef11d  42536  cxp112d  42538  cxp111d  42539  cxpi11d  42540  dffltz  42819  lzenom  42954  rexzrexnn0  42988  pell1234qrne0  43037  pell1234qrreccl  43038  pell1234qrmulcl  43039  pell1234qrdich  43045  pell14qrdich  43053  reglogexp  43078  reglogexpbas  43081  rmxm1  43118  rmym1  43119  rmxdbl  43123  rmydbl  43124  jm2.24  43147  congtr  43149  congadd  43150  congmul  43151  congsym  43152  congneg  43153  congid  43155  congabseq  43158  acongsym  43160  acongneg2  43161  acongtr  43162  acongrep  43164  jm2.19lem3  43175  jm2.19lem4  43176  jm2.19  43177  jm2.25  43183  jm2.26a  43184  oddfl  45468  coskpi2  46052  cosknegpi  46055  dvdsn1add  46125  itgsinexp  46141  fourierdlem42  46335  fourierdlem97  46389  fourierswlem  46416  sinnpoly  47079  2elfz2melfz  47506  ceilbi  47521  submodaddmod  47529  submodneaddmod  47539  mod0mul  47544  m1modmmod  47546  modmkpkne  47549  modlt0b  47551  sfprmdvdsmersenne  47791  proththd  47802  dfodd6  47825  dfeven4  47826  evenm1odd  47827  evenp1odd  47828  enege  47833  onego  47834  dfeven2  47837  bits0ALTV  47867  opoeALTV  47871  opeoALTV  47872  evensumeven  47895  fppr2odd  47919  sbgoldbwt  47965  nnsum3primesgbe  47980  gpgedgvtx0  48249  gpg5nbgrvtx03starlem2  48257  gpg5nbgrvtx13starlem2  48260  0nodd  48358  2nodd  48360  1neven  48426  2zlidl  48428  2zrngamgm  48433  2zrngasgrp  48434  2zrngagrp  48437  2zrngmmgm  48440  2zrngmsgrp  48441  2zrngnmrid  48444  zlmodzxzsub  48548  flsubz  48710  zofldiv2  48719  dignn0flhalflem1  48803  dignn0flhalflem2  48804