Theorem zred 9601

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 9485	. 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 8030   ZZcz 9478

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 6020  df-neg 8352  df-z 9479

This theorem is referenced by:  zcnd  9602  btwnapz  9609  eluzmn  9761  eluzelre  9765  eluzadd  9784  eluzsub  9785  uzm1  9786  z2ge  10060  zltaddlt1le  10241  fztri3or  10273  fznlem  10275  fzdisj  10286  fzpreddisj  10305  fznatpl1  10310  uzdisj  10327  fzm1  10334  fz0fzdiffz0  10364  elfzmlbm  10365  elfzmlbp  10366  difelfznle  10369  nn0disj  10372  elfzolt3  10392  fzonel  10395  fzouzdisj  10416  fzodisjsn  10418  fzonmapblen  10425  fzoaddel  10431  elincfzoext  10437  elfzonelfzo  10474  zsupcl  10490  zssinfcl  10491  infssuzex  10492  suprzubdc  10495  zsupssdc  10497  suprzcl2dc  10498  qtri3or  10499  exbtwnzlemstep  10506  exbtwnzlemex  10508  exbtwnz  10509  rebtwn2zlemstep  10511  rebtwn2z  10513  qbtwnrelemcalc  10514  qbtwnre  10515  apbtwnz  10533  qfraclt1  10539  qfracge0  10540  flqge  10541  flid  10543  flqltnz  10546  flqwordi  10547  flqaddz  10556  flqmulnn0  10558  btwnzge0  10559  2tnp1ge0ge0  10560  flhalf  10561  flltdivnn0lt  10563  fldiv4p1lem1div2  10564  fldiv4lem1div2uz2  10565  ceiqge  10570  ceiqm1l  10572  ceiqle  10574  flqleceil  10578  flqeqceilz  10579  intfracq  10581  modqval  10585  modqge0  10593  modqlt  10594  modqmulnn  10603  mulp1mod1  10626  modaddmodup  10648  modaddmodlo  10649  modsumfzodifsn  10657  addmodlteq  10659  frec2uzlt2d  10665  frec2uzf1od  10667  uzennn  10697  seq3split  10749  iseqf1olemkle  10758  iseqf1olemqcl  10760  iseqf1olemnab  10762  iseqf1olemab  10763  iseqf1olemqk  10768  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seq3f1olemqsum  10774  seqf1oglem1  10780  seqf1oglem2  10781  seqfeq4g  10792  exp3val  10802  expcanlem  10976  expcan  10977  facavg  11007  bcval4  11013  bcp1nk  11023  bcval5  11024  zfz1isolemiso  11102  seq3coll  11105  iswrdiz  11119  ccatrn  11185  ccatalpha  11189  seq3shft  11398  resqrexlemdecn  11572  fzomaxdiflem  11672  nn0maxcl  11785  fsum3cvg3  11956  fsumm1  11976  fsum1p  11978  fsum0diaglem  12000  isumshft  12050  isumsplit  12051  divcnv  12057  geolim2  12072  cvgratnnlemabsle  12087  cvgratnnlemsumlt  12088  cvgratnnlemrate  12090  cvgratz  12092  mertenslemi1  12095  fprodntrivap  12144  prodsnf  12152  fprod1p  12159  fprodeq0  12177  zdvdsdc  12372  dvdslelemd  12403  oexpneg  12437  ltoddhalfle  12453  divalglemnqt  12480  divalglemex  12482  divalglemeuneg  12483  flodddiv4t2lthalf  12499  bitsfzolem  12514  bitsfzo  12515  bitsmod  12516  bitscmp  12518  dvdsbnd  12526  dvdslegcd  12534  gcd0id  12549  gcdneg  12552  bezoutlemsup  12579  dfgcd2  12584  uzwodc  12607  nn0seqcvgd  12612  lcmgcdlem  12648  ncoprmgcdne1b  12660  nprm  12694  prmdc  12701  prmdvdsfz  12710  isprm5lem  12712  coprm  12715  prmexpb  12722  prmfac1  12723  znege1  12749  sqrt2irrap  12751  hashdvds  12792  eulerthlemrprm  12800  eulerthlema  12801  hashgcdlem  12809  pythagtriplem13  12848  pythagtriplem16  12851  pcxcl  12883  pcaddlem  12911  pcadd  12912  pcfac  12922  qexpz  12924  4sqlem7  12956  4sqlem10  12959  4sqexercise2  12971  4sqlemsdc  12972  4sqlem11  12973  4sqlem12  12974  4sqlem15  12977  4sqlem16  12978  4sqlem17  12979  oddennn  13012  ennnfoneleminc  13031  nninfdclemp1  13070  nninfdclemlt  13071  gsumfzval  13473  gsumfzz  13577  gsumfzcl  13581  mulgfng  13710  subgmulg  13774  gsumfzreidx  13923  gsumfzsubmcl  13924  gsumfzmptfidmadd  13925  gsumfzmhm  13929  gsumfzfsumlemm  14600  gsumfzfsum  14601  ltexp2  15664  logblt  15685  mersenne  15720  lgsval2lem  15738  lgsvalmod  15747  lgsneg  15752  lgsdilem  15755  lgssq  15768  lgssq2  15769  gausslemma2dlem1a  15786  gausslemma2dlem3  15791  lgseisenlem2  15799  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad3  15812  2lgslem1a2  15815  2sqlem3  15845  2sqlem8  15851  supfz  16675  inffz  16676  gsumgfsumlem  16683