Theorem zred 9772

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   RRcr 8178   ZZcz 9648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-rab 2537  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088  df-neg 8501  df-z 9649

This theorem is used by:  zcnd  9773  btwnapz  9780  eluzmn  9937  eluzelre  9941  eluzadd  9960  eluzsub  9961  uzm1  9962  ltesubnnd  10180  z2ge  10238  zltaddlt1le  10420  fztri3or  10453  fznlem  10455  fzdisj  10467  fzpreddisj  10488  fznatpl1  10493  uzdisj  10510  fzm1  10517  fz0fzdiffz0  10547  elfzmlbm  10548  elfzmlbp  10549  difelfznle  10552  nn0disj  10555  elfzolt3  10575  fzonel  10578  fzouzdisj  10599  fzodisjsn  10601  fzonmapblen  10609  fzoaddel  10615  elincfzoext  10621  elfzonelfzo  10658  zsupcl  10674  zssinfcl  10675  infssuzex  10676  suprzubdc  10681  zsupssdc  10683  suprzcl2dc  10684  qtri3or  10685  exbtwnzlemstep  10692  exbtwnzlemex  10694  exbtwnz  10695  rebtwn2zlemstep  10697  rebtwn2z  10699  qbtwnrelemcalc  10700  qbtwnre  10701  apbtwnz  10719  qfraclt1  10727  qfracge0  10728  flqge  10729  flapge  10730  flid  10732  flqltnz  10735  flqwordi  10736  flqaddz  10745  flqmulnn0  10747  btwnzge0  10748  2tnp1ge0ge0  10749  flhalf  10750  flltdivnn0lt  10752  fldiv4p1lem1div2  10753  fldiv4lem1div2uz2  10754  ceiqge  10759  ceiqm1l  10761  ceiqle  10763  flqleceil  10767  flqeqceilz  10768  intfracq  10770  modqval  10774  modqge0  10782  modqlt  10783  modqmulnn  10792  mulp1mod1  10815  modaddmodup  10837  modaddmodlo  10838  modsumfzodifsn  10846  addmodlteq  10848  frec2uzlt2d  10854  frec2uzf1od  10856  uzennn  10886  seq3split  10938  iseqf1olemkle  10947  iseqf1olemqcl  10949  iseqf1olemnab  10951  iseqf1olemab  10952  iseqf1olemqk  10957  seq3f1olemqsumkj  10961  seq3f1olemqsumk  10962  seq3f1olemqsum  10963  seqf1oglem1  10969  seqf1oglem2  10970  seqfeq4g  10981  exp3val  10991  expcanlem  11167  expcan  11168  facavg  11198  bcval4  11204  bcp1nk  11214  bcval5  11215  bcm1n  11221  zfz1isolemiso  11305  seq3coll  11308  iswrdiz  11325  ccatrn  11391  ccatalpha  11395  seq3shft  11617  resqrexlemdecn  11792  fzomaxdiflem  11893  nn0maxcl  12006  fsum3cvg3  12179  fsumm1  12199  fsum1p  12201  fsum0diaglem  12223  isumshft  12273  isumsplit  12274  divcnv  12280  geolim2  12295  cvgratnnlemabsle  12310  cvgratnnlemsumlt  12311  cvgratnnlemrate  12313  cvgratz  12315  mertenslemi1  12318  fprodntrivap  12367  prodsnf  12375  fprod1p  12382  fprodeq0  12400  zdvdsdc  12595  dvdslelemd  12626  oexpneg  12660  ltoddhalfle  12676  divalglemnqt  12703  divalglemex  12705  divalglemeuneg  12706  flodddiv4t2lthalf  12722  bitsfzolem  12737  bitsfzo  12738  bitsmod  12739  bitscmp  12741  dvdsbnd  12749  dvdslegcd  12757  gcd0id  12772  gcdneg  12775  bezoutlemsup  12802  dfgcd2  12807  uzwodc  12830  nn0seqcvgd  12835  lcmgcdlem  12871  ncoprmgcdne1b  12883  nprm  12917  prmdc  12924  prmdvdsfz  12934  isprm5lem  12936  coprm  12939  prmexpb  12946  prmfac1  12947  znege1  12974  sqrt2irrap  12976  hashdvds  13019  eulerthlemrprm  13027  eulerthlema  13028  hashgcdlem  13036  pythagtriplem13  13075  pythagtriplem16  13078  pcxcl  13110  pcaddlem  13138  pcadd  13139  pcfac  13149  qexpz  13151  4sqlem7  13183  4sqlem10  13186  4sqexercise2  13198  4sqlemsdc  13199  4sqlem11  13200  4sqlem12  13201  4sqlem15  13204  4sqlem16  13205  4sqlem17  13206  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemimin  13298  ballotfilemsgt1  13303  ballotfilemsel1i  13305  ballotfilemsi  13307  ballotfilemsima  13308  ballotfilemgun  13317  ballotfilemfrceq  13321  ballotfilemfrcn0  13322  ballotfilemirc  13324  oddennn  13332  ennnfoneleminc  13351  nninfdclemp1  13390  nninfdclemlt  13391  gzsumfzval  13760  gzsumcl  13853  mulgfng  13976  subgmulg  14040  gzsumreidx  14190  gzsumsubmcl  14191  gzsummhm  14194  gzsumsplit0  14197  gzsumshift  14198  ltexp2  16096  logblt  16117  ppiqfi  16158  ppidif  16175  ppiqub  16194  mersenne  16195  bcmono  16202  bcmax  16203  prmefexple  16206  bposlem1  16209  bposlem3  16211  bposlem4  16212  bposlem5  16213  lgsval2lem  16227  lgsvalmod  16236  lgsneg  16241  lgsdilem  16244  lgssq  16257  lgssq2  16258  gausslemma2dlem1a  16275  gausslemma2dlem3  16280  lgseisenlem2  16288  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad3  16301  2lgslem1a2  16304  2sqlem3  16334  2sqlem8  16340  supfz  17219  inffz  17220