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

Theorem eluzelre 11533
Description: A member of an upper set of integers is a real. (Contributed by Mario Carneiro, 31-Aug-2013.)
Assertion
Ref Expression
eluzelre (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℝ)

Proof of Theorem eluzelre
StepHypRef Expression
1 eluzelz 11532 . 2 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
21zred 11317 1 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  cfv 5790  cr 9792  cuz 11522
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-cnex 9849  ax-resscn 9850
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-br 4579  df-opab 4639  df-mpt 4640  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-fv 5798  df-ov 6530  df-neg 10121  df-z 11214  df-uz 11523
This theorem is referenced by:  eluzelcn  11534  uzm1  11553  ssfzunsn  12215  uzsplit  12239  fzneuz  12248  fzouzsplit  12330  fzouzdisj  12331  eluzgtdifelfzo  12355  elfzonelfzo  12394  fldiv4lem1div2uz2  12457  mulp1mod1  12531  m1modge3gt1  12537  om2uzlt2i  12570  bernneq3  12812  hashfzp1  13033  seqcoll  13060  seqcoll2  13061  rexuzre  13889  rlimclim1  14073  climrlim2  14075  isprm5  15206  isprm7  15207  ncoprmlnprm  15223  dfphi2  15266  pclem  15330  pcmpt  15383  pockthg  15397  prmlem1  15601  prmlem2  15614  setsstruct  15676  mtest  23907  logbleb  24266  isppw  24585  chtdif  24629  chtub  24682  fsumvma2  24684  chpval2  24688  bpos1lem  24752  bpos1  24753  gausslemma2dlem4  24839  chebbnd1lem1  24903  dchrisumlem2  24924  axlowdimlem16  25583  axlowdimlem17  25584  extwwlkfablem2  26399  fzspl  28732  supfz  30660  nn0prpwlem  31281  rmspecsqrtnq  36282  rmspecsqrtnqOLD  36283  rmspecnonsq  36284  rmspecfund  36286  rmspecpos  36293  rmxypos  36326  ltrmynn0  36327  ltrmxnn0  36328  jm2.24nn  36338  jm2.17a  36339  jm2.17b  36340  jm2.17c  36341  jm3.1lem1  36396  jm3.1lem2  36397  climsuselem1  38468  climsuse  38469  ioodvbdlimc1lem2  38616  ioodvbdlimc2lem  38618  itgspltprt  38665  stoweidlem14  38701  wallispilem3  38754  stirlinglem11  38771  fourierdlem103  38896  fourierdlem104  38897  iccpartigtl  39756  fmtnoprmfac2lem1  39811  fmtno4prmfac  39817  lighneallem4a  39858  gboage9  39981  nnsum3primesle9  40005  bgoldbnnsum3prm  40015  bgoldbtbndlem3  40018  bgoldbtbndlem4  40019  bgoldbtbnd  40020  crctcsh1wlkn0lem5  41009  av-extwwlkfablem2  41502  expnegico01  42094  fllog2  42152  dignn0ldlem  42186  dignnld  42187  digexp  42191  dignn0flhalf  42202
  Copyright terms: Public domain W3C validator