Theorem zred 9602

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

Hypothesis

Ref	Expression
zred.1	|- ( ph -> A e. ZZ )

Assertion

Ref	Expression
zred	|- ( ph -> A e. RR )

Proof of Theorem zred

Step	Hyp	Ref	Expression
1		zssre 9486	. 2 |- ZZ C_ RR
2		zred.1	. 2 |- ( ph -> A e. ZZ )
3	1, 2	sselid 3225	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8031   ZZcz 9479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021  df-neg 8353  df-z 9480

This theorem is referenced by:  zcnd  9603  btwnapz  9610  eluzmn  9762  eluzelre  9766  eluzadd  9785  eluzsub  9786  uzm1  9787  z2ge  10061  zltaddlt1le  10242  fztri3or  10274  fznlem  10276  fzdisj  10287  fzpreddisj  10306  fznatpl1  10311  uzdisj  10328  fzm1  10335  fz0fzdiffz0  10365  elfzmlbm  10366  elfzmlbp  10367  difelfznle  10370  nn0disj  10373  elfzolt3  10393  fzonel  10396  fzouzdisj  10417  fzodisjsn  10419  fzonmapblen  10427  fzoaddel  10433  elincfzoext  10439  elfzonelfzo  10476  zsupcl  10492  zssinfcl  10493  infssuzex  10494  suprzubdc  10497  zsupssdc  10499  suprzcl2dc  10500  qtri3or  10501  exbtwnzlemstep  10508  exbtwnzlemex  10510  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2z  10515  qbtwnrelemcalc  10516  qbtwnre  10517  apbtwnz  10535  qfraclt1  10541  qfracge0  10542  flqge  10543  flid  10545  flqltnz  10548  flqwordi  10549  flqaddz  10558  flqmulnn0  10560  btwnzge0  10561  2tnp1ge0ge0  10562  flhalf  10563  flltdivnn0lt  10565  fldiv4p1lem1div2  10566  fldiv4lem1div2uz2  10567  ceiqge  10572  ceiqm1l  10574  ceiqle  10576  flqleceil  10580  flqeqceilz  10581  intfracq  10583  modqval  10587  modqge0  10595  modqlt  10596  modqmulnn  10605  mulp1mod1  10628  modaddmodup  10650  modaddmodlo  10651  modsumfzodifsn  10659  addmodlteq  10661  frec2uzlt2d  10667  frec2uzf1od  10669  uzennn  10699  seq3split  10751  iseqf1olemkle  10760  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemab  10765  iseqf1olemqk  10770  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seqf1oglem1  10782  seqf1oglem2  10783  seqfeq4g  10794  exp3val  10804  expcanlem  10978  expcan  10979  facavg  11009  bcval4  11015  bcp1nk  11025  bcval5  11026  zfz1isolemiso  11104  seq3coll  11107  iswrdiz  11121  ccatrn  11187  ccatalpha  11191  seq3shft  11400  resqrexlemdecn  11574  fzomaxdiflem  11674  nn0maxcl  11787  fsum3cvg3  11959  fsumm1  11979  fsum1p  11981  fsum0diaglem  12003  isumshft  12053  isumsplit  12054  divcnv  12060  geolim2  12075  cvgratnnlemabsle  12090  cvgratnnlemsumlt  12091  cvgratnnlemrate  12093  cvgratz  12095  mertenslemi1  12098  fprodntrivap  12147  prodsnf  12155  fprod1p  12162  fprodeq0  12180  zdvdsdc  12375  dvdslelemd  12406  oexpneg  12440  ltoddhalfle  12456  divalglemnqt  12483  divalglemex  12485  divalglemeuneg  12486  flodddiv4t2lthalf  12502  bitsfzolem  12517  bitsfzo  12518  bitsmod  12519  bitscmp  12521  dvdsbnd  12529  dvdslegcd  12537  gcd0id  12552  gcdneg  12555  bezoutlemsup  12582  dfgcd2  12587  uzwodc  12610  nn0seqcvgd  12615  lcmgcdlem  12651  ncoprmgcdne1b  12663  nprm  12697  prmdc  12704  prmdvdsfz  12713  isprm5lem  12715  coprm  12718  prmexpb  12725  prmfac1  12726  znege1  12752  sqrt2irrap  12754  hashdvds  12795  eulerthlemrprm  12803  eulerthlema  12804  hashgcdlem  12812  pythagtriplem13  12851  pythagtriplem16  12854  pcxcl  12886  pcaddlem  12914  pcadd  12915  pcfac  12925  qexpz  12927  4sqlem7  12959  4sqlem10  12962  4sqexercise2  12974  4sqlemsdc  12975  4sqlem11  12976  4sqlem12  12977  4sqlem15  12980  4sqlem16  12981  4sqlem17  12982  oddennn  13015  ennnfoneleminc  13034  nninfdclemp1  13073  nninfdclemlt  13074  gsumfzval  13476  gsumfzz  13580  gsumfzcl  13584  mulgfng  13713  subgmulg  13777  gsumfzreidx  13926  gsumfzsubmcl  13927  gsumfzmptfidmadd  13928  gsumfzmhm  13932  gsumsplit0  13935  gsumfzfsumlemm  14604  gsumfzfsum  14605  ltexp2  15668  logblt  15689  mersenne  15724  lgsval2lem  15742  lgsvalmod  15751  lgsneg  15756  lgsdilem  15759  lgssq  15772  lgssq2  15773  gausslemma2dlem1a  15790  gausslemma2dlem3  15795  lgseisenlem2  15803  lgsquadlem1  15809  lgsquadlem2  15810  lgsquadlem3  15811  lgsquad3  15816  2lgslem1a2  15819  2sqlem3  15849  2sqlem8  15855  supfz  16692  inffz  16693  gsumgfsumlem  16700