Theorem zred 9448

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 9333	. 2 |- ZZ C_ RR
2		zred.1	. 2 |- ( ph -> A e. ZZ )
3	1, 2	sselid 3181	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2167   RRcr 7878   ZZcz 9326

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-rab 2484  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266  df-ov 5925  df-neg 8200  df-z 9327

This theorem is referenced by:  zcnd  9449  btwnapz  9456  eluzelre  9611  eluzadd  9630  eluzsub  9631  uzm1  9632  z2ge  9901  zltaddlt1le  10082  fztri3or  10114  fznlem  10116  fzdisj  10127  fzpreddisj  10146  fznatpl1  10151  uzdisj  10168  fzm1  10175  fz0fzdiffz0  10205  elfzmlbm  10206  elfzmlbp  10207  difelfznle  10210  nn0disj  10213  elfzolt3  10233  fzonel  10236  fzouzdisj  10256  fzonmapblen  10263  fzoaddel  10268  elfzonelfzo  10306  zsupcl  10321  zssinfcl  10322  infssuzex  10323  suprzubdc  10326  zsupssdc  10328  suprzcl2dc  10329  qtri3or  10330  exbtwnzlemstep  10337  exbtwnzlemex  10339  exbtwnz  10340  rebtwn2zlemstep  10342  rebtwn2z  10344  qbtwnrelemcalc  10345  qbtwnre  10346  apbtwnz  10364  qfraclt1  10370  qfracge0  10371  flqge  10372  flid  10374  flqltnz  10377  flqwordi  10378  flqaddz  10387  flqmulnn0  10389  btwnzge0  10390  2tnp1ge0ge0  10391  flhalf  10392  flltdivnn0lt  10394  fldiv4p1lem1div2  10395  fldiv4lem1div2uz2  10396  ceiqge  10401  ceiqm1l  10403  ceiqle  10405  flqleceil  10409  flqeqceilz  10410  intfracq  10412  modqval  10416  modqge0  10424  modqlt  10425  modqmulnn  10434  mulp1mod1  10457  modaddmodup  10479  modaddmodlo  10480  modsumfzodifsn  10488  addmodlteq  10490  frec2uzlt2d  10496  frec2uzf1od  10498  uzennn  10528  seq3split  10580  iseqf1olemkle  10589  iseqf1olemqcl  10591  iseqf1olemnab  10593  iseqf1olemab  10594  iseqf1olemqk  10599  seq3f1olemqsumkj  10603  seq3f1olemqsumk  10604  seq3f1olemqsum  10605  seqf1oglem1  10611  seqf1oglem2  10612  seqfeq4g  10623  exp3val  10633  expcanlem  10807  expcan  10808  facavg  10838  bcval4  10844  bcp1nk  10854  bcval5  10855  zfz1isolemiso  10931  seq3coll  10934  iswrdiz  10942  seq3shft  11003  resqrexlemdecn  11177  fzomaxdiflem  11277  nn0maxcl  11390  fsum3cvg3  11561  fsumm1  11581  fsum1p  11583  fsum0diaglem  11605  isumshft  11655  isumsplit  11656  divcnv  11662  geolim2  11677  cvgratnnlemabsle  11692  cvgratnnlemsumlt  11693  cvgratnnlemrate  11695  cvgratz  11697  mertenslemi1  11700  fprodntrivap  11749  prodsnf  11757  fprod1p  11764  fprodeq0  11782  zdvdsdc  11977  dvdslelemd  12008  oexpneg  12042  ltoddhalfle  12058  divalglemnqt  12085  divalglemex  12087  divalglemeuneg  12088  flodddiv4t2lthalf  12104  bitsfzolem  12118  bitsfzo  12119  dvdsbnd  12123  dvdslegcd  12131  gcd0id  12146  gcdneg  12149  bezoutlemsup  12176  dfgcd2  12181  uzwodc  12204  nn0seqcvgd  12209  lcmgcdlem  12245  ncoprmgcdne1b  12257  nprm  12291  prmdc  12298  prmdvdsfz  12307  isprm5lem  12309  coprm  12312  prmexpb  12319  prmfac1  12320  znege1  12346  sqrt2irrap  12348  hashdvds  12389  eulerthlemrprm  12397  eulerthlema  12398  hashgcdlem  12406  pythagtriplem13  12445  pythagtriplem16  12448  pcxcl  12480  pcaddlem  12508  pcadd  12509  pcfac  12519  qexpz  12521  4sqlem7  12553  4sqlem10  12556  4sqexercise2  12568  4sqlemsdc  12569  4sqlem11  12570  4sqlem12  12571  4sqlem15  12574  4sqlem16  12575  4sqlem17  12576  oddennn  12609  ennnfoneleminc  12628  nninfdclemp1  12667  nninfdclemlt  12668  gsumfzval  13034  gsumfzz  13127  gsumfzcl  13131  mulgfng  13254  subgmulg  13318  gsumfzreidx  13467  gsumfzsubmcl  13468  gsumfzmptfidmadd  13469  gsumfzmhm  13473  gsumfzfsumlemm  14143  gsumfzfsum  14144  ltexp2  15177  logblt  15198  mersenne  15233  lgsval2lem  15251  lgsvalmod  15260  lgsneg  15265  lgsdilem  15268  lgssq  15281  lgssq2  15282  gausslemma2dlem1a  15299  gausslemma2dlem3  15304  lgseisenlem2  15312  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad3  15325  2lgslem1a2  15328  2sqlem3  15358  2sqlem8  15364  supfz  15715  inffz  15716