Theorem zred 9585

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8014  ℤcz 9462

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 5281  df-fv 5329  df-ov 6013  df-neg 8336  df-z 9463

This theorem is referenced by:  zcnd  9586  btwnapz  9593  eluzmn  9745  eluzelre  9749  eluzadd  9768  eluzsub  9769  uzm1  9770  z2ge  10039  zltaddlt1le  10220  fztri3or  10252  fznlem  10254  fzdisj  10265  fzpreddisj  10284  fznatpl1  10289  uzdisj  10306  fzm1  10313  fz0fzdiffz0  10343  elfzmlbm  10344  elfzmlbp  10345  difelfznle  10348  nn0disj  10351  elfzolt3  10371  fzonel  10374  fzouzdisj  10395  fzodisjsn  10397  fzonmapblen  10404  fzoaddel  10410  elincfzoext  10416  elfzonelfzo  10453  zsupcl  10468  zssinfcl  10469  infssuzex  10470  suprzubdc  10473  zsupssdc  10475  suprzcl2dc  10476  qtri3or  10477  exbtwnzlemstep  10484  exbtwnzlemex  10486  exbtwnz  10487  rebtwn2zlemstep  10489  rebtwn2z  10491  qbtwnrelemcalc  10492  qbtwnre  10493  apbtwnz  10511  qfraclt1  10517  qfracge0  10518  flqge  10519  flid  10521  flqltnz  10524  flqwordi  10525  flqaddz  10534  flqmulnn0  10536  btwnzge0  10537  2tnp1ge0ge0  10538  flhalf  10539  flltdivnn0lt  10541  fldiv4p1lem1div2  10542  fldiv4lem1div2uz2  10543  ceiqge  10548  ceiqm1l  10550  ceiqle  10552  flqleceil  10556  flqeqceilz  10557  intfracq  10559  modqval  10563  modqge0  10571  modqlt  10572  modqmulnn  10581  mulp1mod1  10604  modaddmodup  10626  modaddmodlo  10627  modsumfzodifsn  10635  addmodlteq  10637  frec2uzlt2d  10643  frec2uzf1od  10645  uzennn  10675  seq3split  10727  iseqf1olemkle  10736  iseqf1olemqcl  10738  iseqf1olemnab  10740  iseqf1olemab  10741  iseqf1olemqk  10746  seq3f1olemqsumkj  10750  seq3f1olemqsumk  10751  seq3f1olemqsum  10752  seqf1oglem1  10758  seqf1oglem2  10759  seqfeq4g  10770  exp3val  10780  expcanlem  10954  expcan  10955  facavg  10985  bcval4  10991  bcp1nk  11001  bcval5  11002  zfz1isolemiso  11079  seq3coll  11082  iswrdiz  11096  ccatrn  11162  ccatalpha  11166  seq3shft  11370  resqrexlemdecn  11544  fzomaxdiflem  11644  nn0maxcl  11757  fsum3cvg3  11928  fsumm1  11948  fsum1p  11950  fsum0diaglem  11972  isumshft  12022  isumsplit  12023  divcnv  12029  geolim2  12044  cvgratnnlemabsle  12059  cvgratnnlemsumlt  12060  cvgratnnlemrate  12062  cvgratz  12064  mertenslemi1  12067  fprodntrivap  12116  prodsnf  12124  fprod1p  12131  fprodeq0  12149  zdvdsdc  12344  dvdslelemd  12375  oexpneg  12409  ltoddhalfle  12425  divalglemnqt  12452  divalglemex  12454  divalglemeuneg  12455  flodddiv4t2lthalf  12471  bitsfzolem  12486  bitsfzo  12487  bitsmod  12488  bitscmp  12490  dvdsbnd  12498  dvdslegcd  12506  gcd0id  12521  gcdneg  12524  bezoutlemsup  12551  dfgcd2  12556  uzwodc  12579  nn0seqcvgd  12584  lcmgcdlem  12620  ncoprmgcdne1b  12632  nprm  12666  prmdc  12673  prmdvdsfz  12682  isprm5lem  12684  coprm  12687  prmexpb  12694  prmfac1  12695  znege1  12721  sqrt2irrap  12723  hashdvds  12764  eulerthlemrprm  12772  eulerthlema  12773  hashgcdlem  12781  pythagtriplem13  12820  pythagtriplem16  12823  pcxcl  12855  pcaddlem  12883  pcadd  12884  pcfac  12894  qexpz  12896  4sqlem7  12928  4sqlem10  12931  4sqexercise2  12943  4sqlemsdc  12944  4sqlem11  12945  4sqlem12  12946  4sqlem15  12949  4sqlem16  12950  4sqlem17  12951  oddennn  12984  ennnfoneleminc  13003  nninfdclemp1  13042  nninfdclemlt  13043  gsumfzval  13445  gsumfzz  13549  gsumfzcl  13553  mulgfng  13682  subgmulg  13746  gsumfzreidx  13895  gsumfzsubmcl  13896  gsumfzmptfidmadd  13897  gsumfzmhm  13901  gsumfzfsumlemm  14572  gsumfzfsum  14573  ltexp2  15636  logblt  15657  mersenne  15692  lgsval2lem  15710  lgsvalmod  15719  lgsneg  15724  lgsdilem  15727  lgssq  15740  lgssq2  15741  gausslemma2dlem1a  15758  gausslemma2dlem3  15763  lgseisenlem2  15771  lgsquadlem1  15777  lgsquadlem2  15778  lgsquadlem3  15779  lgsquad3  15784  2lgslem1a2  15787  2sqlem3  15817  2sqlem8  15823  supfz  16553  inffz  16554