Theorem zred 9467

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 9352	. 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 7897   ZZcz 9345

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 8219  df-z 9346

This theorem is referenced by:  zcnd  9468  btwnapz  9475  eluzelre  9630  eluzadd  9649  eluzsub  9650  uzm1  9651  z2ge  9920  zltaddlt1le  10101  fztri3or  10133  fznlem  10135  fzdisj  10146  fzpreddisj  10165  fznatpl1  10170  uzdisj  10187  fzm1  10194  fz0fzdiffz0  10224  elfzmlbm  10225  elfzmlbp  10226  difelfznle  10229  nn0disj  10232  elfzolt3  10252  fzonel  10255  fzouzdisj  10275  fzonmapblen  10282  fzoaddel  10287  elfzonelfzo  10325  zsupcl  10340  zssinfcl  10341  infssuzex  10342  suprzubdc  10345  zsupssdc  10347  suprzcl2dc  10348  qtri3or  10349  exbtwnzlemstep  10356  exbtwnzlemex  10358  exbtwnz  10359  rebtwn2zlemstep  10361  rebtwn2z  10363  qbtwnrelemcalc  10364  qbtwnre  10365  apbtwnz  10383  qfraclt1  10389  qfracge0  10390  flqge  10391  flid  10393  flqltnz  10396  flqwordi  10397  flqaddz  10406  flqmulnn0  10408  btwnzge0  10409  2tnp1ge0ge0  10410  flhalf  10411  flltdivnn0lt  10413  fldiv4p1lem1div2  10414  fldiv4lem1div2uz2  10415  ceiqge  10420  ceiqm1l  10422  ceiqle  10424  flqleceil  10428  flqeqceilz  10429  intfracq  10431  modqval  10435  modqge0  10443  modqlt  10444  modqmulnn  10453  mulp1mod1  10476  modaddmodup  10498  modaddmodlo  10499  modsumfzodifsn  10507  addmodlteq  10509  frec2uzlt2d  10515  frec2uzf1od  10517  uzennn  10547  seq3split  10599  iseqf1olemkle  10608  iseqf1olemqcl  10610  iseqf1olemnab  10612  iseqf1olemab  10613  iseqf1olemqk  10618  seq3f1olemqsumkj  10622  seq3f1olemqsumk  10623  seq3f1olemqsum  10624  seqf1oglem1  10630  seqf1oglem2  10631  seqfeq4g  10642  exp3val  10652  expcanlem  10826  expcan  10827  facavg  10857  bcval4  10863  bcp1nk  10873  bcval5  10874  zfz1isolemiso  10950  seq3coll  10953  iswrdiz  10961  seq3shft  11022  resqrexlemdecn  11196  fzomaxdiflem  11296  nn0maxcl  11409  fsum3cvg3  11580  fsumm1  11600  fsum1p  11602  fsum0diaglem  11624  isumshft  11674  isumsplit  11675  divcnv  11681  geolim2  11696  cvgratnnlemabsle  11711  cvgratnnlemsumlt  11712  cvgratnnlemrate  11714  cvgratz  11716  mertenslemi1  11719  fprodntrivap  11768  prodsnf  11776  fprod1p  11783  fprodeq0  11801  zdvdsdc  11996  dvdslelemd  12027  oexpneg  12061  ltoddhalfle  12077  divalglemnqt  12104  divalglemex  12106  divalglemeuneg  12107  flodddiv4t2lthalf  12123  bitsfzolem  12138  bitsfzo  12139  bitsmod  12140  bitscmp  12142  dvdsbnd  12150  dvdslegcd  12158  gcd0id  12173  gcdneg  12176  bezoutlemsup  12203  dfgcd2  12208  uzwodc  12231  nn0seqcvgd  12236  lcmgcdlem  12272  ncoprmgcdne1b  12284  nprm  12318  prmdc  12325  prmdvdsfz  12334  isprm5lem  12336  coprm  12339  prmexpb  12346  prmfac1  12347  znege1  12373  sqrt2irrap  12375  hashdvds  12416  eulerthlemrprm  12424  eulerthlema  12425  hashgcdlem  12433  pythagtriplem13  12472  pythagtriplem16  12475  pcxcl  12507  pcaddlem  12535  pcadd  12536  pcfac  12546  qexpz  12548  4sqlem7  12580  4sqlem10  12583  4sqexercise2  12595  4sqlemsdc  12596  4sqlem11  12597  4sqlem12  12598  4sqlem15  12601  4sqlem16  12602  4sqlem17  12603  oddennn  12636  ennnfoneleminc  12655  nninfdclemp1  12694  nninfdclemlt  12695  gsumfzval  13095  gsumfzz  13199  gsumfzcl  13203  mulgfng  13332  subgmulg  13396  gsumfzreidx  13545  gsumfzsubmcl  13546  gsumfzmptfidmadd  13547  gsumfzmhm  13551  gsumfzfsumlemm  14221  gsumfzfsum  14222  ltexp2  15285  logblt  15306  mersenne  15341  lgsval2lem  15359  lgsvalmod  15368  lgsneg  15373  lgsdilem  15376  lgssq  15389  lgssq2  15390  gausslemma2dlem1a  15407  gausslemma2dlem3  15412  lgseisenlem2  15420  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428  lgsquad3  15433  2lgslem1a2  15436  2sqlem3  15466  2sqlem8  15472  supfz  15828  inffz  15829