Theorem zcn 12523

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11030  ℤcz 12518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-neg 11374  df-z 12519

This theorem is referenced by:  zsscn  12526  zsubcl  12563  zrevaddcl  12566  nzadd  12569  zlem1lt  12573  zltlem1  12574  zdiv  12593  zdivadd  12594  zdivmul  12595  zextlt  12597  zneo  12606  zeo2  12610  peano5uzi  12612  zindd  12624  znnn0nn  12634  zriotaneg  12636  zmax  12889  rebtwnz  12891  qmulz  12895  zq  12898  qaddcl  12909  qnegcl  12910  qmulcl  12911  qreccl  12913  fzen  13489  uzsubsubfz  13494  fz01en  13500  fzmmmeqm  13505  fzsubel  13508  fztp  13528  fzsuc2  13530  fzrev2  13536  fzrev3  13538  elfzp1b  13549  fzrevral  13560  fzrevral2  13561  fzrevral3  13562  fzshftral  13563  fzo0addel  13667  fzo0addelr  13668  fzoaddel2  13669  fzosubel2  13674  eluzgtdifelfzo  13676  fzocatel  13678  elfzom1elp1fzo  13681  fzval3  13683  zpnn0elfzo1  13688  fzosplitprm1  13727  fzoshftral  13736  flzadd  13779  2tnp1ge0ge0  13782  ceilid  13804  quoremz  13808  intfracq  13812  mulmod0  13830  zmod10  13840  modcyc  13859  modcyc2  13860  muladdmodid  13866  mulp1mod1  13867  modmuladdnn0  13871  modmul1  13880  modmulmodr  13893  modaddmulmod  13894  uzrdgxfr  13923  fzen2  13925  seqshft2  13984  sermono  13990  m1expeven  14065  expsub  14066  zesq  14182  modexp  14194  sqoddm1div8  14199  bccmpl  14265  swrd00  14601  swrdswrd  14661  swrdpfx  14663  pfxccatin12lem4  14682  pfxccatin12lem1  14684  swrdccatin2  14685  pfxccatin12lem2  14687  pfxccatin12  14689  repswrevw  14743  cshwsublen  14752  cshwidxmodr  14760  cshwidx0mod  14761  2cshw  14769  2cshwid  14770  2cshwcom  14772  cshweqdif2  14775  cshweqrep  14777  cshw1  14778  2cshwcshw  14781  shftuz  15025  seqshft  15041  nn0abscl  15268  zabs0b  15270  nnabscl  15282  climshftlem  15530  climshft  15532  isershft  15620  mptfzshft  15734  fsumrev  15735  fsum0diag2  15739  efexp  16062  efzval  16063  demoivre  16161  sqrt2irr  16210  dvdsval2  16218  iddvds  16232  1dvds  16233  dvds0  16234  negdvdsb  16235  dvdsnegb  16236  0dvds  16239  dvdsmul1  16240  iddvdsexp  16242  muldvds1  16243  muldvds2  16244  dvdscmul  16245  dvdsmulc  16246  dvdscmulr  16247  dvdsmulcr  16248  summodnegmod  16249  difmod0  16250  modmulconst  16251  dvds2ln  16252  dvds2add  16253  dvds2sub  16254  dvdstr  16257  dvdssub2  16264  dvdsadd  16265  dvdsaddr  16266  dvdssub  16267  dvdssubr  16268  dvdsadd2b  16269  dvdsaddre2b  16270  dvdsabseq  16276  divconjdvds  16278  alzdvds  16283  addmodlteqALT  16288  dvdsexp2im  16290  odd2np1lem  16303  odd2np1  16304  even2n  16305  oddp1even  16307  mod2eq1n2dvds  16310  mulsucdiv2z  16316  zob  16322  ltoddhalfle  16324  halfleoddlt  16325  opoe  16326  omoe  16327  opeo  16328  omeo  16329  m1exp1  16339  divalglem0  16356  divalglem2  16358  divalglem4  16359  divalglem5  16360  divalglem9  16364  divalgb  16367  divalgmod  16369  modremain  16371  ndvdssub  16372  ndvdsadd  16373  flodddiv4  16378  flodddiv4t2lthalf  16381  bits0  16391  bitsp1e  16395  bitsp1o  16396  gcdneg  16485  gcdaddmlem  16487  gcdaddm  16488  gcdadd  16489  gcdid  16490  modgcd  16495  gcdmultiplez  16498  bezoutlem1  16502  bezoutlem2  16503  bezoutlem4  16505  dvdsgcd  16507  mulgcd  16511  absmulgcd  16512  mulgcdr  16513  gcddiv  16514  dvdssqim  16517  dvdsexpim  16518  zexpgcd  16528  dvdssq  16530  bezoutr1  16532  lcmcllem  16559  lcmneg  16566  lcmgcdlem  16569  lcmgcd  16570  lcmid  16572  lcm1  16573  coprmdvds  16616  coprmdvds2  16617  qredeq  16620  qredeu  16621  divgcdcoprmex  16629  cncongr1  16630  cncongr2  16631  prmdvdsexp  16679  rpexp1i  16687  divnumden  16712  zsqrtelqelz  16722  phiprmpw  16740  vfermltlALT  16767  nnnn0modprm0  16771  modprmn0modprm0  16772  coprimeprodsq2  16774  iserodd  16800  pclem  16803  pcprendvds2  16806  pcpremul  16808  pcmul  16816  pcneg  16839  fldivp1  16862  prmpwdvds  16869  zgz  16898  modxai  17033  mod2xnegi  17036  chnccat  18586  chnrev  18587  mulgfval  19039  mulgz  19072  mulgassr  19082  mulgmodid  19083  odmod  19515  odf1  19531  odf1o1  19541  gexdvds  19553  zaddablx  19841  ablfacrp  20037  pgpfac1lem3  20048  ablsimpgfindlem1  20078  zsubrg  21413  zsssubrg  21418  zringsub  21448  zringmulg  21449  zringinvg  21458  zringunit  21459  zringcyg  21462  prmirred  21467  mulgrhm2  21471  pzriprnglem6  21479  pzriprnglem8  21481  pzriprnglem10  21483  pzriprnglem12  21485  fermltlchr  21522  znunit  21556  degltp1le  26051  ef2kpi  26458  efper  26459  sinperlem  26460  sin2kpi  26463  cos2kpi  26464  abssinper  26501  sinkpi  26502  coskpi  26503  eflogeq  26582  cxpexpz  26647  root1eq1  26735  cxpeq  26737  zrtelqelz  26738  zrtdvds  26739  relogbexp  26760  sgmval2  27123  ppiprm  27131  ppinprm  27132  chtprm  27133  chtnprm  27134  lgslem3  27279  lgsneg  27301  lgsdir2lem2  27306  lgsdir2lem4  27308  lgsdir2  27310  lgssq  27317  lgsmulsqcoprm  27323  lgsdirnn0  27324  gausslemma2dlem3  27348  lgsquadlem1  27360  lgsquadlem2  27361  lgsquad2  27366  2lgslem1a2  27370  2lgsoddprmlem1  27388  2lgsoddprmlem2  27389  2sqlem2  27398  2sqlem7  27404  rplogsumlem2  27465  axlowdimlem13  29040  wlk1walk  29725  clwwisshclwwslemlem  30101  ipasslem5  30924  rearchi  33424  znfermltl  33444  knoppndvlem9  36799  poimirlem19  37977  itg2addnclem2  38010  gcdaddmzz2nncomi  42451  zdivgd  42786  ef11d  42788  cxp112d  42790  cxp111d  42791  cxpi11d  42792  dffltz  43084  lzenom  43219  rexzrexnn0  43253  pell1234qrne0  43302  pell1234qrreccl  43303  pell1234qrmulcl  43304  pell1234qrdich  43310  pell14qrdich  43318  reglogexp  43343  reglogexpbas  43346  rmxm1  43383  rmym1  43384  rmxdbl  43388  rmydbl  43389  jm2.24  43412  congtr  43414  congadd  43415  congmul  43416  congsym  43417  congneg  43418  congid  43420  congabseq  43423  acongsym  43425  acongneg2  43426  acongtr  43427  acongrep  43429  jm2.19lem3  43440  jm2.19lem4  43441  jm2.19  43442  jm2.25  43448  jm2.26a  43449  oddfl  45732  coskpi2  46315  cosknegpi  46318  dvdsn1add  46388  itgsinexp  46404  fourierdlem42  46598  fourierdlem97  46652  fourierswlem  46679  sinnpoly  47354  2elfz2melfz  47781  ceilbi  47800  flmrecm1  47806  submodaddmod  47810  submodneaddmod  47820  mod0mul  47825  m1modmmod  47827  modmkpkne  47830  modlt0b  47832  sfprmdvdsmersenne  48081  proththd  48092  ppivalnnprm  48103  ppivalnnnprmge6  48104  dfodd6  48128  dfeven4  48129  evenm1odd  48130  evenp1odd  48131  enege  48136  onego  48137  dfeven2  48140  bits0ALTV  48170  opoeALTV  48174  opeoALTV  48175  evensumeven  48198  fppr2odd  48222  sbgoldbwt  48268  nnsum3primesgbe  48283  gpgedgvtx0  48552  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx13starlem2  48563  0nodd  48661  2nodd  48663  1neven  48729  2zlidl  48731  2zrngamgm  48736  2zrngasgrp  48737  2zrngagrp  48740  2zrngmmgm  48743  2zrngmsgrp  48744  2zrngnmrid  48747  zlmodzxzsub  48851  flsubz  49013  zofldiv2  49022  dignn0flhalflem1  49106  dignn0flhalflem2  49107