Theorem zcn 12573

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

Syntax hints:   → wi 4   ∈ wcel 2142  ℂcc 11071  ℤcz 12568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-resscn 11130

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-neg 11417  df-z 12569

This theorem is referenced by:  zsscn  12576  zsubcl  12613  zrevaddcl  12616  nzadd  12619  zlem1lt  12623  zltlem1  12624  zdiv  12643  zdivadd  12644  zdivmul  12645  zextlt  12647  zneo  12656  zeo2  12660  peano5uzi  12662  zindd  12674  znnn0nn  12684  zriotaneg  12686  zmax  12946  rebtwnz  12948  qmulz  12952  zq  12955  qaddcl  12966  qnegcl  12967  qmulcl  12968  qreccl  12970  fzen  13546  uzsubsubfz  13551  fz01en  13557  fzmmmeqm  13562  fzsubel  13565  fztp  13585  fzsuc2  13587  fzrev2  13593  fzrev3  13595  elfzp1b  13606  fzrevral  13617  fzrevral2  13618  fzrevral3  13619  fzshftral  13620  fzo0addel  13724  fzo0addelr  13725  fzoaddel2  13726  fzosubel2  13731  eluzgtdifelfzo  13733  fzocatel  13735  elfzom1elp1fzo  13738  fzval3  13740  zpnn0elfzo1  13745  fzosplitprm1  13784  fzoshftral  13793  flzadd  13836  2tnp1ge0ge0  13839  ceilid  13861  quoremz  13865  intfracq  13869  mulmod0  13887  zmod10  13897  modcyc  13916  modcyc2  13917  muladdmodid  13923  mulp1mod1  13924  modmuladdnn0  13928  modmul1  13937  modmulmodr  13950  modaddmulmod  13951  uzrdgxfr  13980  fzen2  13982  seqshft2  14041  sermono  14047  m1expeven  14122  expsub  14123  zesq  14239  modexp  14251  sqoddm1div8  14256  bccmpl  14322  swrd00  14658  swrdswrd  14718  swrdpfx  14720  pfxccatin12lem4  14739  pfxccatin12lem1  14741  swrdccatin2  14742  pfxccatin12lem2  14744  pfxccatin12  14746  repswrevw  14800  cshwsublen  14809  cshwidxmodr  14817  cshwidx0mod  14818  2cshw  14826  2cshwid  14827  2cshwcom  14829  cshweqdif2  14832  cshweqrep  14834  cshw1  14835  2cshwcshw  14838  shftuz  15082  seqshft  15098  nn0abscl  15339  zabs0b  15341  nnabscl  15353  climshftlem  15601  climshft  15603  isershft  15691  mptfzshft  15805  fsumrev  15806  fsum0diag2  15810  efexp  16133  efzval  16134  demoivre  16232  sqrt2irr  16281  dvdsval2  16289  iddvds  16303  1dvds  16304  dvds0  16305  negdvdsb  16306  dvdsnegb  16307  0dvds  16310  dvdsmul1  16311  iddvdsexp  16313  muldvds1  16314  muldvds2  16315  dvdscmul  16316  dvdsmulc  16317  dvdscmulr  16318  dvdsmulcr  16319  summodnegmod  16320  difmod0  16321  modmulconst  16322  dvds2ln  16323  dvds2add  16324  dvds2sub  16325  dvdstr  16328  dvdssub2  16335  dvdsadd  16336  dvdsaddr  16337  dvdssub  16338  dvdssubr  16339  dvdsadd2b  16340  dvdsaddre2b  16341  dvdsabseq  16347  divconjdvds  16349  alzdvds  16354  addmodlteqALT  16359  dvdsexp2im  16361  odd2np1lem  16374  odd2np1  16375  even2n  16376  oddp1even  16378  mod2eq1n2dvds  16381  mulsucdiv2z  16387  zob  16393  ltoddhalfle  16395  halfleoddlt  16396  opoe  16397  omoe  16398  opeo  16399  omeo  16400  m1exp1  16410  divalglem0  16427  divalglem2  16429  divalglem4  16430  divalglem5  16431  divalglem9  16435  divalgb  16438  divalgmod  16440  modremain  16442  ndvdssub  16443  ndvdsadd  16444  flodddiv4  16449  flodddiv4t2lthalf  16452  bits0  16462  bitsp1e  16466  bitsp1o  16467  gcdneg  16556  gcdaddmlem  16558  gcdaddm  16559  gcdadd  16560  gcdid  16561  modgcd  16566  gcdmultiplez  16569  bezoutlem1  16573  bezoutlem2  16574  bezoutlem4  16576  dvdsgcd  16578  mulgcd  16582  absmulgcd  16583  mulgcdr  16584  gcddiv  16585  dvdssqim  16588  dvdsexpim  16589  zexpgcd  16599  dvdssq  16601  bezoutr1  16603  lcmcllem  16630  lcmneg  16637  lcmgcdlem  16640  lcmgcd  16641  lcmid  16643  lcm1  16644  coprmdvds  16687  coprmdvds2  16688  qredeq  16691  qredeu  16692  divgcdcoprmex  16700  cncongr1  16701  cncongr2  16702  prmdvdsexp  16750  rpexp1i  16758  divnumden  16783  zsqrtelqelz  16793  phiprmpw  16811  vfermltlALT  16838  nnnn0modprm0  16842  modprmn0modprm0  16843  coprimeprodsq2  16845  iserodd  16871  pclem  16874  pcprendvds2  16877  pcpremul  16879  pcmul  16887  pcneg  16910  fldivp1  16933  prmpwdvds  16940  zgz  16969  modxai  17104  mod2xnegi  17107  chnccat  18658  chnrev  18659  mulgfval  19111  mulgz  19144  mulgassr  19154  mulgmodid  19155  odmod  19586  odf1  19602  odf1o1  19612  gexdvds  19624  zaddablx  19912  ablfacrp  20108  pgpfac1lem3  20119  ablsimpgfindlem1  20149  zsubrg  21472  zsssubrg  21477  zringsub  21507  zringmulg  21508  zringinvg  21517  zringunit  21518  zringcyg  21521  prmirred  21526  mulgrhm2  21530  pzriprnglem6  21538  pzriprnglem8  21540  pzriprnglem10  21542  pzriprnglem12  21544  fermltlchr  21581  znunit  21615  degltp1le  26133  ef2kpi  26543  efper  26544  sinperlem  26545  sin2kpi  26548  cos2kpi  26549  abssinper  26586  sinkpi  26587  coskpi  26588  eflogeq  26667  cxpexpz  26732  root1eq1  26820  cxpeq  26822  zrtelqelz  26823  zrtdvds  26824  relogbexp  26845  sgmval2  27207  ppiprm  27215  ppinprm  27216  chtprm  27217  chtnprm  27218  lgslem3  27363  lgsneg  27385  lgsdir2lem2  27390  lgsdir2lem4  27392  lgsdir2  27394  lgssq  27401  lgsmulsqcoprm  27407  lgsdirnn0  27408  gausslemma2dlem3  27432  lgsquadlem1  27444  lgsquadlem2  27445  lgsquad2  27450  2lgslem1a2  27454  2lgsoddprmlem1  27472  2lgsoddprmlem2  27473  2sqlem2  27482  2sqlem7  27488  rplogsumlem2  27549  axlowdimlem13  29155  wlk1walk  29839  clwwisshclwwslemlem  30215  ipasslem5  31038  rearchi  33532  znfermltl  33552  knoppndvlem9  36958  poimirlem19  38138  itg2addnclem2  38171  gcdaddmzz2nncomi  42612  zdivgd  42946  ef11d  42948  cxp112d  42950  cxp111d  42951  cxpi11d  42952  dffltz  43216  lzenom  43351  rexzrexnn0  43381  pell1234qrne0  43430  pell1234qrreccl  43431  pell1234qrmulcl  43432  pell1234qrdich  43438  pell14qrdich  43446  reglogexp  43471  reglogexpbas  43474  rmxm1  43511  rmym1  43512  rmxdbl  43516  rmydbl  43517  jm2.24  43540  congtr  43542  congadd  43543  congmul  43544  congsym  43545  congneg  43546  congid  43548  congabseq  43551  acongsym  43553  acongneg2  43554  acongtr  43555  acongrep  43557  jm2.19lem3  43568  jm2.19lem4  43569  jm2.19  43570  jm2.25  43576  jm2.26a  43577  oddfl  45857  coskpi2  46440  cosknegpi  46443  dvdsn1add  46513  itgsinexp  46529  fourierdlem42  46723  fourierdlem97  46777  fourierswlem  46804  sinnpoly  47485  2elfz2melfz  47912  ceilbi  47931  flmrecm1  47937  submodaddmod  47941  submodneaddmod  47951  mod0mul  47956  m1modmmod  47958  modmkpkne  47961  modlt0b  47963  sfprmdvdsmersenne  48212  proththd  48223  ppivalnnprm  48234  ppivalnnnprmge6  48235  dfodd6  48259  dfeven4  48260  evenm1odd  48261  evenp1odd  48262  enege  48267  onego  48268  dfeven2  48271  bits0ALTV  48301  opoeALTV  48305  opeoALTV  48306  evensumeven  48329  fppr2odd  48353  sbgoldbwt  48399  nnsum3primesgbe  48414  gpgedgvtx0  48683  gpg5nbgrvtx03starlem2  48691  gpg5nbgrvtx13starlem2  48694  0nodd  48792  2nodd  48794  1neven  48860  2zlidl  48862  2zrngamgm  48867  2zrngasgrp  48868  2zrngagrp  48871  2zrngmmgm  48874  2zrngmsgrp  48875  2zrngnmrid  48878  zlmodzxzsub  48982  flsubz  49144  zofldiv2  49153  dignn0flhalflem1  49237  dignn0flhalflem2  49238