Theorem zred 9577

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8006  ℤcz 9454

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-rab 2517  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010  df-neg 8328  df-z 9455

This theorem is referenced by:  zcnd  9578  btwnapz  9585  eluzelre  9740  eluzadd  9759  eluzsub  9760  uzm1  9761  z2ge  10030  zltaddlt1le  10211  fztri3or  10243  fznlem  10245  fzdisj  10256  fzpreddisj  10275  fznatpl1  10280  uzdisj  10297  fzm1  10304  fz0fzdiffz0  10334  elfzmlbm  10335  elfzmlbp  10336  difelfznle  10339  nn0disj  10342  elfzolt3  10362  fzonel  10365  fzouzdisj  10386  fzodisjsn  10388  fzonmapblen  10395  fzoaddel  10401  elincfzoext  10407  elfzonelfzo  10444  zsupcl  10459  zssinfcl  10460  infssuzex  10461  suprzubdc  10464  zsupssdc  10466  suprzcl2dc  10467  qtri3or  10468  exbtwnzlemstep  10475  exbtwnzlemex  10477  exbtwnz  10478  rebtwn2zlemstep  10480  rebtwn2z  10482  qbtwnrelemcalc  10483  qbtwnre  10484  apbtwnz  10502  qfraclt1  10508  qfracge0  10509  flqge  10510  flid  10512  flqltnz  10515  flqwordi  10516  flqaddz  10525  flqmulnn0  10527  btwnzge0  10528  2tnp1ge0ge0  10529  flhalf  10530  flltdivnn0lt  10532  fldiv4p1lem1div2  10533  fldiv4lem1div2uz2  10534  ceiqge  10539  ceiqm1l  10541  ceiqle  10543  flqleceil  10547  flqeqceilz  10548  intfracq  10550  modqval  10554  modqge0  10562  modqlt  10563  modqmulnn  10572  mulp1mod1  10595  modaddmodup  10617  modaddmodlo  10618  modsumfzodifsn  10626  addmodlteq  10628  frec2uzlt2d  10634  frec2uzf1od  10636  uzennn  10666  seq3split  10718  iseqf1olemkle  10727  iseqf1olemqcl  10729  iseqf1olemnab  10731  iseqf1olemab  10732  iseqf1olemqk  10737  seq3f1olemqsumkj  10741  seq3f1olemqsumk  10742  seq3f1olemqsum  10743  seqf1oglem1  10749  seqf1oglem2  10750  seqfeq4g  10761  exp3val  10771  expcanlem  10945  expcan  10946  facavg  10976  bcval4  10982  bcp1nk  10992  bcval5  10993  zfz1isolemiso  11069  seq3coll  11072  iswrdiz  11086  ccatrn  11152  seq3shft  11357  resqrexlemdecn  11531  fzomaxdiflem  11631  nn0maxcl  11744  fsum3cvg3  11915  fsumm1  11935  fsum1p  11937  fsum0diaglem  11959  isumshft  12009  isumsplit  12010  divcnv  12016  geolim2  12031  cvgratnnlemabsle  12046  cvgratnnlemsumlt  12047  cvgratnnlemrate  12049  cvgratz  12051  mertenslemi1  12054  fprodntrivap  12103  prodsnf  12111  fprod1p  12118  fprodeq0  12136  zdvdsdc  12331  dvdslelemd  12362  oexpneg  12396  ltoddhalfle  12412  divalglemnqt  12439  divalglemex  12441  divalglemeuneg  12442  flodddiv4t2lthalf  12458  bitsfzolem  12473  bitsfzo  12474  bitsmod  12475  bitscmp  12477  dvdsbnd  12485  dvdslegcd  12493  gcd0id  12508  gcdneg  12511  bezoutlemsup  12538  dfgcd2  12543  uzwodc  12566  nn0seqcvgd  12571  lcmgcdlem  12607  ncoprmgcdne1b  12619  nprm  12653  prmdc  12660  prmdvdsfz  12669  isprm5lem  12671  coprm  12674  prmexpb  12681  prmfac1  12682  znege1  12708  sqrt2irrap  12710  hashdvds  12751  eulerthlemrprm  12759  eulerthlema  12760  hashgcdlem  12768  pythagtriplem13  12807  pythagtriplem16  12810  pcxcl  12842  pcaddlem  12870  pcadd  12871  pcfac  12881  qexpz  12883  4sqlem7  12915  4sqlem10  12918  4sqexercise2  12930  4sqlemsdc  12931  4sqlem11  12932  4sqlem12  12933  4sqlem15  12936  4sqlem16  12937  4sqlem17  12938  oddennn  12971  ennnfoneleminc  12990  nninfdclemp1  13029  nninfdclemlt  13030  gsumfzval  13432  gsumfzz  13536  gsumfzcl  13540  mulgfng  13669  subgmulg  13733  gsumfzreidx  13882  gsumfzsubmcl  13883  gsumfzmptfidmadd  13884  gsumfzmhm  13888  gsumfzfsumlemm  14559  gsumfzfsum  14560  ltexp2  15623  logblt  15644  mersenne  15679  lgsval2lem  15697  lgsvalmod  15706  lgsneg  15711  lgsdilem  15714  lgssq  15727  lgssq2  15728  gausslemma2dlem1a  15745  gausslemma2dlem3  15750  lgseisenlem2  15758  lgsquadlem1  15764  lgsquadlem2  15765  lgsquadlem3  15766  lgsquad3  15771  2lgslem1a2  15774  2sqlem3  15804  2sqlem8  15810  supfz  16469  inffz  16470