Theorem zred 9773

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 9656	. 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 8179   ZZcz 9649

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 8502  df-z 9650

This theorem is used by:  zcnd  9774  btwnapz  9781  eluzmn  9938  eluzelre  9942  eluzadd  9961  eluzsub  9962  uzm1  9963  ltesubnnd  10181  z2ge  10239  zltaddlt1le  10421  fztri3or  10454  fznlem  10456  fzdisj  10468  fzpreddisj  10489  fznatpl1  10494  uzdisj  10511  fzm1  10518  fz0fzdiffz0  10548  elfzmlbm  10549  elfzmlbp  10550  difelfznle  10553  nn0disj  10556  elfzolt3  10576  fzonel  10579  fzouzdisj  10600  fzodisjsn  10602  fzonmapblen  10610  fzoaddel  10616  elincfzoext  10622  elfzonelfzo  10659  zsupcl  10675  zssinfcl  10676  infssuzex  10677  suprzubdc  10682  zsupssdc  10684  suprzcl2dc  10685  qtri3or  10686  exbtwnzlemstep  10693  exbtwnzlemex  10695  exbtwnz  10696  rebtwn2zlemstep  10698  rebtwn2z  10700  qbtwnrelemcalc  10701  qbtwnre  10702  apbtwnz  10720  qfraclt1  10728  qfracge0  10729  flqge  10730  flapge  10731  flaplt  10733  flid  10734  flqltnz  10737  flqwordi  10738  flqaddz  10747  flqmulnn0  10749  btwnzge0  10750  2tnp1ge0ge0  10751  flhalf  10752  flltdivnn0lt  10754  fldiv4p1lem1div2  10755  fldiv4lem1div2uz2  10756  ceiqge  10761  ceiqm1l  10763  ceiqle  10765  flqleceil  10769  flqeqceilz  10770  intfracq  10772  modqval  10776  modqge0  10784  modqlt  10785  modqmulnn  10794  mulp1mod1  10817  modaddmodup  10839  modaddmodlo  10840  modsumfzodifsn  10848  addmodlteq  10850  frec2uzlt2d  10856  frec2uzf1od  10858  uzennn  10888  seq3split  10940  iseqf1olemkle  10949  iseqf1olemqcl  10951  iseqf1olemnab  10953  iseqf1olemab  10954  iseqf1olemqk  10959  seq3f1olemqsumkj  10963  seq3f1olemqsumk  10964  seq3f1olemqsum  10965  seqf1oglem1  10971  seqf1oglem2  10972  seqfeq4g  10983  exp3val  10993  expcanlem  11169  expcan  11170  facavg  11200  bcval4  11206  bcp1nk  11216  bcval5  11217  bcm1n  11223  zfz1isolemiso  11307  seq3coll  11310  iswrdiz  11327  ccatrn  11393  ccatalpha  11397  seq3shft  11619  resqrexlemdecn  11794  fzomaxdiflem  11895  nn0maxcl  12008  fiidxsupcl  12012  fsum3cvg3  12182  fsumm1  12202  fsum1p  12204  fsum0diaglem  12226  isumshft  12276  isumsplit  12277  divcnv  12283  geolim2  12298  cvgratnnlemabsle  12313  cvgratnnlemsumlt  12314  cvgratnnlemrate  12316  cvgratz  12318  mertenslemi1  12321  fprodntrivap  12370  prodsnf  12378  fprod1p  12385  fprodeq0  12403  zdvdsdc  12598  dvdslelemd  12629  oexpneg  12663  ltoddhalfle  12679  divalglemnqt  12706  divalglemex  12708  divalglemeuneg  12709  flodddiv4t2lthalf  12725  bitsfzolem  12740  bitsfzo  12741  bitsmod  12742  bitscmp  12744  dvdsbnd  12752  dvdslegcd  12760  gcd0id  12775  gcdneg  12778  bezoutlemsup  12805  dfgcd2  12810  uzwodc  12833  nn0seqcvgd  12838  lcmgcdlem  12874  ncoprmgcdne1b  12886  nprm  12920  prmdc  12927  prmdvdsfz  12937  isprm5lem  12939  coprm  12942  prmexpb  12949  prmfac1  12950  znege1  12977  sqrt2irrap  12979  hashdvds  13022  eulerthlemrprm  13030  eulerthlema  13031  hashgcdlem  13039  pythagtriplem13  13078  pythagtriplem16  13081  pcxcl  13113  pcaddlem  13141  pcadd  13142  pcfac  13152  qexpz  13154  4sqlem7  13186  4sqlem10  13189  4sqexercise2  13201  4sqlemsdc  13202  4sqlem11  13203  4sqlem12  13204  4sqlem15  13207  4sqlem16  13208  4sqlem17  13209  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemimin  13301  ballotfilemsgt1  13306  ballotfilemsel1i  13308  ballotfilemsi  13310  ballotfilemsima  13311  ballotfilemgun  13320  ballotfilemfrceq  13324  ballotfilemfrcn0  13325  ballotfilemirc  13327  oddennn  13335  ennnfoneleminc  13354  nninfdclemp1  13393  nninfdclemlt  13394  gzsumfzval  13764  gzsumcl  13857  mulgfng  13980  subgmulg  14044  gzsumreidx  14225  gzsumsubmcl  14226  gzsummhm  14229  gzsumsplit0  14232  gzsumshift  14233  psrbaglefifi  15147  ltexp2  16138  logblt  16159  ppiqfi  16203  chtdif  16225  ppidif  16230  ppiqub  16254  chtqub  16257  mersenne  16258  bcmono  16265  bcmax  16266  prmefexple  16269  bposlem1  16272  bposlem3  16274  bposlem4  16275  bposlem5  16276  bposlem6  16277  lgsval2lem  16295  lgsvalmod  16304  lgsneg  16309  lgsdilem  16312  lgssq  16325  lgssq2  16326  gausslemma2dlem1a  16343  gausslemma2dlem3  16348  lgseisenlem2  16356  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  lgsquad3  16369  2lgslem1a2  16372  2sqlem3  16402  2sqlem8  16408  supfz  17288  inffz  17289