Theorem zcn 12596

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

Syntax hints:   → wi 4   ∈ wcel 2149  ℂcc 11098  ℤcz 12591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-resscn 11157

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-neg 11444  df-z 12592

This theorem is referenced by:  zsscn  12599  zsubcl  12636  zrevaddcl  12639  nzadd  12642  zlem1lt  12646  zltlem1  12647  zdiv  12666  zdivadd  12667  zdivmul  12668  zextlt  12670  zneo  12679  zeo2  12683  peano5uzi  12685  zindd  12697  znnn0nn  12707  zriotaneg  12709  zmax  12969  rebtwnz  12971  qmulz  12975  zq  12978  qaddcl  12989  qnegcl  12990  qmulcl  12991  qreccl  12993  fzen  13569  uzsubsubfz  13574  fz01en  13580  fzmmmeqm  13585  fzsubel  13588  fztp  13608  fzsuc2  13610  fzrev2  13616  fzrev3  13618  elfzp1b  13629  fzrevral  13640  fzrevral2  13641  fzrevral3  13642  fzshftral  13643  fzo0addel  13747  fzo0addelr  13748  fzoaddel2  13749  fzosubel2  13754  eluzgtdifelfzo  13756  fzocatel  13758  elfzom1elp1fzo  13761  fzval3  13763  zpnn0elfzo1  13768  fzosplitprm1  13807  fzoshftral  13816  flzadd  13859  2tnp1ge0ge0  13862  ceilid  13884  quoremz  13888  intfracq  13892  mulmod0  13910  zmod10  13920  modcyc  13939  modcyc2  13940  muladdmodid  13946  mulp1mod1  13947  modmuladdnn0  13951  modmul1  13960  modmulmodr  13973  modaddmulmod  13974  uzrdgxfr  14003  fzen2  14005  seqshft2  14064  sermono  14070  m1expeven  14145  expsub  14146  zesq  14262  modexp  14274  sqoddm1div8  14279  bccmpl  14345  swrd00  14682  swrdswrd  14742  swrdpfx  14744  pfxccatin12lem4  14763  pfxccatin12lem1  14765  swrdccatin2  14766  pfxccatin12lem2  14768  pfxccatin12  14770  repswrevw  14824  cshwsublen  14833  cshwidxmodr  14841  cshwidx0mod  14842  2cshw  14850  2cshwid  14851  2cshwcom  14853  cshweqdif2  14856  cshweqrep  14858  cshw1  14859  2cshwcshw  14862  shftuz  15106  seqshft  15122  nn0abscl  15363  zabs0b  15365  nnabscl  15377  climshftlem  15625  climshft  15627  isershft  15715  mptfzshft  15829  fsumrev  15830  fsum0diag2  15834  efexp  16157  efzval  16158  demoivre  16256  sqrt2irr  16305  dvdsval2  16313  iddvds  16327  1dvds  16328  dvds0  16329  negdvdsb  16330  dvdsnegb  16331  0dvds  16334  dvdsmul1  16335  iddvdsexp  16337  muldvds1  16338  muldvds2  16339  dvdscmul  16340  dvdsmulc  16341  dvdscmulr  16342  dvdsmulcr  16343  summodnegmod  16344  difmod0  16345  modmulconst  16346  dvds2ln  16347  dvds2add  16348  dvds2sub  16349  dvdstr  16352  dvdssub2  16359  dvdsadd  16360  dvdsaddr  16361  dvdssub  16362  dvdssubr  16363  dvdsadd2b  16364  dvdsaddre2b  16365  dvdsabseq  16371  divconjdvds  16373  alzdvds  16378  addmodlteqALT  16383  dvdsexp2im  16385  odd2np1lem  16398  odd2np1  16399  even2n  16400  oddp1even  16402  mod2eq1n2dvds  16405  mulsucdiv2z  16411  zob  16417  ltoddhalfle  16419  halfleoddlt  16420  opoe  16421  omoe  16422  opeo  16423  omeo  16424  m1exp1  16434  divalglem0  16451  divalglem2  16453  divalglem4  16454  divalglem5  16455  divalglem9  16459  divalgb  16462  divalgmod  16464  modremain  16466  ndvdssub  16467  ndvdsadd  16468  flodddiv4  16473  flodddiv4t2lthalf  16476  bits0  16486  bitsp1e  16490  bitsp1o  16491  gcdneg  16580  gcdaddmlem  16582  gcdaddm  16583  gcdadd  16584  gcdid  16585  modgcd  16590  gcdmultiplez  16593  bezoutlem1  16597  bezoutlem2  16598  bezoutlem4  16600  dvdsgcd  16602  mulgcd  16606  absmulgcd  16607  mulgcdr  16608  gcddiv  16609  dvdssqim  16612  dvdsexpim  16613  zexpgcd  16623  dvdssq  16625  bezoutr1  16627  lcmcllem  16654  lcmneg  16661  lcmgcdlem  16664  lcmgcd  16665  lcmid  16667  lcm1  16668  coprmdvds  16711  coprmdvds2  16712  qredeq  16715  qredeu  16716  divgcdcoprmex  16724  cncongr1  16725  cncongr2  16726  prmdvdsexp  16774  rpexp1i  16782  divnumden  16807  zsqrtelqelz  16817  phiprmpw  16835  vfermltlALT  16862  nnnn0modprm0  16866  modprmn0modprm0  16867  coprimeprodsq2  16869  iserodd  16895  pclem  16898  pcprendvds2  16901  pcpremul  16903  pcmul  16911  pcneg  16934  fldivp1  16957  prmpwdvds  16964  zgz  16993  modxai  17128  mod2xnegi  17131  chnccat  18682  chnrev  18683  mulgfval  19135  mulgz  19168  mulgassr  19178  mulgmodid  19179  odmod  19616  odf1  19632  odf1o1  19642  gexdvds  19654  zaddablx  19942  ablfacrp  20138  pgpfac1lem3  20149  ablsimpgfindlem1  20179  zsubrg  21539  zsssubrg  21544  zringsub  21574  zringmulg  21575  zringinvg  21584  zringunit  21585  zringcyg  21588  prmirred  21593  mulgrhm2  21597  pzriprnglem6  21605  pzriprnglem8  21607  pzriprnglem10  21609  pzriprnglem12  21611  fermltlchr  21648  znunit  21682  degltp1le  26199  ef2kpi  26609  efper  26610  sinperlem  26611  sin2kpi  26614  cos2kpi  26615  abssinper  26652  sinkpi  26653  coskpi  26654  eflogeq  26733  cxpexpz  26798  root1eq1  26886  cxpeq  26888  zrtelqelz  26889  zrtdvds  26890  relogbexp  26911  sgmval2  27273  ppiprm  27281  ppinprm  27282  chtprm  27283  chtnprm  27284  lgslem3  27429  lgsneg  27451  lgsdir2lem2  27456  lgsdir2lem4  27458  lgsdir2  27460  lgssq  27467  lgsmulsqcoprm  27473  lgsdirnn0  27474  gausslemma2dlem3  27498  lgsquadlem1  27510  lgsquadlem2  27511  lgsquad2  27516  2lgslem1a2  27520  2lgsoddprmlem1  27538  2lgsoddprmlem2  27539  2sqlem2  27548  2sqlem7  27554  rplogsumlem2  27615  axlowdimlem13  29245  wlk1walk  29929  clwwisshclwwslemlem  30305  ipasslem5  31128  rearchi  33609  znfermltl  33624  knoppndvlem9  36998  poimirlem19  38178  itg2addnclem2  38211  gcdaddmzz2nncomi  42652  zdivgd  42988  ef11d  42990  cxp112d  42992  cxp111d  42993  cxpi11d  42994  dffltz  43258  lzenom  43393  rexzrexnn0  43423  pell1234qrne0  43472  pell1234qrreccl  43473  pell1234qrmulcl  43474  pell1234qrdich  43480  pell14qrdich  43488  reglogexp  43513  reglogexpbas  43516  rmxm1  43553  rmym1  43554  rmxdbl  43558  rmydbl  43559  jm2.24  43582  congtr  43584  congadd  43585  congmul  43586  congsym  43587  congneg  43588  congid  43590  congabseq  43593  acongsym  43595  acongneg2  43596  acongtr  43597  acongrep  43599  jm2.19lem3  43610  jm2.19lem4  43611  jm2.19  43612  jm2.25  43618  jm2.26a  43619  oddfl  45889  coskpi2  46472  cosknegpi  46475  dvdsn1add  46545  itgsinexp  46561  fourierdlem42  46755  fourierdlem97  46809  fourierswlem  46836  sinnpoly  47517  2elfz2melfz  47944  ceilbi  47963  flmrecm1  47969  submodaddmod  47973  submodneaddmod  47983  mod0mul  47988  m1modmmod  47990  modmkpkne  47993  modlt0b  47995  sfprmdvdsmersenne  48244  proththd  48255  ppivalnnprm  48266  ppivalnnnprmge6  48267  dfodd6  48291  dfeven4  48292  evenm1odd  48293  evenp1odd  48294  enege  48299  onego  48300  dfeven2  48303  bits0ALTV  48333  opoeALTV  48337  opeoALTV  48338  evensumeven  48361  fppr2odd  48385  sbgoldbwt  48431  nnsum3primesgbe  48446  gpgedgvtx0  48715  gpg5nbgrvtx03starlem2  48723  gpg5nbgrvtx13starlem2  48726  0nodd  48824  2nodd  48826  1neven  48892  2zlidl  48894  2zrngamgm  48899  2zrngasgrp  48900  2zrngagrp  48903  2zrngmmgm  48906  2zrngmsgrp  48907  2zrngnmrid  48910  zlmodzxzsub  49025  flsubz  49187  zofldiv2  49196  dignn0flhalflem1  49280  dignn0flhalflem2  49281