Theorem zcnd 12720

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℂcc 11150  ℤcz 12610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-neg 11492  df-z 12611

This theorem is referenced by:  zsupss  12976  rpnnen1lem5  13020  fzm1  13643  fzrevral  13648  fzshftral  13651  nn0disj  13680  predfz  13689  fzoss2  13723  elfzo0suble  13742  fzo0addelr  13754  elfzoext  13757  fzosubel  13759  fzosubel3  13761  fzocatel  13764  fzosplitsnm1  13775  elfzom1elp1fzo1  13802  2tnp1ge0ge0  13865  quoremz  13891  intfrac2  13894  intfracq  13895  flpmodeq  13910  moddiffl  13918  modmul1  13961  modmul12d  13962  modfzo0difsn  13980  modsumfzodifsn  13981  addmodlteq  13983  uzrdgxfr  14004  fzen2  14006  monoord2  14070  seqf1olem1  14078  seqf1olem2  14079  seqz  14087  expaddzlem  14142  znsqcld  14198  modexp  14273  sqoddm1div8  14278  bcm1k  14350  bcp1nk  14352  bcval5  14353  bcpasc  14356  hashfz  14462  hashfzo  14464  hashfzp1  14466  hashbclem  14487  seqcoll  14499  ccatval3  14613  ccatlid  14620  ccatass  14622  ccatalpha  14627  swrdfv0  14683  swrdfv2  14695  swrds1  14700  ccatswrd  14702  pfxfv  14716  ccatpfx  14735  swrdpfx  14741  pfxccatin12lem2  14765  spllen  14788  revccat  14800  revrev  14801  cshwidxmod  14837  cshwidxm1  14841  cshweqrep  14855  2cshwcshw  14860  cshimadifsn0  14865  swrds2m  14976  seqshft  15120  fzomaxdif  15378  climshft2  15614  iserex  15689  isercoll2  15701  serf0  15713  iseraltlem2  15715  iseraltlem3  15716  iseralt  15717  sumrblem  15743  fsumm1  15783  fsumsplitsnun  15787  fsump1  15788  fsumshftm  15813  fsumrev2  15814  telfsumo  15834  fsumparts  15838  binomlem  15861  isumshft  15871  isumsplit  15872  isum1p  15873  arisum  15892  pwdif  15900  cvgrat  15915  mertenslem1  15916  ntrivcvg  15929  ntrivcvgtail  15932  prodrblem  15961  fprodser  15981  fprodm1  15999  fprodp1  16001  fprodrev  16009  fprodmodd  16029  fallfacval3  16044  fallfacfwd  16068  0fallfac  16069  binomfallfaclem2  16072  fallfacval4  16075  fsumkthpow  16088  eirrlem  16236  sqrt2irrlem  16280  addmulmodb  16299  dvds2ln  16322  dvdsadd2b  16339  fsumdvds  16341  fzocongeq  16357  addmodlteqALT  16358  dvdsexp  16361  dvdsmod  16362  3dvds  16364  fprodfvdvdsd  16367  odd2np1  16374  oddm1even  16376  oexpneg  16378  mod2eq1n2dvds  16380  mulsucdiv2z  16386  zob  16392  ltoddhalfle  16394  sumodd  16421  pwp1fsum  16424  divalglem0  16426  divalglem4  16429  divalglem8  16433  divalgb  16437  divalgmod  16439  modremain  16441  flodddiv4  16448  bitsp1  16464  bitsfzo  16468  bitsmod  16469  bitsinv1lem  16474  bitsf1  16479  sadaddlem  16499  bitsres  16506  bitsuz  16507  bitsshft  16508  smumullem  16525  modgcd  16565  gcdmultipled  16567  dvdsgcdidd  16570  bezoutlem1  16572  bezoutlem2  16573  bezoutlem3  16574  bezoutlem4  16575  dvdsmulgcd  16589  rplpwr  16591  lcmid  16642  absprodnn  16651  mulgcddvds  16688  divgcdcoprm0  16698  cncongr1  16700  cncongr2  16701  dvdszzq  16754  rpexp  16755  prmdvdsbc  16759  qmuldeneqnum  16780  numdensq  16787  qden1elz  16790  numdenexp  16793  hashdvds  16808  phiprm  16810  eulerthlem2  16815  fermltl  16817  prmdiv  16818  prmdiveq  16819  hashgcdlem  16821  odzdvds  16828  vfermltlALT  16835  modprm0  16838  modprmn0modprm0  16840  pythagtriplem6  16854  pythagtriplem7  16855  pythagtriplem15  16862  pcpremul  16876  pceulem  16878  pczpre  16880  pcdiv  16885  pcqmul  16886  pcqdiv  16890  pcexp  16892  pcaddlem  16921  pcadd  16922  fldivp1  16930  pcfac  16932  pcbc  16933  prmpwdvds  16937  prmreclem4  16952  4sqlem5  16975  4sqlem8  16978  4sqlem9  16979  4sqlem10  16980  4sqlem11  16988  4sqlem14  16991  4sqlem16  16993  4sqlem17  16994  vdwapun  17007  vdwnnlem2  17029  prmop1  17071  prmdvdsprmo  17075  prmgaplem7  17090  prmlem0  17139  mulgsubcl  19118  mulgdirlem  19135  mulgdir  19136  mulgass  19141  mulgmodid  19143  mulgsubdir  19144  psgnunilem5  19526  psgnunilem2  19527  psgnunilem4  19529  m1expaddsub  19530  psgnuni  19531  odnncl  19577  odmulg  19588  odbezout  19590  sylow1lem1  19630  sylow2alem2  19650  efgsres  19770  efgredleme  19775  efgredlemc  19777  odadd1  19880  odadd2  19881  cyggeninv  19915  gsummptshft  19968  ablfacrp  20100  pgpfac1lem3  20111  fincygsubgodd  20146  srgbinomlem3  20245  srgbinomlem4  20246  zringmulg  21484  zringlpirlem1  21490  zringlpirlem3  21492  prmirredlem  21500  fermltlchr  21561  zndvds0  21586  znf1o  21587  znunit  21599  cayhamlem1  22887  tgpmulg  24116  zdis  24851  uniioombllem3  25633  mbfi1fseqlem4  25767  dvexp3  26030  aareccl  26382  aalioulem1  26388  geolim3  26395  aaliou3lem2  26399  aaliou3lem6  26404  ulmshft  26447  sineq0  26580  efif1olem2  26599  igamz  27105  wilthlem1  27125  wilthlem2  27126  basellem3  27140  mumul  27238  musum  27248  musumsum  27249  muinv  27250  ppiub  27262  chtub  27270  logfac2  27275  chpchtsum  27277  dchrptlem1  27322  pcbcctr  27334  bcmono  27335  bposlem5  27346  bposlem6  27347  lgslem1  27355  lgsval2lem  27365  lgsval4a  27377  lgsneg  27379  lgsneg1  27380  lgsmod  27381  lgsdirprm  27389  lgsdir  27390  lgsdilem2  27391  lgsdi  27392  lgsne0  27393  lgsabs1  27394  lgssq  27395  lgssq2  27396  lgsmulsqcoprm  27401  lgsdirnn0  27402  lgsdinn0  27403  lgsqrlem1  27404  gausslemma2dlem1a  27423  gausslemma2dlem1  27424  gausslemma2dlem4  27427  gausslemma2dlem5a  27428  gausslemma2dlem5  27429  gausslemma2dlem6  27430  gausslemma2d  27432  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgseisenlem4  27436  lgsquadlem1  27438  lgsquad2lem1  27442  lgsquad3  27445  2lgslem1b  27450  2lgsoddprmlem2  27467  2sqlem3  27478  2sqlem4  27479  2sqlem8a  27483  2sqlem8  27484  2sqlem11  27487  2sqblem  27489  2sqn0  27492  2sqmod  27494  dchrisumlem1  27547  dchrmusum2  27552  dchrvmasumlem1  27553  dchrvmasum2lem  27554  mudivsum  27588  mulogsum  27590  mulog2sumlem2  27593  selberglem1  27603  selberglem3  27605  selberg  27606  pntpbnd2  27645  pntlemf  27663  padicabvcxp  27690  axlowdimlem14  28984  axlowdimlem16  28986  pthdadjvtx  29762  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  crctcshlem4  29849  crctcsh  29853  clwwlkccatlem  30017  clwwisshclwws  30043  eucrctshift  30271  fzm1ne1  32796  fzspl  32797  bcm1n  32802  fzom1ne1  32808  znumd  32818  zdend  32819  numdenneg  32820  divnumden2  32821  ltesubnnd  32828  ccatf1  32917  swrdrn3  32924  swrdf1  32925  cshwrnid  32930  chnlt  32986  gsumzrsum  33044  cycpmco2lem3  33130  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2  33135  archiabllem1  33182  archiabllem2c  33184  elrgspnlem1  33231  elrgspnlem2  33232  znfermltl  33373  zringidom  33558  zringfrac  33561  zrhnm  33929  cnzh  33930  rezh  33931  zrhcntr  33941  qqhval2lem  33943  qqhghm  33950  qqhrhm  33951  qqhnm  33952  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemic  34487  ballotlem1c  34488  ballotlemsgt1  34491  ballotlemsdom  34492  ballotlemsel1i  34493  ballotlemsf1o  34494  ballotlemsima  34496  ballotlemfrceq  34509  ballotlemfrcn0  34510  ballotlem1ri  34515  signsplypnf  34543  itgexpif  34599  fsum2dsub  34600  breprexplemc  34625  vtsprod  34632  circlemeth  34633  revpfxsfxrev  35099  swrdrevpfx  35100  revwlk  35108  swrdwlk  35110  divcnvlin  35712  fwddifnp1  36146  knoppndvlem2  36495  knoppndvlem7  36500  knoppndvlem14  36507  knoppndvlem16  36509  ltflcei  37594  poimirlem1  37607  poimirlem2  37608  poimirlem7  37613  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem24  37630  poimirlem31  37637  poimirlem32  37638  fdc  37731  mettrifi  37743  caushft  37747  cntotbnd  37782  fzsplitnd  41963  lcmineqlem6  42015  lcmineqlem18  42027  aks4d1p1p1  42044  aks4d1p8d3  42067  aks4d1p8  42068  primrootscoprmpow  42080  posbezout  42081  primrootscoprbij  42083  primrootspoweq0  42087  hashscontpow1  42102  aks6d1c3  42104  aks6d1c4  42105  aks6d1c5lem1  42117  aks6d1c5lem2  42119  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  aks6d1c6lem3  42153  unitscyglem2  42177  unitscyglem4  42179  metakunt12  42197  metakunt15  42200  metakunt16  42201  metakunt28  42213  sumcubes  42325  oexpreposd  42335  exp11d  42339  dvdsexpb  42348  mzpsubmpt  42730  lzenom  42757  diophun  42760  eqrabdioph  42764  irrapxlem2  42810  irrapxlem3  42811  pellexlem6  42821  pell1234qrreccl  42841  pellfund14  42885  rmxyneg  42908  rmxyadd  42909  rmxp1  42920  rmxm1  42922  rmym1  42923  rmxluc  42924  rmyluc  42925  rmyluc2  42926  rmxdbl  42927  rmydbl  42928  congadd  42954  congsub  42958  congabseq  42962  acongrep  42968  acongeq  42971  jm2.18  42976  jm2.19lem1  42977  jm2.19lem2  42978  jm2.19lem3  42979  jm2.22  42983  jm2.23  42984  jm2.20nn  42985  jm2.25  42987  jm2.26lem3  42989  jm2.27c  42995  nzss  44312  hashnzfz  44315  hashnzfz2  44316  hashnzfzclim  44317  uzmptshftfval  44341  sineq0ALT  44934  fzisoeu  45250  fperiodmul  45254  monoord2xrv  45433  fmul01lt1lem2  45540  sumnnodd  45585  dvdsn1add  45894  dvnmul  45898  dvnprodlem1  45901  stoweidlem11  45966  stoweidlem26  45981  dirkertrigeqlem1  46053  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkeritg  46057  fourierdlem26  46088  fourierdlem48  46109  fourierdlem49  46110  fourierdlem79  46140  fourierdlem91  46152  fourierdlem103  46164  fourierdlem104  46165  fouriersw  46186  etransclem1  46190  etransclem4  46193  etransclem8  46197  etransclem9  46198  etransclem15  46204  etransclem17  46206  etransclem18  46207  etransclem20  46209  etransclem21  46210  etransclem22  46211  etransclem23  46212  etransclem24  46213  etransclem25  46214  etransclem35  46224  etransclem38  46227  etransclem41  46230  etransclem44  46233  etransclem45  46234  etransclem46  46235  etransclem47  46236  etransclem48  46237  2elfz2melfz  47267  fldivmod  47277  submodaddmod  47280  zplusmodne  47282  m1modne  47287  minusmod5ne  47288  submodlt  47289  minusmodnep2tmod  47292  fsumsplitsndif  47297  iccpartgtprec  47344  fargshiftf1  47365  fargshiftfo  47366  mod42tp1mod8  47526  sfprmdvdsmersenne  47527  lighneallem3  47531  lighneallem4b  47533  modexp2m1d  47536  dfodd6  47561  onego  47570  m1expoddALTV  47572  zofldiv2ALTV  47586  oddflALTV  47587  oexpnegALTV  47601  omoeALTV  47609  omeoALTV  47610  epoo  47627  emoo  47628  epee  47629  emee  47630  evensumeven  47631  evenltle  47641  even3prm2  47643  mogoldbblem  47644  fppr2odd  47655  fpprwppr  47663  fpprwpprb  47664  sbgoldbst  47702  sbgoldbaltlem2  47704  sgoldbeven3prm  47707  nnsum3primesprm  47714  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  bgoldbtbndlem2  47730  bgoldbtbndlem4  47732  bgoldbtbnd  47733  gpgedgvtx1  47954  gpgvtxedg0  47955  gpgvtxedg1  47956  gpg3nbgrvtxlem  47957  gpg5nbgrvtx13starlem2  47962  gpg3nbgrvtx0  47966  2zrngamnd  48090  2zrngacmnd  48091  2zrngagrp  48092  2zrngALT  48097  2zrngnmlid  48098  2zrngnmlid2  48100  ztprmneprm  48191  altgsumbcALT  48197  m1modmmod  48370  zofldiv2  48380  fllogbd  48409  nnpw2blen  48429  blen1b  48437  blennngt2o2  48441  blennn0e2  48443  dig2nn1st  48454  dignn0flhalflem1  48464