Theorem zcn 12613

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℂcc 11115  ℤcz 12608

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 2148  ax-9 2156  ax-ext 2737  ax-resscn 11174

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-neg 11461  df-z 12609

This theorem is used by:  zsscn  12616  zsubcl  12653  zrevaddcl  12656  nzadd  12659  zlem1lt  12663  zltlem1  12664  zdiv  12684  zdivadd  12685  zdivmul  12686  zextlt  12688  zneo  12697  zeo2  12701  peano5uzi  12703  zindd  12715  znnn0nn  12725  zriotaneg  12727  zmax  12987  rebtwnz  12989  qmulz  12993  zq  12996  qaddcl  13007  qnegcl  13008  qmulcl  13009  qreccl  13011  fzen  13587  uzsubsubfz  13593  fz01en  13599  fzmmmeqm  13604  fzsubel  13607  fztp  13627  fzsuc2  13629  fzrev2  13635  fzrev3  13637  elfzp1b  13648  fzrevral  13659  fzrevral2  13660  fzrevral3  13661  fzshftral  13662  fzo0addel  13766  fzo0addelr  13767  fzoaddel2  13768  fzosubel2  13773  eluzgtdifelfzo  13775  fzocatel  13777  elfzom1elp1fzo  13780  fzval3  13782  zpnn0elfzo1  13787  fzosplitprm1  13826  fzoshftral  13835  flzadd  13879  2tnp1ge0ge0  13882  ceilid  13904  quoremz  13908  intfracq  13912  mulmod0  13930  zmod10  13940  modcyc  13959  modcyc2  13960  muladdmodid  13966  mulp1mod1  13967  modmuladdnn0  13971  modmul1  13980  modmulmodr  13993  modaddmulmod  13994  uzrdgxfr  14023  fzen2  14025  seqshft2  14084  sermono  14090  m1expeven  14165  expsub  14166  zesq  14282  modexp  14294  sqoddm1div8  14299  bccmpl  14365  swrd00  14704  swrdswrd  14766  swrdpfx  14768  pfxccatin12lem4  14787  pfxccatin12lem1  14789  swrdccatin2  14790  pfxccatin12lem2  14792  pfxccatin12  14794  repswrevw  14850  cshwsublen  14859  cshwidxmodr  14867  cshwidx0mod  14868  2cshw  14876  2cshwid  14877  2cshwcom  14879  cshweqdif2  14882  cshweqrep  14884  cshw1  14885  2cshwcshw  14888  shftuz  15132  seqshft  15148  nn0abscl  15389  zabs0b  15391  nnabscl  15403  climshftlem  15651  climshft  15653  isershft  15741  mptfzshft  15854  fsumrev  15855  fsum0diag2  15859  efexp  16181  efzval  16182  demoivre  16280  sqrt2irr  16329  dvdsval2  16337  iddvds  16351  1dvds  16352  dvds0  16353  negdvdsb  16354  dvdsnegb  16355  0dvds  16358  dvdsmul1  16359  iddvdsexp  16361  muldvds1  16362  muldvds2  16363  dvdscmul  16364  dvdsmulc  16365  dvdscmulr  16366  dvdsmulcr  16367  summodnegmod  16368  difmod0  16369  modmulconst  16370  dvds2ln  16371  dvds2add  16372  dvds2sub  16373  dvdstr  16376  dvdssub2  16383  dvdsadd  16384  dvdsaddr  16385  dvdssub  16386  dvdssubr  16387  dvdsadd2b  16388  dvdsaddre2b  16389  dvdsabseq  16395  divconjdvds  16397  alzdvds  16402  addmodlteqALT  16407  dvdsexp2im  16409  odd2np1lem  16422  odd2np1  16423  even2n  16424  oddp1even  16426  mod2eq1n2dvds  16429  mulsucdiv2z  16435  zob  16441  ltoddhalfle  16443  halfleoddlt  16444  opoe  16445  omoe  16446  opeo  16447  omeo  16448  m1exp1  16458  divalglem0  16475  divalglem2  16477  divalglem4  16478  divalglem5  16479  divalglem9  16483  divalgb  16486  divalgmod  16488  modremain  16490  ndvdssub  16491  ndvdsadd  16492  flodddiv4  16497  flodddiv4t2lthalf  16500  bits0  16510  bitsp1e  16514  bitsp1o  16515  gcdneg  16604  gcdaddmlem  16606  gcdaddm  16607  gcdadd  16608  gcdid  16609  modgcd  16614  gcdmultiplez  16617  bezoutlem1  16621  bezoutlem2  16622  bezoutlem4  16624  dvdsgcd  16626  mulgcd  16630  absmulgcd  16631  mulgcdr  16632  gcddiv  16633  dvdssqim  16636  dvdsexpim  16637  zexpgcd  16647  dvdssq  16649  bezoutr1  16651  lcmcllem  16678  lcmneg  16685  lcmgcdlem  16688  lcmgcd  16689  lcmid  16691  lcm1  16692  coprmdvds  16735  coprmdvds2  16736  qredeq  16739  qredeu  16740  divgcdcoprmex  16748  cncongr1  16749  cncongr2  16750  prmdvdsexp  16798  rpexp1i  16806  divnumden  16831  zsqrtelqelz  16841  phiprmpw  16859  vfermltlALT  16886  nnnn0modprm0  16890  modprmn0modprm0  16891  coprimeprodsq2  16893  iserodd  16919  pclem  16922  pcprendvds2  16925  pcpremul  16927  pcmul  16935  pcneg  16958  fldivp1  16981  prmpwdvds  16988  zgz  17017  modxai  17152  mod2xnegi  17155  chnccat  18706  chnrev  18707  mulgfval  19181  mulgz  19214  mulgassr  19224  mulgmodid  19225  odmod  19662  odf1  19678  odf1o1  19688  gexdvds  19700  zaddablx  19988  ablfacrp  20184  pgpfac1lem3  20195  ablsimpgfindlem1  20225  zsubrg  21622  zsssubrg  21627  zringsub  21657  zringmulg  21658  zringinvg  21667  zringunit  21668  zringcyg  21671  prmirred  21676  mulgrhm2  21680  pzriprnglem6  21688  pzriprnglem8  21690  pzriprnglem10  21692  pzriprnglem12  21694  fermltlchr  21731  znunit  21765  degltp1le  26283  ef2kpi  26696  efper  26697  sinperlem  26698  sin2kpi  26701  cos2kpi  26702  abssinper  26739  sinkpi  26740  coskpi  26741  eflogeq  26820  cxpexpz  26885  root1eq1  26973  cxpeq  26975  zrtelqelz  26976  zrtdvds  26977  relogbexp  26998  sgmval2  27360  ppiprm  27368  ppinprm  27369  chtprm  27370  chtnprm  27371  lgslem3  27516  lgsneg  27538  lgsdir2lem2  27543  lgsdir2lem4  27545  lgsdir2  27547  lgssq  27554  lgsmulsqcoprm  27560  lgsdirnn0  27561  gausslemma2dlem3  27585  lgsquadlem1  27597  lgsquadlem2  27598  lgsquad2  27603  2lgslem1a2  27607  2lgsoddprmlem1  27625  2lgsoddprmlem2  27626  2sqlem2  27635  2sqlem7  27641  rplogsumlem2  27702  axlowdimlem13  29361  wlk1walk  30048  clwwisshclwwslemlem  30433  ipasslem5  31260  rearchi  33732  znfermltl  33747  knoppndvlem9  37168  poimirlem19  38349  itg2addnclem2  38382  gcdaddmzz2nncomi  42822  zdivgd  43158  ef11d  43160  cxp112d  43162  cxp111d  43163  cxpi11d  43164  dffltz  43426  lzenom  43561  rexzrexnn0  43591  pell1234qrne0  43640  pell1234qrreccl  43641  pell1234qrmulcl  43642  pell1234qrdich  43648  pell14qrdich  43656  reglogexp  43681  reglogexpbas  43684  rmxm1  43721  rmym1  43722  rmxdbl  43726  rmydbl  43727  jm2.24  43750  congtr  43752  congadd  43753  congmul  43754  congsym  43755  congneg  43756  congid  43758  congabseq  43761  acongsym  43763  acongneg2  43764  acongtr  43765  acongrep  43767  jm2.19lem3  43778  jm2.19lem4  43779  jm2.19  43780  jm2.25  43786  jm2.26a  43787  oddfl  46057  coskpi2  46640  cosknegpi  46643  dvdsn1add  46713  itgsinexp  46729  fourierdlem42  46923  fourierdlem97  46977  fourierswlem  47004  sinnpoly  47688  2elfz2melfz  48115  ceilbi  48134  flmrecm1  48140  submodaddmod  48144  submodneaddmod  48154  mod0mul  48159  m1modmmod  48161  modmkpkne  48164  modlt0b  48166  sfprmdvdsmersenne  48415  proththd  48426  ppivalnnprm  48437  ppivalnnnprmge6  48438  dfodd6  48462  dfeven4  48463  evenm1odd  48464  evenp1odd  48465  enege  48470  onego  48471  dfeven2  48474  bits0ALTV  48504  opoeALTV  48508  opeoALTV  48509  evensumeven  48532  fppr2odd  48556  sbgoldbwt  48602  nnsum3primesgbe  48617  gpgedgvtx0  48886  gpg5nbgrvtx03starlem2  48894  gpg5nbgrvtx13starlem2  48897  0nodd  48994  2nodd  48996  1neven  49062  2zlidl  49064  2zrngamgm  49069  2zrngasgrp  49070  2zrngagrp  49073  2zrngmmgm  49076  2zrngmsgrp  49077  2zrngnmrid  49080  zlmodzxzsub  49199  flsubz  49361  zofldiv2  49370  dignn0flhalflem1  49454  dignn0flhalflem2  49455