Theorem zcn 12621

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11123  ℤcz 12616

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-resscn 11182

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417  df-neg 11469  df-z 12617

This theorem is used by:  zsscn  12624  zsubcl  12661  zrevaddcl  12664  nzadd  12667  zlem1lt  12671  zltlem1  12672  zdiv  12692  zdivadd  12693  zdivmul  12694  zextlt  12696  zneo  12705  zeo2  12709  peano5uzi  12711  zindd  12723  znnn0nn  12733  zriotaneg  12735  zmax  12995  rebtwnz  12997  qmulz  13001  zq  13004  qaddcl  13016  qnegcl  13017  qmulcl  13018  qreccl  13020  fzen  13596  uzsubsubfz  13602  fz01en  13608  fzmmmeqm  13613  fzsubel  13616  fztp  13636  fzsuc2  13638  fzrev2  13644  fzrev3  13646  elfzp1b  13657  fzrevral  13668  fzrevral2  13669  fzrevral3  13670  fzshftral  13671  fzo0addel  13775  fzo0addelr  13776  fzoaddel2  13777  fzosubel2  13782  eluzgtdifelfzo  13784  fzocatel  13786  elfzom1elp1fzo  13789  fzval3  13791  zpnn0elfzo1  13796  fzosplitprm1  13835  fzoshftral  13844  flzadd  13888  2tnp1ge0ge0  13891  ceilid  13913  quoremz  13917  intfracq  13921  mulmod0  13939  zmod10  13949  modcyc  13968  modcyc2  13969  muladdmodid  13975  mulp1mod1  13976  modmuladdnn0  13980  modmul1  13989  modmulmodr  14002  modaddmulmod  14003  uzrdgxfr  14032  fzen2  14034  seqshft2  14093  sermono  14099  m1expeven  14174  expsub  14175  zesq  14291  modexp  14303  sqoddm1div8  14308  bccmpl  14374  swrd00  14713  swrdswrd  14775  swrdpfx  14777  pfxccatin12lem4  14796  pfxccatin12lem1  14798  swrdccatin2  14799  pfxccatin12lem2  14801  pfxccatin12  14803  repswrevw  14859  cshwsublen  14868  cshwidxmodr  14876  cshwidx0mod  14877  2cshw  14885  2cshwid  14886  2cshwcom  14888  cshweqdif2  14891  cshweqrep  14893  cshw1  14894  2cshwcshw  14897  shftuz  15143  seqshft  15159  nn0abscl  15400  zabs0b  15402  nnabscl  15414  climshftlem  15662  climshft  15664  isershft  15752  mptfzshft  15865  fsumrev  15866  fsum0diag2  15870  efexp  16190  efzval  16191  demoivre  16289  sqrt2irr  16338  dvdsval2  16346  iddvds  16360  1dvds  16361  dvds0  16362  negdvdsb  16363  dvdsnegb  16364  0dvds  16367  dvdsmul1  16368  iddvdsexp  16370  muldvds1  16371  muldvds2  16372  dvdscmul  16373  dvdsmulc  16374  dvdscmulr  16375  dvdsmulcr  16376  summodnegmod  16377  difmod0  16378  modmulconst  16379  dvds2ln  16380  dvds2add  16381  dvds2sub  16382  dvdstr  16385  dvdssub2  16392  dvdsadd  16393  dvdsaddr  16394  dvdssub  16395  dvdssubr  16396  dvdsadd2b  16397  dvdsaddre2b  16398  dvdsabseq  16404  divconjdvds  16406  alzdvds  16411  addmodlteqALT  16416  dvdsexp2im  16418  odd2np1lem  16431  odd2np1  16432  even2n  16433  oddp1even  16435  mod2eq1n2dvds  16438  mulsucdiv2z  16444  zob  16450  ltoddhalfle  16452  halfleoddlt  16453  opoe  16454  omoe  16455  opeo  16456  omeo  16457  m1exp1  16467  divalglem0  16484  divalglem2  16486  divalglem4  16487  divalglem5  16488  divalglem9  16492  divalgb  16495  divalgmod  16497  modremain  16499  ndvdssub  16500  ndvdsadd  16501  flodddiv4  16506  flodddiv4t2lthalf  16509  bits0  16519  bitsp1e  16523  bitsp1o  16524  gcdneg  16613  gcdaddmlem  16615  gcdaddm  16616  gcdadd  16617  gcdid  16618  modgcd  16623  gcdmultiplez  16626  bezoutlem1  16630  bezoutlem2  16631  bezoutlem4  16633  dvdsgcd  16635  mulgcd  16639  absmulgcd  16640  mulgcdr  16641  gcddiv  16642  dvdssqim  16645  dvdsexpim  16646  zexpgcd  16656  dvdssq  16658  bezoutr1  16660  lcmcllem  16687  lcmneg  16694  lcmgcdlem  16697  lcmgcd  16698  lcmid  16700  lcm1  16701  coprmdvds  16744  coprmdvds2  16745  qredeq  16748  qredeu  16749  divgcdcoprmex  16757  cncongr1  16758  cncongr2  16759  prmdvdsexp  16807  rpexp1i  16815  divnumden  16840  zsqrtelqelz  16850  phiprmpw  16868  vfermltlALT  16895  nnnn0modprm0  16899  modprmn0modprm0  16900  coprimeprodsq2  16902  iserodd  16928  pclem  16931  pcprendvds2  16934  pcpremul  16936  pcmul  16944  pcneg  16967  fldivp1  16990  prmpwdvds  16997  zgz  17026  modxai  17161  mod2xnegi  17164  chnccat  18715  chnrev  18716  mulgfval  19193  mulgz  19226  mulgassr  19236  mulgmodid  19237  odmod  19674  odf1  19690  odf1o1  19700  gexdvds  19712  zaddablx  20000  ablfacrp  20196  pgpfac1lem3  20207  ablsimpgfindlem1  20237  zsubrg  21634  zsssubrg  21639  zringsub  21669  zringmulg  21670  zringinvg  21679  zringunit  21680  zringcyg  21683  prmirred  21688  mulgrhm2  21692  pzriprnglem6  21700  pzriprnglem8  21702  pzriprnglem10  21704  pzriprnglem12  21706  fermltlchr  21743  znunit  21777  degltp1le  26299  ef2kpi  26717  efper  26718  sinperlem  26719  sin2kpi  26722  cos2kpi  26723  abssinper  26759  sinkpi  26760  coskpi  26761  eflogeq  26840  cxpexpz  26905  root1eq1  26993  cxpeq  26995  zrtelqelz  26996  zrtdvds  26997  relogbexp  27018  sgmval2  27380  ppiprm  27388  ppinprm  27389  chtprm  27390  chtnprm  27391  lgslem3  27536  lgsneg  27558  lgsdir2lem2  27563  lgsdir2lem4  27565  lgsdir2  27567  lgssq  27574  lgsmulsqcoprm  27580  lgsdirnn0  27581  gausslemma2dlem3  27605  lgsquadlem1  27617  lgsquadlem2  27618  lgsquad2  27623  2lgslem1a2  27627  2lgsoddprmlem1  27645  2lgsoddprmlem2  27646  2sqlem2  27655  2sqlem7  27661  rplogsumlem2  27722  axlowdimlem13  29412  wlk1walk  30099  clwwisshclwwslemlem  30484  ipasslem5  31317  rearchi  33787  znfermltl  33802  knoppndvlem9  37218  poimirlem19  38389  itg2addnclem2  38422  gcdaddmzz2nncomi  42862  zdivgd  43213  ef11d  43215  cxp112d  43217  cxp111d  43218  cxpi11d  43219  dffltz  43481  lzenom  43616  rexzrexnn0  43646  pell1234qrne0  43695  pell1234qrreccl  43696  pell1234qrmulcl  43697  pell1234qrdich  43703  pell14qrdich  43711  reglogexp  43736  reglogexpbas  43739  rmxm1  43776  rmym1  43777  rmxdbl  43781  rmydbl  43782  jm2.24  43805  congtr  43807  congadd  43808  congmul  43809  congsym  43810  congneg  43811  congid  43813  congabseq  43816  acongsym  43818  acongneg2  43819  acongtr  43820  acongrep  43822  jm2.19lem3  43833  jm2.19lem4  43834  jm2.19  43835  jm2.25  43841  jm2.26a  43842  oddfl  46112  coskpi2  46695  cosknegpi  46698  dvdsn1add  46768  itgsinexp  46784  fourierdlem42  46978  fourierdlem97  47032  fourierswlem  47059  sinnpoly  47760  2elfz2melfz  48207  ceilbi  48226  flmrecm1  48232  submodaddmod  48236  submodneaddmod  48246  mod0mul  48251  m1modmmod  48253  modmkpkne  48256  modlt0b  48258  sfprmdvdsmersenne  48507  proththd  48518  ppivalnnprm  48529  ppivalnnnprmge6  48530  dfodd6  48554  dfeven4  48555  evenm1odd  48556  evenp1odd  48557  enege  48562  onego  48563  dfeven2  48566  bits0ALTV  48596  opoeALTV  48600  opeoALTV  48601  evensumeven  48624  fppr2odd  48648  sbgoldbwt  48694  nnsum3primesgbe  48709  gpgedgvtx0  48978  gpg5nbgrvtx03starlem2  48986  gpg5nbgrvtx13starlem2  48989  0nodd  49086  2nodd  49088  1neven  49154  2zlidl  49156  2zrngamgm  49161  2zrngasgrp  49162  2zrngagrp  49165  2zrngmmgm  49168  2zrngmsgrp  49169  2zrngnmrid  49172  zlmodzxzsub  49291  flsubz  49453  zofldiv2  49462  dignn0flhalflem1  49546  dignn0flhalflem2  49547