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  11124  ccatrn  11190  ccatalpha  11194  seq3shft  11416  resqrexlemdecn  11590  fzomaxdiflem  11690  nn0maxcl  11803  fsum3cvg3  11975  fsumm1  11995  fsum1p  11997  fsum0diaglem  12019  isumshft  12069  isumsplit  12070  divcnv  12076  geolim2  12091  cvgratnnlemabsle  12106  cvgratnnlemsumlt  12107  cvgratnnlemrate  12109  cvgratz  12111  mertenslemi1  12114  fprodntrivap  12163  prodsnf  12171  fprod1p  12178  fprodeq0  12196  zdvdsdc  12391  dvdslelemd  12422  oexpneg  12456  ltoddhalfle  12472  divalglemnqt  12499  divalglemex  12501  divalglemeuneg  12502  flodddiv4t2lthalf  12518  bitsfzolem  12533  bitsfzo  12534  bitsmod  12535  bitscmp  12537  dvdsbnd  12545  dvdslegcd  12553  gcd0id  12568  gcdneg  12571  bezoutlemsup  12598  dfgcd2  12603  uzwodc  12626  nn0seqcvgd  12631  lcmgcdlem  12667  ncoprmgcdne1b  12679  nprm  12713  prmdc  12720  prmdvdsfz  12729  isprm5lem  12731  coprm  12734  prmexpb  12741  prmfac1  12742  znege1  12768  sqrt2irrap  12770  hashdvds  12811  eulerthlemrprm  12819  eulerthlema  12820  hashgcdlem  12828  pythagtriplem13  12867  pythagtriplem16  12870  pcxcl  12902  pcaddlem  12930  pcadd  12931  pcfac  12941  qexpz  12943  4sqlem7  12975  4sqlem10  12978  4sqexercise2  12990  4sqlemsdc  12991  4sqlem11  12992  4sqlem12  12993  4sqlem15  12996  4sqlem16  12997  4sqlem17  12998  oddennn  13031  ennnfoneleminc  13050  nninfdclemp1  13089  nninfdclemlt  13090  gsumfzval  13492  gsumfzz  13596  gsumfzcl  13600  mulgfng  13729  subgmulg  13793  gsumfzreidx  13942  gsumfzsubmcl  13943  gsumfzmptfidmadd  13944  gsumfzmhm  13948  gsumsplit0  13951  gsumfzfsumlemm  14620  gsumfzfsum  14621  ltexp2  15684  logblt  15705  mersenne  15740  lgsval2lem  15758  lgsvalmod  15767  lgsneg  15772  lgsdilem  15775  lgssq  15788  lgssq2  15789  gausslemma2dlem1a  15806  gausslemma2dlem3  15811  lgseisenlem2  15819  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad3  15832  2lgslem1a2  15835  2sqlem3  15865  2sqlem8  15871  supfz  16727  inffz  16728  gsumgfsumlem  16735