Theorem zred 9508

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

Syntax hints:   → wi 4   ∈ wcel 2177  ℝcr 7937  ℤcz 9385

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491  df-rab 2494  df-v 2775  df-un 3172  df-in 3174  df-ss 3181  df-sn 3641  df-pr 3642  df-op 3644  df-uni 3854  df-br 4049  df-iota 5238  df-fv 5285  df-ov 5957  df-neg 8259  df-z 9386

This theorem is referenced by:  zcnd  9509  btwnapz  9516  eluzelre  9671  eluzadd  9690  eluzsub  9691  uzm1  9692  z2ge  9961  zltaddlt1le  10142  fztri3or  10174  fznlem  10176  fzdisj  10187  fzpreddisj  10206  fznatpl1  10211  uzdisj  10228  fzm1  10235  fz0fzdiffz0  10265  elfzmlbm  10266  elfzmlbp  10267  difelfznle  10270  nn0disj  10273  elfzolt3  10293  fzonel  10296  fzouzdisj  10317  fzonmapblen  10324  fzoaddel  10329  elincfzoext  10335  elfzonelfzo  10372  zsupcl  10387  zssinfcl  10388  infssuzex  10389  suprzubdc  10392  zsupssdc  10394  suprzcl2dc  10395  qtri3or  10396  exbtwnzlemstep  10403  exbtwnzlemex  10405  exbtwnz  10406  rebtwn2zlemstep  10408  rebtwn2z  10410  qbtwnrelemcalc  10411  qbtwnre  10412  apbtwnz  10430  qfraclt1  10436  qfracge0  10437  flqge  10438  flid  10440  flqltnz  10443  flqwordi  10444  flqaddz  10453  flqmulnn0  10455  btwnzge0  10456  2tnp1ge0ge0  10457  flhalf  10458  flltdivnn0lt  10460  fldiv4p1lem1div2  10461  fldiv4lem1div2uz2  10462  ceiqge  10467  ceiqm1l  10469  ceiqle  10471  flqleceil  10475  flqeqceilz  10476  intfracq  10478  modqval  10482  modqge0  10490  modqlt  10491  modqmulnn  10500  mulp1mod1  10523  modaddmodup  10545  modaddmodlo  10546  modsumfzodifsn  10554  addmodlteq  10556  frec2uzlt2d  10562  frec2uzf1od  10564  uzennn  10594  seq3split  10646  iseqf1olemkle  10655  iseqf1olemqcl  10657  iseqf1olemnab  10659  iseqf1olemab  10660  iseqf1olemqk  10665  seq3f1olemqsumkj  10669  seq3f1olemqsumk  10670  seq3f1olemqsum  10671  seqf1oglem1  10677  seqf1oglem2  10678  seqfeq4g  10689  exp3val  10699  expcanlem  10873  expcan  10874  facavg  10904  bcval4  10910  bcp1nk  10920  bcval5  10921  zfz1isolemiso  10997  seq3coll  11000  iswrdiz  11014  ccatrn  11079  seq3shft  11199  resqrexlemdecn  11373  fzomaxdiflem  11473  nn0maxcl  11586  fsum3cvg3  11757  fsumm1  11777  fsum1p  11779  fsum0diaglem  11801  isumshft  11851  isumsplit  11852  divcnv  11858  geolim2  11873  cvgratnnlemabsle  11888  cvgratnnlemsumlt  11889  cvgratnnlemrate  11891  cvgratz  11893  mertenslemi1  11896  fprodntrivap  11945  prodsnf  11953  fprod1p  11960  fprodeq0  11978  zdvdsdc  12173  dvdslelemd  12204  oexpneg  12238  ltoddhalfle  12254  divalglemnqt  12281  divalglemex  12283  divalglemeuneg  12284  flodddiv4t2lthalf  12300  bitsfzolem  12315  bitsfzo  12316  bitsmod  12317  bitscmp  12319  dvdsbnd  12327  dvdslegcd  12335  gcd0id  12350  gcdneg  12353  bezoutlemsup  12380  dfgcd2  12385  uzwodc  12408  nn0seqcvgd  12413  lcmgcdlem  12449  ncoprmgcdne1b  12461  nprm  12495  prmdc  12502  prmdvdsfz  12511  isprm5lem  12513  coprm  12516  prmexpb  12523  prmfac1  12524  znege1  12550  sqrt2irrap  12552  hashdvds  12593  eulerthlemrprm  12601  eulerthlema  12602  hashgcdlem  12610  pythagtriplem13  12649  pythagtriplem16  12652  pcxcl  12684  pcaddlem  12712  pcadd  12713  pcfac  12723  qexpz  12725  4sqlem7  12757  4sqlem10  12760  4sqexercise2  12772  4sqlemsdc  12773  4sqlem11  12774  4sqlem12  12775  4sqlem15  12778  4sqlem16  12779  4sqlem17  12780  oddennn  12813  ennnfoneleminc  12832  nninfdclemp1  12871  nninfdclemlt  12872  gsumfzval  13273  gsumfzz  13377  gsumfzcl  13381  mulgfng  13510  subgmulg  13574  gsumfzreidx  13723  gsumfzsubmcl  13724  gsumfzmptfidmadd  13725  gsumfzmhm  13729  gsumfzfsumlemm  14399  gsumfzfsum  14400  ltexp2  15463  logblt  15484  mersenne  15519  lgsval2lem  15537  lgsvalmod  15546  lgsneg  15551  lgsdilem  15554  lgssq  15567  lgssq2  15568  gausslemma2dlem1a  15585  gausslemma2dlem3  15590  lgseisenlem2  15598  lgsquadlem1  15604  lgsquadlem2  15605  lgsquadlem3  15606  lgsquad3  15611  2lgslem1a2  15614  2sqlem3  15644  2sqlem8  15650  supfz  16125  inffz  16126