Theorem zcn 12510

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11042  ℤcz 12505

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 2701  ax-resscn 11101

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 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-neg 11384  df-z 12506

This theorem is referenced by:  zsscn  12513  zsubcl  12551  zrevaddcl  12554  nzadd  12557  zlem1lt  12561  zltlem1  12562  zdiv  12580  zdivadd  12581  zdivmul  12582  zextlt  12584  zneo  12593  zeo2  12597  peano5uzi  12599  zindd  12611  znnn0nn  12621  zriotaneg  12623  zmax  12880  rebtwnz  12882  qmulz  12886  zq  12889  qaddcl  12900  qnegcl  12901  qmulcl  12902  qreccl  12904  fzen  13478  uzsubsubfz  13483  fz01en  13489  fzmmmeqm  13494  fzsubel  13497  fztp  13517  fzsuc2  13519  fzrev2  13525  fzrev3  13527  elfzp1b  13538  fzrevral  13549  fzrevral2  13550  fzrevral3  13551  fzshftral  13552  fzo0addel  13655  fzo0addelr  13656  fzoaddel2  13657  fzosubel2  13662  eluzgtdifelfzo  13664  fzocatel  13666  elfzom1elp1fzo  13669  fzval3  13671  zpnn0elfzo1  13676  fzosplitprm1  13714  fzoshftral  13721  flzadd  13764  2tnp1ge0ge0  13767  ceilid  13789  quoremz  13793  intfracq  13797  mulmod0  13815  zmod10  13825  modcyc  13844  modcyc2  13845  muladdmodid  13851  mulp1mod1  13852  modmuladdnn0  13856  modmul1  13865  modmulmodr  13878  modaddmulmod  13879  uzrdgxfr  13908  fzen2  13910  seqshft2  13969  sermono  13975  m1expeven  14050  expsub  14051  zesq  14167  modexp  14179  sqoddm1div8  14184  bccmpl  14250  swrd00  14585  addlenrevpfx  14631  swrdswrd  14646  swrdpfx  14648  pfxccatin12lem4  14667  pfxccatin12lem1  14669  swrdccatin2  14670  pfxccatin12lem2  14672  pfxccatin12  14674  repswrevw  14728  cshwsublen  14737  cshwidxmodr  14745  cshwidx0mod  14746  2cshw  14754  2cshwid  14755  2cshwcom  14757  cshweqdif2  14760  cshweqrep  14762  cshw1  14763  2cshwcshw  14767  shftuz  15011  seqshft  15027  nn0abscl  15254  zabs0b  15256  nnabscl  15268  climshftlem  15516  climshft  15518  isershft  15606  mptfzshft  15720  fsumrev  15721  fsum0diag2  15725  efexp  16045  efzval  16046  demoivre  16144  sqrt2irr  16193  dvdsval2  16201  iddvds  16215  1dvds  16216  dvds0  16217  negdvdsb  16218  dvdsnegb  16219  0dvds  16222  dvdsmul1  16223  iddvdsexp  16225  muldvds1  16226  muldvds2  16227  dvdscmul  16228  dvdsmulc  16229  dvdscmulr  16230  dvdsmulcr  16231  summodnegmod  16232  difmod0  16233  modmulconst  16234  dvds2ln  16235  dvds2add  16236  dvds2sub  16237  dvdstr  16240  dvdssub2  16247  dvdsadd  16248  dvdsaddr  16249  dvdssub  16250  dvdssubr  16251  dvdsadd2b  16252  dvdsaddre2b  16253  dvdsabseq  16259  divconjdvds  16261  alzdvds  16266  addmodlteqALT  16271  dvdsexp2im  16273  odd2np1lem  16286  odd2np1  16287  even2n  16288  oddp1even  16290  mod2eq1n2dvds  16293  mulsucdiv2z  16299  zob  16305  ltoddhalfle  16307  halfleoddlt  16308  opoe  16309  omoe  16310  opeo  16311  omeo  16312  m1exp1  16322  divalglem0  16339  divalglem2  16341  divalglem4  16342  divalglem5  16343  divalglem9  16347  divalgb  16350  divalgmod  16352  modremain  16354  ndvdssub  16355  ndvdsadd  16356  flodddiv4  16361  flodddiv4t2lthalf  16364  bits0  16374  bitsp1e  16378  bitsp1o  16379  gcdneg  16468  gcdaddmlem  16470  gcdaddm  16471  gcdadd  16472  gcdid  16473  modgcd  16478  gcdmultiplez  16481  bezoutlem1  16485  bezoutlem2  16486  bezoutlem4  16488  dvdsgcd  16490  mulgcd  16494  absmulgcd  16495  mulgcdr  16496  gcddiv  16497  dvdssqim  16500  dvdsexpim  16501  zexpgcd  16511  dvdssq  16513  bezoutr1  16515  lcmcllem  16542  lcmneg  16549  lcmgcdlem  16552  lcmgcd  16553  lcmid  16555  lcm1  16556  coprmdvds  16599  coprmdvds2  16600  qredeq  16603  qredeu  16604  divgcdcoprmex  16612  cncongr1  16613  cncongr2  16614  prmdvdsexp  16661  rpexp1i  16669  divnumden  16694  zsqrtelqelz  16704  phiprmpw  16722  vfermltlALT  16749  nnnn0modprm0  16753  modprmn0modprm0  16754  coprimeprodsq2  16756  iserodd  16782  pclem  16785  pcprendvds2  16788  pcpremul  16790  pcmul  16798  pcneg  16821  fldivp1  16844  prmpwdvds  16851  zgz  16880  modxai  17015  mod2xnegi  17018  mulgfval  18983  mulgz  19016  mulgassr  19026  mulgmodid  19027  odmod  19460  odf1  19476  odf1o1  19486  gexdvds  19498  zaddablx  19786  ablfacrp  19982  pgpfac1lem3  19993  ablsimpgfindlem1  20023  zsubrg  21362  zsssubrg  21367  zringsub  21397  zringmulg  21398  zringinvg  21407  zringunit  21408  zringcyg  21411  prmirred  21416  mulgrhm2  21420  pzriprnglem6  21428  pzriprnglem8  21430  pzriprnglem10  21432  pzriprnglem12  21434  fermltlchr  21471  znunit  21505  degltp1le  26011  ef2kpi  26420  efper  26421  sinperlem  26422  sin2kpi  26425  cos2kpi  26426  abssinper  26463  sinkpi  26464  coskpi  26465  eflogeq  26544  cxpexpz  26609  root1eq1  26698  cxpeq  26700  zrtelqelz  26701  zrtdvds  26702  relogbexp  26723  sgmval2  27086  ppiprm  27094  ppinprm  27095  chtprm  27096  chtnprm  27097  lgslem3  27243  lgsneg  27265  lgsdir2lem2  27270  lgsdir2lem4  27272  lgsdir2  27274  lgssq  27281  lgsmulsqcoprm  27287  lgsdirnn0  27288  gausslemma2dlem3  27312  lgsquadlem1  27324  lgsquadlem2  27325  lgsquad2  27330  2lgslem1a2  27334  2lgsoddprmlem1  27352  2lgsoddprmlem2  27353  2sqlem2  27362  2sqlem7  27368  rplogsumlem2  27429  axlowdimlem13  28934  wlk1walk  29619  clwwisshclwwslemlem  29992  ipasslem5  30814  rearchi  33310  znfermltl  33330  knoppndvlem9  36501  poimirlem19  37626  itg2addnclem2  37659  gcdaddmzz2nncomi  41976  zdivgd  42318  ef11d  42320  cxp112d  42322  cxp111d  42323  cxpi11d  42324  dffltz  42615  lzenom  42751  rexzrexnn0  42785  pell1234qrne0  42834  pell1234qrreccl  42835  pell1234qrmulcl  42836  pell1234qrdich  42842  pell14qrdich  42850  reglogexp  42875  reglogexpbas  42878  rmxm1  42916  rmym1  42917  rmxdbl  42921  rmydbl  42922  jm2.24  42945  congtr  42947  congadd  42948  congmul  42949  congsym  42950  congneg  42951  congid  42953  congabseq  42956  acongsym  42958  acongneg2  42959  acongtr  42960  acongrep  42962  jm2.19lem3  42973  jm2.19lem4  42974  jm2.19  42975  jm2.25  42981  jm2.26a  42982  oddfl  45269  coskpi2  45857  cosknegpi  45860  dvdsn1add  45930  itgsinexp  45946  fourierdlem42  46140  fourierdlem97  46194  fourierswlem  46221  sinnpoly  46885  2elfz2melfz  47312  ceilbi  47327  submodaddmod  47335  submodneaddmod  47345  mod0mul  47350  m1modmmod  47352  modmkpkne  47355  modlt0b  47357  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  48053  gpg5nbgrvtx13starlem2  48056  0nodd  48151  2nodd  48153  1neven  48219  2zlidl  48221  2zrngamgm  48226  2zrngasgrp  48227  2zrngagrp  48230  2zrngmmgm  48233  2zrngmsgrp  48234  2zrngnmrid  48237  zlmodzxzsub  48341  flsubz  48504  zofldiv2  48513  dignn0flhalflem1  48597  dignn0flhalflem2  48598