Theorem zcnd 12667

Description: An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
zred.1	⊢ (𝜑 → 𝐴 ∈ ℤ)

Assertion

Ref	Expression
zcnd	⊢ (𝜑 → 𝐴 ∈ ℂ)

Proof of Theorem zcnd

Step	Hyp	Ref	Expression
1		zred.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℤ)
2	1	zred 12666	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	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:  zsupss  12921  rpnnen1lem5  12965  fzm1  13581  fzrevral  13586  fzshftral  13589  nn0disj  13617  predfz  13626  fzoss2  13660  fzo0addelr  13687  fzosubel  13691  fzosubel3  13693  fzocatel  13696  fzosplitsnm1  13707  elfzom1elp1fzo1  13732  2tnp1ge0ge0  13794  quoremz  13820  intfrac2  13823  intfracq  13824  flpmodeq  13839  moddiffl  13847  modmul1  13889  modmul12d  13890  modfzo0difsn  13908  modsumfzodifsn  13909  addmodlteq  13911  uzrdgxfr  13932  fzen2  13934  monoord2  13999  seqf1olem1  14007  seqf1olem2  14008  seqz  14016  expaddzlem  14071  znsqcld  14127  modexp  14201  sqoddm1div8  14206  bcm1k  14275  bcp1nk  14277  bcval5  14278  bcpasc  14281  hashfz  14387  hashfzo  14389  hashfzp1  14391  hashbclem  14411  seqcoll  14425  ccatval3  14529  ccatlid  14536  ccatass  14538  ccatalpha  14543  swrdfv0  14599  swrdfv2  14611  swrds1  14616  ccatswrd  14618  pfxfv  14632  ccatpfx  14651  swrdpfx  14657  pfxccatin12lem2  14681  spllen  14704  revccat  14716  revrev  14717  cshwidxmod  14753  cshwidxm1  14757  cshweqrep  14771  2cshwcshw  14776  cshimadifsn0  14781  swrds2m  14892  seqshft  15032  fzomaxdif  15290  climshft2  15526  iserex  15603  isercoll2  15615  serf0  15627  iseraltlem2  15629  iseraltlem3  15630  iseralt  15631  sumrblem  15657  fsumm1  15697  fsumsplitsnun  15701  fsump1  15702  fsumshftm  15727  fsumrev2  15728  telfsumo  15748  fsumparts  15752  binomlem  15775  isumshft  15785  isumsplit  15786  isum1p  15787  arisum  15806  pwdif  15814  cvgrat  15829  mertenslem1  15830  ntrivcvg  15843  ntrivcvgtail  15846  prodrblem  15873  fprodser  15893  fprodm1  15911  fprodp1  15913  fprodrev  15921  fprodmodd  15941  fallfacval3  15956  fallfacfwd  15980  0fallfac  15981  binomfallfaclem2  15984  fallfacval4  15987  fsumkthpow  16000  eirrlem  16147  sqrt2irrlem  16191  dvds2ln  16232  dvdsadd2b  16249  fsumdvds  16251  fzocongeq  16267  addmodlteqALT  16268  dvdsexp  16271  dvdsmod  16272  3dvds  16274  fprodfvdvdsd  16277  odd2np1  16284  oddm1even  16286  oexpneg  16288  mod2eq1n2dvds  16290  mulsucdiv2z  16296  zob  16302  ltoddhalfle  16304  sumodd  16331  pwp1fsum  16334  divalglem0  16336  divalglem4  16339  divalglem8  16343  divalgb  16347  divalgmod  16349  modremain  16351  flodddiv4  16356  bitsp1  16372  bitsfzo  16376  bitsmod  16377  bitsinv1lem  16382  bitsf1  16387  sadaddlem  16407  bitsres  16414  bitsuz  16415  bitsshft  16416  smumullem  16433  modgcd  16474  gcdmultipled  16476  dvdsgcdidd  16479  bezoutlem1  16481  bezoutlem2  16482  bezoutlem3  16483  bezoutlem4  16484  dvdsmulgcd  16497  rplpwr  16499  lcmid  16546  absprodnn  16555  mulgcddvds  16592  divgcdcoprm0  16602  cncongr1  16604  cncongr2  16605  rpexp  16659  qmuldeneqnum  16683  numdensq  16690  qden1elz  16693  hashdvds  16708  phiprm  16710  eulerthlem2  16715  fermltl  16717  prmdiv  16718  prmdiveq  16719  hashgcdlem  16721  odzdvds  16728  vfermltlALT  16735  modprm0  16738  modprmn0modprm0  16740  pythagtriplem6  16754  pythagtriplem7  16755  pythagtriplem15  16762  pcpremul  16776  pceulem  16778  pczpre  16780  pcdiv  16785  pcqmul  16786  pcqdiv  16790  pcexp  16792  pcaddlem  16821  pcadd  16822  fldivp1  16830  pcfac  16832  pcbc  16833  prmpwdvds  16837  prmreclem4  16852  4sqlem5  16875  4sqlem8  16878  4sqlem9  16879  4sqlem10  16880  4sqlem11  16888  4sqlem14  16891  4sqlem16  16893  4sqlem17  16894  vdwapun  16907  vdwnnlem2  16929  prmop1  16971  prmdvdsprmo  16975  prmgaplem7  16990  prmlem0  17039  mulgsubcl  18968  mulgdirlem  18985  mulgdir  18986  mulgass  18991  mulgmodid  18993  mulgsubdir  18994  psgnunilem5  19362  psgnunilem2  19363  psgnunilem4  19365  m1expaddsub  19366  psgnuni  19367  odnncl  19413  odmulg  19424  odbezout  19426  sylow1lem1  19466  sylow2alem2  19486  efgsres  19606  efgredleme  19611  efgredlemc  19613  odadd1  19716  odadd2  19717  cyggeninv  19751  gsummptshft  19804  ablfacrp  19936  pgpfac1lem3  19947  fincygsubgodd  19982  srgbinomlem3  20051  srgbinomlem4  20052  zringmulg  21026  zringlpirlem1  21032  zringlpirlem3  21034  prmirredlem  21042  zndvds0  21106  znf1o  21107  znunit  21119  cayhamlem1  22368  tgpmulg  23597  zdis  24332  uniioombllem3  25102  mbfi1fseqlem4  25236  dvexp3  25495  aareccl  25839  aalioulem1  25845  geolim3  25852  aaliou3lem2  25856  aaliou3lem6  25861  ulmshft  25902  sineq0  26033  efif1olem2  26052  igamz  26552  wilthlem1  26572  wilthlem2  26573  basellem3  26587  mumul  26685  musum  26695  musumsum  26696  muinv  26697  ppiub  26707  chtub  26715  logfac2  26720  chpchtsum  26722  dchrptlem1  26767  pcbcctr  26779  bcmono  26780  bposlem5  26791  bposlem6  26792  lgslem1  26800  lgsval2lem  26810  lgsval4a  26822  lgsneg  26824  lgsneg1  26825  lgsmod  26826  lgsdirprm  26834  lgsdir  26835  lgsdilem2  26836  lgsdi  26837  lgsne0  26838  lgsabs1  26839  lgssq  26840  lgssq2  26841  lgsmulsqcoprm  26846  lgsdirnn0  26847  lgsdinn0  26848  lgsqrlem1  26849  gausslemma2dlem1a  26868  gausslemma2dlem1  26869  gausslemma2dlem4  26872  gausslemma2dlem5a  26873  gausslemma2dlem5  26874  gausslemma2dlem6  26875  gausslemma2d  26877  lgseisenlem1  26878  lgseisenlem2  26879  lgseisenlem3  26880  lgseisenlem4  26881  lgsquadlem1  26883  lgsquad2lem1  26887  lgsquad3  26890  2lgslem1b  26895  2lgsoddprmlem2  26912  2sqlem3  26923  2sqlem4  26924  2sqlem8a  26928  2sqlem8  26929  2sqlem11  26932  2sqblem  26934  2sqn0  26937  2sqmod  26939  dchrisumlem1  26992  dchrmusum2  26997  dchrvmasumlem1  26998  dchrvmasum2lem  26999  mudivsum  27033  mulogsum  27035  mulog2sumlem2  27038  selberglem1  27048  selberglem3  27050  selberg  27051  pntpbnd2  27090  pntlemf  27108  padicabvcxp  27135  axlowdimlem14  28213  axlowdimlem16  28215  pthdadjvtx  28987  crctcshwlkn0lem4  29067  crctcshwlkn0lem5  29068  crctcshlem4  29074  crctcsh  29078  clwwlkccatlem  29242  clwwisshclwws  29268  eucrctshift  29496  fzm1ne1  32000  fzspl  32001  bcm1n  32006  fzom1ne1  32012  dvdszzq  32021  prmdvdsbc  32022  numdenneg  32023  divnumden2  32024  ltesubnnd  32028  ccatf1  32115  swrdrn3  32119  swrdf1  32120  cshwrnid  32125  cycpmco2lem3  32287  cycpmco2lem4  32288  cycpmco2lem5  32289  cycpmco2lem6  32290  cycpmco2  32292  archiabllem1  32339  archiabllem2c  32341  fermltlchr  32478  znfermltl  32479  zrhnm  32949  cnzh  32950  rezh  32951  qqhval2lem  32961  qqhghm  32968  qqhrhm  32969  qqhnm  32970  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemic  33505  ballotlem1c  33506  ballotlemsgt1  33509  ballotlemsdom  33510  ballotlemsel1i  33511  ballotlemsf1o  33512  ballotlemsima  33514  ballotlemfrceq  33527  ballotlemfrcn0  33528  ballotlem1ri  33533  signsplypnf  33561  itgexpif  33618  fsum2dsub  33619  breprexplemc  33644  vtsprod  33651  circlemeth  33652  revpfxsfxrev  34106  swrdrevpfx  34107  revwlk  34115  swrdwlk  34117  divcnvlin  34702  fwddifnp1  35137  knoppndvlem2  35389  knoppndvlem7  35394  knoppndvlem14  35401  knoppndvlem16  35403  ltflcei  36476  poimirlem1  36489  poimirlem2  36490  poimirlem7  36495  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem24  36512  poimirlem31  36519  poimirlem32  36520  fdc  36613  mettrifi  36625  caushft  36629  cntotbnd  36664  fzsplitnd  40848  lcmineqlem6  40899  lcmineqlem18  40911  aks4d1p1p1  40928  aks4d1p8d3  40951  aks4d1p8  40952  sticksstones10  40971  sticksstones12a  40973  sticksstones12  40974  metakunt12  40996  metakunt15  40999  metakunt16  41000  metakunt28  41012  sumcubes  41211  oexpreposd  41212  exp11d  41216  numdenexp  41228  dvdsexpb  41233  mzpsubmpt  41481  lzenom  41508  diophun  41511  eqrabdioph  41515  irrapxlem2  41561  irrapxlem3  41562  pellexlem6  41572  pell1234qrreccl  41592  pellfund14  41636  rmxyneg  41659  rmxyadd  41660  rmxp1  41671  rmxm1  41673  rmym1  41674  rmxluc  41675  rmyluc  41676  rmyluc2  41677  rmxdbl  41678  rmydbl  41679  congadd  41705  congsub  41709  congabseq  41713  acongrep  41719  acongeq  41722  jm2.18  41727  jm2.19lem1  41728  jm2.19lem2  41729  jm2.19lem3  41730  jm2.22  41734  jm2.23  41735  jm2.20nn  41736  jm2.25  41738  jm2.26lem3  41740  jm2.27c  41746  nzss  43076  hashnzfz  43079  hashnzfz2  43080  hashnzfzclim  43081  uzmptshftfval  43105  sineq0ALT  43698  fzisoeu  44010  fperiodmul  44014  monoord2xrv  44194  fmul01lt1lem2  44301  sumnnodd  44346  dvdsn1add  44655  dvnmul  44659  dvnprodlem1  44662  stoweidlem11  44727  stoweidlem26  44742  dirkertrigeqlem1  44814  dirkertrigeqlem2  44815  dirkertrigeqlem3  44816  dirkertrigeq  44817  dirkeritg  44818  fourierdlem26  44849  fourierdlem48  44870  fourierdlem49  44871  fourierdlem79  44901  fourierdlem91  44913  fourierdlem103  44925  fourierdlem104  44926  fouriersw  44947  etransclem1  44951  etransclem4  44954  etransclem8  44958  etransclem9  44959  etransclem15  44965  etransclem17  44967  etransclem18  44968  etransclem20  44970  etransclem21  44971  etransclem22  44972  etransclem23  44973  etransclem24  44974  etransclem25  44975  etransclem35  44985  etransclem38  44988  etransclem41  44991  etransclem44  44994  etransclem45  44995  etransclem46  44996  etransclem47  44997  etransclem48  44998  2elfz2melfz  46026  fsumsplitsndif  46041  iccpartgtprec  46088  fargshiftf1  46109  fargshiftfo  46110  mod42tp1mod8  46270  sfprmdvdsmersenne  46271  lighneallem3  46275  lighneallem4b  46277  modexp2m1d  46280  dfodd6  46305  onego  46314  m1expoddALTV  46316  zofldiv2ALTV  46330  oddflALTV  46331  oexpnegALTV  46345  omoeALTV  46353  omeoALTV  46354  epoo  46371  emoo  46372  epee  46373  emee  46374  evensumeven  46375  evenltle  46385  even3prm2  46387  mogoldbblem  46388  fppr2odd  46399  fpprwppr  46407  fpprwpprb  46408  sbgoldbst  46446  sbgoldbaltlem2  46448  sgoldbeven3prm  46451  nnsum3primesprm  46458  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  bgoldbtbndlem2  46474  bgoldbtbndlem4  46476  bgoldbtbnd  46477  2zrngamnd  46839  2zrngacmnd  46840  2zrngagrp  46841  2zrngALT  46846  2zrngnmlid  46847  2zrngnmlid2  46849  ztprmneprm  47023  altgsumbcALT  47029  fldivmod  47204  m1modmmod  47207  zofldiv2  47217  fllogbd  47246  nnpw2blen  47266  blen1b  47274  blennngt2o2  47278  blennn0e2  47280  dig2nn1st  47291  dignn0flhalflem1  47301