Theorem zcn 12644

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11182  ℤcz 12639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-neg 11523  df-z 12640

This theorem is referenced by:  zsscn  12647  zsubcl  12685  zrevaddcl  12688  nzadd  12691  zlem1lt  12695  zltlem1  12696  zdiv  12713  zdivadd  12714  zdivmul  12715  zextlt  12717  zneo  12726  zeo2  12730  peano5uzi  12732  zindd  12744  znnn0nn  12754  zriotaneg  12756  zmax  13010  rebtwnz  13012  qmulz  13016  zq  13019  qaddcl  13030  qnegcl  13031  qmulcl  13032  qreccl  13034  fzen  13601  uzsubsubfz  13606  fz01en  13612  fzmmmeqm  13617  fzsubel  13620  fztp  13640  fzsuc2  13642  fzrev2  13648  fzrev3  13650  elfzp1b  13661  fzrevral  13669  fzrevral2  13670  fzrevral3  13671  fzshftral  13672  fzo0addel  13770  fzo0addelr  13771  fzoaddel2  13772  elfzoext  13773  fzosubel2  13776  eluzgtdifelfzo  13778  fzocatel  13780  elfzom1elp1fzo  13783  fzval3  13785  zpnn0elfzo1  13790  fzosplitprm1  13827  fzoshftral  13834  flzadd  13877  2tnp1ge0ge0  13880  ceilid  13902  quoremz  13906  intfracq  13910  mulmod0  13928  zmod10  13938  modcyc  13957  modcyc2  13958  muladdmodid  13962  mulp1mod1  13963  modmuladdnn0  13966  modmul1  13975  modmulmodr  13988  modaddmulmod  13989  uzrdgxfr  14018  fzen2  14020  seqshft2  14079  sermono  14085  m1expeven  14160  expsub  14161  zesq  14275  modexp  14287  sqoddm1div8  14292  bccmpl  14358  swrd00  14692  addlenrevpfx  14738  swrdswrd  14753  swrdpfx  14755  pfxccatin12lem4  14774  pfxccatin12lem1  14776  swrdccatin2  14777  pfxccatin12lem2  14779  pfxccatin12  14781  repswrevw  14835  cshwsublen  14844  cshwidxmodr  14852  cshwidx0mod  14853  2cshw  14861  2cshwid  14862  2cshwcom  14864  cshweqdif2  14867  cshweqrep  14869  cshw1  14870  2cshwcshw  14874  shftuz  15118  seqshft  15134  nn0abscl  15361  nnabscl  15374  climshftlem  15620  climshft  15622  isershft  15712  mptfzshft  15826  fsumrev  15827  fsum0diag2  15831  efexp  16149  efzval  16150  demoivre  16248  sqrt2irr  16297  dvdsval2  16305  iddvds  16318  1dvds  16319  dvds0  16320  negdvdsb  16321  dvdsnegb  16322  0dvds  16325  dvdsmul1  16326  iddvdsexp  16328  muldvds1  16329  muldvds2  16330  dvdscmul  16331  dvdsmulc  16332  dvdscmulr  16333  dvdsmulcr  16334  summodnegmod  16335  modmulconst  16336  dvds2ln  16337  dvds2add  16338  dvds2sub  16339  dvdstr  16342  dvdssub2  16349  dvdsadd  16350  dvdsaddr  16351  dvdssub  16352  dvdssubr  16353  dvdsadd2b  16354  dvdsaddre2b  16355  dvdsabseq  16361  divconjdvds  16363  alzdvds  16368  addmodlteqALT  16373  dvdsexp2im  16375  odd2np1lem  16388  odd2np1  16389  even2n  16390  oddp1even  16392  mod2eq1n2dvds  16395  mulsucdiv2z  16401  zob  16407  ltoddhalfle  16409  halfleoddlt  16410  opoe  16411  omoe  16412  opeo  16413  omeo  16414  m1exp1  16424  divalglem0  16441  divalglem2  16443  divalglem4  16444  divalglem5  16445  divalglem9  16449  divalgb  16452  divalgmod  16454  modremain  16456  ndvdssub  16457  ndvdsadd  16458  flodddiv4  16461  flodddiv4t2lthalf  16464  bits0  16474  bitsp1e  16478  bitsp1o  16479  gcdneg  16568  gcdaddmlem  16570  gcdaddm  16571  gcdadd  16572  gcdid  16573  modgcd  16579  gcdmultiplez  16582  bezoutlem1  16586  bezoutlem2  16587  bezoutlem4  16589  dvdsgcd  16591  mulgcd  16595  absmulgcd  16596  mulgcdr  16597  gcddiv  16598  dvdssqim  16601  dvdsexpim  16602  zexpgcd  16612  dvdssq  16614  bezoutr1  16616  lcmcllem  16643  lcmneg  16650  lcmgcdlem  16653  lcmgcd  16654  lcmid  16656  lcm1  16657  coprmdvds  16700  coprmdvds2  16701  qredeq  16704  qredeu  16705  divgcdcoprmex  16713  cncongr1  16714  cncongr2  16715  prmdvdsexp  16762  rpexp1i  16770  divnumden  16795  zsqrtelqelz  16805  phiprmpw  16823  vfermltlALT  16849  nnnn0modprm0  16853  modprmn0modprm0  16854  coprimeprodsq2  16856  iserodd  16882  pclem  16885  pcprendvds2  16888  pcpremul  16890  pcmul  16898  pcneg  16921  fldivp1  16944  prmpwdvds  16951  zgz  16980  modxai  17115  mod2xnegi  17118  mulgfval  19109  mulgz  19142  mulgassr  19152  mulgmodid  19153  odmod  19588  odf1  19604  odf1o1  19614  gexdvds  19626  zaddablx  19914  ablfacrp  20110  pgpfac1lem3  20121  ablsimpgfindlem1  20151  zsubrg  21461  zsssubrg  21466  zringsub  21489  zringmulg  21490  zringinvg  21499  zringunit  21500  zringcyg  21503  prmirred  21508  mulgrhm2  21512  pzriprnglem6  21520  pzriprnglem8  21522  pzriprnglem10  21524  pzriprnglem12  21526  fermltlchr  21567  znunit  21605  degltp1le  26132  ef2kpi  26538  efper  26539  sinperlem  26540  sin2kpi  26543  cos2kpi  26544  abssinper  26581  sinkpi  26582  coskpi  26583  eflogeq  26662  cxpexpz  26727  root1eq1  26816  cxpeq  26818  zrtelqelz  26819  zrtdvds  26820  relogbexp  26841  sgmval2  27204  ppiprm  27212  ppinprm  27213  chtprm  27214  chtnprm  27215  lgslem3  27361  lgsneg  27383  lgsdir2lem2  27388  lgsdir2lem4  27390  lgsdir2  27392  lgssq  27399  lgsmulsqcoprm  27405  lgsdirnn0  27406  gausslemma2dlem3  27430  lgsquadlem1  27442  lgsquadlem2  27443  lgsquad2  27448  2lgslem1a2  27452  2lgsoddprmlem1  27470  2lgsoddprmlem2  27471  2sqlem2  27480  2sqlem7  27486  rplogsumlem2  27547  axlowdimlem13  28987  wlk1walk  29675  clwwisshclwwslemlem  30045  ipasslem5  30867  rearchi  33339  znfermltl  33359  knoppndvlem9  36486  poimirlem19  37599  itg2addnclem2  37632  gcdaddmzz2nncomi  41952  metakunt16  42177  zdivgd  42324  ef11d  42327  cxp112d  42329  cxp111d  42330  cxpi11d  42331  dffltz  42589  lzenom  42726  rexzrexnn0  42760  pell1234qrne0  42809  pell1234qrreccl  42810  pell1234qrmulcl  42811  pell1234qrdich  42817  pell14qrdich  42825  reglogexp  42850  reglogexpbas  42853  rmxm1  42891  rmym1  42892  rmxdbl  42896  rmydbl  42897  jm2.24  42920  congtr  42922  congadd  42923  congmul  42924  congsym  42925  congneg  42926  congid  42928  congabseq  42931  acongsym  42933  acongneg2  42934  acongtr  42935  acongrep  42937  jm2.19lem3  42948  jm2.19lem4  42949  jm2.19  42950  jm2.25  42956  jm2.26a  42957  oddfl  45192  coskpi2  45787  cosknegpi  45790  dvdsn1add  45860  itgsinexp  45876  fourierdlem42  46070  fourierdlem97  46124  fourierswlem  46151  2elfz2melfz  47233  sfprmdvdsmersenne  47477  proththd  47488  dfodd6  47511  dfeven4  47512  evenm1odd  47513  evenp1odd  47514  enege  47519  onego  47520  dfeven2  47523  bits0ALTV  47553  opoeALTV  47557  opeoALTV  47558  evensumeven  47581  fppr2odd  47605  sbgoldbwt  47651  nnsum3primesgbe  47666  0nodd  47893  2nodd  47895  1neven  47961  2zlidl  47963  2zrngamgm  47968  2zrngasgrp  47969  2zrngagrp  47972  2zrngmmgm  47975  2zrngmsgrp  47976  2zrngnmrid  47979  zlmodzxzsub  48085  flsubz  48251  mod0mul  48253  m1modmmod  48255  zofldiv2  48265  dignn0flhalflem1  48349  dignn0flhalflem2  48350