Theorem zred 9495

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

Syntax hints:   -> wi 4   e. wcel 2176   RRcr 7924   ZZcz 9372

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-rab 2493  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-iota 5232  df-fv 5279  df-ov 5947  df-neg 8246  df-z 9373

This theorem is referenced by:  zcnd  9496  btwnapz  9503  eluzelre  9658  eluzadd  9677  eluzsub  9678  uzm1  9679  z2ge  9948  zltaddlt1le  10129  fztri3or  10161  fznlem  10163  fzdisj  10174  fzpreddisj  10193  fznatpl1  10198  uzdisj  10215  fzm1  10222  fz0fzdiffz0  10252  elfzmlbm  10253  elfzmlbp  10254  difelfznle  10257  nn0disj  10260  elfzolt3  10280  fzonel  10283  fzouzdisj  10304  fzonmapblen  10311  fzoaddel  10316  elincfzoext  10322  elfzonelfzo  10359  zsupcl  10374  zssinfcl  10375  infssuzex  10376  suprzubdc  10379  zsupssdc  10381  suprzcl2dc  10382  qtri3or  10383  exbtwnzlemstep  10390  exbtwnzlemex  10392  exbtwnz  10393  rebtwn2zlemstep  10395  rebtwn2z  10397  qbtwnrelemcalc  10398  qbtwnre  10399  apbtwnz  10417  qfraclt1  10423  qfracge0  10424  flqge  10425  flid  10427  flqltnz  10430  flqwordi  10431  flqaddz  10440  flqmulnn0  10442  btwnzge0  10443  2tnp1ge0ge0  10444  flhalf  10445  flltdivnn0lt  10447  fldiv4p1lem1div2  10448  fldiv4lem1div2uz2  10449  ceiqge  10454  ceiqm1l  10456  ceiqle  10458  flqleceil  10462  flqeqceilz  10463  intfracq  10465  modqval  10469  modqge0  10477  modqlt  10478  modqmulnn  10487  mulp1mod1  10510  modaddmodup  10532  modaddmodlo  10533  modsumfzodifsn  10541  addmodlteq  10543  frec2uzlt2d  10549  frec2uzf1od  10551  uzennn  10581  seq3split  10633  iseqf1olemkle  10642  iseqf1olemqcl  10644  iseqf1olemnab  10646  iseqf1olemab  10647  iseqf1olemqk  10652  seq3f1olemqsumkj  10656  seq3f1olemqsumk  10657  seq3f1olemqsum  10658  seqf1oglem1  10664  seqf1oglem2  10665  seqfeq4g  10676  exp3val  10686  expcanlem  10860  expcan  10861  facavg  10891  bcval4  10897  bcp1nk  10907  bcval5  10908  zfz1isolemiso  10984  seq3coll  10987  iswrdiz  11001  ccatrn  11065  seq3shft  11149  resqrexlemdecn  11323  fzomaxdiflem  11423  nn0maxcl  11536  fsum3cvg3  11707  fsumm1  11727  fsum1p  11729  fsum0diaglem  11751  isumshft  11801  isumsplit  11802  divcnv  11808  geolim2  11823  cvgratnnlemabsle  11838  cvgratnnlemsumlt  11839  cvgratnnlemrate  11841  cvgratz  11843  mertenslemi1  11846  fprodntrivap  11895  prodsnf  11903  fprod1p  11910  fprodeq0  11928  zdvdsdc  12123  dvdslelemd  12154  oexpneg  12188  ltoddhalfle  12204  divalglemnqt  12231  divalglemex  12233  divalglemeuneg  12234  flodddiv4t2lthalf  12250  bitsfzolem  12265  bitsfzo  12266  bitsmod  12267  bitscmp  12269  dvdsbnd  12277  dvdslegcd  12285  gcd0id  12300  gcdneg  12303  bezoutlemsup  12330  dfgcd2  12335  uzwodc  12358  nn0seqcvgd  12363  lcmgcdlem  12399  ncoprmgcdne1b  12411  nprm  12445  prmdc  12452  prmdvdsfz  12461  isprm5lem  12463  coprm  12466  prmexpb  12473  prmfac1  12474  znege1  12500  sqrt2irrap  12502  hashdvds  12543  eulerthlemrprm  12551  eulerthlema  12552  hashgcdlem  12560  pythagtriplem13  12599  pythagtriplem16  12602  pcxcl  12634  pcaddlem  12662  pcadd  12663  pcfac  12673  qexpz  12675  4sqlem7  12707  4sqlem10  12710  4sqexercise2  12722  4sqlemsdc  12723  4sqlem11  12724  4sqlem12  12725  4sqlem15  12728  4sqlem16  12729  4sqlem17  12730  oddennn  12763  ennnfoneleminc  12782  nninfdclemp1  12821  nninfdclemlt  12822  gsumfzval  13223  gsumfzz  13327  gsumfzcl  13331  mulgfng  13460  subgmulg  13524  gsumfzreidx  13673  gsumfzsubmcl  13674  gsumfzmptfidmadd  13675  gsumfzmhm  13679  gsumfzfsumlemm  14349  gsumfzfsum  14350  ltexp2  15413  logblt  15434  mersenne  15469  lgsval2lem  15487  lgsvalmod  15496  lgsneg  15501  lgsdilem  15504  lgssq  15517  lgssq2  15518  gausslemma2dlem1a  15535  gausslemma2dlem3  15540  lgseisenlem2  15548  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556  lgsquad3  15561  2lgslem1a2  15564  2sqlem3  15594  2sqlem8  15600  supfz  16010  inffz  16011