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

Theorem zred 8801
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 8690 . 2 ℤ ⊆ ℝ
2 zred.1 . 2 (𝜑𝐴 ∈ ℤ)
31, 2sseldi 3012 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1436  cr 7293  cz 8683
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-3or 923  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rex 2361  df-rab 2364  df-v 2617  df-un 2992  df-in 2994  df-ss 3001  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3637  df-br 3821  df-iota 4946  df-fv 4989  df-ov 5616  df-neg 7600  df-z 8684
This theorem is referenced by:  zcnd  8802  eluzelre  8961  eluzadd  8979  eluzsub  8980  uzm1  8981  z2ge  9220  zltaddlt1le  9355  fztri3or  9385  fznlem  9387  fzdisj  9398  fzpreddisj  9415  fznatpl1  9420  uzdisj  9437  fzm1  9444  fz0fzdiffz0  9469  elfzmlbm  9470  elfzmlbp  9471  difelfznle  9474  nn0disj  9477  elfzolt3  9496  fzonel  9499  fzouzdisj  9519  fzonmapblen  9526  fzoaddel  9531  elfzonelfzo  9569  qtri3or  9582  exbtwnzlemstep  9587  exbtwnzlemex  9589  exbtwnz  9590  rebtwn2zlemstep  9592  rebtwn2z  9594  qbtwnrelemcalc  9595  qbtwnre  9596  apbtwnz  9609  qfraclt1  9615  qfracge0  9616  flqge  9617  flid  9619  flqltnz  9622  flqwordi  9623  flqaddz  9632  flqmulnn0  9634  btwnzge0  9635  2tnp1ge0ge0  9636  flhalf  9637  flltdivnn0lt  9639  fldiv4p1lem1div2  9640  ceiqge  9644  ceiqm1l  9646  ceiqle  9648  flqleceil  9652  flqeqceilz  9653  intfracq  9655  modqval  9659  modqge0  9667  modqlt  9668  modqmulnn  9677  mulp1mod1  9700  modaddmodup  9722  modaddmodlo  9723  modsumfzodifsn  9731  addmodlteq  9733  frec2uzlt2d  9739  frec2uzf1od  9741  iseqf1olemkle  9818  iseqf1olemqcl  9820  iseqf1olemnab  9822  iseqf1olemab  9823  iseqf1olemqk  9828  iseqf1olemqsumkj  9832  iseqf1olemqsumk  9833  iseqf1olemqsum  9834  expival  9856  expcanlem  10021  expcan  10022  facavg  10051  bcval4  10057  bcp1nk  10067  ibcval5  10068  zfz1isolemiso  10141  iseqcoll  10144  resqrexlemdecn  10341  fzomaxdiflem  10441  fisumcvg3  10676  zdvdsdc  10699  dvdslelemd  10726  oexpneg  10759  ltoddhalfle  10775  divalglemnqt  10802  divalglemex  10804  divalglemeuneg  10805  flodddiv4t2lthalf  10819  zsupcl  10825  zssinfcl  10826  infssuzex  10827  dvdsbnd  10830  dvdslegcd  10838  gcd0id  10852  gcdneg  10855  bezoutlemsup  10880  dfgcd2  10885  nn0seqcvgd  10905  lcmgcdlem  10941  ncoprmgcdne1b  10953  nprm  10987  prmdvdsfz  11002  coprm  11005  prmexpb  11012  prmfac1  11013  znege1  11038  sqrt2irrap  11040  hashdvds  11079  hashgcdlem  11085  oddennn  11087
  Copyright terms: Public domain W3C validator