Theorem zred 9602

Description: An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
zred.1	⊢ (𝜑 → 𝐴 ∈ ℤ)

Assertion

Ref	Expression
zred	⊢ (𝜑 → 𝐴 ∈ ℝ)

Proof of Theorem zred

Step	Hyp	Ref	Expression
1		zssre 9486	. 2 ⊢ ℤ ⊆ ℝ
2		zred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℤ)
3	1, 2	sselid 3225	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8031  ℤcz 9479

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021  df-neg 8353  df-z 9480

This theorem is referenced by:  zcnd  9603  btwnapz  9610  eluzmn  9762  eluzelre  9766  eluzadd  9785  eluzsub  9786  uzm1  9787  z2ge  10061  zltaddlt1le  10242  fztri3or  10274  fznlem  10276  fzdisj  10287  fzpreddisj  10306  fznatpl1  10311  uzdisj  10328  fzm1  10335  fz0fzdiffz0  10365  elfzmlbm  10366  elfzmlbp  10367  difelfznle  10370  nn0disj  10373  elfzolt3  10393  fzonel  10396  fzouzdisj  10417  fzodisjsn  10419  fzonmapblen  10427  fzoaddel  10433  elincfzoext  10439  elfzonelfzo  10476  zsupcl  10492  zssinfcl  10493  infssuzex  10494  suprzubdc  10497  zsupssdc  10499  suprzcl2dc  10500  qtri3or  10501  exbtwnzlemstep  10508  exbtwnzlemex  10510  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2z  10515  qbtwnrelemcalc  10516  qbtwnre  10517  apbtwnz  10535  qfraclt1  10541  qfracge0  10542  flqge  10543  flid  10545  flqltnz  10548  flqwordi  10549  flqaddz  10558  flqmulnn0  10560  btwnzge0  10561  2tnp1ge0ge0  10562  flhalf  10563  flltdivnn0lt  10565  fldiv4p1lem1div2  10566  fldiv4lem1div2uz2  10567  ceiqge  10572  ceiqm1l  10574  ceiqle  10576  flqleceil  10580  flqeqceilz  10581  intfracq  10583  modqval  10587  modqge0  10595  modqlt  10596  modqmulnn  10605  mulp1mod1  10628  modaddmodup  10650  modaddmodlo  10651  modsumfzodifsn  10659  addmodlteq  10661  frec2uzlt2d  10667  frec2uzf1od  10669  uzennn  10699  seq3split  10751  iseqf1olemkle  10760  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemab  10765  iseqf1olemqk  10770  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seqf1oglem1  10782  seqf1oglem2  10783  seqfeq4g  10794  exp3val  10804  expcanlem  10978  expcan  10979  facavg  11009  bcval4  11015  bcp1nk  11025  bcval5  11026  zfz1isolemiso  11104  seq3coll  11107  iswrdiz  11124  ccatrn  11190  ccatalpha  11194  seq3shft  11403  resqrexlemdecn  11577  fzomaxdiflem  11677  nn0maxcl  11790  fsum3cvg3  11962  fsumm1  11982  fsum1p  11984  fsum0diaglem  12006  isumshft  12056  isumsplit  12057  divcnv  12063  geolim2  12078  cvgratnnlemabsle  12093  cvgratnnlemsumlt  12094  cvgratnnlemrate  12096  cvgratz  12098  mertenslemi1  12101  fprodntrivap  12150  prodsnf  12158  fprod1p  12165  fprodeq0  12183  zdvdsdc  12378  dvdslelemd  12409  oexpneg  12443  ltoddhalfle  12459  divalglemnqt  12486  divalglemex  12488  divalglemeuneg  12489  flodddiv4t2lthalf  12505  bitsfzolem  12520  bitsfzo  12521  bitsmod  12522  bitscmp  12524  dvdsbnd  12532  dvdslegcd  12540  gcd0id  12555  gcdneg  12558  bezoutlemsup  12585  dfgcd2  12590  uzwodc  12613  nn0seqcvgd  12618  lcmgcdlem  12654  ncoprmgcdne1b  12666  nprm  12700  prmdc  12707  prmdvdsfz  12716  isprm5lem  12718  coprm  12721  prmexpb  12728  prmfac1  12729  znege1  12755  sqrt2irrap  12757  hashdvds  12798  eulerthlemrprm  12806  eulerthlema  12807  hashgcdlem  12815  pythagtriplem13  12854  pythagtriplem16  12857  pcxcl  12889  pcaddlem  12917  pcadd  12918  pcfac  12928  qexpz  12930  4sqlem7  12962  4sqlem10  12965  4sqexercise2  12977  4sqlemsdc  12978  4sqlem11  12979  4sqlem12  12980  4sqlem15  12983  4sqlem16  12984  4sqlem17  12985  oddennn  13018  ennnfoneleminc  13037  nninfdclemp1  13076  nninfdclemlt  13077  gsumfzval  13479  gsumfzz  13583  gsumfzcl  13587  mulgfng  13716  subgmulg  13780  gsumfzreidx  13929  gsumfzsubmcl  13930  gsumfzmptfidmadd  13931  gsumfzmhm  13935  gsumsplit0  13938  gsumfzfsumlemm  14607  gsumfzfsum  14608  ltexp2  15671  logblt  15692  mersenne  15727  lgsval2lem  15745  lgsvalmod  15754  lgsneg  15759  lgsdilem  15762  lgssq  15775  lgssq2  15776  gausslemma2dlem1a  15793  gausslemma2dlem3  15798  lgseisenlem2  15806  lgsquadlem1  15812  lgsquadlem2  15813  lgsquadlem3  15814  lgsquad3  15819  2lgslem1a2  15822  2sqlem3  15852  2sqlem8  15858  supfz  16701  inffz  16702  gsumgfsumlem  16709