Theorem zred 8929

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

Syntax hints:   → wi 4   ∈ wcel 1439  ℝcr 7410  ℤcz 8811

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-3or 926  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-rex 2366  df-rab 2369  df-v 2622  df-un 3004  df-in 3006  df-ss 3013  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-br 3852  df-iota 4993  df-fv 5036  df-ov 5669  df-neg 7717  df-z 8812

This theorem is referenced by:  zcnd  8930  btwnapz  8937  eluzelre  9090  eluzadd  9108  eluzsub  9109  uzm1  9110  z2ge  9349  zltaddlt1le  9484  fztri3or  9514  fznlem  9516  fzdisj  9527  fzpreddisj  9546  fznatpl1  9551  uzdisj  9568  fzm1  9575  fz0fzdiffz0  9602  elfzmlbm  9603  elfzmlbp  9604  difelfznle  9607  nn0disj  9610  elfzolt3  9629  fzonel  9632  fzouzdisj  9652  fzonmapblen  9659  fzoaddel  9664  elfzonelfzo  9702  qtri3or  9715  exbtwnzlemstep  9720  exbtwnzlemex  9722  exbtwnz  9723  rebtwn2zlemstep  9725  rebtwn2z  9727  qbtwnrelemcalc  9728  qbtwnre  9729  apbtwnz  9742  qfraclt1  9748  qfracge0  9749  flqge  9750  flid  9752  flqltnz  9755  flqwordi  9756  flqaddz  9765  flqmulnn0  9767  btwnzge0  9768  2tnp1ge0ge0  9769  flhalf  9770  flltdivnn0lt  9772  fldiv4p1lem1div2  9773  ceiqge  9777  ceiqm1l  9779  ceiqle  9781  flqleceil  9785  flqeqceilz  9786  intfracq  9788  modqval  9792  modqge0  9800  modqlt  9801  modqmulnn  9810  mulp1mod1  9833  modaddmodup  9855  modaddmodlo  9856  modsumfzodifsn  9864  addmodlteq  9866  frec2uzlt2d  9872  frec2uzf1od  9874  seq3split  9968  iseqf1olemkle  9974  iseqf1olemqcl  9976  iseqf1olemnab  9978  iseqf1olemab  9979  iseqf1olemqk  9984  seq3f1olemqsumkj  9988  seq3f1olemqsumk  9989  seq3f1olemqsum  9990  exp3val  10018  expcanlem  10185  expcan  10186  facavg  10215  bcval4  10221  bcp1nk  10231  ibcval5  10232  zfz1isolemiso  10305  iseqcoll  10308  seq3shft  10333  resqrexlemdecn  10506  fzomaxdiflem  10606  fsum3cvg3  10850  fsumm1  10871  fsum1p  10873  fsum0diaglem  10895  isumshft  10945  isumsplit  10946  divcnv  10952  geolim2  10967  cvgratnnlemabsle  10982  cvgratnnlemsumlt  10983  cvgratnnlemrate  10985  cvgratz  10987  mertenslemi1  10990  zdvdsdc  11156  dvdslelemd  11183  oexpneg  11216  ltoddhalfle  11232  divalglemnqt  11259  divalglemex  11261  divalglemeuneg  11262  flodddiv4t2lthalf  11276  zsupcl  11282  zssinfcl  11283  infssuzex  11284  dvdsbnd  11287  dvdslegcd  11295  gcd0id  11309  gcdneg  11312  bezoutlemsup  11337  dfgcd2  11342  nn0seqcvgd  11362  lcmgcdlem  11398  ncoprmgcdne1b  11410  nprm  11444  prmdvdsfz  11459  coprm  11462  prmexpb  11469  prmfac1  11470  znege1  11495  sqrt2irrap  11497  hashdvds  11536  hashgcdlem  11542  oddennn  11544  supfz  12188  inffz  12189