Theorem zred 9557

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 7986  ℤcz 9434

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 3888  df-br 4083  df-iota 5274  df-fv 5322  df-ov 5997  df-neg 8308  df-z 9435

This theorem is referenced by:  zcnd  9558  btwnapz  9565  eluzelre  9720  eluzadd  9739  eluzsub  9740  uzm1  9741  z2ge  10010  zltaddlt1le  10191  fztri3or  10223  fznlem  10225  fzdisj  10236  fzpreddisj  10255  fznatpl1  10260  uzdisj  10277  fzm1  10284  fz0fzdiffz0  10314  elfzmlbm  10315  elfzmlbp  10316  difelfznle  10319  nn0disj  10322  elfzolt3  10342  fzonel  10345  fzouzdisj  10366  fzodisjsn  10368  fzonmapblen  10375  fzoaddel  10380  elincfzoext  10386  elfzonelfzo  10423  zsupcl  10438  zssinfcl  10439  infssuzex  10440  suprzubdc  10443  zsupssdc  10445  suprzcl2dc  10446  qtri3or  10447  exbtwnzlemstep  10454  exbtwnzlemex  10456  exbtwnz  10457  rebtwn2zlemstep  10459  rebtwn2z  10461  qbtwnrelemcalc  10462  qbtwnre  10463  apbtwnz  10481  qfraclt1  10487  qfracge0  10488  flqge  10489  flid  10491  flqltnz  10494  flqwordi  10495  flqaddz  10504  flqmulnn0  10506  btwnzge0  10507  2tnp1ge0ge0  10508  flhalf  10509  flltdivnn0lt  10511  fldiv4p1lem1div2  10512  fldiv4lem1div2uz2  10513  ceiqge  10518  ceiqm1l  10520  ceiqle  10522  flqleceil  10526  flqeqceilz  10527  intfracq  10529  modqval  10533  modqge0  10541  modqlt  10542  modqmulnn  10551  mulp1mod1  10574  modaddmodup  10596  modaddmodlo  10597  modsumfzodifsn  10605  addmodlteq  10607  frec2uzlt2d  10613  frec2uzf1od  10615  uzennn  10645  seq3split  10697  iseqf1olemkle  10706  iseqf1olemqcl  10708  iseqf1olemnab  10710  iseqf1olemab  10711  iseqf1olemqk  10716  seq3f1olemqsumkj  10720  seq3f1olemqsumk  10721  seq3f1olemqsum  10722  seqf1oglem1  10728  seqf1oglem2  10729  seqfeq4g  10740  exp3val  10750  expcanlem  10924  expcan  10925  facavg  10955  bcval4  10961  bcp1nk  10971  bcval5  10972  zfz1isolemiso  11048  seq3coll  11051  iswrdiz  11065  ccatrn  11130  seq3shft  11335  resqrexlemdecn  11509  fzomaxdiflem  11609  nn0maxcl  11722  fsum3cvg3  11893  fsumm1  11913  fsum1p  11915  fsum0diaglem  11937  isumshft  11987  isumsplit  11988  divcnv  11994  geolim2  12009  cvgratnnlemabsle  12024  cvgratnnlemsumlt  12025  cvgratnnlemrate  12027  cvgratz  12029  mertenslemi1  12032  fprodntrivap  12081  prodsnf  12089  fprod1p  12096  fprodeq0  12114  zdvdsdc  12309  dvdslelemd  12340  oexpneg  12374  ltoddhalfle  12390  divalglemnqt  12417  divalglemex  12419  divalglemeuneg  12420  flodddiv4t2lthalf  12436  bitsfzolem  12451  bitsfzo  12452  bitsmod  12453  bitscmp  12455  dvdsbnd  12463  dvdslegcd  12471  gcd0id  12486  gcdneg  12489  bezoutlemsup  12516  dfgcd2  12521  uzwodc  12544  nn0seqcvgd  12549  lcmgcdlem  12585  ncoprmgcdne1b  12597  nprm  12631  prmdc  12638  prmdvdsfz  12647  isprm5lem  12649  coprm  12652  prmexpb  12659  prmfac1  12660  znege1  12686  sqrt2irrap  12688  hashdvds  12729  eulerthlemrprm  12737  eulerthlema  12738  hashgcdlem  12746  pythagtriplem13  12785  pythagtriplem16  12788  pcxcl  12820  pcaddlem  12848  pcadd  12849  pcfac  12859  qexpz  12861  4sqlem7  12893  4sqlem10  12896  4sqexercise2  12908  4sqlemsdc  12909  4sqlem11  12910  4sqlem12  12911  4sqlem15  12914  4sqlem16  12915  4sqlem17  12916  oddennn  12949  ennnfoneleminc  12968  nninfdclemp1  13007  nninfdclemlt  13008  gsumfzval  13410  gsumfzz  13514  gsumfzcl  13518  mulgfng  13647  subgmulg  13711  gsumfzreidx  13860  gsumfzsubmcl  13861  gsumfzmptfidmadd  13862  gsumfzmhm  13866  gsumfzfsumlemm  14536  gsumfzfsum  14537  ltexp2  15600  logblt  15621  mersenne  15656  lgsval2lem  15674  lgsvalmod  15683  lgsneg  15688  lgsdilem  15691  lgssq  15704  lgssq2  15705  gausslemma2dlem1a  15722  gausslemma2dlem3  15727  lgseisenlem2  15735  lgsquadlem1  15741  lgsquadlem2  15742  lgsquadlem3  15743  lgsquad3  15748  2lgslem1a2  15751  2sqlem3  15781  2sqlem8  15787  supfz  16370  inffz  16371