Theorem zred 9580

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

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 8009   ZZcz 9457

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 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010  df-neg 8331  df-z 9458

This theorem is referenced by:  zcnd  9581  btwnapz  9588  eluzmn  9740  eluzelre  9744  eluzadd  9763  eluzsub  9764  uzm1  9765  z2ge  10034  zltaddlt1le  10215  fztri3or  10247  fznlem  10249  fzdisj  10260  fzpreddisj  10279  fznatpl1  10284  uzdisj  10301  fzm1  10308  fz0fzdiffz0  10338  elfzmlbm  10339  elfzmlbp  10340  difelfznle  10343  nn0disj  10346  elfzolt3  10366  fzonel  10369  fzouzdisj  10390  fzodisjsn  10392  fzonmapblen  10399  fzoaddel  10405  elincfzoext  10411  elfzonelfzo  10448  zsupcl  10463  zssinfcl  10464  infssuzex  10465  suprzubdc  10468  zsupssdc  10470  suprzcl2dc  10471  qtri3or  10472  exbtwnzlemstep  10479  exbtwnzlemex  10481  exbtwnz  10482  rebtwn2zlemstep  10484  rebtwn2z  10486  qbtwnrelemcalc  10487  qbtwnre  10488  apbtwnz  10506  qfraclt1  10512  qfracge0  10513  flqge  10514  flid  10516  flqltnz  10519  flqwordi  10520  flqaddz  10529  flqmulnn0  10531  btwnzge0  10532  2tnp1ge0ge0  10533  flhalf  10534  flltdivnn0lt  10536  fldiv4p1lem1div2  10537  fldiv4lem1div2uz2  10538  ceiqge  10543  ceiqm1l  10545  ceiqle  10547  flqleceil  10551  flqeqceilz  10552  intfracq  10554  modqval  10558  modqge0  10566  modqlt  10567  modqmulnn  10576  mulp1mod1  10599  modaddmodup  10621  modaddmodlo  10622  modsumfzodifsn  10630  addmodlteq  10632  frec2uzlt2d  10638  frec2uzf1od  10640  uzennn  10670  seq3split  10722  iseqf1olemkle  10731  iseqf1olemqcl  10733  iseqf1olemnab  10735  iseqf1olemab  10736  iseqf1olemqk  10741  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seqf1oglem1  10753  seqf1oglem2  10754  seqfeq4g  10765  exp3val  10775  expcanlem  10949  expcan  10950  facavg  10980  bcval4  10986  bcp1nk  10996  bcval5  10997  zfz1isolemiso  11074  seq3coll  11077  iswrdiz  11091  ccatrn  11157  ccatalpha  11161  seq3shft  11365  resqrexlemdecn  11539  fzomaxdiflem  11639  nn0maxcl  11752  fsum3cvg3  11923  fsumm1  11943  fsum1p  11945  fsum0diaglem  11967  isumshft  12017  isumsplit  12018  divcnv  12024  geolim2  12039  cvgratnnlemabsle  12054  cvgratnnlemsumlt  12055  cvgratnnlemrate  12057  cvgratz  12059  mertenslemi1  12062  fprodntrivap  12111  prodsnf  12119  fprod1p  12126  fprodeq0  12144  zdvdsdc  12339  dvdslelemd  12370  oexpneg  12404  ltoddhalfle  12420  divalglemnqt  12447  divalglemex  12449  divalglemeuneg  12450  flodddiv4t2lthalf  12466  bitsfzolem  12481  bitsfzo  12482  bitsmod  12483  bitscmp  12485  dvdsbnd  12493  dvdslegcd  12501  gcd0id  12516  gcdneg  12519  bezoutlemsup  12546  dfgcd2  12551  uzwodc  12574  nn0seqcvgd  12579  lcmgcdlem  12615  ncoprmgcdne1b  12627  nprm  12661  prmdc  12668  prmdvdsfz  12677  isprm5lem  12679  coprm  12682  prmexpb  12689  prmfac1  12690  znege1  12716  sqrt2irrap  12718  hashdvds  12759  eulerthlemrprm  12767  eulerthlema  12768  hashgcdlem  12776  pythagtriplem13  12815  pythagtriplem16  12818  pcxcl  12850  pcaddlem  12878  pcadd  12879  pcfac  12889  qexpz  12891  4sqlem7  12923  4sqlem10  12926  4sqexercise2  12938  4sqlemsdc  12939  4sqlem11  12940  4sqlem12  12941  4sqlem15  12944  4sqlem16  12945  4sqlem17  12946  oddennn  12979  ennnfoneleminc  12998  nninfdclemp1  13037  nninfdclemlt  13038  gsumfzval  13440  gsumfzz  13544  gsumfzcl  13548  mulgfng  13677  subgmulg  13741  gsumfzreidx  13890  gsumfzsubmcl  13891  gsumfzmptfidmadd  13892  gsumfzmhm  13896  gsumfzfsumlemm  14567  gsumfzfsum  14568  ltexp2  15631  logblt  15652  mersenne  15687  lgsval2lem  15705  lgsvalmod  15714  lgsneg  15719  lgsdilem  15722  lgssq  15735  lgssq2  15736  gausslemma2dlem1a  15753  gausslemma2dlem3  15758  lgseisenlem2  15766  lgsquadlem1  15772  lgsquadlem2  15773  lgsquadlem3  15774  lgsquad3  15779  2lgslem1a2  15782  2sqlem3  15812  2sqlem8  15818  supfz  16527  inffz  16528