Theorem zred 9595

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8024  ℤcz 9472

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 2802  df-un 3202  df-in 3204  df-ss 3211  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016  df-neg 8346  df-z 9473

This theorem is referenced by:  zcnd  9596  btwnapz  9603  eluzmn  9755  eluzelre  9759  eluzadd  9778  eluzsub  9779  uzm1  9780  z2ge  10054  zltaddlt1le  10235  fztri3or  10267  fznlem  10269  fzdisj  10280  fzpreddisj  10299  fznatpl1  10304  uzdisj  10321  fzm1  10328  fz0fzdiffz0  10358  elfzmlbm  10359  elfzmlbp  10360  difelfznle  10363  nn0disj  10366  elfzolt3  10386  fzonel  10389  fzouzdisj  10410  fzodisjsn  10412  fzonmapblen  10419  fzoaddel  10425  elincfzoext  10431  elfzonelfzo  10468  zsupcl  10484  zssinfcl  10485  infssuzex  10486  suprzubdc  10489  zsupssdc  10491  suprzcl2dc  10492  qtri3or  10493  exbtwnzlemstep  10500  exbtwnzlemex  10502  exbtwnz  10503  rebtwn2zlemstep  10505  rebtwn2z  10507  qbtwnrelemcalc  10508  qbtwnre  10509  apbtwnz  10527  qfraclt1  10533  qfracge0  10534  flqge  10535  flid  10537  flqltnz  10540  flqwordi  10541  flqaddz  10550  flqmulnn0  10552  btwnzge0  10553  2tnp1ge0ge0  10554  flhalf  10555  flltdivnn0lt  10557  fldiv4p1lem1div2  10558  fldiv4lem1div2uz2  10559  ceiqge  10564  ceiqm1l  10566  ceiqle  10568  flqleceil  10572  flqeqceilz  10573  intfracq  10575  modqval  10579  modqge0  10587  modqlt  10588  modqmulnn  10597  mulp1mod1  10620  modaddmodup  10642  modaddmodlo  10643  modsumfzodifsn  10651  addmodlteq  10653  frec2uzlt2d  10659  frec2uzf1od  10661  uzennn  10691  seq3split  10743  iseqf1olemkle  10752  iseqf1olemqcl  10754  iseqf1olemnab  10756  iseqf1olemab  10757  iseqf1olemqk  10762  seq3f1olemqsumkj  10766  seq3f1olemqsumk  10767  seq3f1olemqsum  10768  seqf1oglem1  10774  seqf1oglem2  10775  seqfeq4g  10786  exp3val  10796  expcanlem  10970  expcan  10971  facavg  11001  bcval4  11007  bcp1nk  11017  bcval5  11018  zfz1isolemiso  11096  seq3coll  11099  iswrdiz  11113  ccatrn  11179  ccatalpha  11183  seq3shft  11392  resqrexlemdecn  11566  fzomaxdiflem  11666  nn0maxcl  11779  fsum3cvg3  11950  fsumm1  11970  fsum1p  11972  fsum0diaglem  11994  isumshft  12044  isumsplit  12045  divcnv  12051  geolim2  12066  cvgratnnlemabsle  12081  cvgratnnlemsumlt  12082  cvgratnnlemrate  12084  cvgratz  12086  mertenslemi1  12089  fprodntrivap  12138  prodsnf  12146  fprod1p  12153  fprodeq0  12171  zdvdsdc  12366  dvdslelemd  12397  oexpneg  12431  ltoddhalfle  12447  divalglemnqt  12474  divalglemex  12476  divalglemeuneg  12477  flodddiv4t2lthalf  12493  bitsfzolem  12508  bitsfzo  12509  bitsmod  12510  bitscmp  12512  dvdsbnd  12520  dvdslegcd  12528  gcd0id  12543  gcdneg  12546  bezoutlemsup  12573  dfgcd2  12578  uzwodc  12601  nn0seqcvgd  12606  lcmgcdlem  12642  ncoprmgcdne1b  12654  nprm  12688  prmdc  12695  prmdvdsfz  12704  isprm5lem  12706  coprm  12709  prmexpb  12716  prmfac1  12717  znege1  12743  sqrt2irrap  12745  hashdvds  12786  eulerthlemrprm  12794  eulerthlema  12795  hashgcdlem  12803  pythagtriplem13  12842  pythagtriplem16  12845  pcxcl  12877  pcaddlem  12905  pcadd  12906  pcfac  12916  qexpz  12918  4sqlem7  12950  4sqlem10  12953  4sqexercise2  12965  4sqlemsdc  12966  4sqlem11  12967  4sqlem12  12968  4sqlem15  12971  4sqlem16  12972  4sqlem17  12973  oddennn  13006  ennnfoneleminc  13025  nninfdclemp1  13064  nninfdclemlt  13065  gsumfzval  13467  gsumfzz  13571  gsumfzcl  13575  mulgfng  13704  subgmulg  13768  gsumfzreidx  13917  gsumfzsubmcl  13918  gsumfzmptfidmadd  13919  gsumfzmhm  13923  gsumfzfsumlemm  14594  gsumfzfsum  14595  ltexp2  15658  logblt  15679  mersenne  15714  lgsval2lem  15732  lgsvalmod  15741  lgsneg  15746  lgsdilem  15749  lgssq  15762  lgssq2  15763  gausslemma2dlem1a  15780  gausslemma2dlem3  15785  lgseisenlem2  15793  lgsquadlem1  15799  lgsquadlem2  15800  lgsquadlem3  15801  lgsquad3  15806  2lgslem1a2  15809  2sqlem3  15839  2sqlem8  15845  supfz  16625  inffz  16626  gsumgfsumlem  16633