Theorem zred 9645

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 9529	. 2 ⊢ ℤ ⊆ ℝ
2		zred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℤ)
3	1, 2	sselid 3226	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8074  ℤcz 9522

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-rab 2520  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031  df-neg 8396  df-z 9523

This theorem is referenced by:  zcnd  9646  btwnapz  9653  eluzmn  9805  eluzelre  9809  eluzadd  9828  eluzsub  9829  uzm1  9830  z2ge  10104  zltaddlt1le  10285  fztri3or  10317  fznlem  10319  fzdisj  10330  fzpreddisj  10349  fznatpl1  10354  uzdisj  10371  fzm1  10378  fz0fzdiffz0  10408  elfzmlbm  10409  elfzmlbp  10410  difelfznle  10413  nn0disj  10416  elfzolt3  10436  fzonel  10439  fzouzdisj  10460  fzodisjsn  10462  fzonmapblen  10470  fzoaddel  10476  elincfzoext  10482  elfzonelfzo  10519  zsupcl  10535  zssinfcl  10536  infssuzex  10537  suprzubdc  10540  zsupssdc  10542  suprzcl2dc  10543  qtri3or  10544  exbtwnzlemstep  10551  exbtwnzlemex  10553  exbtwnz  10554  rebtwn2zlemstep  10556  rebtwn2z  10558  qbtwnrelemcalc  10559  qbtwnre  10560  apbtwnz  10578  qfraclt1  10584  qfracge0  10585  flqge  10586  flid  10588  flqltnz  10591  flqwordi  10592  flqaddz  10601  flqmulnn0  10603  btwnzge0  10604  2tnp1ge0ge0  10605  flhalf  10606  flltdivnn0lt  10608  fldiv4p1lem1div2  10609  fldiv4lem1div2uz2  10610  ceiqge  10615  ceiqm1l  10617  ceiqle  10619  flqleceil  10623  flqeqceilz  10624  intfracq  10626  modqval  10630  modqge0  10638  modqlt  10639  modqmulnn  10648  mulp1mod1  10671  modaddmodup  10693  modaddmodlo  10694  modsumfzodifsn  10702  addmodlteq  10704  frec2uzlt2d  10710  frec2uzf1od  10712  uzennn  10742  seq3split  10794  iseqf1olemkle  10803  iseqf1olemqcl  10805  iseqf1olemnab  10807  iseqf1olemab  10808  iseqf1olemqk  10813  seq3f1olemqsumkj  10817  seq3f1olemqsumk  10818  seq3f1olemqsum  10819  seqf1oglem1  10825  seqf1oglem2  10826  seqfeq4g  10837  exp3val  10847  expcanlem  11021  expcan  11022  facavg  11052  bcval4  11058  bcp1nk  11068  bcval5  11069  zfz1isolemiso  11147  seq3coll  11150  iswrdiz  11167  ccatrn  11233  ccatalpha  11237  seq3shft  11459  resqrexlemdecn  11633  fzomaxdiflem  11733  nn0maxcl  11846  fsum3cvg3  12018  fsumm1  12038  fsum1p  12040  fsum0diaglem  12062  isumshft  12112  isumsplit  12113  divcnv  12119  geolim2  12134  cvgratnnlemabsle  12149  cvgratnnlemsumlt  12150  cvgratnnlemrate  12152  cvgratz  12154  mertenslemi1  12157  fprodntrivap  12206  prodsnf  12214  fprod1p  12221  fprodeq0  12239  zdvdsdc  12434  dvdslelemd  12465  oexpneg  12499  ltoddhalfle  12515  divalglemnqt  12542  divalglemex  12544  divalglemeuneg  12545  flodddiv4t2lthalf  12561  bitsfzolem  12576  bitsfzo  12577  bitsmod  12578  bitscmp  12580  dvdsbnd  12588  dvdslegcd  12596  gcd0id  12611  gcdneg  12614  bezoutlemsup  12641  dfgcd2  12646  uzwodc  12669  nn0seqcvgd  12674  lcmgcdlem  12710  ncoprmgcdne1b  12722  nprm  12756  prmdc  12763  prmdvdsfz  12772  isprm5lem  12774  coprm  12777  prmexpb  12784  prmfac1  12785  znege1  12811  sqrt2irrap  12813  hashdvds  12854  eulerthlemrprm  12862  eulerthlema  12863  hashgcdlem  12871  pythagtriplem13  12910  pythagtriplem16  12913  pcxcl  12945  pcaddlem  12973  pcadd  12974  pcfac  12984  qexpz  12986  4sqlem7  13018  4sqlem10  13021  4sqexercise2  13033  4sqlemsdc  13034  4sqlem11  13035  4sqlem12  13036  4sqlem15  13039  4sqlem16  13040  4sqlem17  13041  oddennn  13074  ennnfoneleminc  13093  nninfdclemp1  13132  nninfdclemlt  13133  gsumfzval  13535  gsumfzz  13639  gsumfzcl  13643  mulgfng  13772  subgmulg  13836  gsumfzreidx  13985  gsumfzsubmcl  13986  gsumfzmptfidmadd  13987  gsumfzmhm  13991  gsumsplit0  13994  gsumfzfsumlemm  14663  gsumfzfsum  14664  ltexp2  15732  logblt  15753  mersenne  15791  lgsval2lem  15809  lgsvalmod  15818  lgsneg  15823  lgsdilem  15826  lgssq  15839  lgssq2  15840  gausslemma2dlem1a  15857  gausslemma2dlem3  15862  lgseisenlem2  15870  lgsquadlem1  15876  lgsquadlem2  15877  lgsquadlem3  15878  lgsquad3  15883  2lgslem1a2  15886  2sqlem3  15916  2sqlem8  15922  supfz  16784  inffz  16785  gsumgfsumlem  16792