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

Theorem zred 9166
Description: An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
zred.1 (𝜑𝐴 ∈ ℤ)
Assertion
Ref Expression
zred (𝜑𝐴 ∈ ℝ)

Proof of Theorem zred
StepHypRef Expression
1 zssre 9054 . 2 ℤ ⊆ ℝ
2 zred.1 . 2 (𝜑𝐴 ∈ ℤ)
31, 2sseldi 3090 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1480  cr 7612  cz 9047
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 2119
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 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-rex 2420  df-rab 2423  df-v 2683  df-un 3070  df-in 3072  df-ss 3079  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-br 3925  df-iota 5083  df-fv 5126  df-ov 5770  df-neg 7929  df-z 9048
This theorem is referenced by:  zcnd  9167  btwnapz  9174  eluzelre  9329  eluzadd  9347  eluzsub  9348  uzm1  9349  z2ge  9602  zltaddlt1le  9782  fztri3or  9812  fznlem  9814  fzdisj  9825  fzpreddisj  9844  fznatpl1  9849  uzdisj  9866  fzm1  9873  fz0fzdiffz0  9900  elfzmlbm  9901  elfzmlbp  9902  difelfznle  9905  nn0disj  9908  elfzolt3  9927  fzonel  9930  fzouzdisj  9950  fzonmapblen  9957  fzoaddel  9962  elfzonelfzo  10000  qtri3or  10013  exbtwnzlemstep  10018  exbtwnzlemex  10020  exbtwnz  10021  rebtwn2zlemstep  10023  rebtwn2z  10025  qbtwnrelemcalc  10026  qbtwnre  10027  apbtwnz  10040  qfraclt1  10046  qfracge0  10047  flqge  10048  flid  10050  flqltnz  10053  flqwordi  10054  flqaddz  10063  flqmulnn0  10065  btwnzge0  10066  2tnp1ge0ge0  10067  flhalf  10068  flltdivnn0lt  10070  fldiv4p1lem1div2  10071  ceiqge  10075  ceiqm1l  10077  ceiqle  10079  flqleceil  10083  flqeqceilz  10084  intfracq  10086  modqval  10090  modqge0  10098  modqlt  10099  modqmulnn  10108  mulp1mod1  10131  modaddmodup  10153  modaddmodlo  10154  modsumfzodifsn  10162  addmodlteq  10164  frec2uzlt2d  10170  frec2uzf1od  10172  uzennn  10202  seq3split  10245  iseqf1olemkle  10250  iseqf1olemqcl  10252  iseqf1olemnab  10254  iseqf1olemab  10255  iseqf1olemqk  10260  seq3f1olemqsumkj  10264  seq3f1olemqsumk  10265  seq3f1olemqsum  10266  exp3val  10288  expcanlem  10455  expcan  10456  facavg  10485  bcval4  10491  bcp1nk  10501  bcval5  10502  zfz1isolemiso  10575  seq3coll  10578  seq3shft  10603  resqrexlemdecn  10777  fzomaxdiflem  10877  fsum3cvg3  11158  fsumm1  11178  fsum1p  11180  fsum0diaglem  11202  isumshft  11252  isumsplit  11253  divcnv  11259  geolim2  11274  cvgratnnlemabsle  11289  cvgratnnlemsumlt  11290  cvgratnnlemrate  11292  cvgratz  11294  mertenslemi1  11297  zdvdsdc  11503  dvdslelemd  11530  oexpneg  11563  ltoddhalfle  11579  divalglemnqt  11606  divalglemex  11608  divalglemeuneg  11609  flodddiv4t2lthalf  11623  zsupcl  11629  zssinfcl  11630  infssuzex  11631  dvdsbnd  11634  dvdslegcd  11642  gcd0id  11656  gcdneg  11659  bezoutlemsup  11686  dfgcd2  11691  nn0seqcvgd  11711  lcmgcdlem  11747  ncoprmgcdne1b  11759  nprm  11793  prmdvdsfz  11808  coprm  11811  prmexpb  11818  prmfac1  11819  znege1  11845  sqrt2irrap  11847  hashdvds  11886  hashgcdlem  11892  oddennn  11894  ennnfoneleminc  11913  supfz  13226  inffz  13227
  Copyright terms: Public domain W3C validator