Theorem zcn 12493

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11024  ℤcz 12488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-resscn 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-neg 11367  df-z 12489

This theorem is referenced by:  zsscn  12496  zsubcl  12533  zrevaddcl  12536  nzadd  12539  zlem1lt  12543  zltlem1  12544  zdiv  12562  zdivadd  12563  zdivmul  12564  zextlt  12566  zneo  12575  zeo2  12579  peano5uzi  12581  zindd  12593  znnn0nn  12603  zriotaneg  12605  zmax  12858  rebtwnz  12860  qmulz  12864  zq  12867  qaddcl  12878  qnegcl  12879  qmulcl  12880  qreccl  12882  fzen  13457  uzsubsubfz  13462  fz01en  13468  fzmmmeqm  13473  fzsubel  13476  fztp  13496  fzsuc2  13498  fzrev2  13504  fzrev3  13506  elfzp1b  13517  fzrevral  13528  fzrevral2  13529  fzrevral3  13530  fzshftral  13531  fzo0addel  13634  fzo0addelr  13635  fzoaddel2  13636  fzosubel2  13641  eluzgtdifelfzo  13643  fzocatel  13645  elfzom1elp1fzo  13648  fzval3  13650  zpnn0elfzo1  13655  fzosplitprm1  13694  fzoshftral  13703  flzadd  13746  2tnp1ge0ge0  13749  ceilid  13771  quoremz  13775  intfracq  13779  mulmod0  13797  zmod10  13807  modcyc  13826  modcyc2  13827  muladdmodid  13833  mulp1mod1  13834  modmuladdnn0  13838  modmul1  13847  modmulmodr  13860  modaddmulmod  13861  uzrdgxfr  13890  fzen2  13892  seqshft2  13951  sermono  13957  m1expeven  14032  expsub  14033  zesq  14149  modexp  14161  sqoddm1div8  14166  bccmpl  14232  swrd00  14568  swrdswrd  14628  swrdpfx  14630  pfxccatin12lem4  14649  pfxccatin12lem1  14651  swrdccatin2  14652  pfxccatin12lem2  14654  pfxccatin12  14656  repswrevw  14710  cshwsublen  14719  cshwidxmodr  14727  cshwidx0mod  14728  2cshw  14736  2cshwid  14737  2cshwcom  14739  cshweqdif2  14742  cshweqrep  14744  cshw1  14745  2cshwcshw  14748  shftuz  14992  seqshft  15008  nn0abscl  15235  zabs0b  15237  nnabscl  15249  climshftlem  15497  climshft  15499  isershft  15587  mptfzshft  15701  fsumrev  15702  fsum0diag2  15706  efexp  16026  efzval  16027  demoivre  16125  sqrt2irr  16174  dvdsval2  16182  iddvds  16196  1dvds  16197  dvds0  16198  negdvdsb  16199  dvdsnegb  16200  0dvds  16203  dvdsmul1  16204  iddvdsexp  16206  muldvds1  16207  muldvds2  16208  dvdscmul  16209  dvdsmulc  16210  dvdscmulr  16211  dvdsmulcr  16212  summodnegmod  16213  difmod0  16214  modmulconst  16215  dvds2ln  16216  dvds2add  16217  dvds2sub  16218  dvdstr  16221  dvdssub2  16228  dvdsadd  16229  dvdsaddr  16230  dvdssub  16231  dvdssubr  16232  dvdsadd2b  16233  dvdsaddre2b  16234  dvdsabseq  16240  divconjdvds  16242  alzdvds  16247  addmodlteqALT  16252  dvdsexp2im  16254  odd2np1lem  16267  odd2np1  16268  even2n  16269  oddp1even  16271  mod2eq1n2dvds  16274  mulsucdiv2z  16280  zob  16286  ltoddhalfle  16288  halfleoddlt  16289  opoe  16290  omoe  16291  opeo  16292  omeo  16293  m1exp1  16303  divalglem0  16320  divalglem2  16322  divalglem4  16323  divalglem5  16324  divalglem9  16328  divalgb  16331  divalgmod  16333  modremain  16335  ndvdssub  16336  ndvdsadd  16337  flodddiv4  16342  flodddiv4t2lthalf  16345  bits0  16355  bitsp1e  16359  bitsp1o  16360  gcdneg  16449  gcdaddmlem  16451  gcdaddm  16452  gcdadd  16453  gcdid  16454  modgcd  16459  gcdmultiplez  16462  bezoutlem1  16466  bezoutlem2  16467  bezoutlem4  16469  dvdsgcd  16471  mulgcd  16475  absmulgcd  16476  mulgcdr  16477  gcddiv  16478  dvdssqim  16481  dvdsexpim  16482  zexpgcd  16492  dvdssq  16494  bezoutr1  16496  lcmcllem  16523  lcmneg  16530  lcmgcdlem  16533  lcmgcd  16534  lcmid  16536  lcm1  16537  coprmdvds  16580  coprmdvds2  16581  qredeq  16584  qredeu  16585  divgcdcoprmex  16593  cncongr1  16594  cncongr2  16595  prmdvdsexp  16642  rpexp1i  16650  divnumden  16675  zsqrtelqelz  16685  phiprmpw  16703  vfermltlALT  16730  nnnn0modprm0  16734  modprmn0modprm0  16735  coprimeprodsq2  16737  iserodd  16763  pclem  16766  pcprendvds2  16769  pcpremul  16771  pcmul  16779  pcneg  16802  fldivp1  16825  prmpwdvds  16832  zgz  16861  modxai  16996  mod2xnegi  16999  chnccat  18549  chnrev  18550  mulgfval  18999  mulgz  19032  mulgassr  19042  mulgmodid  19043  odmod  19475  odf1  19491  odf1o1  19501  gexdvds  19513  zaddablx  19801  ablfacrp  19997  pgpfac1lem3  20008  ablsimpgfindlem1  20038  zsubrg  21375  zsssubrg  21380  zringsub  21410  zringmulg  21411  zringinvg  21420  zringunit  21421  zringcyg  21424  prmirred  21429  mulgrhm2  21433  pzriprnglem6  21441  pzriprnglem8  21443  pzriprnglem10  21445  pzriprnglem12  21447  fermltlchr  21484  znunit  21518  degltp1le  26034  ef2kpi  26443  efper  26444  sinperlem  26445  sin2kpi  26448  cos2kpi  26449  abssinper  26486  sinkpi  26487  coskpi  26488  eflogeq  26567  cxpexpz  26632  root1eq1  26721  cxpeq  26723  zrtelqelz  26724  zrtdvds  26725  relogbexp  26746  sgmval2  27109  ppiprm  27117  ppinprm  27118  chtprm  27119  chtnprm  27120  lgslem3  27266  lgsneg  27288  lgsdir2lem2  27293  lgsdir2lem4  27295  lgsdir2  27297  lgssq  27304  lgsmulsqcoprm  27310  lgsdirnn0  27311  gausslemma2dlem3  27335  lgsquadlem1  27347  lgsquadlem2  27348  lgsquad2  27353  2lgslem1a2  27357  2lgsoddprmlem1  27375  2lgsoddprmlem2  27376  2sqlem2  27385  2sqlem7  27391  rplogsumlem2  27452  axlowdimlem13  29027  wlk1walk  29712  clwwisshclwwslemlem  30088  ipasslem5  30910  rearchi  33427  znfermltl  33447  knoppndvlem9  36720  poimirlem19  37840  itg2addnclem2  37873  gcdaddmzz2nncomi  42259  zdivgd  42602  ef11d  42604  cxp112d  42606  cxp111d  42607  cxpi11d  42608  dffltz  42887  lzenom  43022  rexzrexnn0  43056  pell1234qrne0  43105  pell1234qrreccl  43106  pell1234qrmulcl  43107  pell1234qrdich  43113  pell14qrdich  43121  reglogexp  43146  reglogexpbas  43149  rmxm1  43186  rmym1  43187  rmxdbl  43191  rmydbl  43192  jm2.24  43215  congtr  43217  congadd  43218  congmul  43219  congsym  43220  congneg  43221  congid  43223  congabseq  43226  acongsym  43228  acongneg2  43229  acongtr  43230  acongrep  43232  jm2.19lem3  43243  jm2.19lem4  43244  jm2.19  43245  jm2.25  43251  jm2.26a  43252  oddfl  45536  coskpi2  46120  cosknegpi  46123  dvdsn1add  46193  itgsinexp  46209  fourierdlem42  46403  fourierdlem97  46457  fourierswlem  46484  sinnpoly  47147  2elfz2melfz  47574  ceilbi  47589  submodaddmod  47597  submodneaddmod  47607  mod0mul  47612  m1modmmod  47614  modmkpkne  47617  modlt0b  47619  sfprmdvdsmersenne  47859  proththd  47870  dfodd6  47893  dfeven4  47894  evenm1odd  47895  evenp1odd  47896  enege  47901  onego  47902  dfeven2  47905  bits0ALTV  47935  opoeALTV  47939  opeoALTV  47940  evensumeven  47963  fppr2odd  47987  sbgoldbwt  48033  nnsum3primesgbe  48048  gpgedgvtx0  48317  gpg5nbgrvtx03starlem2  48325  gpg5nbgrvtx13starlem2  48328  0nodd  48426  2nodd  48428  1neven  48494  2zlidl  48496  2zrngamgm  48501  2zrngasgrp  48502  2zrngagrp  48505  2zrngmmgm  48508  2zrngmsgrp  48509  2zrngnmrid  48512  zlmodzxzsub  48616  flsubz  48778  zofldiv2  48787  dignn0flhalflem1  48871  dignn0flhalflem2  48872