Theorem zcn 12473

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℂcc 11004  ℤcz 12468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-resscn 11063

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349  df-neg 11347  df-z 12469

This theorem is referenced by:  zsscn  12476  zsubcl  12514  zrevaddcl  12517  nzadd  12520  zlem1lt  12524  zltlem1  12525  zdiv  12543  zdivadd  12544  zdivmul  12545  zextlt  12547  zneo  12556  zeo2  12560  peano5uzi  12562  zindd  12574  znnn0nn  12584  zriotaneg  12586  zmax  12843  rebtwnz  12845  qmulz  12849  zq  12852  qaddcl  12863  qnegcl  12864  qmulcl  12865  qreccl  12867  fzen  13441  uzsubsubfz  13446  fz01en  13452  fzmmmeqm  13457  fzsubel  13460  fztp  13480  fzsuc2  13482  fzrev2  13488  fzrev3  13490  elfzp1b  13501  fzrevral  13512  fzrevral2  13513  fzrevral3  13514  fzshftral  13515  fzo0addel  13618  fzo0addelr  13619  fzoaddel2  13620  fzosubel2  13625  eluzgtdifelfzo  13627  fzocatel  13629  elfzom1elp1fzo  13632  fzval3  13634  zpnn0elfzo1  13639  fzosplitprm1  13678  fzoshftral  13687  flzadd  13730  2tnp1ge0ge0  13733  ceilid  13755  quoremz  13759  intfracq  13763  mulmod0  13781  zmod10  13791  modcyc  13810  modcyc2  13811  muladdmodid  13817  mulp1mod1  13818  modmuladdnn0  13822  modmul1  13831  modmulmodr  13844  modaddmulmod  13845  uzrdgxfr  13874  fzen2  13876  seqshft2  13935  sermono  13941  m1expeven  14016  expsub  14017  zesq  14133  modexp  14145  sqoddm1div8  14150  bccmpl  14216  swrd00  14552  swrdswrd  14612  swrdpfx  14614  pfxccatin12lem4  14633  pfxccatin12lem1  14635  swrdccatin2  14636  pfxccatin12lem2  14638  pfxccatin12  14640  repswrevw  14694  cshwsublen  14703  cshwidxmodr  14711  cshwidx0mod  14712  2cshw  14720  2cshwid  14721  2cshwcom  14723  cshweqdif2  14726  cshweqrep  14728  cshw1  14729  2cshwcshw  14732  shftuz  14976  seqshft  14992  nn0abscl  15219  zabs0b  15221  nnabscl  15233  climshftlem  15481  climshft  15483  isershft  15571  mptfzshft  15685  fsumrev  15686  fsum0diag2  15690  efexp  16010  efzval  16011  demoivre  16109  sqrt2irr  16158  dvdsval2  16166  iddvds  16180  1dvds  16181  dvds0  16182  negdvdsb  16183  dvdsnegb  16184  0dvds  16187  dvdsmul1  16188  iddvdsexp  16190  muldvds1  16191  muldvds2  16192  dvdscmul  16193  dvdsmulc  16194  dvdscmulr  16195  dvdsmulcr  16196  summodnegmod  16197  difmod0  16198  modmulconst  16199  dvds2ln  16200  dvds2add  16201  dvds2sub  16202  dvdstr  16205  dvdssub2  16212  dvdsadd  16213  dvdsaddr  16214  dvdssub  16215  dvdssubr  16216  dvdsadd2b  16217  dvdsaddre2b  16218  dvdsabseq  16224  divconjdvds  16226  alzdvds  16231  addmodlteqALT  16236  dvdsexp2im  16238  odd2np1lem  16251  odd2np1  16252  even2n  16253  oddp1even  16255  mod2eq1n2dvds  16258  mulsucdiv2z  16264  zob  16270  ltoddhalfle  16272  halfleoddlt  16273  opoe  16274  omoe  16275  opeo  16276  omeo  16277  m1exp1  16287  divalglem0  16304  divalglem2  16306  divalglem4  16307  divalglem5  16308  divalglem9  16312  divalgb  16315  divalgmod  16317  modremain  16319  ndvdssub  16320  ndvdsadd  16321  flodddiv4  16326  flodddiv4t2lthalf  16329  bits0  16339  bitsp1e  16343  bitsp1o  16344  gcdneg  16433  gcdaddmlem  16435  gcdaddm  16436  gcdadd  16437  gcdid  16438  modgcd  16443  gcdmultiplez  16446  bezoutlem1  16450  bezoutlem2  16451  bezoutlem4  16453  dvdsgcd  16455  mulgcd  16459  absmulgcd  16460  mulgcdr  16461  gcddiv  16462  dvdssqim  16465  dvdsexpim  16466  zexpgcd  16476  dvdssq  16478  bezoutr1  16480  lcmcllem  16507  lcmneg  16514  lcmgcdlem  16517  lcmgcd  16518  lcmid  16520  lcm1  16521  coprmdvds  16564  coprmdvds2  16565  qredeq  16568  qredeu  16569  divgcdcoprmex  16577  cncongr1  16578  cncongr2  16579  prmdvdsexp  16626  rpexp1i  16634  divnumden  16659  zsqrtelqelz  16669  phiprmpw  16687  vfermltlALT  16714  nnnn0modprm0  16718  modprmn0modprm0  16719  coprimeprodsq2  16721  iserodd  16747  pclem  16750  pcprendvds2  16753  pcpremul  16755  pcmul  16763  pcneg  16786  fldivp1  16809  prmpwdvds  16816  zgz  16845  modxai  16980  mod2xnegi  16983  chnccat  18532  chnrev  18533  mulgfval  18982  mulgz  19015  mulgassr  19025  mulgmodid  19026  odmod  19458  odf1  19474  odf1o1  19484  gexdvds  19496  zaddablx  19784  ablfacrp  19980  pgpfac1lem3  19991  ablsimpgfindlem1  20021  zsubrg  21357  zsssubrg  21362  zringsub  21392  zringmulg  21393  zringinvg  21402  zringunit  21403  zringcyg  21406  prmirred  21411  mulgrhm2  21415  pzriprnglem6  21423  pzriprnglem8  21425  pzriprnglem10  21427  pzriprnglem12  21429  fermltlchr  21466  znunit  21500  degltp1le  26005  ef2kpi  26414  efper  26415  sinperlem  26416  sin2kpi  26419  cos2kpi  26420  abssinper  26457  sinkpi  26458  coskpi  26459  eflogeq  26538  cxpexpz  26603  root1eq1  26692  cxpeq  26694  zrtelqelz  26695  zrtdvds  26696  relogbexp  26717  sgmval2  27080  ppiprm  27088  ppinprm  27089  chtprm  27090  chtnprm  27091  lgslem3  27237  lgsneg  27259  lgsdir2lem2  27264  lgsdir2lem4  27266  lgsdir2  27268  lgssq  27275  lgsmulsqcoprm  27281  lgsdirnn0  27282  gausslemma2dlem3  27306  lgsquadlem1  27318  lgsquadlem2  27319  lgsquad2  27324  2lgslem1a2  27328  2lgsoddprmlem1  27346  2lgsoddprmlem2  27347  2sqlem2  27356  2sqlem7  27362  rplogsumlem2  27423  axlowdimlem13  28932  wlk1walk  29617  clwwisshclwwslemlem  29993  ipasslem5  30815  rearchi  33311  znfermltl  33331  knoppndvlem9  36564  poimirlem19  37689  itg2addnclem2  37722  gcdaddmzz2nncomi  42098  zdivgd  42440  ef11d  42442  cxp112d  42444  cxp111d  42445  cxpi11d  42446  dffltz  42737  lzenom  42873  rexzrexnn0  42907  pell1234qrne0  42956  pell1234qrreccl  42957  pell1234qrmulcl  42958  pell1234qrdich  42964  pell14qrdich  42972  reglogexp  42997  reglogexpbas  43000  rmxm1  43037  rmym1  43038  rmxdbl  43042  rmydbl  43043  jm2.24  43066  congtr  43068  congadd  43069  congmul  43070  congsym  43071  congneg  43072  congid  43074  congabseq  43077  acongsym  43079  acongneg2  43080  acongtr  43081  acongrep  43083  jm2.19lem3  43094  jm2.19lem4  43095  jm2.19  43096  jm2.25  43102  jm2.26a  43103  oddfl  45389  coskpi2  45974  cosknegpi  45977  dvdsn1add  46047  itgsinexp  46063  fourierdlem42  46257  fourierdlem97  46311  fourierswlem  46338  sinnpoly  47001  2elfz2melfz  47428  ceilbi  47443  submodaddmod  47451  submodneaddmod  47461  mod0mul  47466  m1modmmod  47468  modmkpkne  47471  modlt0b  47473  sfprmdvdsmersenne  47713  proththd  47724  dfodd6  47747  dfeven4  47748  evenm1odd  47749  evenp1odd  47750  enege  47755  onego  47756  dfeven2  47759  bits0ALTV  47789  opoeALTV  47793  opeoALTV  47794  evensumeven  47817  fppr2odd  47841  sbgoldbwt  47887  nnsum3primesgbe  47902  gpgedgvtx0  48171  gpg5nbgrvtx03starlem2  48179  gpg5nbgrvtx13starlem2  48182  0nodd  48280  2nodd  48282  1neven  48348  2zlidl  48350  2zrngamgm  48355  2zrngasgrp  48356  2zrngagrp  48359  2zrngmmgm  48362  2zrngmsgrp  48363  2zrngnmrid  48366  zlmodzxzsub  48470  flsubz  48633  zofldiv2  48642  dignn0flhalflem1  48726  dignn0flhalflem2  48727