Theorem zred 9569

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

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 7998   ZZcz 9446

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-rab 2517  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6004  df-neg 8320  df-z 9447

This theorem is referenced by:  zcnd  9570  btwnapz  9577  eluzelre  9732  eluzadd  9751  eluzsub  9752  uzm1  9753  z2ge  10022  zltaddlt1le  10203  fztri3or  10235  fznlem  10237  fzdisj  10248  fzpreddisj  10267  fznatpl1  10272  uzdisj  10289  fzm1  10296  fz0fzdiffz0  10326  elfzmlbm  10327  elfzmlbp  10328  difelfznle  10331  nn0disj  10334  elfzolt3  10354  fzonel  10357  fzouzdisj  10378  fzodisjsn  10380  fzonmapblen  10387  fzoaddel  10393  elincfzoext  10399  elfzonelfzo  10436  zsupcl  10451  zssinfcl  10452  infssuzex  10453  suprzubdc  10456  zsupssdc  10458  suprzcl2dc  10459  qtri3or  10460  exbtwnzlemstep  10467  exbtwnzlemex  10469  exbtwnz  10470  rebtwn2zlemstep  10472  rebtwn2z  10474  qbtwnrelemcalc  10475  qbtwnre  10476  apbtwnz  10494  qfraclt1  10500  qfracge0  10501  flqge  10502  flid  10504  flqltnz  10507  flqwordi  10508  flqaddz  10517  flqmulnn0  10519  btwnzge0  10520  2tnp1ge0ge0  10521  flhalf  10522  flltdivnn0lt  10524  fldiv4p1lem1div2  10525  fldiv4lem1div2uz2  10526  ceiqge  10531  ceiqm1l  10533  ceiqle  10535  flqleceil  10539  flqeqceilz  10540  intfracq  10542  modqval  10546  modqge0  10554  modqlt  10555  modqmulnn  10564  mulp1mod1  10587  modaddmodup  10609  modaddmodlo  10610  modsumfzodifsn  10618  addmodlteq  10620  frec2uzlt2d  10626  frec2uzf1od  10628  uzennn  10658  seq3split  10710  iseqf1olemkle  10719  iseqf1olemqcl  10721  iseqf1olemnab  10723  iseqf1olemab  10724  iseqf1olemqk  10729  seq3f1olemqsumkj  10733  seq3f1olemqsumk  10734  seq3f1olemqsum  10735  seqf1oglem1  10741  seqf1oglem2  10742  seqfeq4g  10753  exp3val  10763  expcanlem  10937  expcan  10938  facavg  10968  bcval4  10974  bcp1nk  10984  bcval5  10985  zfz1isolemiso  11061  seq3coll  11064  iswrdiz  11078  ccatrn  11144  seq3shft  11349  resqrexlemdecn  11523  fzomaxdiflem  11623  nn0maxcl  11736  fsum3cvg3  11907  fsumm1  11927  fsum1p  11929  fsum0diaglem  11951  isumshft  12001  isumsplit  12002  divcnv  12008  geolim2  12023  cvgratnnlemabsle  12038  cvgratnnlemsumlt  12039  cvgratnnlemrate  12041  cvgratz  12043  mertenslemi1  12046  fprodntrivap  12095  prodsnf  12103  fprod1p  12110  fprodeq0  12128  zdvdsdc  12323  dvdslelemd  12354  oexpneg  12388  ltoddhalfle  12404  divalglemnqt  12431  divalglemex  12433  divalglemeuneg  12434  flodddiv4t2lthalf  12450  bitsfzolem  12465  bitsfzo  12466  bitsmod  12467  bitscmp  12469  dvdsbnd  12477  dvdslegcd  12485  gcd0id  12500  gcdneg  12503  bezoutlemsup  12530  dfgcd2  12535  uzwodc  12558  nn0seqcvgd  12563  lcmgcdlem  12599  ncoprmgcdne1b  12611  nprm  12645  prmdc  12652  prmdvdsfz  12661  isprm5lem  12663  coprm  12666  prmexpb  12673  prmfac1  12674  znege1  12700  sqrt2irrap  12702  hashdvds  12743  eulerthlemrprm  12751  eulerthlema  12752  hashgcdlem  12760  pythagtriplem13  12799  pythagtriplem16  12802  pcxcl  12834  pcaddlem  12862  pcadd  12863  pcfac  12873  qexpz  12875  4sqlem7  12907  4sqlem10  12910  4sqexercise2  12922  4sqlemsdc  12923  4sqlem11  12924  4sqlem12  12925  4sqlem15  12928  4sqlem16  12929  4sqlem17  12930  oddennn  12963  ennnfoneleminc  12982  nninfdclemp1  13021  nninfdclemlt  13022  gsumfzval  13424  gsumfzz  13528  gsumfzcl  13532  mulgfng  13661  subgmulg  13725  gsumfzreidx  13874  gsumfzsubmcl  13875  gsumfzmptfidmadd  13876  gsumfzmhm  13880  gsumfzfsumlemm  14551  gsumfzfsum  14552  ltexp2  15615  logblt  15636  mersenne  15671  lgsval2lem  15689  lgsvalmod  15698  lgsneg  15703  lgsdilem  15706  lgssq  15719  lgssq2  15720  gausslemma2dlem1a  15737  gausslemma2dlem3  15742  lgseisenlem2  15750  lgsquadlem1  15756  lgsquadlem2  15757  lgsquadlem3  15758  lgsquad3  15763  2lgslem1a2  15766  2sqlem3  15796  2sqlem8  15802  supfz  16439  inffz  16440