Theorem zcn 12559

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11104  ℤcz 12554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-resscn 11163

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7407  df-neg 11443  df-z 12555

This theorem is referenced by:  zsscn  12562  zsubcl  12600  zrevaddcl  12603  nzadd  12606  zlem1lt  12610  zltlem1  12611  zdiv  12628  zdivadd  12629  zdivmul  12630  zextlt  12632  zneo  12641  zeo2  12645  peano5uzi  12647  zindd  12659  znnn0nn  12669  zriotaneg  12671  zmax  12925  rebtwnz  12927  qmulz  12931  zq  12934  qaddcl  12945  qnegcl  12946  qmulcl  12947  qreccl  12949  fzen  13514  uzsubsubfz  13519  fz01en  13525  fzmmmeqm  13530  fzsubel  13533  fztp  13553  fzsuc2  13555  fzrev2  13561  fzrev3  13563  elfzp1b  13574  fzrevral  13582  fzrevral2  13583  fzrevral3  13584  fzshftral  13585  fzo0addel  13682  fzo0addelr  13683  fzoaddel2  13684  elfzoext  13685  fzosubel2  13688  eluzgtdifelfzo  13690  fzocatel  13692  elfzom1elp1fzo  13695  fzval3  13697  zpnn0elfzo1  13702  fzosplitprm1  13738  fzoshftral  13745  flzadd  13787  2tnp1ge0ge0  13790  ceilid  13812  quoremz  13816  intfracq  13820  mulmod0  13838  zmod10  13848  modcyc  13867  modcyc2  13868  muladdmodid  13872  mulp1mod1  13873  modmuladdnn0  13876  modmul1  13885  modmulmodr  13898  modaddmulmod  13899  uzrdgxfr  13928  fzen2  13930  seqshft2  13990  sermono  13996  m1expeven  14071  expsub  14072  zesq  14185  modexp  14197  sqoddm1div8  14202  bccmpl  14265  swrd00  14590  addlenrevpfx  14636  swrdswrd  14651  swrdpfx  14653  pfxccatin12lem4  14672  pfxccatin12lem1  14674  swrdccatin2  14675  pfxccatin12lem2  14677  pfxccatin12  14679  repswrevw  14733  cshwsublen  14742  cshwidxmodr  14750  cshwidx0mod  14751  2cshw  14759  2cshwid  14760  2cshwcom  14762  cshweqdif2  14765  cshweqrep  14767  cshw1  14768  2cshwcshw  14772  shftuz  15012  seqshft  15028  nn0abscl  15255  nnabscl  15268  climshftlem  15514  climshft  15516  isershft  15606  mptfzshft  15720  fsumrev  15721  fsum0diag2  15725  efexp  16040  efzval  16041  demoivre  16139  sqrt2irr  16188  dvdsval2  16196  iddvds  16209  1dvds  16210  dvds0  16211  negdvdsb  16212  dvdsnegb  16213  0dvds  16216  dvdsmul1  16217  iddvdsexp  16219  muldvds1  16220  muldvds2  16221  dvdscmul  16222  dvdsmulc  16223  dvdscmulr  16224  dvdsmulcr  16225  summodnegmod  16226  modmulconst  16227  dvds2ln  16228  dvds2add  16229  dvds2sub  16230  dvdstr  16233  dvdssub2  16240  dvdsadd  16241  dvdsaddr  16242  dvdssub  16243  dvdssubr  16244  dvdsadd2b  16245  dvdsaddre2b  16246  dvdsabseq  16252  divconjdvds  16254  alzdvds  16259  addmodlteqALT  16264  dvdsexp2im  16266  odd2np1lem  16279  odd2np1  16280  even2n  16281  oddp1even  16283  mod2eq1n2dvds  16286  mulsucdiv2z  16292  zob  16298  ltoddhalfle  16300  halfleoddlt  16301  opoe  16302  omoe  16303  opeo  16304  omeo  16305  m1exp1  16315  divalglem0  16332  divalglem2  16334  divalglem4  16335  divalglem5  16336  divalglem9  16340  divalgb  16343  divalgmod  16345  modremain  16347  ndvdssub  16348  ndvdsadd  16349  flodddiv4  16352  flodddiv4t2lthalf  16355  bits0  16365  bitsp1e  16369  bitsp1o  16370  gcdneg  16459  gcdaddmlem  16461  gcdaddm  16462  gcdadd  16463  gcdid  16464  modgcd  16470  gcdmultiplez  16473  bezoutlem1  16477  bezoutlem2  16478  bezoutlem4  16480  dvdsgcd  16482  mulgcd  16486  absmulgcd  16487  mulgcdr  16488  gcddiv  16489  dvdssqim  16492  dvdssq  16500  bezoutr1  16502  lcmcllem  16529  lcmneg  16536  lcmgcdlem  16539  lcmgcd  16540  lcmid  16542  lcm1  16543  coprmdvds  16586  coprmdvds2  16587  qredeq  16590  qredeu  16591  divgcdcoprmex  16599  cncongr1  16600  cncongr2  16601  prmdvdsexp  16648  prmdvdssqOLD  16652  rpexp1i  16656  divnumden  16680  zsqrtelqelz  16690  phiprmpw  16705  vfermltlALT  16731  nnnn0modprm0  16735  modprmn0modprm0  16736  coprimeprodsq2  16738  iserodd  16764  pclem  16767  pcprendvds2  16770  pcpremul  16772  pcmul  16780  pcneg  16803  fldivp1  16826  prmpwdvds  16833  zgz  16862  modxai  16997  mod2xnegi  17000  mulgfval  18946  mulgz  18976  mulgassr  18986  mulgmodid  18987  odmod  19407  odf1  19423  odf1o1  19433  gexdvds  19445  zaddablx  19732  ablfacrp  19928  pgpfac1lem3  19939  ablsimpgfindlem1  19969  zsubrg  20983  zsssubrg  20988  zringmulg  21010  zringinvg  21019  zringunit  21020  zringcyg  21023  prmirred  21028  mulgrhm2  21032  znunit  21103  degltp1le  25573  ef2kpi  25970  efper  25971  sinperlem  25972  sin2kpi  25975  cos2kpi  25976  abssinper  26012  sinkpi  26013  coskpi  26014  eflogeq  26092  cxpexpz  26157  root1eq1  26243  cxpeq  26245  relogbexp  26265  sgmval2  26627  ppiprm  26635  ppinprm  26636  chtprm  26637  chtnprm  26638  lgslem3  26782  lgsneg  26804  lgsdir2lem2  26809  lgsdir2lem4  26811  lgsdir2  26813  lgssq  26820  lgsmulsqcoprm  26826  lgsdirnn0  26827  gausslemma2dlem3  26851  lgsquadlem1  26863  lgsquadlem2  26864  lgsquad2  26869  2lgslem1a2  26873  2lgsoddprmlem1  26891  2lgsoddprmlem2  26892  2sqlem2  26901  2sqlem7  26907  rplogsumlem2  26968  axlowdimlem13  28192  wlk1walk  28876  clwwisshclwwslemlem  29246  ipasslem5  30066  rearchi  32430  fermltlchr  32447  znfermltl  32448  knoppndvlem9  35334  poimirlem19  36445  itg2addnclem2  36478  gcdaddmzz2nncomi  40799  metakunt16  40938  dvdsexpim  41162  zexpgcd  41170  zrtelqelz  41179  zrtdvds  41180  dffltz  41320  lzenom  41441  rexzrexnn0  41475  pell1234qrne0  41524  pell1234qrreccl  41525  pell1234qrmulcl  41526  pell1234qrdich  41532  pell14qrdich  41540  reglogexp  41565  reglogexpbas  41568  rmxm1  41606  rmym1  41607  rmxdbl  41611  rmydbl  41612  jm2.24  41635  congtr  41637  congadd  41638  congmul  41639  congsym  41640  congneg  41641  congid  41643  congabseq  41646  acongsym  41648  acongneg2  41649  acongtr  41650  acongrep  41652  jm2.19lem3  41663  jm2.19lem4  41664  jm2.19  41665  jm2.25  41671  jm2.26a  41672  oddfl  43922  coskpi2  44517  cosknegpi  44520  dvdsn1add  44590  itgsinexp  44606  fourierdlem42  44800  fourierdlem97  44854  fourierswlem  44881  2elfz2melfz  45961  sfprmdvdsmersenne  46206  proththd  46217  dfodd6  46240  dfeven4  46241  evenm1odd  46242  evenp1odd  46243  enege  46248  onego  46249  dfeven2  46252  bits0ALTV  46282  opoeALTV  46286  opeoALTV  46287  evensumeven  46310  fppr2odd  46334  sbgoldbwt  46380  nnsum3primesgbe  46395  0nodd  46515  2nodd  46517  1neven  46732  2zlidl  46734  2zrngamgm  46739  2zrngasgrp  46740  2zrngagrp  46743  2zrngmmgm  46746  2zrngmsgrp  46747  2zrngnmrid  46750  zlmodzxzsub  46938  flsubz  47105  mod0mul  47107  m1modmmod  47109  zofldiv2  47119  dignn0flhalflem1  47203  dignn0flhalflem2  47204