Theorem zcn 12563

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11108  ℤcz 12558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-resscn 11167

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-neg 11447  df-z 12559

This theorem is referenced by:  zsscn  12566  zsubcl  12604  zrevaddcl  12607  nzadd  12610  zlem1lt  12614  zltlem1  12615  zdiv  12632  zdivadd  12633  zdivmul  12634  zextlt  12636  zneo  12645  zeo2  12649  peano5uzi  12651  zindd  12663  znnn0nn  12673  zriotaneg  12675  zmax  12929  rebtwnz  12931  qmulz  12935  zq  12938  qaddcl  12949  qnegcl  12950  qmulcl  12951  qreccl  12953  fzen  13518  uzsubsubfz  13523  fz01en  13529  fzmmmeqm  13534  fzsubel  13537  fztp  13557  fzsuc2  13559  fzrev2  13565  fzrev3  13567  elfzp1b  13578  fzrevral  13586  fzrevral2  13587  fzrevral3  13588  fzshftral  13589  fzo0addel  13686  fzo0addelr  13687  fzoaddel2  13688  elfzoext  13689  fzosubel2  13692  eluzgtdifelfzo  13694  fzocatel  13696  elfzom1elp1fzo  13699  fzval3  13701  zpnn0elfzo1  13706  fzosplitprm1  13742  fzoshftral  13749  flzadd  13791  2tnp1ge0ge0  13794  ceilid  13816  quoremz  13820  intfracq  13824  mulmod0  13842  zmod10  13852  modcyc  13871  modcyc2  13872  muladdmodid  13876  mulp1mod1  13877  modmuladdnn0  13880  modmul1  13889  modmulmodr  13902  modaddmulmod  13903  uzrdgxfr  13932  fzen2  13934  seqshft2  13994  sermono  14000  m1expeven  14075  expsub  14076  zesq  14189  modexp  14201  sqoddm1div8  14206  bccmpl  14269  swrd00  14594  addlenrevpfx  14640  swrdswrd  14655  swrdpfx  14657  pfxccatin12lem4  14676  pfxccatin12lem1  14678  swrdccatin2  14679  pfxccatin12lem2  14681  pfxccatin12  14683  repswrevw  14737  cshwsublen  14746  cshwidxmodr  14754  cshwidx0mod  14755  2cshw  14763  2cshwid  14764  2cshwcom  14766  cshweqdif2  14769  cshweqrep  14771  cshw1  14772  2cshwcshw  14776  shftuz  15016  seqshft  15032  nn0abscl  15259  nnabscl  15272  climshftlem  15518  climshft  15520  isershft  15610  mptfzshft  15724  fsumrev  15725  fsum0diag2  15729  efexp  16044  efzval  16045  demoivre  16143  sqrt2irr  16192  dvdsval2  16200  iddvds  16213  1dvds  16214  dvds0  16215  negdvdsb  16216  dvdsnegb  16217  0dvds  16220  dvdsmul1  16221  iddvdsexp  16223  muldvds1  16224  muldvds2  16225  dvdscmul  16226  dvdsmulc  16227  dvdscmulr  16228  dvdsmulcr  16229  summodnegmod  16230  modmulconst  16231  dvds2ln  16232  dvds2add  16233  dvds2sub  16234  dvdstr  16237  dvdssub2  16244  dvdsadd  16245  dvdsaddr  16246  dvdssub  16247  dvdssubr  16248  dvdsadd2b  16249  dvdsaddre2b  16250  dvdsabseq  16256  divconjdvds  16258  alzdvds  16263  addmodlteqALT  16268  dvdsexp2im  16270  odd2np1lem  16283  odd2np1  16284  even2n  16285  oddp1even  16287  mod2eq1n2dvds  16290  mulsucdiv2z  16296  zob  16302  ltoddhalfle  16304  halfleoddlt  16305  opoe  16306  omoe  16307  opeo  16308  omeo  16309  m1exp1  16319  divalglem0  16336  divalglem2  16338  divalglem4  16339  divalglem5  16340  divalglem9  16344  divalgb  16347  divalgmod  16349  modremain  16351  ndvdssub  16352  ndvdsadd  16353  flodddiv4  16356  flodddiv4t2lthalf  16359  bits0  16369  bitsp1e  16373  bitsp1o  16374  gcdneg  16463  gcdaddmlem  16465  gcdaddm  16466  gcdadd  16467  gcdid  16468  modgcd  16474  gcdmultiplez  16477  bezoutlem1  16481  bezoutlem2  16482  bezoutlem4  16484  dvdsgcd  16486  mulgcd  16490  absmulgcd  16491  mulgcdr  16492  gcddiv  16493  dvdssqim  16496  dvdssq  16504  bezoutr1  16506  lcmcllem  16533  lcmneg  16540  lcmgcdlem  16543  lcmgcd  16544  lcmid  16546  lcm1  16547  coprmdvds  16590  coprmdvds2  16591  qredeq  16594  qredeu  16595  divgcdcoprmex  16603  cncongr1  16604  cncongr2  16605  prmdvdsexp  16652  prmdvdssqOLD  16656  rpexp1i  16660  divnumden  16684  zsqrtelqelz  16694  phiprmpw  16709  vfermltlALT  16735  nnnn0modprm0  16739  modprmn0modprm0  16740  coprimeprodsq2  16742  iserodd  16768  pclem  16771  pcprendvds2  16774  pcpremul  16776  pcmul  16784  pcneg  16807  fldivp1  16830  prmpwdvds  16837  zgz  16866  modxai  17001  mod2xnegi  17004  mulgfval  18952  mulgz  18982  mulgassr  18992  mulgmodid  18993  odmod  19414  odf1  19430  odf1o1  19440  gexdvds  19452  zaddablx  19740  ablfacrp  19936  pgpfac1lem3  19947  ablsimpgfindlem1  19977  zsubrg  20998  zsssubrg  21003  zringsub  21025  zringmulg  21026  zringinvg  21035  zringunit  21036  zringcyg  21039  prmirred  21044  mulgrhm2  21048  znunit  21119  degltp1le  25591  ef2kpi  25988  efper  25989  sinperlem  25990  sin2kpi  25993  cos2kpi  25994  abssinper  26030  sinkpi  26031  coskpi  26032  eflogeq  26110  cxpexpz  26175  root1eq1  26263  cxpeq  26265  relogbexp  26285  sgmval2  26647  ppiprm  26655  ppinprm  26656  chtprm  26657  chtnprm  26658  lgslem3  26802  lgsneg  26824  lgsdir2lem2  26829  lgsdir2lem4  26831  lgsdir2  26833  lgssq  26840  lgsmulsqcoprm  26846  lgsdirnn0  26847  gausslemma2dlem3  26871  lgsquadlem1  26883  lgsquadlem2  26884  lgsquad2  26889  2lgslem1a2  26893  2lgsoddprmlem1  26911  2lgsoddprmlem2  26912  2sqlem2  26921  2sqlem7  26927  rplogsumlem2  26988  axlowdimlem13  28212  wlk1walk  28896  clwwisshclwwslemlem  29266  ipasslem5  30088  rearchi  32461  fermltlchr  32478  znfermltl  32479  knoppndvlem9  35396  poimirlem19  36507  itg2addnclem2  36540  gcdaddmzz2nncomi  40861  metakunt16  41000  dvdsexpim  41219  zexpgcd  41227  zrtelqelz  41235  zrtdvds  41236  dffltz  41376  lzenom  41508  rexzrexnn0  41542  pell1234qrne0  41591  pell1234qrreccl  41592  pell1234qrmulcl  41593  pell1234qrdich  41599  pell14qrdich  41607  reglogexp  41632  reglogexpbas  41635  rmxm1  41673  rmym1  41674  rmxdbl  41678  rmydbl  41679  jm2.24  41702  congtr  41704  congadd  41705  congmul  41706  congsym  41707  congneg  41708  congid  41710  congabseq  41713  acongsym  41715  acongneg2  41716  acongtr  41717  acongrep  41719  jm2.19lem3  41730  jm2.19lem4  41731  jm2.19  41732  jm2.25  41738  jm2.26a  41739  oddfl  43987  coskpi2  44582  cosknegpi  44585  dvdsn1add  44655  itgsinexp  44671  fourierdlem42  44865  fourierdlem97  44919  fourierswlem  44946  2elfz2melfz  46026  sfprmdvdsmersenne  46271  proththd  46282  dfodd6  46305  dfeven4  46306  evenm1odd  46307  evenp1odd  46308  enege  46313  onego  46314  dfeven2  46317  bits0ALTV  46347  opoeALTV  46351  opeoALTV  46352  evensumeven  46375  fppr2odd  46399  sbgoldbwt  46445  nnsum3primesgbe  46460  0nodd  46580  2nodd  46582  pzriprnglem6  46810  pzriprnglem8  46812  pzriprnglem10  46814  pzriprnglem12  46816  1neven  46830  2zlidl  46832  2zrngamgm  46837  2zrngasgrp  46838  2zrngagrp  46841  2zrngmmgm  46844  2zrngmsgrp  46845  2zrngnmrid  46848  zlmodzxzsub  47036  flsubz  47203  mod0mul  47205  m1modmmod  47207  zofldiv2  47217  dignn0flhalflem1  47301  dignn0flhalflem2  47302