Theorem zcn 12333

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 10878  ℤcz 12328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-resscn 10937

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287  df-neg 11217  df-z 12329

This theorem is referenced by:  zsscn  12336  zsubcl  12371  zrevaddcl  12374  nzadd  12377  zlem1lt  12381  zltlem1  12382  zdiv  12399  zdivadd  12400  zdivmul  12401  zextlt  12403  zneo  12412  zeo2  12416  peano5uzi  12418  zindd  12430  znnn0nn  12442  zriotaneg  12444  zmax  12694  rebtwnz  12696  qmulz  12700  zq  12703  qaddcl  12714  qnegcl  12715  qmulcl  12716  qreccl  12718  fzen  13282  uzsubsubfz  13287  fz01en  13293  fzmmmeqm  13298  fzsubel  13301  fztp  13321  fzsuc2  13323  fzrev2  13329  fzrev3  13331  elfzp1b  13342  fzrevral  13350  fzrevral2  13351  fzrevral3  13352  fzshftral  13353  fzo0addel  13450  fzo0addelr  13451  fzoaddel2  13452  elfzoext  13453  fzosubel2  13456  eluzgtdifelfzo  13458  fzocatel  13460  elfzom1elp1fzo  13463  fzval3  13465  zpnn0elfzo1  13470  fzosplitprm1  13506  fzoshftral  13513  flzadd  13555  2tnp1ge0ge0  13558  ceilid  13580  quoremz  13584  intfracq  13588  mulmod0  13606  zmod10  13616  modcyc  13635  modcyc2  13636  muladdmodid  13640  mulp1mod1  13641  modmuladdnn0  13644  modmul1  13653  modmulmodr  13666  modaddmulmod  13667  uzrdgxfr  13696  fzen2  13698  seqshft2  13758  sermono  13764  m1expeven  13839  expsub  13840  zesq  13950  modexp  13962  sqoddm1div8  13967  bccmpl  14032  swrd00  14366  addlenrevpfx  14412  swrdswrd  14427  swrdpfx  14429  pfxccatin12lem4  14448  pfxccatin12lem1  14450  swrdccatin2  14451  pfxccatin12lem2  14453  pfxccatin12  14455  repswrevw  14509  cshwsublen  14518  cshwidxmodr  14526  cshwidx0mod  14527  2cshw  14535  2cshwid  14536  2cshwcom  14538  cshweqdif2  14541  cshweqrep  14543  cshw1  14544  2cshwcshw  14547  shftuz  14789  seqshft  14805  nn0abscl  15033  nnabscl  15046  climshftlem  15292  climshft  15294  isershft  15384  mptfzshft  15499  fsumrev  15500  fsum0diag2  15504  efexp  15819  efzval  15820  demoivre  15918  sqrt2irr  15967  dvdsval2  15975  iddvds  15988  1dvds  15989  dvds0  15990  negdvdsb  15991  dvdsnegb  15992  0dvds  15995  dvdsmul1  15996  iddvdsexp  15998  muldvds1  15999  muldvds2  16000  dvdscmul  16001  dvdsmulc  16002  dvdscmulr  16003  dvdsmulcr  16004  summodnegmod  16005  modmulconst  16006  dvds2ln  16007  dvds2add  16008  dvds2sub  16009  dvdstr  16012  dvdssub2  16019  dvdsadd  16020  dvdsaddr  16021  dvdssub  16022  dvdssubr  16023  dvdsadd2b  16024  dvdsaddre2b  16025  dvdsabseq  16031  divconjdvds  16033  alzdvds  16038  addmodlteqALT  16043  dvdsexp2im  16045  odd2np1lem  16058  odd2np1  16059  even2n  16060  oddp1even  16062  mod2eq1n2dvds  16065  mulsucdiv2z  16071  zob  16077  ltoddhalfle  16079  halfleoddlt  16080  opoe  16081  omoe  16082  opeo  16083  omeo  16084  m1exp1  16094  divalglem0  16111  divalglem2  16113  divalglem4  16114  divalglem5  16115  divalglem9  16119  divalgb  16122  divalgmod  16124  modremain  16126  ndvdssub  16127  ndvdsadd  16128  flodddiv4  16131  flodddiv4t2lthalf  16134  bits0  16144  bitsp1e  16148  bitsp1o  16149  gcdneg  16238  gcdaddmlem  16240  gcdaddm  16241  gcdadd  16242  gcdid  16243  modgcd  16249  gcdmultiplez  16252  bezoutlem1  16256  bezoutlem2  16257  bezoutlem4  16259  dvdsgcd  16261  mulgcd  16265  absmulgcd  16266  mulgcdr  16267  gcddiv  16268  gcdmultiplezOLD  16270  dvdssqim  16273  dvdssq  16281  bezoutr1  16283  lcmcllem  16310  lcmneg  16317  lcmgcdlem  16320  lcmgcd  16321  lcmid  16323  lcm1  16324  coprmdvds  16367  coprmdvds2  16368  qredeq  16371  qredeu  16372  divgcdcoprmex  16380  cncongr1  16381  cncongr2  16382  prmdvdsexp  16429  prmdvdssqOLD  16433  rpexp1i  16437  divnumden  16461  zsqrtelqelz  16471  phiprmpw  16486  vfermltlALT  16512  nnnn0modprm0  16516  modprmn0modprm0  16517  coprimeprodsq2  16519  iserodd  16545  pclem  16548  pcprendvds2  16551  pcpremul  16553  pcmul  16561  pcneg  16584  fldivp1  16607  prmpwdvds  16614  zgz  16643  modxai  16778  mod2xnegi  16781  mulgfval  18711  mulgz  18740  mulgassr  18750  mulgmodid  18751  odmod  19163  odf1  19178  odf1o1  19186  gexdvds  19198  zaddablx  19482  cygablOLD  19501  ablfacrp  19678  pgpfac1lem3  19689  ablsimpgfindlem1  19719  zsubrg  20660  zsssubrg  20665  zringmulg  20687  zringinvg  20696  zringunit  20697  zringcyg  20700  prmirred  20705  mulgrhm2  20709  znunit  20780  degltp1le  25247  ef2kpi  25644  efper  25645  sinperlem  25646  sin2kpi  25649  cos2kpi  25650  abssinper  25686  sinkpi  25687  coskpi  25688  eflogeq  25766  cxpexpz  25831  root1eq1  25917  cxpeq  25919  relogbexp  25939  sgmval2  26301  ppiprm  26309  ppinprm  26310  chtprm  26311  chtnprm  26312  lgslem3  26456  lgsneg  26478  lgsdir2lem2  26483  lgsdir2lem4  26485  lgsdir2  26487  lgssq  26494  lgsmulsqcoprm  26500  lgsdirnn0  26501  gausslemma2dlem3  26525  lgsquadlem1  26537  lgsquadlem2  26538  lgsquad2  26543  2lgslem1a2  26547  2lgsoddprmlem1  26565  2lgsoddprmlem2  26566  2sqlem2  26575  2sqlem7  26581  rplogsumlem2  26642  axlowdimlem13  27331  wlk1walk  28015  clwwisshclwwslemlem  28386  ipasslem5  29206  rearchi  31555  znfermltl  31571  knoppndvlem9  34709  poimirlem19  35805  itg2addnclem2  35838  gcdaddmzz2nncomi  40011  metakunt16  40147  dvdsexpim  40335  zexpgcd  40343  zrtelqelz  40352  zrtdvds  40353  dffltz  40478  lzenom  40599  rexzrexnn0  40633  pell1234qrne0  40682  pell1234qrreccl  40683  pell1234qrmulcl  40684  pell1234qrdich  40690  pell14qrdich  40698  reglogexp  40723  reglogexpbas  40726  rmxm1  40763  rmym1  40764  rmxdbl  40768  rmydbl  40769  jm2.24  40792  congtr  40794  congadd  40795  congmul  40796  congsym  40797  congneg  40798  congid  40800  congabseq  40803  acongsym  40805  acongneg2  40806  acongtr  40807  acongrep  40809  jm2.19lem3  40820  jm2.19lem4  40821  jm2.19  40822  jm2.25  40828  jm2.26a  40829  oddfl  42823  coskpi2  43414  cosknegpi  43417  dvdsn1add  43487  itgsinexp  43503  fourierdlem42  43697  fourierdlem97  43751  fourierswlem  43778  2elfz2melfz  44821  sfprmdvdsmersenne  45066  proththd  45077  dfodd6  45100  dfeven4  45101  evenm1odd  45102  evenp1odd  45103  enege  45108  onego  45109  dfeven2  45112  bits0ALTV  45142  opoeALTV  45146  opeoALTV  45147  evensumeven  45170  fppr2odd  45194  sbgoldbwt  45240  nnsum3primesgbe  45255  0nodd  45375  2nodd  45377  1neven  45501  2zlidl  45503  2zrngamgm  45508  2zrngasgrp  45509  2zrngagrp  45512  2zrngmmgm  45515  2zrngmsgrp  45516  2zrngnmrid  45519  zlmodzxzsub  45707  flsubz  45874  mod0mul  45876  m1modmmod  45878  zofldiv2  45888  dignn0flhalflem1  45972  dignn0flhalflem2  45973