ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  zred Unicode version

Theorem zred 9185
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
StepHypRef Expression
1 zssre 9073 . 2  |-  ZZ  C_  RR
2 zred.1 . 2  |-  ( ph  ->  A  e.  ZZ )
31, 2sseldi 3095 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1480   RRcr 7631   ZZcz 9066
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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-rab 2425  df-v 2688  df-un 3075  df-in 3077  df-ss 3084  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131  df-ov 5777  df-neg 7948  df-z 9067
This theorem is referenced by:  zcnd  9186  btwnapz  9193  eluzelre  9348  eluzadd  9366  eluzsub  9367  uzm1  9368  z2ge  9621  zltaddlt1le  9801  fztri3or  9831  fznlem  9833  fzdisj  9844  fzpreddisj  9863  fznatpl1  9868  uzdisj  9885  fzm1  9892  fz0fzdiffz0  9919  elfzmlbm  9920  elfzmlbp  9921  difelfznle  9924  nn0disj  9927  elfzolt3  9946  fzonel  9949  fzouzdisj  9969  fzonmapblen  9976  fzoaddel  9981  elfzonelfzo  10019  qtri3or  10032  exbtwnzlemstep  10037  exbtwnzlemex  10039  exbtwnz  10040  rebtwn2zlemstep  10042  rebtwn2z  10044  qbtwnrelemcalc  10045  qbtwnre  10046  apbtwnz  10059  qfraclt1  10065  qfracge0  10066  flqge  10067  flid  10069  flqltnz  10072  flqwordi  10073  flqaddz  10082  flqmulnn0  10084  btwnzge0  10085  2tnp1ge0ge0  10086  flhalf  10087  flltdivnn0lt  10089  fldiv4p1lem1div2  10090  ceiqge  10094  ceiqm1l  10096  ceiqle  10098  flqleceil  10102  flqeqceilz  10103  intfracq  10105  modqval  10109  modqge0  10117  modqlt  10118  modqmulnn  10127  mulp1mod1  10150  modaddmodup  10172  modaddmodlo  10173  modsumfzodifsn  10181  addmodlteq  10183  frec2uzlt2d  10189  frec2uzf1od  10191  uzennn  10221  seq3split  10264  iseqf1olemkle  10269  iseqf1olemqcl  10271  iseqf1olemnab  10273  iseqf1olemab  10274  iseqf1olemqk  10279  seq3f1olemqsumkj  10283  seq3f1olemqsumk  10284  seq3f1olemqsum  10285  exp3val  10307  expcanlem  10474  expcan  10475  facavg  10504  bcval4  10510  bcp1nk  10520  bcval5  10521  zfz1isolemiso  10594  seq3coll  10597  seq3shft  10622  resqrexlemdecn  10796  fzomaxdiflem  10896  fsum3cvg3  11177  fsumm1  11197  fsum1p  11199  fsum0diaglem  11221  isumshft  11271  isumsplit  11272  divcnv  11278  geolim2  11293  cvgratnnlemabsle  11308  cvgratnnlemsumlt  11309  cvgratnnlemrate  11311  cvgratz  11313  mertenslemi1  11316  zdvdsdc  11525  dvdslelemd  11552  oexpneg  11585  ltoddhalfle  11601  divalglemnqt  11628  divalglemex  11630  divalglemeuneg  11631  flodddiv4t2lthalf  11645  zsupcl  11651  zssinfcl  11652  infssuzex  11653  dvdsbnd  11656  dvdslegcd  11664  gcd0id  11678  gcdneg  11681  bezoutlemsup  11708  dfgcd2  11713  nn0seqcvgd  11733  lcmgcdlem  11769  ncoprmgcdne1b  11781  nprm  11815  prmdvdsfz  11830  coprm  11833  prmexpb  11840  prmfac1  11841  znege1  11867  sqrt2irrap  11869  hashdvds  11908  hashgcdlem  11914  oddennn  11916  ennnfoneleminc  11935  supfz  13349  inffz  13350
  Copyright terms: Public domain W3C validator