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  18977  mulgz  19010  mulgassr  19020  mulgmodid  19021  odmod  19452  odf1  19468  odf1o1  19478  gexdvds  19490  zaddablx  19778  ablfacrp  19974  pgpfac1lem3  19985  ablsimpgfindlem1  20015  zsubrg  21313  zsssubrg  21318  zringsub  21341  zringmulg  21342  zringinvg  21351  zringunit  21352  zringcyg  21355  prmirred  21360  mulgrhm2  21364  pzriprnglem6  21372  pzriprnglem8  21374  pzriprnglem10  21376  pzriprnglem12  21378  fermltlchr  21415  znunit  21449  degltp1le  25954  ef2kpi  26363  efper  26364  sinperlem  26365  sin2kpi  26368  cos2kpi  26369  abssinper  26406  sinkpi  26407  coskpi  26408  eflogeq  26487  cxpexpz  26552  root1eq1  26641  cxpeq  26643  zrtelqelz  26644  zrtdvds  26645  relogbexp  26666  sgmval2  27029  ppiprm  27037  ppinprm  27038  chtprm  27039  chtnprm  27040  lgslem3  27186  lgsneg  27208  lgsdir2lem2  27213  lgsdir2lem4  27215  lgsdir2  27217  lgssq  27224  lgsmulsqcoprm  27230  lgsdirnn0  27231  gausslemma2dlem3  27255  lgsquadlem1  27267  lgsquadlem2  27268  lgsquad2  27273  2lgslem1a2  27277  2lgsoddprmlem1  27295  2lgsoddprmlem2  27296  2sqlem2  27305  2sqlem7  27311  rplogsumlem2  27372  axlowdimlem13  28857  wlk1walk  29542  clwwisshclwwslemlem  29915  ipasslem5  30737  rearchi  33290  znfermltl  33310  knoppndvlem9  36481  poimirlem19  37606  itg2addnclem2  37639  gcdaddmzz2nncomi  41956  zdivgd  42298  ef11d  42300  cxp112d  42302  cxp111d  42303  cxpi11d  42304  dffltz  42595  lzenom  42731  rexzrexnn0  42765  pell1234qrne0  42814  pell1234qrreccl  42815  pell1234qrmulcl  42816  pell1234qrdich  42822  pell14qrdich  42830  reglogexp  42855  reglogexpbas  42858  rmxm1  42896  rmym1  42897  rmxdbl  42901  rmydbl  42902  jm2.24  42925  congtr  42927  congadd  42928  congmul  42929  congsym  42930  congneg  42931  congid  42933  congabseq  42936  acongsym  42938  acongneg2  42939  acongtr  42940  acongrep  42942  jm2.19lem3  42953  jm2.19lem4  42954  jm2.19  42955  jm2.25  42961  jm2.26a  42962  oddfl  45249  coskpi2  45837  cosknegpi  45840  dvdsn1add  45910  itgsinexp  45926  fourierdlem42  46120  fourierdlem97  46174  fourierswlem  46201  sinnpoly  46865  2elfz2melfz  47292  ceilbi  47307  submodaddmod  47315  submodneaddmod  47325  mod0mul  47330  m1modmmod  47332  modmkpkne  47335  modlt0b  47337  sfprmdvdsmersenne  47577  proththd  47588  dfodd6  47611  dfeven4  47612  evenm1odd  47613  evenp1odd  47614  enege  47619  onego  47620  dfeven2  47623  bits0ALTV  47653  opoeALTV  47657  opeoALTV  47658  evensumeven  47681  fppr2odd  47705  sbgoldbwt  47751  nnsum3primesgbe  47766  gpgedgvtx0  48025  gpg5nbgrvtx03starlem2  48033  gpg5nbgrvtx13starlem2  48036  0nodd  48131  2nodd  48133  1neven  48199  2zlidl  48201  2zrngamgm  48206  2zrngasgrp  48207  2zrngagrp  48210  2zrngmmgm  48213  2zrngmsgrp  48214  2zrngnmrid  48217  zlmodzxzsub  48321  flsubz  48484  zofldiv2  48493  dignn0flhalflem1  48577  dignn0flhalflem2  48578