Theorem zcn 12505

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  ℤcz 12500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-neg 11379  df-z 12501

This theorem is referenced by:  zsscn  12508  zsubcl  12545  zrevaddcl  12548  nzadd  12551  zlem1lt  12555  zltlem1  12556  zdiv  12574  zdivadd  12575  zdivmul  12576  zextlt  12578  zneo  12587  zeo2  12591  peano5uzi  12593  zindd  12605  znnn0nn  12615  zriotaneg  12617  zmax  12870  rebtwnz  12872  qmulz  12876  zq  12879  qaddcl  12890  qnegcl  12891  qmulcl  12892  qreccl  12894  fzen  13469  uzsubsubfz  13474  fz01en  13480  fzmmmeqm  13485  fzsubel  13488  fztp  13508  fzsuc2  13510  fzrev2  13516  fzrev3  13518  elfzp1b  13529  fzrevral  13540  fzrevral2  13541  fzrevral3  13542  fzshftral  13543  fzo0addel  13646  fzo0addelr  13647  fzoaddel2  13648  fzosubel2  13653  eluzgtdifelfzo  13655  fzocatel  13657  elfzom1elp1fzo  13660  fzval3  13662  zpnn0elfzo1  13667  fzosplitprm1  13706  fzoshftral  13715  flzadd  13758  2tnp1ge0ge0  13761  ceilid  13783  quoremz  13787  intfracq  13791  mulmod0  13809  zmod10  13819  modcyc  13838  modcyc2  13839  muladdmodid  13845  mulp1mod1  13846  modmuladdnn0  13850  modmul1  13859  modmulmodr  13872  modaddmulmod  13873  uzrdgxfr  13902  fzen2  13904  seqshft2  13963  sermono  13969  m1expeven  14044  expsub  14045  zesq  14161  modexp  14173  sqoddm1div8  14178  bccmpl  14244  swrd00  14580  swrdswrd  14640  swrdpfx  14642  pfxccatin12lem4  14661  pfxccatin12lem1  14663  swrdccatin2  14664  pfxccatin12lem2  14666  pfxccatin12  14668  repswrevw  14722  cshwsublen  14731  cshwidxmodr  14739  cshwidx0mod  14740  2cshw  14748  2cshwid  14749  2cshwcom  14751  cshweqdif2  14754  cshweqrep  14756  cshw1  14757  2cshwcshw  14760  shftuz  15004  seqshft  15020  nn0abscl  15247  zabs0b  15249  nnabscl  15261  climshftlem  15509  climshft  15511  isershft  15599  mptfzshft  15713  fsumrev  15714  fsum0diag2  15718  efexp  16038  efzval  16039  demoivre  16137  sqrt2irr  16186  dvdsval2  16194  iddvds  16208  1dvds  16209  dvds0  16210  negdvdsb  16211  dvdsnegb  16212  0dvds  16215  dvdsmul1  16216  iddvdsexp  16218  muldvds1  16219  muldvds2  16220  dvdscmul  16221  dvdsmulc  16222  dvdscmulr  16223  dvdsmulcr  16224  summodnegmod  16225  difmod0  16226  modmulconst  16227  dvds2ln  16228  dvds2add  16229  dvds2sub  16230  dvdstr  16233  dvdssub2  16240  dvdsadd  16241  dvdsaddr  16242  dvdssub  16243  dvdssubr  16244  dvdsadd2b  16245  dvdsaddre2b  16246  dvdsabseq  16252  divconjdvds  16254  alzdvds  16259  addmodlteqALT  16264  dvdsexp2im  16266  odd2np1lem  16279  odd2np1  16280  even2n  16281  oddp1even  16283  mod2eq1n2dvds  16286  mulsucdiv2z  16292  zob  16298  ltoddhalfle  16300  halfleoddlt  16301  opoe  16302  omoe  16303  opeo  16304  omeo  16305  m1exp1  16315  divalglem0  16332  divalglem2  16334  divalglem4  16335  divalglem5  16336  divalglem9  16340  divalgb  16343  divalgmod  16345  modremain  16347  ndvdssub  16348  ndvdsadd  16349  flodddiv4  16354  flodddiv4t2lthalf  16357  bits0  16367  bitsp1e  16371  bitsp1o  16372  gcdneg  16461  gcdaddmlem  16463  gcdaddm  16464  gcdadd  16465  gcdid  16466  modgcd  16471  gcdmultiplez  16474  bezoutlem1  16478  bezoutlem2  16479  bezoutlem4  16481  dvdsgcd  16483  mulgcd  16487  absmulgcd  16488  mulgcdr  16489  gcddiv  16490  dvdssqim  16493  dvdsexpim  16494  zexpgcd  16504  dvdssq  16506  bezoutr1  16508  lcmcllem  16535  lcmneg  16542  lcmgcdlem  16545  lcmgcd  16546  lcmid  16548  lcm1  16549  coprmdvds  16592  coprmdvds2  16593  qredeq  16596  qredeu  16597  divgcdcoprmex  16605  cncongr1  16606  cncongr2  16607  prmdvdsexp  16654  rpexp1i  16662  divnumden  16687  zsqrtelqelz  16697  phiprmpw  16715  vfermltlALT  16742  nnnn0modprm0  16746  modprmn0modprm0  16747  coprimeprodsq2  16749  iserodd  16775  pclem  16778  pcprendvds2  16781  pcpremul  16783  pcmul  16791  pcneg  16814  fldivp1  16837  prmpwdvds  16844  zgz  16873  modxai  17008  mod2xnegi  17011  chnccat  18561  chnrev  18562  mulgfval  19011  mulgz  19044  mulgassr  19054  mulgmodid  19055  odmod  19487  odf1  19503  odf1o1  19513  gexdvds  19525  zaddablx  19813  ablfacrp  20009  pgpfac1lem3  20020  ablsimpgfindlem1  20050  zsubrg  21387  zsssubrg  21392  zringsub  21422  zringmulg  21423  zringinvg  21432  zringunit  21433  zringcyg  21436  prmirred  21441  mulgrhm2  21445  pzriprnglem6  21453  pzriprnglem8  21455  pzriprnglem10  21457  pzriprnglem12  21459  fermltlchr  21496  znunit  21530  degltp1le  26046  ef2kpi  26455  efper  26456  sinperlem  26457  sin2kpi  26460  cos2kpi  26461  abssinper  26498  sinkpi  26499  coskpi  26500  eflogeq  26579  cxpexpz  26644  root1eq1  26733  cxpeq  26735  zrtelqelz  26736  zrtdvds  26737  relogbexp  26758  sgmval2  27121  ppiprm  27129  ppinprm  27130  chtprm  27131  chtnprm  27132  lgslem3  27278  lgsneg  27300  lgsdir2lem2  27305  lgsdir2lem4  27307  lgsdir2  27309  lgssq  27316  lgsmulsqcoprm  27322  lgsdirnn0  27323  gausslemma2dlem3  27347  lgsquadlem1  27359  lgsquadlem2  27360  lgsquad2  27365  2lgslem1a2  27369  2lgsoddprmlem1  27387  2lgsoddprmlem2  27388  2sqlem2  27397  2sqlem7  27403  rplogsumlem2  27464  axlowdimlem13  29039  wlk1walk  29724  clwwisshclwwslemlem  30100  ipasslem5  30923  rearchi  33439  znfermltl  33459  knoppndvlem9  36742  poimirlem19  37890  itg2addnclem2  37923  gcdaddmzz2nncomi  42365  zdivgd  42707  ef11d  42709  cxp112d  42711  cxp111d  42712  cxpi11d  42713  dffltz  42992  lzenom  43127  rexzrexnn0  43161  pell1234qrne0  43210  pell1234qrreccl  43211  pell1234qrmulcl  43212  pell1234qrdich  43218  pell14qrdich  43226  reglogexp  43251  reglogexpbas  43254  rmxm1  43291  rmym1  43292  rmxdbl  43296  rmydbl  43297  jm2.24  43320  congtr  43322  congadd  43323  congmul  43324  congsym  43325  congneg  43326  congid  43328  congabseq  43331  acongsym  43333  acongneg2  43334  acongtr  43335  acongrep  43337  jm2.19lem3  43348  jm2.19lem4  43349  jm2.19  43350  jm2.25  43356  jm2.26a  43357  oddfl  45640  coskpi2  46224  cosknegpi  46227  dvdsn1add  46297  itgsinexp  46313  fourierdlem42  46507  fourierdlem97  46561  fourierswlem  46588  sinnpoly  47251  2elfz2melfz  47678  ceilbi  47693  submodaddmod  47701  submodneaddmod  47711  mod0mul  47716  m1modmmod  47718  modmkpkne  47721  modlt0b  47723  sfprmdvdsmersenne  47963  proththd  47974  dfodd6  47997  dfeven4  47998  evenm1odd  47999  evenp1odd  48000  enege  48005  onego  48006  dfeven2  48009  bits0ALTV  48039  opoeALTV  48043  opeoALTV  48044  evensumeven  48067  fppr2odd  48091  sbgoldbwt  48137  nnsum3primesgbe  48152  gpgedgvtx0  48421  gpg5nbgrvtx03starlem2  48429  gpg5nbgrvtx13starlem2  48432  0nodd  48530  2nodd  48532  1neven  48598  2zlidl  48600  2zrngamgm  48605  2zrngasgrp  48606  2zrngagrp  48609  2zrngmmgm  48612  2zrngmsgrp  48613  2zrngnmrid  48616  zlmodzxzsub  48720  flsubz  48882  zofldiv2  48891  dignn0flhalflem1  48975  dignn0flhalflem2  48976