Theorem zred 9197

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

Syntax hints:   → wi 4   ∈ wcel 1481  ℝcr 7643  ℤcz 9078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-rab 2426  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139  df-ov 5785  df-neg 7960  df-z 9079

This theorem is referenced by:  zcnd  9198  btwnapz  9205  eluzelre  9360  eluzadd  9378  eluzsub  9379  uzm1  9380  z2ge  9639  zltaddlt1le  9820  fztri3or  9850  fznlem  9852  fzdisj  9863  fzpreddisj  9882  fznatpl1  9887  uzdisj  9904  fzm1  9911  fz0fzdiffz0  9938  elfzmlbm  9939  elfzmlbp  9940  difelfznle  9943  nn0disj  9946  elfzolt3  9965  fzonel  9968  fzouzdisj  9988  fzonmapblen  9995  fzoaddel  10000  elfzonelfzo  10038  qtri3or  10051  exbtwnzlemstep  10056  exbtwnzlemex  10058  exbtwnz  10059  rebtwn2zlemstep  10061  rebtwn2z  10063  qbtwnrelemcalc  10064  qbtwnre  10065  apbtwnz  10078  qfraclt1  10084  qfracge0  10085  flqge  10086  flid  10088  flqltnz  10091  flqwordi  10092  flqaddz  10101  flqmulnn0  10103  btwnzge0  10104  2tnp1ge0ge0  10105  flhalf  10106  flltdivnn0lt  10108  fldiv4p1lem1div2  10109  ceiqge  10113  ceiqm1l  10115  ceiqle  10117  flqleceil  10121  flqeqceilz  10122  intfracq  10124  modqval  10128  modqge0  10136  modqlt  10137  modqmulnn  10146  mulp1mod1  10169  modaddmodup  10191  modaddmodlo  10192  modsumfzodifsn  10200  addmodlteq  10202  frec2uzlt2d  10208  frec2uzf1od  10210  uzennn  10240  seq3split  10283  iseqf1olemkle  10288  iseqf1olemqcl  10290  iseqf1olemnab  10292  iseqf1olemab  10293  iseqf1olemqk  10298  seq3f1olemqsumkj  10302  seq3f1olemqsumk  10303  seq3f1olemqsum  10304  exp3val  10326  expcanlem  10493  expcan  10494  facavg  10524  bcval4  10530  bcp1nk  10540  bcval5  10541  zfz1isolemiso  10614  seq3coll  10617  seq3shft  10642  resqrexlemdecn  10816  fzomaxdiflem  10916  fsum3cvg3  11197  fsumm1  11217  fsum1p  11219  fsum0diaglem  11241  isumshft  11291  isumsplit  11292  divcnv  11298  geolim2  11313  cvgratnnlemabsle  11328  cvgratnnlemsumlt  11329  cvgratnnlemrate  11331  cvgratz  11333  mertenslemi1  11336  zdvdsdc  11550  dvdslelemd  11577  oexpneg  11610  ltoddhalfle  11626  divalglemnqt  11653  divalglemex  11655  divalglemeuneg  11656  flodddiv4t2lthalf  11670  zsupcl  11676  zssinfcl  11677  infssuzex  11678  dvdsbnd  11681  dvdslegcd  11689  gcd0id  11703  gcdneg  11706  bezoutlemsup  11733  dfgcd2  11738  nn0seqcvgd  11758  lcmgcdlem  11794  ncoprmgcdne1b  11806  nprm  11840  prmdvdsfz  11855  coprm  11858  prmexpb  11865  prmfac1  11866  znege1  11892  sqrt2irrap  11894  hashdvds  11933  hashgcdlem  11939  oddennn  11941  ennnfoneleminc  11960  logblt  13087  supfz  13428  inffz  13429