Theorem zred 9071

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 8959	. 2 |- ZZ C_ RR
2		zred.1	. 2 |- ( ph -> A e. ZZ )
3	1, 2	sseldi 3059	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1461   RRcr 7540   ZZcz 8952

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-3or 944  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-rex 2394  df-rab 2397  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-br 3894  df-iota 5044  df-fv 5087  df-ov 5729  df-neg 7853  df-z 8953

This theorem is referenced by:  zcnd  9072  btwnapz  9079  eluzelre  9232  eluzadd  9250  eluzsub  9251  uzm1  9252  z2ge  9496  zltaddlt1le  9676  fztri3or  9706  fznlem  9708  fzdisj  9719  fzpreddisj  9738  fznatpl1  9743  uzdisj  9760  fzm1  9767  fz0fzdiffz0  9794  elfzmlbm  9795  elfzmlbp  9796  difelfznle  9799  nn0disj  9802  elfzolt3  9821  fzonel  9824  fzouzdisj  9844  fzonmapblen  9851  fzoaddel  9856  elfzonelfzo  9894  qtri3or  9907  exbtwnzlemstep  9912  exbtwnzlemex  9914  exbtwnz  9915  rebtwn2zlemstep  9917  rebtwn2z  9919  qbtwnrelemcalc  9920  qbtwnre  9921  apbtwnz  9934  qfraclt1  9940  qfracge0  9941  flqge  9942  flid  9944  flqltnz  9947  flqwordi  9948  flqaddz  9957  flqmulnn0  9959  btwnzge0  9960  2tnp1ge0ge0  9961  flhalf  9962  flltdivnn0lt  9964  fldiv4p1lem1div2  9965  ceiqge  9969  ceiqm1l  9971  ceiqle  9973  flqleceil  9977  flqeqceilz  9978  intfracq  9980  modqval  9984  modqge0  9992  modqlt  9993  modqmulnn  10002  mulp1mod1  10025  modaddmodup  10047  modaddmodlo  10048  modsumfzodifsn  10056  addmodlteq  10058  frec2uzlt2d  10064  frec2uzf1od  10066  uzennn  10096  seq3split  10139  iseqf1olemkle  10144  iseqf1olemqcl  10146  iseqf1olemnab  10148  iseqf1olemab  10149  iseqf1olemqk  10154  seq3f1olemqsumkj  10158  seq3f1olemqsumk  10159  seq3f1olemqsum  10160  exp3val  10182  expcanlem  10349  expcan  10350  facavg  10379  bcval4  10385  bcp1nk  10395  bcval5  10396  zfz1isolemiso  10469  seq3coll  10472  seq3shft  10497  resqrexlemdecn  10670  fzomaxdiflem  10770  fsum3cvg3  11051  fsumm1  11071  fsum1p  11073  fsum0diaglem  11095  isumshft  11145  isumsplit  11146  divcnv  11152  geolim2  11167  cvgratnnlemabsle  11182  cvgratnnlemsumlt  11183  cvgratnnlemrate  11185  cvgratz  11187  mertenslemi1  11190  zdvdsdc  11356  dvdslelemd  11383  oexpneg  11416  ltoddhalfle  11432  divalglemnqt  11459  divalglemex  11461  divalglemeuneg  11462  flodddiv4t2lthalf  11476  zsupcl  11482  zssinfcl  11483  infssuzex  11484  dvdsbnd  11487  dvdslegcd  11495  gcd0id  11509  gcdneg  11512  bezoutlemsup  11537  dfgcd2  11542  nn0seqcvgd  11562  lcmgcdlem  11598  ncoprmgcdne1b  11610  nprm  11644  prmdvdsfz  11659  coprm  11662  prmexpb  11669  prmfac1  11670  znege1  11695  sqrt2irrap  11697  hashdvds  11736  hashgcdlem  11742  oddennn  11744  ennnfoneleminc  11763  supfz  12918  inffz  12919