Theorem zred 9530

Description: An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
zred.1	|- ( ph -> A e. ZZ )

Assertion

Ref	Expression
zred	|- ( ph -> A e. RR )

Proof of Theorem zred

Step	Hyp	Ref	Expression
1		zssre 9414	. 2 |- ZZ C_ RR
2		zred.1	. 2 |- ( ph -> A e. ZZ )
3	1, 2	sselid 3199	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2178   RRcr 7959   ZZcz 9407

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 2189

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 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-rab 2495  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970  df-neg 8281  df-z 9408

This theorem is referenced by:  zcnd  9531  btwnapz  9538  eluzelre  9693  eluzadd  9712  eluzsub  9713  uzm1  9714  z2ge  9983  zltaddlt1le  10164  fztri3or  10196  fznlem  10198  fzdisj  10209  fzpreddisj  10228  fznatpl1  10233  uzdisj  10250  fzm1  10257  fz0fzdiffz0  10287  elfzmlbm  10288  elfzmlbp  10289  difelfznle  10292  nn0disj  10295  elfzolt3  10315  fzonel  10318  fzouzdisj  10339  fzodisjsn  10341  fzonmapblen  10348  fzoaddel  10353  elincfzoext  10359  elfzonelfzo  10396  zsupcl  10411  zssinfcl  10412  infssuzex  10413  suprzubdc  10416  zsupssdc  10418  suprzcl2dc  10419  qtri3or  10420  exbtwnzlemstep  10427  exbtwnzlemex  10429  exbtwnz  10430  rebtwn2zlemstep  10432  rebtwn2z  10434  qbtwnrelemcalc  10435  qbtwnre  10436  apbtwnz  10454  qfraclt1  10460  qfracge0  10461  flqge  10462  flid  10464  flqltnz  10467  flqwordi  10468  flqaddz  10477  flqmulnn0  10479  btwnzge0  10480  2tnp1ge0ge0  10481  flhalf  10482  flltdivnn0lt  10484  fldiv4p1lem1div2  10485  fldiv4lem1div2uz2  10486  ceiqge  10491  ceiqm1l  10493  ceiqle  10495  flqleceil  10499  flqeqceilz  10500  intfracq  10502  modqval  10506  modqge0  10514  modqlt  10515  modqmulnn  10524  mulp1mod1  10547  modaddmodup  10569  modaddmodlo  10570  modsumfzodifsn  10578  addmodlteq  10580  frec2uzlt2d  10586  frec2uzf1od  10588  uzennn  10618  seq3split  10670  iseqf1olemkle  10679  iseqf1olemqcl  10681  iseqf1olemnab  10683  iseqf1olemab  10684  iseqf1olemqk  10689  seq3f1olemqsumkj  10693  seq3f1olemqsumk  10694  seq3f1olemqsum  10695  seqf1oglem1  10701  seqf1oglem2  10702  seqfeq4g  10713  exp3val  10723  expcanlem  10897  expcan  10898  facavg  10928  bcval4  10934  bcp1nk  10944  bcval5  10945  zfz1isolemiso  11021  seq3coll  11024  iswrdiz  11038  ccatrn  11103  seq3shft  11264  resqrexlemdecn  11438  fzomaxdiflem  11538  nn0maxcl  11651  fsum3cvg3  11822  fsumm1  11842  fsum1p  11844  fsum0diaglem  11866  isumshft  11916  isumsplit  11917  divcnv  11923  geolim2  11938  cvgratnnlemabsle  11953  cvgratnnlemsumlt  11954  cvgratnnlemrate  11956  cvgratz  11958  mertenslemi1  11961  fprodntrivap  12010  prodsnf  12018  fprod1p  12025  fprodeq0  12043  zdvdsdc  12238  dvdslelemd  12269  oexpneg  12303  ltoddhalfle  12319  divalglemnqt  12346  divalglemex  12348  divalglemeuneg  12349  flodddiv4t2lthalf  12365  bitsfzolem  12380  bitsfzo  12381  bitsmod  12382  bitscmp  12384  dvdsbnd  12392  dvdslegcd  12400  gcd0id  12415  gcdneg  12418  bezoutlemsup  12445  dfgcd2  12450  uzwodc  12473  nn0seqcvgd  12478  lcmgcdlem  12514  ncoprmgcdne1b  12526  nprm  12560  prmdc  12567  prmdvdsfz  12576  isprm5lem  12578  coprm  12581  prmexpb  12588  prmfac1  12589  znege1  12615  sqrt2irrap  12617  hashdvds  12658  eulerthlemrprm  12666  eulerthlema  12667  hashgcdlem  12675  pythagtriplem13  12714  pythagtriplem16  12717  pcxcl  12749  pcaddlem  12777  pcadd  12778  pcfac  12788  qexpz  12790  4sqlem7  12822  4sqlem10  12825  4sqexercise2  12837  4sqlemsdc  12838  4sqlem11  12839  4sqlem12  12840  4sqlem15  12843  4sqlem16  12844  4sqlem17  12845  oddennn  12878  ennnfoneleminc  12897  nninfdclemp1  12936  nninfdclemlt  12937  gsumfzval  13338  gsumfzz  13442  gsumfzcl  13446  mulgfng  13575  subgmulg  13639  gsumfzreidx  13788  gsumfzsubmcl  13789  gsumfzmptfidmadd  13790  gsumfzmhm  13794  gsumfzfsumlemm  14464  gsumfzfsum  14465  ltexp2  15528  logblt  15549  mersenne  15584  lgsval2lem  15602  lgsvalmod  15611  lgsneg  15616  lgsdilem  15619  lgssq  15632  lgssq2  15633  gausslemma2dlem1a  15650  gausslemma2dlem3  15655  lgseisenlem2  15663  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  lgsquad3  15676  2lgslem1a2  15679  2sqlem3  15709  2sqlem8  15715  supfz  16212  inffz  16213