Theorem zcn 12520

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℂcc 11027  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-resscn 11086

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359  df-neg 11371  df-z 12516

This theorem is referenced by:  zsscn  12523  zsubcl  12560  zrevaddcl  12563  nzadd  12566  zlem1lt  12570  zltlem1  12571  zdiv  12590  zdivadd  12591  zdivmul  12592  zextlt  12594  zneo  12603  zeo2  12607  peano5uzi  12609  zindd  12621  znnn0nn  12631  zriotaneg  12633  zmax  12886  rebtwnz  12888  qmulz  12892  zq  12895  qaddcl  12906  qnegcl  12907  qmulcl  12908  qreccl  12910  fzen  13486  uzsubsubfz  13491  fz01en  13497  fzmmmeqm  13502  fzsubel  13505  fztp  13525  fzsuc2  13527  fzrev2  13533  fzrev3  13535  elfzp1b  13546  fzrevral  13557  fzrevral2  13558  fzrevral3  13559  fzshftral  13560  fzo0addel  13664  fzo0addelr  13665  fzoaddel2  13666  fzosubel2  13671  eluzgtdifelfzo  13673  fzocatel  13675  elfzom1elp1fzo  13678  fzval3  13680  zpnn0elfzo1  13685  fzosplitprm1  13724  fzoshftral  13733  flzadd  13776  2tnp1ge0ge0  13779  ceilid  13801  quoremz  13805  intfracq  13809  mulmod0  13827  zmod10  13837  modcyc  13856  modcyc2  13857  muladdmodid  13863  mulp1mod1  13864  modmuladdnn0  13868  modmul1  13877  modmulmodr  13890  modaddmulmod  13891  uzrdgxfr  13920  fzen2  13922  seqshft2  13981  sermono  13987  m1expeven  14062  expsub  14063  zesq  14179  modexp  14191  sqoddm1div8  14196  bccmpl  14262  swrd00  14598  swrdswrd  14658  swrdpfx  14660  pfxccatin12lem4  14679  pfxccatin12lem1  14681  swrdccatin2  14682  pfxccatin12lem2  14684  pfxccatin12  14686  repswrevw  14740  cshwsublen  14749  cshwidxmodr  14757  cshwidx0mod  14758  2cshw  14766  2cshwid  14767  2cshwcom  14769  cshweqdif2  14772  cshweqrep  14774  cshw1  14775  2cshwcshw  14778  shftuz  15022  seqshft  15038  nn0abscl  15265  zabs0b  15267  nnabscl  15279  climshftlem  15527  climshft  15529  isershft  15617  mptfzshft  15731  fsumrev  15732  fsum0diag2  15736  efexp  16059  efzval  16060  demoivre  16158  sqrt2irr  16207  dvdsval2  16215  iddvds  16229  1dvds  16230  dvds0  16231  negdvdsb  16232  dvdsnegb  16233  0dvds  16236  dvdsmul1  16237  iddvdsexp  16239  muldvds1  16240  muldvds2  16241  dvdscmul  16242  dvdsmulc  16243  dvdscmulr  16244  dvdsmulcr  16245  summodnegmod  16246  difmod0  16247  modmulconst  16248  dvds2ln  16249  dvds2add  16250  dvds2sub  16251  dvdstr  16254  dvdssub2  16261  dvdsadd  16262  dvdsaddr  16263  dvdssub  16264  dvdssubr  16265  dvdsadd2b  16266  dvdsaddre2b  16267  dvdsabseq  16273  divconjdvds  16275  alzdvds  16280  addmodlteqALT  16285  dvdsexp2im  16287  odd2np1lem  16300  odd2np1  16301  even2n  16302  oddp1even  16304  mod2eq1n2dvds  16307  mulsucdiv2z  16313  zob  16319  ltoddhalfle  16321  halfleoddlt  16322  opoe  16323  omoe  16324  opeo  16325  omeo  16326  m1exp1  16336  divalglem0  16353  divalglem2  16355  divalglem4  16356  divalglem5  16357  divalglem9  16361  divalgb  16364  divalgmod  16366  modremain  16368  ndvdssub  16369  ndvdsadd  16370  flodddiv4  16375  flodddiv4t2lthalf  16378  bits0  16388  bitsp1e  16392  bitsp1o  16393  gcdneg  16482  gcdaddmlem  16484  gcdaddm  16485  gcdadd  16486  gcdid  16487  modgcd  16492  gcdmultiplez  16495  bezoutlem1  16499  bezoutlem2  16500  bezoutlem4  16502  dvdsgcd  16504  mulgcd  16508  absmulgcd  16509  mulgcdr  16510  gcddiv  16511  dvdssqim  16514  dvdsexpim  16515  zexpgcd  16525  dvdssq  16527  bezoutr1  16529  lcmcllem  16556  lcmneg  16563  lcmgcdlem  16566  lcmgcd  16567  lcmid  16569  lcm1  16570  coprmdvds  16613  coprmdvds2  16614  qredeq  16617  qredeu  16618  divgcdcoprmex  16626  cncongr1  16627  cncongr2  16628  prmdvdsexp  16676  rpexp1i  16684  divnumden  16709  zsqrtelqelz  16719  phiprmpw  16737  vfermltlALT  16764  nnnn0modprm0  16768  modprmn0modprm0  16769  coprimeprodsq2  16771  iserodd  16797  pclem  16800  pcprendvds2  16803  pcpremul  16805  pcmul  16813  pcneg  16836  fldivp1  16859  prmpwdvds  16866  zgz  16895  modxai  17030  mod2xnegi  17033  chnccat  18583  chnrev  18584  mulgfval  19036  mulgz  19069  mulgassr  19079  mulgmodid  19080  odmod  19512  odf1  19528  odf1o1  19538  gexdvds  19550  zaddablx  19838  ablfacrp  20034  pgpfac1lem3  20045  ablsimpgfindlem1  20075  zsubrg  21395  zsssubrg  21400  zringsub  21430  zringmulg  21431  zringinvg  21440  zringunit  21441  zringcyg  21444  prmirred  21449  mulgrhm2  21453  pzriprnglem6  21461  pzriprnglem8  21463  pzriprnglem10  21465  pzriprnglem12  21467  fermltlchr  21504  znunit  21538  degltp1le  26056  ef2kpi  26460  efper  26461  sinperlem  26462  sin2kpi  26465  cos2kpi  26466  abssinper  26503  sinkpi  26504  coskpi  26505  eflogeq  26584  cxpexpz  26649  root1eq1  26737  cxpeq  26739  zrtelqelz  26740  zrtdvds  26741  relogbexp  26762  sgmval2  27124  ppiprm  27132  ppinprm  27133  chtprm  27134  chtnprm  27135  lgslem3  27280  lgsneg  27302  lgsdir2lem2  27307  lgsdir2lem4  27309  lgsdir2  27311  lgssq  27318  lgsmulsqcoprm  27324  lgsdirnn0  27325  gausslemma2dlem3  27349  lgsquadlem1  27361  lgsquadlem2  27362  lgsquad2  27367  2lgslem1a2  27371  2lgsoddprmlem1  27389  2lgsoddprmlem2  27390  2sqlem2  27399  2sqlem7  27405  rplogsumlem2  27466  axlowdimlem13  29041  wlk1walk  29725  clwwisshclwwslemlem  30101  ipasslem5  30924  rearchi  33429  znfermltl  33449  knoppndvlem9  36826  poimirlem19  38006  itg2addnclem2  38039  gcdaddmzz2nncomi  42480  zdivgd  42814  ef11d  42816  cxp112d  42818  cxp111d  42819  cxpi11d  42820  dffltz  43084  lzenom  43219  rexzrexnn0  43249  pell1234qrne0  43298  pell1234qrreccl  43299  pell1234qrmulcl  43300  pell1234qrdich  43306  pell14qrdich  43314  reglogexp  43339  reglogexpbas  43342  rmxm1  43379  rmym1  43380  rmxdbl  43384  rmydbl  43385  jm2.24  43408  congtr  43410  congadd  43411  congmul  43412  congsym  43413  congneg  43414  congid  43416  congabseq  43419  acongsym  43421  acongneg2  43422  acongtr  43423  acongrep  43425  jm2.19lem3  43436  jm2.19lem4  43437  jm2.19  43438  jm2.25  43444  jm2.26a  43445  oddfl  45726  coskpi2  46309  cosknegpi  46312  dvdsn1add  46382  itgsinexp  46398  fourierdlem42  46592  fourierdlem97  46646  fourierswlem  46673  sinnpoly  47354  2elfz2melfz  47781  ceilbi  47800  flmrecm1  47806  submodaddmod  47810  submodneaddmod  47820  mod0mul  47825  m1modmmod  47827  modmkpkne  47830  modlt0b  47832  sfprmdvdsmersenne  48081  proththd  48092  ppivalnnprm  48103  ppivalnnnprmge6  48104  dfodd6  48128  dfeven4  48129  evenm1odd  48130  evenp1odd  48131  enege  48136  onego  48137  dfeven2  48140  bits0ALTV  48170  opoeALTV  48174  opeoALTV  48175  evensumeven  48198  fppr2odd  48222  sbgoldbwt  48268  nnsum3primesgbe  48283  gpgedgvtx0  48552  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx13starlem2  48563  0nodd  48661  2nodd  48663  1neven  48729  2zlidl  48731  2zrngamgm  48736  2zrngasgrp  48737  2zrngagrp  48740  2zrngmmgm  48743  2zrngmsgrp  48744  2zrngnmrid  48747  zlmodzxzsub  48851  flsubz  49013  zofldiv2  49022  dignn0flhalflem1  49106  dignn0flhalflem2  49107