Theorem eluzelre 12835

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

Step	Hyp	Ref	Expression
1		eluzelz 12834	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
2	1	zred 12668	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2106  ‘cfv 6543  ℝcr 11111  ℤ_≥cuz 12824

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-cnex 11168  ax-resscn 11169

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7414  df-neg 11449  df-z 12561  df-uz 12825

This theorem is referenced by:  eluzelcn  12836  eluzadd  12853  eluzsub  12854  uzm1  12862  uzsplit  13575  fzneuz  13584  fzouzsplit  13669  fzouzdisj  13670  fzoun  13671  eluzgtdifelfzo  13696  elfzonelfzo  13736  fldiv4lem1div2uz2  13803  mulp1mod1  13879  m1modge3gt1  13885  om2uzlt2i  13918  bernneq3  14196  hashfzp1  14393  seqcoll  14427  seqcoll2  14428  rexuzre  15301  rlimclim1  15491  climrlim2  15493  modm1div  16211  isprm5  16646  isprm7  16647  ncoprmlnprm  16666  dfphi2  16709  pclem  16773  pcmpt  16827  pockthg  16841  prmlem1  17043  prmlem2  17055  mtest  25923  logbleb  26295  logbgcd1irr  26306  isppw  26625  chtdif  26669  chtub  26722  fsumvma2  26724  chpval2  26728  bpos1lem  26792  bpos1  26793  gausslemma2dlem4  26879  chebbnd1lem1  26979  dchrisumlem2  27000  axlowdimlem16  28253  axlowdimlem17  28254  crctcshwlkn0lem5  29106  fzspl  32039  supfz  34767  nn0prpwlem  35293  rtprmirr  41319  rmspecsqrtnq  41726  rmspecnonsq  41727  rmspecfund  41729  rmspecpos  41737  rmxypos  41768  ltrmynn0  41769  ltrmxnn0  41770  jm2.24nn  41780  jm2.17a  41781  jm2.17b  41782  jm2.17c  41783  jm3.1lem1  41838  jm3.1lem2  41839  climsuselem1  44402  climsuse  44403  limsupequzlem  44517  limsupmnfuzlem  44521  ioodvbdlimc1lem2  44727  ioodvbdlimc2lem  44729  itgspltprt  44774  stoweidlem14  44809  wallispilem3  44862  stirlinglem11  44879  fourierdlem103  45004  fourierdlem104  45005  iccpartigtl  46170  fmtnoprmfac2lem1  46313  fmtno4prmfac  46319  lighneallem4a  46355  gboge9  46511  nnsum3primesle9  46541  bgoldbnnsum3prm  46551  bgoldbtbndlem3  46554  bgoldbtbndlem4  46555  bgoldbtbnd  46556  expnegico01  47277  fllog2  47332  dignn0ldlem  47366  dignnld  47367  digexp  47371  dignn0flhalf  47382