Theorem zcn 12534

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11066  ℤcz 12529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11125

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-neg 11408  df-z 12530

This theorem is referenced by:  zsscn  12537  zsubcl  12575  zrevaddcl  12578  nzadd  12581  zlem1lt  12585  zltlem1  12586  zdiv  12604  zdivadd  12605  zdivmul  12606  zextlt  12608  zneo  12617  zeo2  12621  peano5uzi  12623  zindd  12635  znnn0nn  12645  zriotaneg  12647  zmax  12904  rebtwnz  12906  qmulz  12910  zq  12913  qaddcl  12924  qnegcl  12925  qmulcl  12926  qreccl  12928  fzen  13502  uzsubsubfz  13507  fz01en  13513  fzmmmeqm  13518  fzsubel  13521  fztp  13541  fzsuc2  13543  fzrev2  13549  fzrev3  13551  elfzp1b  13562  fzrevral  13573  fzrevral2  13574  fzrevral3  13575  fzshftral  13576  fzo0addel  13679  fzo0addelr  13680  fzoaddel2  13681  fzosubel2  13686  eluzgtdifelfzo  13688  fzocatel  13690  elfzom1elp1fzo  13693  fzval3  13695  zpnn0elfzo1  13700  fzosplitprm1  13738  fzoshftral  13745  flzadd  13788  2tnp1ge0ge0  13791  ceilid  13813  quoremz  13817  intfracq  13821  mulmod0  13839  zmod10  13849  modcyc  13868  modcyc2  13869  muladdmodid  13875  mulp1mod1  13876  modmuladdnn0  13880  modmul1  13889  modmulmodr  13902  modaddmulmod  13903  uzrdgxfr  13932  fzen2  13934  seqshft2  13993  sermono  13999  m1expeven  14074  expsub  14075  zesq  14191  modexp  14203  sqoddm1div8  14208  bccmpl  14274  swrd00  14609  addlenrevpfx  14655  swrdswrd  14670  swrdpfx  14672  pfxccatin12lem4  14691  pfxccatin12lem1  14693  swrdccatin2  14694  pfxccatin12lem2  14696  pfxccatin12  14698  repswrevw  14752  cshwsublen  14761  cshwidxmodr  14769  cshwidx0mod  14770  2cshw  14778  2cshwid  14779  2cshwcom  14781  cshweqdif2  14784  cshweqrep  14786  cshw1  14787  2cshwcshw  14791  shftuz  15035  seqshft  15051  nn0abscl  15278  zabs0b  15280  nnabscl  15292  climshftlem  15540  climshft  15542  isershft  15630  mptfzshft  15744  fsumrev  15745  fsum0diag2  15749  efexp  16069  efzval  16070  demoivre  16168  sqrt2irr  16217  dvdsval2  16225  iddvds  16239  1dvds  16240  dvds0  16241  negdvdsb  16242  dvdsnegb  16243  0dvds  16246  dvdsmul1  16247  iddvdsexp  16249  muldvds1  16250  muldvds2  16251  dvdscmul  16252  dvdsmulc  16253  dvdscmulr  16254  dvdsmulcr  16255  summodnegmod  16256  difmod0  16257  modmulconst  16258  dvds2ln  16259  dvds2add  16260  dvds2sub  16261  dvdstr  16264  dvdssub2  16271  dvdsadd  16272  dvdsaddr  16273  dvdssub  16274  dvdssubr  16275  dvdsadd2b  16276  dvdsaddre2b  16277  dvdsabseq  16283  divconjdvds  16285  alzdvds  16290  addmodlteqALT  16295  dvdsexp2im  16297  odd2np1lem  16310  odd2np1  16311  even2n  16312  oddp1even  16314  mod2eq1n2dvds  16317  mulsucdiv2z  16323  zob  16329  ltoddhalfle  16331  halfleoddlt  16332  opoe  16333  omoe  16334  opeo  16335  omeo  16336  m1exp1  16346  divalglem0  16363  divalglem2  16365  divalglem4  16366  divalglem5  16367  divalglem9  16371  divalgb  16374  divalgmod  16376  modremain  16378  ndvdssub  16379  ndvdsadd  16380  flodddiv4  16385  flodddiv4t2lthalf  16388  bits0  16398  bitsp1e  16402  bitsp1o  16403  gcdneg  16492  gcdaddmlem  16494  gcdaddm  16495  gcdadd  16496  gcdid  16497  modgcd  16502  gcdmultiplez  16505  bezoutlem1  16509  bezoutlem2  16510  bezoutlem4  16512  dvdsgcd  16514  mulgcd  16518  absmulgcd  16519  mulgcdr  16520  gcddiv  16521  dvdssqim  16524  dvdsexpim  16525  zexpgcd  16535  dvdssq  16537  bezoutr1  16539  lcmcllem  16566  lcmneg  16573  lcmgcdlem  16576  lcmgcd  16577  lcmid  16579  lcm1  16580  coprmdvds  16623  coprmdvds2  16624  qredeq  16627  qredeu  16628  divgcdcoprmex  16636  cncongr1  16637  cncongr2  16638  prmdvdsexp  16685  rpexp1i  16693  divnumden  16718  zsqrtelqelz  16728  phiprmpw  16746  vfermltlALT  16773  nnnn0modprm0  16777  modprmn0modprm0  16778  coprimeprodsq2  16780  iserodd  16806  pclem  16809  pcprendvds2  16812  pcpremul  16814  pcmul  16822  pcneg  16845  fldivp1  16868  prmpwdvds  16875  zgz  16904  modxai  17039  mod2xnegi  17042  mulgfval  19001  mulgz  19034  mulgassr  19044  mulgmodid  19045  odmod  19476  odf1  19492  odf1o1  19502  gexdvds  19514  zaddablx  19802  ablfacrp  19998  pgpfac1lem3  20009  ablsimpgfindlem1  20039  zsubrg  21337  zsssubrg  21342  zringsub  21365  zringmulg  21366  zringinvg  21375  zringunit  21376  zringcyg  21379  prmirred  21384  mulgrhm2  21388  pzriprnglem6  21396  pzriprnglem8  21398  pzriprnglem10  21400  pzriprnglem12  21402  fermltlchr  21439  znunit  21473  degltp1le  25978  ef2kpi  26387  efper  26388  sinperlem  26389  sin2kpi  26392  cos2kpi  26393  abssinper  26430  sinkpi  26431  coskpi  26432  eflogeq  26511  cxpexpz  26576  root1eq1  26665  cxpeq  26667  zrtelqelz  26668  zrtdvds  26669  relogbexp  26690  sgmval2  27053  ppiprm  27061  ppinprm  27062  chtprm  27063  chtnprm  27064  lgslem3  27210  lgsneg  27232  lgsdir2lem2  27237  lgsdir2lem4  27239  lgsdir2  27241  lgssq  27248  lgsmulsqcoprm  27254  lgsdirnn0  27255  gausslemma2dlem3  27279  lgsquadlem1  27291  lgsquadlem2  27292  lgsquad2  27297  2lgslem1a2  27301  2lgsoddprmlem1  27319  2lgsoddprmlem2  27320  2sqlem2  27329  2sqlem7  27335  rplogsumlem2  27396  axlowdimlem13  28881  wlk1walk  29567  clwwisshclwwslemlem  29942  ipasslem5  30764  rearchi  33317  znfermltl  33337  knoppndvlem9  36508  poimirlem19  37633  itg2addnclem2  37666  gcdaddmzz2nncomi  41983  zdivgd  42325  ef11d  42327  cxp112d  42329  cxp111d  42330  cxpi11d  42331  dffltz  42622  lzenom  42758  rexzrexnn0  42792  pell1234qrne0  42841  pell1234qrreccl  42842  pell1234qrmulcl  42843  pell1234qrdich  42849  pell14qrdich  42857  reglogexp  42882  reglogexpbas  42885  rmxm1  42923  rmym1  42924  rmxdbl  42928  rmydbl  42929  jm2.24  42952  congtr  42954  congadd  42955  congmul  42956  congsym  42957  congneg  42958  congid  42960  congabseq  42963  acongsym  42965  acongneg2  42966  acongtr  42967  acongrep  42969  jm2.19lem3  42980  jm2.19lem4  42981  jm2.19  42982  jm2.25  42988  jm2.26a  42989  oddfl  45276  coskpi2  45864  cosknegpi  45867  dvdsn1add  45937  itgsinexp  45953  fourierdlem42  46147  fourierdlem97  46201  fourierswlem  46228  sinnpoly  46892  2elfz2melfz  47319  ceilbi  47334  submodaddmod  47342  submodneaddmod  47352  mod0mul  47357  m1modmmod  47359  modmkpkne  47362  modlt0b  47364  sfprmdvdsmersenne  47604  proththd  47615  dfodd6  47638  dfeven4  47639  evenm1odd  47640  evenp1odd  47641  enege  47646  onego  47647  dfeven2  47650  bits0ALTV  47680  opoeALTV  47684  opeoALTV  47685  evensumeven  47708  fppr2odd  47732  sbgoldbwt  47778  nnsum3primesgbe  47793  gpgedgvtx0  48052  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx13starlem2  48063  0nodd  48158  2nodd  48160  1neven  48226  2zlidl  48228  2zrngamgm  48233  2zrngasgrp  48234  2zrngagrp  48237  2zrngmmgm  48240  2zrngmsgrp  48241  2zrngnmrid  48244  zlmodzxzsub  48348  flsubz  48511  zofldiv2  48520  dignn0flhalflem1  48604  dignn0flhalflem2  48605