MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eluzelre Structured version   Unicode version

Theorem eluzelre 11055
Description: A member of an upper set of integers is a real. (Contributed by Mario Carneiro, 31-Aug-2013.)
Assertion
Ref Expression
eluzelre  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  RR )

Proof of Theorem eluzelre
StepHypRef Expression
1 eluzelz 11054 . 2  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ZZ )
21zred 10928 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842   ` cfv 5525   RRcr 9441   ZZ>=cuz 11045
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-cnex 9498  ax-resscn 9499
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-xp 4948  df-rel 4949  df-cnv 4950  df-co 4951  df-dm 4952  df-rn 4953  df-res 4954  df-ima 4955  df-iota 5489  df-fun 5527  df-fn 5528  df-f 5529  df-fv 5533  df-ov 6237  df-neg 9764  df-z 10826  df-uz 11046
This theorem is referenced by:  eluzelcn  11056  uzm1  11075  uzsplit  11722  fzneuz  11731  fzouzsplit  11805  fzouzdisj  11806  eluzgtdifelfzo  11827  elfzonelfzo  11862  om2uzlt2i  12016  bernneq3  12248  seqcoll  12468  seqcoll2  12469  rexuzre  13241  rlimclim1  13424  climrlim2  13426  isprm5  14354  phibndlem  14401  dfphi2  14405  pclem  14463  pcmpt  14512  pockthg  14525  prmlem1  14694  prmlem2  14706  mtest  22983  logbleb  23342  isppw  23661  chtdif  23705  chtub  23760  fsumvma2  23762  chpval2  23766  bpos1lem  23830  bpos1  23831  bposlem6  23837  chebbnd1lem1  23927  dchrisumlem2  23948  axlowdimlem16  24558  axlowdimlem17  24559  extwwlkfablem2  25376  fzspl  27926  supfz  29816  nn0prpwlem  30538  rmspecsqrtnq  35184  rmspecnonsq  35185  rmspecfund  35187  rmspecpos  35194  rmxypos  35227  ltrmynn0  35228  ltrmxnn0  35229  jm2.24nn  35239  jm2.17a  35240  jm2.17b  35241  jm2.17c  35242  jm3.1lem1  35302  jm3.1lem2  35303  isprm7  36021  climsuselem1  36963  climsuse  36964  ioodvbdlimc1lem2  37079  ioodvbdlimc2lem  37081  itgspltprt  37128  stoweidlem14  37146  wallispilem3  37199  stirlinglem11  37216  fourierdlem103  37342  fourierdlem104  37343  iccpartigtl  37670  gboage9  37798  nnsum3primesle9  37822  bgoldbnnsum3prm  37832  bgoldbtbndlem3  37835  bgoldbtbndlem4  37836  bgoldbtbnd  37837  expnegico01  38614  fllog2  38679  dignn0ldlem  38713  dignnld  38714  digexp  38718  dignn0flhalf  38729
  Copyright terms: Public domain W3C validator