Theorem zcnd 12721

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℂcc 11117  ℤcz 12610

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-resscn 11176

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-neg 11463  df-z 12611

This theorem is used by:  zsupss  12981  rpnnen1lem5  13025  fzm1  13656  fzrevral  13661  fzshftral  13664  nn0disj  13693  predfz  13702  fzoss2  13737  elfzo0suble  13756  fzo0addelr  13769  elfzoext  13772  fzosubel  13774  fzosubel3  13776  fzocatel  13779  fzosplitsnm1  13790  elfzom1elp1fzo1  13817  fzom1ne1  13835  2tnp1ge0ge0  13884  quoremz  13910  intfrac2  13913  intfracq  13914  flpmodeq  13929  moddiffl  13937  modmul1  13982  modmul12d  13983  modfzo0difsn  14001  modsumfzodifsn  14002  addmodlteq  14004  uzrdgxfr  14025  fzen2  14027  monoord2  14091  seqf1olem1  14099  seqf1olem2  14100  seqz  14108  expaddzlem  14163  znsqcld  14220  modexp  14296  sqoddm1div8  14301  bcm1k  14373  bcp1nk  14375  bcval5  14376  bcpasc  14379  hashfz  14486  hashfzo  14488  hashfzp1  14490  hashbclem  14511  seqcoll  14523  ccatval3  14638  ccatlid  14646  ccatass  14648  ccatf1  14650  ccatalpha  14654  swrdfv0  14711  swrdf1  14713  swrdrn3  14716  swrdfv2  14725  swrds1  14730  ccatswrd  14732  pfxfv  14746  ccatpfx  14764  swrdpfx  14770  pfxccatin12lem2  14794  spllen  14817  revccat  14829  revrev  14830  revpfxsfxrev  14831  swrdrevpfx  14832  cshwidxmod  14868  cshwidxm1  14872  cshweqrep  14886  2cshwcshw  14890  cshimadifsn0  14895  swrds2m  15006  seqshft  15150  fzomaxdif  15423  climshft2  15661  iserex  15736  isercoll2  15748  serf0  15760  iseraltlem2  15762  iseraltlem3  15763  iseralt  15764  sumrblem  15789  fsumm1  15829  fsumsplitsnun  15833  fsump1  15834  fsumshftm  15859  fsumrev2  15860  telfsumo  15881  fsumparts  15885  binomlem  15910  isumshft  15920  isumsplit  15921  isum1p  15922  arisum  15941  pwdif  15949  cvgrat  15964  mertenslem1  15965  ntrivcvg  15978  ntrivcvgtail  15981  prodrblem  16010  fprodser  16030  fprodm1  16048  fprodp1  16050  fprodrev  16058  fprodmodd  16078  fallfacval3  16093  fallfacfwd  16116  0fallfac  16117  binomfallfaclem2  16120  fallfacval4  16123  fsumkthpow  16136  eirrlem  16286  sqrt2irrlem  16330  addmulmodb  16349  dvds2ln  16373  dvdsadd2b  16390  fsumdvds  16392  fzocongeq  16408  addmodlteqALT  16409  dvdsexp  16412  dvdsmod  16413  3dvds  16415  fprodfvdvdsd  16418  odd2np1  16425  oddm1even  16427  oexpneg  16429  mod2eq1n2dvds  16431  mulsucdiv2z  16437  zob  16443  ltoddhalfle  16445  sumodd  16472  pwp1fsum  16475  divalglem0  16477  divalglem4  16480  divalglem8  16484  divalgb  16488  divalgmod  16490  modremain  16492  flodddiv4  16499  bitsp1  16515  bitsfzo  16519  bitsmod  16520  bitsinv1lem  16525  bitsf1  16530  sadaddlem  16550  bitsres  16557  bitsuz  16558  bitsshft  16559  smumullem  16576  modgcd  16616  gcdmultipled  16618  dvdsgcdidd  16621  bezoutlem1  16623  bezoutlem2  16624  bezoutlem3  16625  bezoutlem4  16626  dvdsmulgcd  16640  rplpwr  16642  lcmid  16693  absprodnn  16702  mulgcddvds  16739  divgcdcoprm0  16749  cncongr1  16751  cncongr2  16752  dvdszzq  16806  rpexp  16807  prmdvdsbc  16811  qmuldeneqnum  16832  numdensq  16839  qden1elz  16842  numdenexp  16845  hashdvds  16860  phiprm  16862  eulerthlem2  16867  fermltl  16869  prmdiv  16870  prmdiveq  16871  hashgcdlem  16873  odzdvds  16881  vfermltlALT  16888  modprm0  16891  modprmn0modprm0  16893  pythagtriplem6  16907  pythagtriplem7  16908  pythagtriplem15  16915  pcpremul  16929  pceulem  16931  pczpre  16933  pcdiv  16938  pcqmul  16939  pcqdiv  16943  pcexp  16945  pcaddlem  16974  pcadd  16975  fldivp1  16983  pcfac  16985  pcbc  16986  prmpwdvds  16990  prmreclem4  17005  4sqlem5  17028  4sqlem8  17031  4sqlem9  17032  4sqlem10  17033  4sqlem11  17041  4sqlem14  17044  4sqlem16  17046  4sqlem17  17047  vdwapun  17060  vdwnnlem2  17082  prmop1  17124  prmdvdsprmo  17128  prmgaplem7  17143  prmlem0  17191  chnlt  18705  mulgsubcl  19202  mulgdirlem  19219  mulgdir  19220  mulgass  19225  mulgmodid  19227  mulgsubdir  19228  psgnunilem5  19612  psgnunilem2  19613  psgnunilem4  19615  m1expaddsub  19616  psgnuni  19617  odnncl  19663  odmulg  19674  odbezout  19676  sylow1lem1  19716  sylow2alem2  19736  efgsres  19856  efgredleme  19861  efgredlemc  19863  odadd1  19966  odadd2  19967  cyggeninv  20001  gsummptshft  20054  ablfacrp  20186  pgpfac1lem3  20197  fincygsubgodd  20232  srgbinomlem3  20358  srgbinomlem4  20359  zringmulg  21660  zringlpirlem1  21666  zringlpirlem3  21668  prmirredlem  21676  fermltlchr  21733  zndvds0  21754  znf1o  21755  znunit  21767  cayhamlem1  23077  tgpmulg  24305  zdis  25029  uniioombllem3  25799  mbfi1fseqlem4  25932  dvexp3  26192  aareccl  26544  aalioulem1  26550  geolim3  26557  aaliou3lem2  26561  aaliou3lem6  26566  ulmshft  26608  sineq0  26744  efif1olem2  26763  igamz  27267  wilthlem1  27287  wilthlem2  27288  basellem3  27302  mumul  27400  musum  27410  musumsum  27411  muinv  27412  ppiub  27423  chtub  27431  logfac2  27436  chpchtsum  27438  dchrptlem1  27483  pcbcctr  27495  bcmono  27496  bposlem5  27507  bposlem6  27508  lgslem1  27516  lgsval2lem  27526  lgsval4a  27538  lgsneg  27540  lgsneg1  27541  lgsmod  27542  lgsdirprm  27550  lgsdir  27551  lgsdilem2  27552  lgsdi  27553  lgsne0  27554  lgsabs1  27555  lgssq  27556  lgssq2  27557  lgsmulsqcoprm  27562  lgsdirnn0  27563  lgsdinn0  27564  lgsqrlem1  27565  gausslemma2dlem1a  27584  gausslemma2dlem1  27585  gausslemma2dlem4  27588  gausslemma2dlem5a  27589  gausslemma2dlem5  27590  gausslemma2dlem6  27591  gausslemma2d  27593  lgseisenlem1  27594  lgseisenlem2  27595  lgseisenlem3  27596  lgseisenlem4  27597  lgsquadlem1  27599  lgsquad2lem1  27603  lgsquad3  27606  2lgslem1b  27611  2lgsoddprmlem2  27628  2sqlem3  27639  2sqlem4  27640  2sqlem8a  27644  2sqlem8  27645  2sqlem11  27648  2sqblem  27650  2sqn0  27653  2sqmod  27655  dchrisumlem1  27708  dchrmusum2  27713  dchrvmasumlem1  27714  dchrvmasum2lem  27715  mudivsum  27749  mulogsum  27751  mulog2sumlem2  27754  selberglem1  27764  selberglem3  27766  selberg  27767  pntpbnd2  27806  pntlemf  27824  padicabvcxp  27851  axlowdimlem14  29364  axlowdimlem16  29366  revwlk  30098  swrdwlk  30099  pthdadjvtx  30144  crctcshwlkn0lem4  30233  crctcshwlkn0lem5  30234  crctcshlem4  30240  crctcsh  30244  clwwlkccatlem  30411  clwwisshclwws  30437  eucrctshift  30669  fzm1ne1  33207  fzspl  33208  bcm1n  33214  elq2  33230  znumd  33231  zdend  33232  numdenneg  33233  divnumden2  33234  ltesubnnd  33241  cshwrnid  33349  gsumzrsum  33453  gsummulsubdishift1  33456  cycpmco2lem3  33516  cycpmco2lem4  33517  cycpmco2lem5  33518  cycpmco2lem6  33519  cycpmco2  33521  archiabllem1  33581  archiabllem2c  33583  elrgspnlem1  33630  elrgspnlem2  33631  znfermltl  33749  zringidom  33909  zringfrac  33912  esplyindfv  34034  zconstr  34222  cos9thpiminplylem2  34241  zrhnm  34425  cnzh  34426  rezh  34427  zrhcntr  34437  qqhval2lem  34439  qqhghm  34446  qqhrhm  34447  qqhnm  34448  ballotlemfc0  34952  ballotlemfcc  34953  ballotlemic  34966  ballotlem1c  34967  ballotlemsgt1  34970  ballotlemsdom  34971  ballotlemsel1i  34972  ballotlemsf1o  34973  ballotlemsima  34975  ballotlemfrceq  34988  ballotlemfrcn0  34989  ballotlem1ri  34994  signsplypnf  35006  itgexpif  35062  fsum2dsub  35063  breprexplemc  35088  vtsprod  35095  circlemeth  35096  divcnvlin  36266  fwddifnp1  36698  knoppndvlem2  37163  knoppndvlem7  37168  knoppndvlem14  37175  knoppndvlem16  37177  ltflcei  38320  poimirlem1  38333  poimirlem2  38334  poimirlem7  38339  poimirlem16  38348  poimirlem17  38349  poimirlem19  38351  poimirlem20  38352  poimirlem24  38356  poimirlem31  38363  poimirlem32  38364  fdc  38458  mettrifi  38470  caushft  38474  cntotbnd  38509  fzsplitnd  42811  lcmineqlem6  42863  lcmineqlem18  42875  aks4d1p1p1  42892  aks4d1p8d3  42915  aks4d1p8  42916  primrootscoprmpow  42928  posbezout  42929  primrootscoprbij  42931  primrootspoweq0  42935  hashscontpow1  42950  aks6d1c3  42952  aks6d1c4  42953  aks6d1c5lem1  42965  aks6d1c5lem2  42967  sticksstones10  42984  sticksstones12a  42986  sticksstones12  42987  aks6d1c6lem3  43001  unitscyglem2  43025  unitscyglem4  43027  sumcubes  43151  oexpreposd  43160  exp11d  43164  dvdsexpb  43173  mzpsubmpt  43551  lzenom  43578  diophun  43581  eqrabdioph  43585  irrapxlem2  43627  irrapxlem3  43628  pellexlem6  43638  pell1234qrreccl  43658  pellfund14  43702  rmxyneg  43724  rmxyadd  43725  rmxp1  43736  rmxm1  43738  rmym1  43739  rmxluc  43740  rmyluc  43741  rmyluc2  43742  rmxdbl  43743  rmydbl  43744  congadd  43770  congsub  43774  congabseq  43778  acongrep  43784  acongeq  43787  jm2.18  43792  jm2.19lem1  43793  jm2.19lem2  43794  jm2.19lem3  43795  jm2.22  43799  jm2.23  43800  jm2.20nn  43801  jm2.25  43803  jm2.26lem3  43805  jm2.27c  43811  nzss  45104  hashnzfz  45107  hashnzfz2  45108  hashnzfzclim  45109  uzmptshftfval  45133  sineq0ALT  45722  fzisoeu  46096  fperiodmul  46100  monoord2xrv  46274  fmul01lt1lem2  46378  sumnnodd  46423  dvdsn1add  46730  dvnmul  46734  dvnprodlem1  46737  stoweidlem11  46802  stoweidlem26  46817  dirkertrigeqlem1  46889  dirkertrigeqlem2  46890  dirkertrigeqlem3  46891  dirkertrigeq  46892  dirkeritg  46893  fourierdlem26  46924  fourierdlem48  46945  fourierdlem49  46946  fourierdlem79  46976  fourierdlem91  46988  fourierdlem103  47000  fourierdlem104  47001  fouriersw  47022  etransclem1  47026  etransclem4  47029  etransclem8  47033  etransclem9  47034  etransclem15  47040  etransclem17  47042  etransclem18  47043  etransclem20  47045  etransclem21  47046  etransclem22  47047  etransclem23  47048  etransclem24  47049  etransclem25  47050  etransclem35  47060  etransclem38  47063  etransclem41  47066  etransclem44  47069  etransclem45  47070  etransclem46  47071  etransclem47  47072  etransclem48  47073  chnerlem2  47676  2elfz2melfz  48132  ceilbi  48151  flmrecm1  48157  fldivmod  48158  submodaddmod  48161  zplusmodne  48163  m1modne  48168  minusmod5ne  48169  submodlt  48170  minusmodnep2tmod  48173  m1modmmod  48178  modmkpkne  48181  modmknepk  48182  mod2addne  48184  modm2nep1  48186  modm1nep2  48188  modm1nem2  48189  2timesltsq  48192  fsumsplitsndif  48195  iccpartgtprec  48246  fargshiftf1  48267  fargshiftfo  48268  nprmmul3  48355  mod42tp1mod8  48431  sfprmdvdsmersenne  48432  lighneallem3  48436  lighneallem4b  48438  modexp2m1d  48441  nprmdvdsfacm1lem1  48449  ppivalnnprm  48454  dfodd6  48479  onego  48488  m1expoddALTV  48490  zofldiv2ALTV  48504  oddflALTV  48505  oexpnegALTV  48519  omoeALTV  48527  omeoALTV  48528  epoo  48545  emoo  48546  epee  48547  emee  48548  evensumeven  48549  evenltle  48559  even3prm2  48561  mogoldbblem  48562  fppr2odd  48573  fpprwppr  48581  fpprwpprb  48582  sbgoldbst  48620  sbgoldbaltlem2  48622  sgoldbeven3prm  48625  nnsum3primesprm  48632  nnsum4primesodd  48638  nnsum4primesoddALTV  48639  nnsum4primeseven  48642  nnsum4primesevenALTV  48643  bgoldbtbndlem2  48648  bgoldbtbndlem4  48650  bgoldbtbnd  48651  gpgedgvtx1  48904  gpgvtxedg0  48905  gpgvtxedg1  48906  gpg5nbgrvtx13starlem2  48914  gpg3nbgrvtx0  48918  pgnbgreunbgrlem2lem1  48956  pgnbgreunbgrlem2lem2  48957  pgnbgreunbgrlem2lem3  48958  2zrngamnd  49088  2zrngacmnd  49089  2zrngagrp  49090  2zrngALT  49095  2zrngnmlid  49096  2zrngnmlid2  49098  ztprmneprm  49203  altgsumbcALT  49209  zofldiv2  49387  fllogbd  49416  nnpw2blen  49436  blen1b  49444  blennngt2o2  49448  blennn0e2  49450  dig2nn1st  49461  dignn0flhalflem1  49471