Theorem zred 9592

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 9476	. 2 |- ZZ C_ RR
2		zred.1	. 2 |- ( ph -> A e. ZZ )
3	1, 2	sselid 3223	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 8021   ZZcz 9469

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 8343  df-z 9470

This theorem is referenced by:  zcnd  9593  btwnapz  9600  eluzmn  9752  eluzelre  9756  eluzadd  9775  eluzsub  9776  uzm1  9777  z2ge  10051  zltaddlt1le  10232  fztri3or  10264  fznlem  10266  fzdisj  10277  fzpreddisj  10296  fznatpl1  10301  uzdisj  10318  fzm1  10325  fz0fzdiffz0  10355  elfzmlbm  10356  elfzmlbp  10357  difelfznle  10360  nn0disj  10363  elfzolt3  10383  fzonel  10386  fzouzdisj  10407  fzodisjsn  10409  fzonmapblen  10416  fzoaddel  10422  elincfzoext  10428  elfzonelfzo  10465  zsupcl  10481  zssinfcl  10482  infssuzex  10483  suprzubdc  10486  zsupssdc  10488  suprzcl2dc  10489  qtri3or  10490  exbtwnzlemstep  10497  exbtwnzlemex  10499  exbtwnz  10500  rebtwn2zlemstep  10502  rebtwn2z  10504  qbtwnrelemcalc  10505  qbtwnre  10506  apbtwnz  10524  qfraclt1  10530  qfracge0  10531  flqge  10532  flid  10534  flqltnz  10537  flqwordi  10538  flqaddz  10547  flqmulnn0  10549  btwnzge0  10550  2tnp1ge0ge0  10551  flhalf  10552  flltdivnn0lt  10554  fldiv4p1lem1div2  10555  fldiv4lem1div2uz2  10556  ceiqge  10561  ceiqm1l  10563  ceiqle  10565  flqleceil  10569  flqeqceilz  10570  intfracq  10572  modqval  10576  modqge0  10584  modqlt  10585  modqmulnn  10594  mulp1mod1  10617  modaddmodup  10639  modaddmodlo  10640  modsumfzodifsn  10648  addmodlteq  10650  frec2uzlt2d  10656  frec2uzf1od  10658  uzennn  10688  seq3split  10740  iseqf1olemkle  10749  iseqf1olemqcl  10751  iseqf1olemnab  10753  iseqf1olemab  10754  iseqf1olemqk  10759  seq3f1olemqsumkj  10763  seq3f1olemqsumk  10764  seq3f1olemqsum  10765  seqf1oglem1  10771  seqf1oglem2  10772  seqfeq4g  10783  exp3val  10793  expcanlem  10967  expcan  10968  facavg  10998  bcval4  11004  bcp1nk  11014  bcval5  11015  zfz1isolemiso  11093  seq3coll  11096  iswrdiz  11110  ccatrn  11176  ccatalpha  11180  seq3shft  11389  resqrexlemdecn  11563  fzomaxdiflem  11663  nn0maxcl  11776  fsum3cvg3  11947  fsumm1  11967  fsum1p  11969  fsum0diaglem  11991  isumshft  12041  isumsplit  12042  divcnv  12048  geolim2  12063  cvgratnnlemabsle  12078  cvgratnnlemsumlt  12079  cvgratnnlemrate  12081  cvgratz  12083  mertenslemi1  12086  fprodntrivap  12135  prodsnf  12143  fprod1p  12150  fprodeq0  12168  zdvdsdc  12363  dvdslelemd  12394  oexpneg  12428  ltoddhalfle  12444  divalglemnqt  12471  divalglemex  12473  divalglemeuneg  12474  flodddiv4t2lthalf  12490  bitsfzolem  12505  bitsfzo  12506  bitsmod  12507  bitscmp  12509  dvdsbnd  12517  dvdslegcd  12525  gcd0id  12540  gcdneg  12543  bezoutlemsup  12570  dfgcd2  12575  uzwodc  12598  nn0seqcvgd  12603  lcmgcdlem  12639  ncoprmgcdne1b  12651  nprm  12685  prmdc  12692  prmdvdsfz  12701  isprm5lem  12703  coprm  12706  prmexpb  12713  prmfac1  12714  znege1  12740  sqrt2irrap  12742  hashdvds  12783  eulerthlemrprm  12791  eulerthlema  12792  hashgcdlem  12800  pythagtriplem13  12839  pythagtriplem16  12842  pcxcl  12874  pcaddlem  12902  pcadd  12903  pcfac  12913  qexpz  12915  4sqlem7  12947  4sqlem10  12950  4sqexercise2  12962  4sqlemsdc  12963  4sqlem11  12964  4sqlem12  12965  4sqlem15  12968  4sqlem16  12969  4sqlem17  12970  oddennn  13003  ennnfoneleminc  13022  nninfdclemp1  13061  nninfdclemlt  13062  gsumfzval  13464  gsumfzz  13568  gsumfzcl  13572  mulgfng  13701  subgmulg  13765  gsumfzreidx  13914  gsumfzsubmcl  13915  gsumfzmptfidmadd  13916  gsumfzmhm  13920  gsumfzfsumlemm  14591  gsumfzfsum  14592  ltexp2  15655  logblt  15676  mersenne  15711  lgsval2lem  15729  lgsvalmod  15738  lgsneg  15743  lgsdilem  15746  lgssq  15759  lgssq2  15760  gausslemma2dlem1a  15777  gausslemma2dlem3  15782  lgseisenlem2  15790  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad3  15803  2lgslem1a2  15806  2sqlem3  15836  2sqlem8  15842  supfz  16611  inffz  16612