Theorem zcn 12598

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11132  ℤcz 12593

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 2708  ax-resscn 11191

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-neg 11474  df-z 12594

This theorem is referenced by:  zsscn  12601  zsubcl  12639  zrevaddcl  12642  nzadd  12645  zlem1lt  12649  zltlem1  12650  zdiv  12668  zdivadd  12669  zdivmul  12670  zextlt  12672  zneo  12681  zeo2  12685  peano5uzi  12687  zindd  12699  znnn0nn  12709  zriotaneg  12711  zmax  12966  rebtwnz  12968  qmulz  12972  zq  12975  qaddcl  12986  qnegcl  12987  qmulcl  12988  qreccl  12990  fzen  13563  uzsubsubfz  13568  fz01en  13574  fzmmmeqm  13579  fzsubel  13582  fztp  13602  fzsuc2  13604  fzrev2  13610  fzrev3  13612  elfzp1b  13623  fzrevral  13634  fzrevral2  13635  fzrevral3  13636  fzshftral  13637  fzo0addel  13739  fzo0addelr  13740  fzoaddel2  13741  fzosubel2  13746  eluzgtdifelfzo  13748  fzocatel  13750  elfzom1elp1fzo  13753  fzval3  13755  zpnn0elfzo1  13760  fzosplitprm1  13798  fzoshftral  13805  flzadd  13848  2tnp1ge0ge0  13851  ceilid  13873  quoremz  13877  intfracq  13881  mulmod0  13899  zmod10  13909  modcyc  13928  modcyc2  13929  muladdmodid  13933  mulp1mod1  13934  modmuladdnn0  13938  modmul1  13947  modmulmodr  13960  modaddmulmod  13961  uzrdgxfr  13990  fzen2  13992  seqshft2  14051  sermono  14057  m1expeven  14132  expsub  14133  zesq  14249  modexp  14261  sqoddm1div8  14266  bccmpl  14332  swrd00  14667  addlenrevpfx  14713  swrdswrd  14728  swrdpfx  14730  pfxccatin12lem4  14749  pfxccatin12lem1  14751  swrdccatin2  14752  pfxccatin12lem2  14754  pfxccatin12  14756  repswrevw  14810  cshwsublen  14819  cshwidxmodr  14827  cshwidx0mod  14828  2cshw  14836  2cshwid  14837  2cshwcom  14839  cshweqdif2  14842  cshweqrep  14844  cshw1  14845  2cshwcshw  14849  shftuz  15093  seqshft  15109  nn0abscl  15336  nnabscl  15349  climshftlem  15595  climshft  15597  isershft  15685  mptfzshft  15799  fsumrev  15800  fsum0diag2  15804  efexp  16124  efzval  16125  demoivre  16223  sqrt2irr  16272  dvdsval2  16280  iddvds  16294  1dvds  16295  dvds0  16296  negdvdsb  16297  dvdsnegb  16298  0dvds  16301  dvdsmul1  16302  iddvdsexp  16304  muldvds1  16305  muldvds2  16306  dvdscmul  16307  dvdsmulc  16308  dvdscmulr  16309  dvdsmulcr  16310  summodnegmod  16311  modmulconst  16312  dvds2ln  16313  dvds2add  16314  dvds2sub  16315  dvdstr  16318  dvdssub2  16325  dvdsadd  16326  dvdsaddr  16327  dvdssub  16328  dvdssubr  16329  dvdsadd2b  16330  dvdsaddre2b  16331  dvdsabseq  16337  divconjdvds  16339  alzdvds  16344  addmodlteqALT  16349  dvdsexp2im  16351  odd2np1lem  16364  odd2np1  16365  even2n  16366  oddp1even  16368  mod2eq1n2dvds  16371  mulsucdiv2z  16377  zob  16383  ltoddhalfle  16385  halfleoddlt  16386  opoe  16387  omoe  16388  opeo  16389  omeo  16390  m1exp1  16400  divalglem0  16417  divalglem2  16419  divalglem4  16420  divalglem5  16421  divalglem9  16425  divalgb  16428  divalgmod  16430  modremain  16432  ndvdssub  16433  ndvdsadd  16434  flodddiv4  16439  flodddiv4t2lthalf  16442  bits0  16452  bitsp1e  16456  bitsp1o  16457  gcdneg  16546  gcdaddmlem  16548  gcdaddm  16549  gcdadd  16550  gcdid  16551  modgcd  16556  gcdmultiplez  16559  bezoutlem1  16563  bezoutlem2  16564  bezoutlem4  16566  dvdsgcd  16568  mulgcd  16572  absmulgcd  16573  mulgcdr  16574  gcddiv  16575  dvdssqim  16578  dvdsexpim  16579  zexpgcd  16589  dvdssq  16591  bezoutr1  16593  lcmcllem  16620  lcmneg  16627  lcmgcdlem  16630  lcmgcd  16631  lcmid  16633  lcm1  16634  coprmdvds  16677  coprmdvds2  16678  qredeq  16681  qredeu  16682  divgcdcoprmex  16690  cncongr1  16691  cncongr2  16692  prmdvdsexp  16739  rpexp1i  16747  divnumden  16772  zsqrtelqelz  16782  phiprmpw  16800  vfermltlALT  16827  nnnn0modprm0  16831  modprmn0modprm0  16832  coprimeprodsq2  16834  iserodd  16860  pclem  16863  pcprendvds2  16866  pcpremul  16868  pcmul  16876  pcneg  16899  fldivp1  16922  prmpwdvds  16929  zgz  16958  modxai  17093  mod2xnegi  17096  mulgfval  19057  mulgz  19090  mulgassr  19100  mulgmodid  19101  odmod  19532  odf1  19548  odf1o1  19558  gexdvds  19570  zaddablx  19858  ablfacrp  20054  pgpfac1lem3  20065  ablsimpgfindlem1  20095  zsubrg  21393  zsssubrg  21398  zringsub  21421  zringmulg  21422  zringinvg  21431  zringunit  21432  zringcyg  21435  prmirred  21440  mulgrhm2  21444  pzriprnglem6  21452  pzriprnglem8  21454  pzriprnglem10  21456  pzriprnglem12  21458  fermltlchr  21495  znunit  21529  degltp1le  26035  ef2kpi  26444  efper  26445  sinperlem  26446  sin2kpi  26449  cos2kpi  26450  abssinper  26487  sinkpi  26488  coskpi  26489  eflogeq  26568  cxpexpz  26633  root1eq1  26722  cxpeq  26724  zrtelqelz  26725  zrtdvds  26726  relogbexp  26747  sgmval2  27110  ppiprm  27118  ppinprm  27119  chtprm  27120  chtnprm  27121  lgslem3  27267  lgsneg  27289  lgsdir2lem2  27294  lgsdir2lem4  27296  lgsdir2  27298  lgssq  27305  lgsmulsqcoprm  27311  lgsdirnn0  27312  gausslemma2dlem3  27336  lgsquadlem1  27348  lgsquadlem2  27349  lgsquad2  27354  2lgslem1a2  27358  2lgsoddprmlem1  27376  2lgsoddprmlem2  27377  2sqlem2  27386  2sqlem7  27392  rplogsumlem2  27453  axlowdimlem13  28938  wlk1walk  29624  clwwisshclwwslemlem  29999  ipasslem5  30821  rearchi  33366  znfermltl  33386  knoppndvlem9  36543  poimirlem19  37668  itg2addnclem2  37701  gcdaddmzz2nncomi  42013  zdivgd  42355  ef11d  42357  cxp112d  42359  cxp111d  42360  cxpi11d  42361  dffltz  42632  lzenom  42768  rexzrexnn0  42802  pell1234qrne0  42851  pell1234qrreccl  42852  pell1234qrmulcl  42853  pell1234qrdich  42859  pell14qrdich  42867  reglogexp  42892  reglogexpbas  42895  rmxm1  42933  rmym1  42934  rmxdbl  42938  rmydbl  42939  jm2.24  42962  congtr  42964  congadd  42965  congmul  42966  congsym  42967  congneg  42968  congid  42970  congabseq  42973  acongsym  42975  acongneg2  42976  acongtr  42977  acongrep  42979  jm2.19lem3  42990  jm2.19lem4  42991  jm2.19  42992  jm2.25  42998  jm2.26a  42999  oddfl  45286  coskpi2  45875  cosknegpi  45878  dvdsn1add  45948  itgsinexp  45964  fourierdlem42  46158  fourierdlem97  46212  fourierswlem  46239  2elfz2melfz  47327  ceilbi  47342  submodaddmod  47350  submodneaddmod  47360  sfprmdvdsmersenne  47597  proththd  47608  dfodd6  47631  dfeven4  47632  evenm1odd  47633  evenp1odd  47634  enege  47639  onego  47640  dfeven2  47643  bits0ALTV  47673  opoeALTV  47677  opeoALTV  47678  evensumeven  47701  fppr2odd  47725  sbgoldbwt  47771  nnsum3primesgbe  47786  gpgedgvtx0  48045  gpg5nbgrvtx03starlem2  48051  gpg5nbgrvtx13starlem2  48054  0nodd  48125  2nodd  48127  1neven  48193  2zlidl  48195  2zrngamgm  48200  2zrngasgrp  48201  2zrngagrp  48204  2zrngmmgm  48207  2zrngmsgrp  48208  2zrngnmrid  48211  zlmodzxzsub  48315  flsubz  48478  mod0mul  48479  m1modmmod  48481  zofldiv2  48491  dignn0flhalflem1  48575  dignn0flhalflem2  48576