Theorem zcn 12483

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11014  ℤcz 12478

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 2705  ax-resscn 11073

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 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-neg 11357  df-z 12479

This theorem is referenced by:  zsscn  12486  zsubcl  12524  zrevaddcl  12527  nzadd  12530  zlem1lt  12534  zltlem1  12535  zdiv  12553  zdivadd  12554  zdivmul  12555  zextlt  12557  zneo  12566  zeo2  12570  peano5uzi  12572  zindd  12584  znnn0nn  12594  zriotaneg  12596  zmax  12853  rebtwnz  12855  qmulz  12859  zq  12862  qaddcl  12873  qnegcl  12874  qmulcl  12875  qreccl  12877  fzen  13451  uzsubsubfz  13456  fz01en  13462  fzmmmeqm  13467  fzsubel  13470  fztp  13490  fzsuc2  13492  fzrev2  13498  fzrev3  13500  elfzp1b  13511  fzrevral  13522  fzrevral2  13523  fzrevral3  13524  fzshftral  13525  fzo0addel  13628  fzo0addelr  13629  fzoaddel2  13630  fzosubel2  13635  eluzgtdifelfzo  13637  fzocatel  13639  elfzom1elp1fzo  13642  fzval3  13644  zpnn0elfzo1  13649  fzosplitprm1  13688  fzoshftral  13697  flzadd  13740  2tnp1ge0ge0  13743  ceilid  13765  quoremz  13769  intfracq  13773  mulmod0  13791  zmod10  13801  modcyc  13820  modcyc2  13821  muladdmodid  13827  mulp1mod1  13828  modmuladdnn0  13832  modmul1  13841  modmulmodr  13854  modaddmulmod  13855  uzrdgxfr  13884  fzen2  13886  seqshft2  13945  sermono  13951  m1expeven  14026  expsub  14027  zesq  14143  modexp  14155  sqoddm1div8  14160  bccmpl  14226  swrd00  14562  swrdswrd  14622  swrdpfx  14624  pfxccatin12lem4  14643  pfxccatin12lem1  14645  swrdccatin2  14646  pfxccatin12lem2  14648  pfxccatin12  14650  repswrevw  14704  cshwsublen  14713  cshwidxmodr  14721  cshwidx0mod  14722  2cshw  14730  2cshwid  14731  2cshwcom  14733  cshweqdif2  14736  cshweqrep  14738  cshw1  14739  2cshwcshw  14742  shftuz  14986  seqshft  15002  nn0abscl  15229  zabs0b  15231  nnabscl  15243  climshftlem  15491  climshft  15493  isershft  15581  mptfzshft  15695  fsumrev  15696  fsum0diag2  15700  efexp  16020  efzval  16021  demoivre  16119  sqrt2irr  16168  dvdsval2  16176  iddvds  16190  1dvds  16191  dvds0  16192  negdvdsb  16193  dvdsnegb  16194  0dvds  16197  dvdsmul1  16198  iddvdsexp  16200  muldvds1  16201  muldvds2  16202  dvdscmul  16203  dvdsmulc  16204  dvdscmulr  16205  dvdsmulcr  16206  summodnegmod  16207  difmod0  16208  modmulconst  16209  dvds2ln  16210  dvds2add  16211  dvds2sub  16212  dvdstr  16215  dvdssub2  16222  dvdsadd  16223  dvdsaddr  16224  dvdssub  16225  dvdssubr  16226  dvdsadd2b  16227  dvdsaddre2b  16228  dvdsabseq  16234  divconjdvds  16236  alzdvds  16241  addmodlteqALT  16246  dvdsexp2im  16248  odd2np1lem  16261  odd2np1  16262  even2n  16263  oddp1even  16265  mod2eq1n2dvds  16268  mulsucdiv2z  16274  zob  16280  ltoddhalfle  16282  halfleoddlt  16283  opoe  16284  omoe  16285  opeo  16286  omeo  16287  m1exp1  16297  divalglem0  16314  divalglem2  16316  divalglem4  16317  divalglem5  16318  divalglem9  16322  divalgb  16325  divalgmod  16327  modremain  16329  ndvdssub  16330  ndvdsadd  16331  flodddiv4  16336  flodddiv4t2lthalf  16339  bits0  16349  bitsp1e  16353  bitsp1o  16354  gcdneg  16443  gcdaddmlem  16445  gcdaddm  16446  gcdadd  16447  gcdid  16448  modgcd  16453  gcdmultiplez  16456  bezoutlem1  16460  bezoutlem2  16461  bezoutlem4  16463  dvdsgcd  16465  mulgcd  16469  absmulgcd  16470  mulgcdr  16471  gcddiv  16472  dvdssqim  16475  dvdsexpim  16476  zexpgcd  16486  dvdssq  16488  bezoutr1  16490  lcmcllem  16517  lcmneg  16524  lcmgcdlem  16527  lcmgcd  16528  lcmid  16530  lcm1  16531  coprmdvds  16574  coprmdvds2  16575  qredeq  16578  qredeu  16579  divgcdcoprmex  16587  cncongr1  16588  cncongr2  16589  prmdvdsexp  16636  rpexp1i  16644  divnumden  16669  zsqrtelqelz  16679  phiprmpw  16697  vfermltlALT  16724  nnnn0modprm0  16728  modprmn0modprm0  16729  coprimeprodsq2  16731  iserodd  16757  pclem  16760  pcprendvds2  16763  pcpremul  16765  pcmul  16773  pcneg  16796  fldivp1  16819  prmpwdvds  16826  zgz  16855  modxai  16990  mod2xnegi  16993  chnccat  18542  chnrev  18543  mulgfval  18992  mulgz  19025  mulgassr  19035  mulgmodid  19036  odmod  19468  odf1  19484  odf1o1  19494  gexdvds  19506  zaddablx  19794  ablfacrp  19990  pgpfac1lem3  20001  ablsimpgfindlem1  20031  zsubrg  21367  zsssubrg  21372  zringsub  21402  zringmulg  21403  zringinvg  21412  zringunit  21413  zringcyg  21416  prmirred  21421  mulgrhm2  21425  pzriprnglem6  21433  pzriprnglem8  21435  pzriprnglem10  21437  pzriprnglem12  21439  fermltlchr  21476  znunit  21510  degltp1le  26015  ef2kpi  26424  efper  26425  sinperlem  26426  sin2kpi  26429  cos2kpi  26430  abssinper  26467  sinkpi  26468  coskpi  26469  eflogeq  26548  cxpexpz  26613  root1eq1  26702  cxpeq  26704  zrtelqelz  26705  zrtdvds  26706  relogbexp  26727  sgmval2  27090  ppiprm  27098  ppinprm  27099  chtprm  27100  chtnprm  27101  lgslem3  27247  lgsneg  27269  lgsdir2lem2  27274  lgsdir2lem4  27276  lgsdir2  27278  lgssq  27285  lgsmulsqcoprm  27291  lgsdirnn0  27292  gausslemma2dlem3  27316  lgsquadlem1  27328  lgsquadlem2  27329  lgsquad2  27334  2lgslem1a2  27338  2lgsoddprmlem1  27356  2lgsoddprmlem2  27357  2sqlem2  27366  2sqlem7  27372  rplogsumlem2  27433  axlowdimlem13  28943  wlk1walk  29628  clwwisshclwwslemlem  30004  ipasslem5  30826  rearchi  33322  znfermltl  33342  knoppndvlem9  36575  poimirlem19  37689  itg2addnclem2  37722  gcdaddmzz2nncomi  42098  zdivgd  42445  ef11d  42447  cxp112d  42449  cxp111d  42450  cxpi11d  42451  dffltz  42742  lzenom  42877  rexzrexnn0  42911  pell1234qrne0  42960  pell1234qrreccl  42961  pell1234qrmulcl  42962  pell1234qrdich  42968  pell14qrdich  42976  reglogexp  43001  reglogexpbas  43004  rmxm1  43041  rmym1  43042  rmxdbl  43046  rmydbl  43047  jm2.24  43070  congtr  43072  congadd  43073  congmul  43074  congsym  43075  congneg  43076  congid  43078  congabseq  43081  acongsym  43083  acongneg2  43084  acongtr  43085  acongrep  43087  jm2.19lem3  43098  jm2.19lem4  43099  jm2.19  43100  jm2.25  43106  jm2.26a  43107  oddfl  45393  coskpi2  45978  cosknegpi  45981  dvdsn1add  46051  itgsinexp  46067  fourierdlem42  46261  fourierdlem97  46315  fourierswlem  46342  sinnpoly  47005  2elfz2melfz  47432  ceilbi  47447  submodaddmod  47455  submodneaddmod  47465  mod0mul  47470  m1modmmod  47472  modmkpkne  47475  modlt0b  47477  sfprmdvdsmersenne  47717  proththd  47728  dfodd6  47751  dfeven4  47752  evenm1odd  47753  evenp1odd  47754  enege  47759  onego  47760  dfeven2  47763  bits0ALTV  47793  opoeALTV  47797  opeoALTV  47798  evensumeven  47821  fppr2odd  47845  sbgoldbwt  47891  nnsum3primesgbe  47906  gpgedgvtx0  48175  gpg5nbgrvtx03starlem2  48183  gpg5nbgrvtx13starlem2  48186  0nodd  48284  2nodd  48286  1neven  48352  2zlidl  48354  2zrngamgm  48359  2zrngasgrp  48360  2zrngagrp  48363  2zrngmmgm  48366  2zrngmsgrp  48367  2zrngnmrid  48370  zlmodzxzsub  48474  flsubz  48637  zofldiv2  48646  dignn0flhalflem1  48730  dignn0flhalflem2  48731