Theorem zcnd 12601

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 12600	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 11164	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11028  ℤcz 12492

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 11087

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 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7363  df-neg 11371  df-z 12493

This theorem is referenced by:  zsupss  12854  rpnnen1lem5  12898  fzm1  13527  fzrevral  13532  fzshftral  13535  nn0disj  13564  predfz  13573  fzoss2  13607  elfzo0suble  13626  fzo0addelr  13639  elfzoext  13642  fzosubel  13644  fzosubel3  13646  fzocatel  13649  fzosplitsnm1  13660  elfzom1elp1fzo1  13687  fzom1ne1  13705  2tnp1ge0ge0  13753  quoremz  13779  intfrac2  13782  intfracq  13783  flpmodeq  13798  moddiffl  13806  modmul1  13851  modmul12d  13852  modfzo0difsn  13870  modsumfzodifsn  13871  addmodlteq  13873  uzrdgxfr  13894  fzen2  13896  monoord2  13960  seqf1olem1  13968  seqf1olem2  13969  seqz  13977  expaddzlem  14032  znsqcld  14089  modexp  14165  sqoddm1div8  14170  bcm1k  14242  bcp1nk  14244  bcval5  14245  bcpasc  14248  hashfz  14354  hashfzo  14356  hashfzp1  14358  hashbclem  14379  seqcoll  14391  ccatval3  14506  ccatlid  14514  ccatass  14516  ccatalpha  14521  swrdfv0  14577  swrdfv2  14589  swrds1  14594  ccatswrd  14596  pfxfv  14610  ccatpfx  14628  swrdpfx  14634  pfxccatin12lem2  14658  spllen  14681  revccat  14693  revrev  14694  cshwidxmod  14730  cshwidxm1  14734  cshweqrep  14748  2cshwcshw  14752  cshimadifsn0  14757  swrds2m  14868  seqshft  15012  fzomaxdif  15271  climshft2  15509  iserex  15584  isercoll2  15596  serf0  15608  iseraltlem2  15610  iseraltlem3  15611  iseralt  15612  sumrblem  15638  fsumm1  15678  fsumsplitsnun  15682  fsump1  15683  fsumshftm  15708  fsumrev2  15709  telfsumo  15729  fsumparts  15733  binomlem  15756  isumshft  15766  isumsplit  15767  isum1p  15768  arisum  15787  pwdif  15795  cvgrat  15810  mertenslem1  15811  ntrivcvg  15824  ntrivcvgtail  15827  prodrblem  15856  fprodser  15876  fprodm1  15894  fprodp1  15896  fprodrev  15904  fprodmodd  15924  fallfacval3  15939  fallfacfwd  15963  0fallfac  15964  binomfallfaclem2  15967  fallfacval4  15970  fsumkthpow  15983  eirrlem  16133  sqrt2irrlem  16177  addmulmodb  16196  dvds2ln  16220  dvdsadd2b  16237  fsumdvds  16239  fzocongeq  16255  addmodlteqALT  16256  dvdsexp  16259  dvdsmod  16260  3dvds  16262  fprodfvdvdsd  16265  odd2np1  16272  oddm1even  16274  oexpneg  16276  mod2eq1n2dvds  16278  mulsucdiv2z  16284  zob  16290  ltoddhalfle  16292  sumodd  16319  pwp1fsum  16322  divalglem0  16324  divalglem4  16327  divalglem8  16331  divalgb  16335  divalgmod  16337  modremain  16339  flodddiv4  16346  bitsp1  16362  bitsfzo  16366  bitsmod  16367  bitsinv1lem  16372  bitsf1  16377  sadaddlem  16397  bitsres  16404  bitsuz  16405  bitsshft  16406  smumullem  16423  modgcd  16463  gcdmultipled  16465  dvdsgcdidd  16468  bezoutlem1  16470  bezoutlem2  16471  bezoutlem3  16472  bezoutlem4  16473  dvdsmulgcd  16487  rplpwr  16489  lcmid  16540  absprodnn  16549  mulgcddvds  16586  divgcdcoprm0  16596  cncongr1  16598  cncongr2  16599  dvdszzq  16652  rpexp  16653  prmdvdsbc  16657  qmuldeneqnum  16678  numdensq  16685  qden1elz  16688  numdenexp  16691  hashdvds  16706  phiprm  16708  eulerthlem2  16713  fermltl  16715  prmdiv  16716  prmdiveq  16717  hashgcdlem  16719  odzdvds  16727  vfermltlALT  16734  modprm0  16737  modprmn0modprm0  16739  pythagtriplem6  16753  pythagtriplem7  16754  pythagtriplem15  16761  pcpremul  16775  pceulem  16777  pczpre  16779  pcdiv  16784  pcqmul  16785  pcqdiv  16789  pcexp  16791  pcaddlem  16820  pcadd  16821  fldivp1  16829  pcfac  16831  pcbc  16832  prmpwdvds  16836  prmreclem4  16851  4sqlem5  16874  4sqlem8  16877  4sqlem9  16878  4sqlem10  16879  4sqlem11  16887  4sqlem14  16890  4sqlem16  16892  4sqlem17  16893  vdwapun  16906  vdwnnlem2  16928  prmop1  16970  prmdvdsprmo  16974  prmgaplem7  16989  prmlem0  17037  chnlt  18550  mulgsubcl  19022  mulgdirlem  19039  mulgdir  19040  mulgass  19045  mulgmodid  19047  mulgsubdir  19048  psgnunilem5  19427  psgnunilem2  19428  psgnunilem4  19430  m1expaddsub  19431  psgnuni  19432  odnncl  19478  odmulg  19489  odbezout  19491  sylow1lem1  19531  sylow2alem2  19551  efgsres  19671  efgredleme  19676  efgredlemc  19678  odadd1  19781  odadd2  19782  cyggeninv  19816  gsummptshft  19869  ablfacrp  20001  pgpfac1lem3  20012  fincygsubgodd  20047  srgbinomlem3  20167  srgbinomlem4  20168  zringmulg  21415  zringlpirlem1  21421  zringlpirlem3  21423  prmirredlem  21431  fermltlchr  21488  zndvds0  21509  znf1o  21510  znunit  21522  cayhamlem1  22814  tgpmulg  24041  zdis  24765  uniioombllem3  25546  mbfi1fseqlem4  25679  dvexp3  25942  aareccl  26294  aalioulem1  26300  geolim3  26307  aaliou3lem2  26311  aaliou3lem6  26316  ulmshft  26359  sineq0  26493  efif1olem2  26512  igamz  27018  wilthlem1  27038  wilthlem2  27039  basellem3  27053  mumul  27151  musum  27161  musumsum  27162  muinv  27163  ppiub  27175  chtub  27183  logfac2  27188  chpchtsum  27190  dchrptlem1  27235  pcbcctr  27247  bcmono  27248  bposlem5  27259  bposlem6  27260  lgslem1  27268  lgsval2lem  27278  lgsval4a  27290  lgsneg  27292  lgsneg1  27293  lgsmod  27294  lgsdirprm  27302  lgsdir  27303  lgsdilem2  27304  lgsdi  27305  lgsne0  27306  lgsabs1  27307  lgssq  27308  lgssq2  27309  lgsmulsqcoprm  27314  lgsdirnn0  27315  lgsdinn0  27316  lgsqrlem1  27317  gausslemma2dlem1a  27336  gausslemma2dlem1  27337  gausslemma2dlem4  27340  gausslemma2dlem5a  27341  gausslemma2dlem5  27342  gausslemma2dlem6  27343  gausslemma2d  27345  lgseisenlem1  27346  lgseisenlem2  27347  lgseisenlem3  27348  lgseisenlem4  27349  lgsquadlem1  27351  lgsquad2lem1  27355  lgsquad3  27358  2lgslem1b  27363  2lgsoddprmlem2  27380  2sqlem3  27391  2sqlem4  27392  2sqlem8a  27396  2sqlem8  27397  2sqlem11  27400  2sqblem  27402  2sqn0  27405  2sqmod  27407  dchrisumlem1  27460  dchrmusum2  27465  dchrvmasumlem1  27466  dchrvmasum2lem  27467  mudivsum  27501  mulogsum  27503  mulog2sumlem2  27506  selberglem1  27516  selberglem3  27518  selberg  27519  pntpbnd2  27558  pntlemf  27576  padicabvcxp  27603  axlowdimlem14  29032  axlowdimlem16  29034  pthdadjvtx  29805  crctcshwlkn0lem4  29890  crctcshwlkn0lem5  29891  crctcshlem4  29897  crctcsh  29901  clwwlkccatlem  30068  clwwisshclwws  30094  eucrctshift  30322  fzm1ne1  32870  fzspl  32871  bcm1n  32877  elq2  32894  znumd  32895  zdend  32896  numdenneg  32897  divnumden2  32898  ltesubnnd  32905  ccatf1  33033  swrdrn3  33039  swrdf1  33040  cshwrnid  33045  gsumzrsum  33150  gsummulsubdishift1  33153  cycpmco2lem3  33212  cycpmco2lem4  33213  cycpmco2lem5  33214  cycpmco2lem6  33215  cycpmco2  33217  archiabllem1  33277  archiabllem2c  33279  elrgspnlem1  33326  elrgspnlem2  33327  znfermltl  33449  zringidom  33634  zringfrac  33637  esplyindfv  33734  zconstr  33923  cos9thpiminplylem2  33942  zrhnm  34126  cnzh  34127  rezh  34128  zrhcntr  34138  qqhval2lem  34140  qqhghm  34147  qqhrhm  34148  qqhnm  34149  ballotlemfc0  34652  ballotlemfcc  34653  ballotlemic  34666  ballotlem1c  34667  ballotlemsgt1  34670  ballotlemsdom  34671  ballotlemsel1i  34672  ballotlemsf1o  34673  ballotlemsima  34675  ballotlemfrceq  34688  ballotlemfrcn0  34689  ballotlem1ri  34694  signsplypnf  34709  itgexpif  34765  fsum2dsub  34766  breprexplemc  34791  vtsprod  34798  circlemeth  34799  revpfxsfxrev  35312  swrdrevpfx  35313  revwlk  35321  swrdwlk  35323  divcnvlin  35929  fwddifnp1  36361  knoppndvlem2  36715  knoppndvlem7  36720  knoppndvlem14  36727  knoppndvlem16  36729  ltflcei  37811  poimirlem1  37824  poimirlem2  37825  poimirlem7  37830  poimirlem16  37839  poimirlem17  37840  poimirlem19  37842  poimirlem20  37843  poimirlem24  37847  poimirlem31  37854  poimirlem32  37855  fdc  37948  mettrifi  37960  caushft  37964  cntotbnd  37999  fzsplitnd  42304  lcmineqlem6  42356  lcmineqlem18  42368  aks4d1p1p1  42385  aks4d1p8d3  42408  aks4d1p8  42409  primrootscoprmpow  42421  posbezout  42422  primrootscoprbij  42424  primrootspoweq0  42428  hashscontpow1  42443  aks6d1c3  42445  aks6d1c4  42446  aks6d1c5lem1  42458  aks6d1c5lem2  42460  sticksstones10  42477  sticksstones12a  42479  sticksstones12  42480  aks6d1c6lem3  42494  unitscyglem2  42518  unitscyglem4  42520  sumcubes  42635  oexpreposd  42644  exp11d  42648  dvdsexpb  42657  mzpsubmpt  43052  lzenom  43079  diophun  43082  eqrabdioph  43086  irrapxlem2  43132  irrapxlem3  43133  pellexlem6  43143  pell1234qrreccl  43163  pellfund14  43207  rmxyneg  43229  rmxyadd  43230  rmxp1  43241  rmxm1  43243  rmym1  43244  rmxluc  43245  rmyluc  43246  rmyluc2  43247  rmxdbl  43248  rmydbl  43249  congadd  43275  congsub  43279  congabseq  43283  acongrep  43289  acongeq  43292  jm2.18  43297  jm2.19lem1  43298  jm2.19lem2  43299  jm2.19lem3  43300  jm2.22  43304  jm2.23  43305  jm2.20nn  43306  jm2.25  43308  jm2.26lem3  43310  jm2.27c  43316  nzss  44625  hashnzfz  44628  hashnzfz2  44629  hashnzfzclim  44630  uzmptshftfval  44654  sineq0ALT  45244  fzisoeu  45615  fperiodmul  45619  monoord2xrv  45794  fmul01lt1lem2  45898  sumnnodd  45943  dvdsn1add  46250  dvnmul  46254  dvnprodlem1  46257  stoweidlem11  46322  stoweidlem26  46337  dirkertrigeqlem1  46409  dirkertrigeqlem2  46410  dirkertrigeqlem3  46411  dirkertrigeq  46412  dirkeritg  46413  fourierdlem26  46444  fourierdlem48  46465  fourierdlem49  46466  fourierdlem79  46496  fourierdlem91  46508  fourierdlem103  46520  fourierdlem104  46521  fouriersw  46542  etransclem1  46546  etransclem4  46549  etransclem8  46553  etransclem9  46554  etransclem15  46560  etransclem17  46562  etransclem18  46563  etransclem20  46565  etransclem21  46566  etransclem22  46567  etransclem23  46568  etransclem24  46569  etransclem25  46570  etransclem35  46580  etransclem38  46583  etransclem41  46586  etransclem44  46589  etransclem45  46590  etransclem46  46591  etransclem47  46592  etransclem48  46593  chnerlem2  47194  2elfz2melfz  47631  ceilbi  47646  fldivmod  47651  submodaddmod  47654  zplusmodne  47656  m1modne  47661  minusmod5ne  47662  submodlt  47663  minusmodnep2tmod  47666  m1modmmod  47671  modmkpkne  47674  modmknepk  47675  mod2addne  47677  modm2nep1  47679  modm1nep2  47681  modm1nem2  47682  fsumsplitsndif  47686  iccpartgtprec  47733  fargshiftf1  47754  fargshiftfo  47755  mod42tp1mod8  47915  sfprmdvdsmersenne  47916  lighneallem3  47920  lighneallem4b  47922  modexp2m1d  47925  dfodd6  47950  onego  47959  m1expoddALTV  47961  zofldiv2ALTV  47975  oddflALTV  47976  oexpnegALTV  47990  omoeALTV  47998  omeoALTV  47999  epoo  48016  emoo  48017  epee  48018  emee  48019  evensumeven  48020  evenltle  48030  even3prm2  48032  mogoldbblem  48033  fppr2odd  48044  fpprwppr  48052  fpprwpprb  48053  sbgoldbst  48091  sbgoldbaltlem2  48093  sgoldbeven3prm  48096  nnsum3primesprm  48103  nnsum4primesodd  48109  nnsum4primesoddALTV  48110  nnsum4primeseven  48113  nnsum4primesevenALTV  48114  bgoldbtbndlem2  48119  bgoldbtbndlem4  48121  bgoldbtbnd  48122  gpgedgvtx1  48375  gpgvtxedg0  48376  gpgvtxedg1  48377  gpg5nbgrvtx13starlem2  48385  gpg3nbgrvtx0  48389  pgnbgreunbgrlem2lem1  48427  pgnbgreunbgrlem2lem2  48428  pgnbgreunbgrlem2lem3  48429  2zrngamnd  48560  2zrngacmnd  48561  2zrngagrp  48562  2zrngALT  48567  2zrngnmlid  48568  2zrngnmlid2  48570  ztprmneprm  48660  altgsumbcALT  48666  zofldiv2  48844  fllogbd  48873  nnpw2blen  48893  blen1b  48901  blennngt2o2  48905  blennn0e2  48907  dig2nn1st  48918  dignn0flhalflem1  48928