Theorem zred 9442

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

Syntax hints:   -> wi 4   e. wcel 2164   RRcr 7873   ZZcz 9320

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-rab 2481  df-v 2762  df-un 3158  df-in 3160  df-ss 3167  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263  df-ov 5922  df-neg 8195  df-z 9321

This theorem is referenced by:  zcnd  9443  btwnapz  9450  eluzelre  9605  eluzadd  9624  eluzsub  9625  uzm1  9626  z2ge  9895  zltaddlt1le  10076  fztri3or  10108  fznlem  10110  fzdisj  10121  fzpreddisj  10140  fznatpl1  10145  uzdisj  10162  fzm1  10169  fz0fzdiffz0  10199  elfzmlbm  10200  elfzmlbp  10201  difelfznle  10204  nn0disj  10207  elfzolt3  10227  fzonel  10230  fzouzdisj  10250  fzonmapblen  10257  fzoaddel  10262  elfzonelfzo  10300  qtri3or  10313  exbtwnzlemstep  10319  exbtwnzlemex  10321  exbtwnz  10322  rebtwn2zlemstep  10324  rebtwn2z  10326  qbtwnrelemcalc  10327  qbtwnre  10328  apbtwnz  10346  qfraclt1  10352  qfracge0  10353  flqge  10354  flid  10356  flqltnz  10359  flqwordi  10360  flqaddz  10369  flqmulnn0  10371  btwnzge0  10372  2tnp1ge0ge0  10373  flhalf  10374  flltdivnn0lt  10376  fldiv4p1lem1div2  10377  fldiv4lem1div2uz2  10378  ceiqge  10383  ceiqm1l  10385  ceiqle  10387  flqleceil  10391  flqeqceilz  10392  intfracq  10394  modqval  10398  modqge0  10406  modqlt  10407  modqmulnn  10416  mulp1mod1  10439  modaddmodup  10461  modaddmodlo  10462  modsumfzodifsn  10470  addmodlteq  10472  frec2uzlt2d  10478  frec2uzf1od  10480  uzennn  10510  seq3split  10562  iseqf1olemkle  10571  iseqf1olemqcl  10573  iseqf1olemnab  10575  iseqf1olemab  10576  iseqf1olemqk  10581  seq3f1olemqsumkj  10585  seq3f1olemqsumk  10586  seq3f1olemqsum  10587  seqf1oglem1  10593  seqf1oglem2  10594  seqfeq4g  10605  exp3val  10615  expcanlem  10789  expcan  10790  facavg  10820  bcval4  10826  bcp1nk  10836  bcval5  10837  zfz1isolemiso  10913  seq3coll  10916  iswrdiz  10924  seq3shft  10985  resqrexlemdecn  11159  fzomaxdiflem  11259  fsum3cvg3  11542  fsumm1  11562  fsum1p  11564  fsum0diaglem  11586  isumshft  11636  isumsplit  11637  divcnv  11643  geolim2  11658  cvgratnnlemabsle  11673  cvgratnnlemsumlt  11674  cvgratnnlemrate  11676  cvgratz  11678  mertenslemi1  11681  fprodntrivap  11730  prodsnf  11738  fprod1p  11745  fprodeq0  11763  zdvdsdc  11958  dvdslelemd  11988  oexpneg  12021  ltoddhalfle  12037  divalglemnqt  12064  divalglemex  12066  divalglemeuneg  12067  flodddiv4t2lthalf  12081  zsupcl  12087  zssinfcl  12088  infssuzex  12089  suprzubdc  12092  zsupssdc  12094  suprzcl2dc  12095  dvdsbnd  12096  dvdslegcd  12104  gcd0id  12119  gcdneg  12122  bezoutlemsup  12149  dfgcd2  12154  uzwodc  12177  nn0seqcvgd  12182  lcmgcdlem  12218  ncoprmgcdne1b  12230  nprm  12264  prmdc  12271  prmdvdsfz  12280  isprm5lem  12282  coprm  12285  prmexpb  12292  prmfac1  12293  znege1  12319  sqrt2irrap  12321  hashdvds  12362  eulerthlemrprm  12370  eulerthlema  12371  hashgcdlem  12379  pythagtriplem13  12417  pythagtriplem16  12420  pcxcl  12452  pcaddlem  12480  pcadd  12481  pcfac  12491  qexpz  12493  4sqlem7  12525  4sqlem10  12528  4sqexercise2  12540  4sqlemsdc  12541  4sqlem11  12542  4sqlem12  12543  4sqlem15  12546  4sqlem16  12547  4sqlem17  12548  oddennn  12552  ennnfoneleminc  12571  nninfdclemp1  12610  nninfdclemlt  12611  gsumfzval  12977  gsumfzz  13070  gsumfzcl  13074  mulgfng  13197  subgmulg  13261  gsumfzreidx  13410  gsumfzsubmcl  13411  gsumfzmptfidmadd  13412  gsumfzmhm  13416  gsumfzfsumlemm  14086  gsumfzfsum  14087  ltexp2  15115  logblt  15135  lgsval2lem  15167  lgsvalmod  15176  lgsneg  15181  lgsdilem  15184  lgssq  15197  lgssq2  15198  gausslemma2dlem1a  15215  gausslemma2dlem3  15220  lgseisenlem2  15228  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad3  15241  2lgslem1a2  15244  2sqlem3  15274  2sqlem8  15280  supfz  15631  inffz  15632