Theorem zcn 12254

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 10800  ℤcz 12249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-neg 11138  df-z 12250

This theorem is referenced by:  zsscn  12257  zsubcl  12292  zrevaddcl  12295  nzadd  12298  zlem1lt  12302  zltlem1  12303  zdiv  12320  zdivadd  12321  zdivmul  12322  zextlt  12324  zneo  12333  zeo2  12337  peano5uzi  12339  zindd  12351  znnn0nn  12362  zriotaneg  12364  zmax  12614  rebtwnz  12616  qmulz  12620  zq  12623  qaddcl  12634  qnegcl  12635  qmulcl  12636  qreccl  12638  fzen  13202  uzsubsubfz  13207  fz01en  13213  fzmmmeqm  13218  fzsubel  13221  fztp  13241  fzsuc2  13243  fzrev2  13249  fzrev3  13251  elfzp1b  13262  fzrevral  13270  fzrevral2  13271  fzrevral3  13272  fzshftral  13273  fzo0addel  13369  fzo0addelr  13370  fzoaddel2  13371  elfzoext  13372  fzosubel2  13375  eluzgtdifelfzo  13377  fzocatel  13379  elfzom1elp1fzo  13382  fzval3  13384  zpnn0elfzo1  13389  fzosplitprm1  13425  fzoshftral  13432  flzadd  13474  2tnp1ge0ge0  13477  ceilid  13499  quoremz  13503  intfracq  13507  mulmod0  13525  zmod10  13535  modcyc  13554  modcyc2  13555  muladdmodid  13559  mulp1mod1  13560  modmuladdnn0  13563  modmul1  13572  modmulmodr  13585  modaddmulmod  13586  uzrdgxfr  13615  fzen2  13617  seqshft2  13677  sermono  13683  m1expeven  13758  expsub  13759  zesq  13869  modexp  13881  sqoddm1div8  13886  bccmpl  13951  swrd00  14285  addlenrevpfx  14331  swrdswrd  14346  swrdpfx  14348  pfxccatin12lem4  14367  pfxccatin12lem1  14369  swrdccatin2  14370  pfxccatin12lem2  14372  pfxccatin12  14374  repswrevw  14428  cshwsublen  14437  cshwidxmodr  14445  cshwidx0mod  14446  2cshw  14454  2cshwid  14455  2cshwcom  14457  cshweqdif2  14460  cshweqrep  14462  cshw1  14463  2cshwcshw  14466  shftuz  14708  seqshft  14724  nn0abscl  14952  nnabscl  14965  climshftlem  15211  climshft  15213  isershft  15303  mptfzshft  15418  fsumrev  15419  fsum0diag2  15423  efexp  15738  efzval  15739  demoivre  15837  sqrt2irr  15886  dvdsval2  15894  iddvds  15907  1dvds  15908  dvds0  15909  negdvdsb  15910  dvdsnegb  15911  0dvds  15914  dvdsmul1  15915  iddvdsexp  15917  muldvds1  15918  muldvds2  15919  dvdscmul  15920  dvdsmulc  15921  dvdscmulr  15922  dvdsmulcr  15923  summodnegmod  15924  modmulconst  15925  dvds2ln  15926  dvds2add  15927  dvds2sub  15928  dvdstr  15931  dvdssub2  15938  dvdsadd  15939  dvdsaddr  15940  dvdssub  15941  dvdssubr  15942  dvdsadd2b  15943  dvdsaddre2b  15944  dvdsabseq  15950  divconjdvds  15952  alzdvds  15957  addmodlteqALT  15962  dvdsexp2im  15964  odd2np1lem  15977  odd2np1  15978  even2n  15979  oddp1even  15981  mod2eq1n2dvds  15984  mulsucdiv2z  15990  zob  15996  ltoddhalfle  15998  halfleoddlt  15999  opoe  16000  omoe  16001  opeo  16002  omeo  16003  m1exp1  16013  divalglem0  16030  divalglem2  16032  divalglem4  16033  divalglem5  16034  divalglem9  16038  divalgb  16041  divalgmod  16043  modremain  16045  ndvdssub  16046  ndvdsadd  16047  flodddiv4  16050  flodddiv4t2lthalf  16053  bits0  16063  bitsp1e  16067  bitsp1o  16068  gcdneg  16157  gcdaddmlem  16159  gcdaddm  16160  gcdadd  16161  gcdid  16162  modgcd  16168  gcdmultiplez  16171  bezoutlem1  16175  bezoutlem2  16176  bezoutlem4  16178  dvdsgcd  16180  mulgcd  16184  absmulgcd  16185  mulgcdr  16186  gcddiv  16187  gcdmultiplezOLD  16189  dvdssqim  16192  dvdssq  16200  bezoutr1  16202  lcmcllem  16229  lcmneg  16236  lcmgcdlem  16239  lcmgcd  16240  lcmid  16242  lcm1  16243  coprmdvds  16286  coprmdvds2  16287  qredeq  16290  qredeu  16291  divgcdcoprmex  16299  cncongr1  16300  cncongr2  16301  prmdvdsexp  16348  prmdvdssqOLD  16352  rpexp1i  16356  divnumden  16380  zsqrtelqelz  16390  phiprmpw  16405  vfermltlALT  16431  nnnn0modprm0  16435  modprmn0modprm0  16436  coprimeprodsq2  16438  iserodd  16464  pclem  16467  pcprendvds2  16470  pcpremul  16472  pcmul  16480  pcneg  16503  fldivp1  16526  prmpwdvds  16533  zgz  16562  modxai  16697  mod2xnegi  16700  mulgfval  18617  mulgz  18646  mulgassr  18656  mulgmodid  18657  odmod  19069  odf1  19084  odf1o1  19092  gexdvds  19104  zaddablx  19388  cygablOLD  19407  ablfacrp  19584  pgpfac1lem3  19595  ablsimpgfindlem1  19625  zsubrg  20563  zsssubrg  20568  zringmulg  20590  zringinvg  20599  zringunit  20600  zringcyg  20603  prmirred  20608  mulgrhm2  20612  znunit  20683  degltp1le  25143  ef2kpi  25540  efper  25541  sinperlem  25542  sin2kpi  25545  cos2kpi  25546  abssinper  25582  sinkpi  25583  coskpi  25584  eflogeq  25662  cxpexpz  25727  root1eq1  25813  cxpeq  25815  relogbexp  25835  sgmval2  26197  ppiprm  26205  ppinprm  26206  chtprm  26207  chtnprm  26208  lgslem3  26352  lgsneg  26374  lgsdir2lem2  26379  lgsdir2lem4  26381  lgsdir2  26383  lgssq  26390  lgsmulsqcoprm  26396  lgsdirnn0  26397  gausslemma2dlem3  26421  lgsquadlem1  26433  lgsquadlem2  26434  lgsquad2  26439  2lgslem1a2  26443  2lgsoddprmlem1  26461  2lgsoddprmlem2  26462  2sqlem2  26471  2sqlem7  26477  rplogsumlem2  26538  axlowdimlem13  27225  wlk1walk  27908  clwwisshclwwslemlem  28278  ipasslem5  29098  rearchi  31448  znfermltl  31464  knoppndvlem9  34627  poimirlem19  35723  itg2addnclem2  35756  gcdaddmzz2nncomi  39932  metakunt16  40068  dvdsexpim  40249  zexpgcd  40257  zrtelqelz  40266  zrtdvds  40267  dffltz  40387  lzenom  40508  rexzrexnn0  40542  pell1234qrne0  40591  pell1234qrreccl  40592  pell1234qrmulcl  40593  pell1234qrdich  40599  pell14qrdich  40607  reglogexp  40632  reglogexpbas  40635  rmxm1  40672  rmym1  40673  rmxdbl  40677  rmydbl  40678  jm2.24  40701  congtr  40703  congadd  40704  congmul  40705  congsym  40706  congneg  40707  congid  40709  congabseq  40712  acongsym  40714  acongneg2  40715  acongtr  40716  acongrep  40718  jm2.19lem3  40729  jm2.19lem4  40730  jm2.19  40731  jm2.25  40737  jm2.26a  40738  oddfl  42705  coskpi2  43297  cosknegpi  43300  dvdsn1add  43370  itgsinexp  43386  fourierdlem42  43580  fourierdlem97  43634  fourierswlem  43661  2elfz2melfz  44698  sfprmdvdsmersenne  44943  proththd  44954  dfodd6  44977  dfeven4  44978  evenm1odd  44979  evenp1odd  44980  enege  44985  onego  44986  dfeven2  44989  bits0ALTV  45019  opoeALTV  45023  opeoALTV  45024  evensumeven  45047  fppr2odd  45071  sbgoldbwt  45117  nnsum3primesgbe  45132  0nodd  45252  2nodd  45254  1neven  45378  2zlidl  45380  2zrngamgm  45385  2zrngasgrp  45386  2zrngagrp  45389  2zrngmmgm  45392  2zrngmsgrp  45393  2zrngnmrid  45396  zlmodzxzsub  45584  flsubz  45751  mod0mul  45753  m1modmmod  45755  zofldiv2  45765  dignn0flhalflem1  45849  dignn0flhalflem2  45850