Theorem zred 9321

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

Syntax hints:   -> wi 4   e. wcel 2141   RRcr 7760   ZZcz 9199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-rab 2457  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-br 3988  df-iota 5158  df-fv 5204  df-ov 5853  df-neg 8080  df-z 9200

This theorem is referenced by:  zcnd  9322  btwnapz  9329  eluzelre  9484  eluzadd  9502  eluzsub  9503  uzm1  9504  z2ge  9770  zltaddlt1le  9951  fztri3or  9982  fznlem  9984  fzdisj  9995  fzpreddisj  10014  fznatpl1  10019  uzdisj  10036  fzm1  10043  fz0fzdiffz0  10073  elfzmlbm  10074  elfzmlbp  10075  difelfznle  10078  nn0disj  10081  elfzolt3  10100  fzonel  10103  fzouzdisj  10123  fzonmapblen  10130  fzoaddel  10135  elfzonelfzo  10173  qtri3or  10186  exbtwnzlemstep  10191  exbtwnzlemex  10193  exbtwnz  10194  rebtwn2zlemstep  10196  rebtwn2z  10198  qbtwnrelemcalc  10199  qbtwnre  10200  apbtwnz  10217  qfraclt1  10223  qfracge0  10224  flqge  10225  flid  10227  flqltnz  10230  flqwordi  10231  flqaddz  10240  flqmulnn0  10242  btwnzge0  10243  2tnp1ge0ge0  10244  flhalf  10245  flltdivnn0lt  10247  fldiv4p1lem1div2  10248  ceiqge  10252  ceiqm1l  10254  ceiqle  10256  flqleceil  10260  flqeqceilz  10261  intfracq  10263  modqval  10267  modqge0  10275  modqlt  10276  modqmulnn  10285  mulp1mod1  10308  modaddmodup  10330  modaddmodlo  10331  modsumfzodifsn  10339  addmodlteq  10341  frec2uzlt2d  10347  frec2uzf1od  10349  uzennn  10379  seq3split  10422  iseqf1olemkle  10427  iseqf1olemqcl  10429  iseqf1olemnab  10431  iseqf1olemab  10432  iseqf1olemqk  10437  seq3f1olemqsumkj  10441  seq3f1olemqsumk  10442  seq3f1olemqsum  10443  exp3val  10465  expcanlem  10636  expcan  10637  facavg  10667  bcval4  10673  bcp1nk  10683  bcval5  10684  zfz1isolemiso  10761  seq3coll  10764  seq3shft  10789  resqrexlemdecn  10963  fzomaxdiflem  11063  fsum3cvg3  11346  fsumm1  11366  fsum1p  11368  fsum0diaglem  11390  isumshft  11440  isumsplit  11441  divcnv  11447  geolim2  11462  cvgratnnlemabsle  11477  cvgratnnlemsumlt  11478  cvgratnnlemrate  11480  cvgratz  11482  mertenslemi1  11485  fprodntrivap  11534  prodsnf  11542  fprod1p  11549  fprodeq0  11567  zdvdsdc  11761  dvdslelemd  11790  oexpneg  11823  ltoddhalfle  11839  divalglemnqt  11866  divalglemex  11868  divalglemeuneg  11869  flodddiv4t2lthalf  11883  zsupcl  11889  zssinfcl  11890  infssuzex  11891  suprzubdc  11894  zsupssdc  11896  suprzcl2dc  11897  dvdsbnd  11898  dvdslegcd  11906  gcd0id  11921  gcdneg  11924  bezoutlemsup  11951  dfgcd2  11956  uzwodc  11979  nn0seqcvgd  11982  lcmgcdlem  12018  ncoprmgcdne1b  12030  nprm  12064  prmdc  12071  prmdvdsfz  12080  isprm5lem  12082  coprm  12085  prmexpb  12092  prmfac1  12093  znege1  12119  sqrt2irrap  12121  hashdvds  12162  eulerthlemrprm  12170  eulerthlema  12171  hashgcdlem  12179  pythagtriplem13  12217  pythagtriplem16  12220  pcxcl  12252  pcaddlem  12279  pcadd  12280  pcfac  12289  qexpz  12291  4sqlem7  12323  4sqlem10  12326  oddennn  12334  ennnfoneleminc  12353  nninfdclemp1  12392  nninfdclemlt  12393  ltexp2  13613  logblt  13633  lgsval2lem  13664  lgsvalmod  13673  lgsneg  13678  lgsdilem  13681  lgssq  13694  lgssq2  13695  2sqlem3  13706  2sqlem8  13712  supfz  14060  inffz  14061