Theorem zred 9465

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

Syntax hints:   -> wi 4   e. wcel 2167   RRcr 7895   ZZcz 9343

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 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928  df-neg 8217  df-z 9344

This theorem is referenced by:  zcnd  9466  btwnapz  9473  eluzelre  9628  eluzadd  9647  eluzsub  9648  uzm1  9649  z2ge  9918  zltaddlt1le  10099  fztri3or  10131  fznlem  10133  fzdisj  10144  fzpreddisj  10163  fznatpl1  10168  uzdisj  10185  fzm1  10192  fz0fzdiffz0  10222  elfzmlbm  10223  elfzmlbp  10224  difelfznle  10227  nn0disj  10230  elfzolt3  10250  fzonel  10253  fzouzdisj  10273  fzonmapblen  10280  fzoaddel  10285  elfzonelfzo  10323  zsupcl  10338  zssinfcl  10339  infssuzex  10340  suprzubdc  10343  zsupssdc  10345  suprzcl2dc  10346  qtri3or  10347  exbtwnzlemstep  10354  exbtwnzlemex  10356  exbtwnz  10357  rebtwn2zlemstep  10359  rebtwn2z  10361  qbtwnrelemcalc  10362  qbtwnre  10363  apbtwnz  10381  qfraclt1  10387  qfracge0  10388  flqge  10389  flid  10391  flqltnz  10394  flqwordi  10395  flqaddz  10404  flqmulnn0  10406  btwnzge0  10407  2tnp1ge0ge0  10408  flhalf  10409  flltdivnn0lt  10411  fldiv4p1lem1div2  10412  fldiv4lem1div2uz2  10413  ceiqge  10418  ceiqm1l  10420  ceiqle  10422  flqleceil  10426  flqeqceilz  10427  intfracq  10429  modqval  10433  modqge0  10441  modqlt  10442  modqmulnn  10451  mulp1mod1  10474  modaddmodup  10496  modaddmodlo  10497  modsumfzodifsn  10505  addmodlteq  10507  frec2uzlt2d  10513  frec2uzf1od  10515  uzennn  10545  seq3split  10597  iseqf1olemkle  10606  iseqf1olemqcl  10608  iseqf1olemnab  10610  iseqf1olemab  10611  iseqf1olemqk  10616  seq3f1olemqsumkj  10620  seq3f1olemqsumk  10621  seq3f1olemqsum  10622  seqf1oglem1  10628  seqf1oglem2  10629  seqfeq4g  10640  exp3val  10650  expcanlem  10824  expcan  10825  facavg  10855  bcval4  10861  bcp1nk  10871  bcval5  10872  zfz1isolemiso  10948  seq3coll  10951  iswrdiz  10959  seq3shft  11020  resqrexlemdecn  11194  fzomaxdiflem  11294  nn0maxcl  11407  fsum3cvg3  11578  fsumm1  11598  fsum1p  11600  fsum0diaglem  11622  isumshft  11672  isumsplit  11673  divcnv  11679  geolim2  11694  cvgratnnlemabsle  11709  cvgratnnlemsumlt  11710  cvgratnnlemrate  11712  cvgratz  11714  mertenslemi1  11717  fprodntrivap  11766  prodsnf  11774  fprod1p  11781  fprodeq0  11799  zdvdsdc  11994  dvdslelemd  12025  oexpneg  12059  ltoddhalfle  12075  divalglemnqt  12102  divalglemex  12104  divalglemeuneg  12105  flodddiv4t2lthalf  12121  bitsfzolem  12136  bitsfzo  12137  bitsmod  12138  bitscmp  12140  dvdsbnd  12148  dvdslegcd  12156  gcd0id  12171  gcdneg  12174  bezoutlemsup  12201  dfgcd2  12206  uzwodc  12229  nn0seqcvgd  12234  lcmgcdlem  12270  ncoprmgcdne1b  12282  nprm  12316  prmdc  12323  prmdvdsfz  12332  isprm5lem  12334  coprm  12337  prmexpb  12344  prmfac1  12345  znege1  12371  sqrt2irrap  12373  hashdvds  12414  eulerthlemrprm  12422  eulerthlema  12423  hashgcdlem  12431  pythagtriplem13  12470  pythagtriplem16  12473  pcxcl  12505  pcaddlem  12533  pcadd  12534  pcfac  12544  qexpz  12546  4sqlem7  12578  4sqlem10  12581  4sqexercise2  12593  4sqlemsdc  12594  4sqlem11  12595  4sqlem12  12596  4sqlem15  12599  4sqlem16  12600  4sqlem17  12601  oddennn  12634  ennnfoneleminc  12653  nninfdclemp1  12692  nninfdclemlt  12693  gsumfzval  13093  gsumfzz  13197  gsumfzcl  13201  mulgfng  13330  subgmulg  13394  gsumfzreidx  13543  gsumfzsubmcl  13544  gsumfzmptfidmadd  13545  gsumfzmhm  13549  gsumfzfsumlemm  14219  gsumfzfsum  14220  ltexp2  15261  logblt  15282  mersenne  15317  lgsval2lem  15335  lgsvalmod  15344  lgsneg  15349  lgsdilem  15352  lgssq  15365  lgssq2  15366  gausslemma2dlem1a  15383  gausslemma2dlem3  15388  lgseisenlem2  15396  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad3  15409  2lgslem1a2  15412  2sqlem3  15442  2sqlem8  15448  supfz  15802  inffz  15803