Theorem eluzelre 12838

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 12837	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
2	1	zred 12671	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2105  ‘cfv 6543  ℝcr 11113  ℤ_≥cuz 12827

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-cnex 11170  ax-resscn 11171

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  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 7415  df-neg 11452  df-z 12564  df-uz 12828

This theorem is referenced by:  eluzelcn  12839  eluzadd  12856  eluzsub  12857  uzm1  12865  uzsplit  13578  fzneuz  13587  fzouzsplit  13672  fzouzdisj  13673  fzoun  13674  eluzgtdifelfzo  13699  elfzonelfzo  13739  fldiv4lem1div2uz2  13806  mulp1mod1  13882  m1modge3gt1  13888  om2uzlt2i  13921  bernneq3  14199  hashfzp1  14396  seqcoll  14430  seqcoll2  14431  rexuzre  15304  rlimclim1  15494  climrlim2  15496  modm1div  16214  isprm5  16649  isprm7  16650  ncoprmlnprm  16669  dfphi2  16712  pclem  16776  pcmpt  16830  pockthg  16844  prmlem1  17046  prmlem2  17058  mtest  26153  logbleb  26525  logbgcd1irr  26536  isppw  26855  chtdif  26899  chtub  26952  fsumvma2  26954  chpval2  26958  bpos1lem  27022  bpos1  27023  gausslemma2dlem4  27109  chebbnd1lem1  27209  dchrisumlem2  27230  axlowdimlem16  28483  axlowdimlem17  28484  crctcshwlkn0lem5  29336  fzspl  32269  supfz  35003  nn0prpwlem  35511  rtprmirr  41540  rmspecsqrtnq  41947  rmspecnonsq  41948  rmspecfund  41950  rmspecpos  41958  rmxypos  41989  ltrmynn0  41990  ltrmxnn0  41991  jm2.24nn  42001  jm2.17a  42002  jm2.17b  42003  jm2.17c  42004  jm3.1lem1  42059  jm3.1lem2  42060  climsuselem1  44622  climsuse  44623  limsupequzlem  44737  limsupmnfuzlem  44741  ioodvbdlimc1lem2  44947  ioodvbdlimc2lem  44949  itgspltprt  44994  stoweidlem14  45029  wallispilem3  45082  stirlinglem11  45099  fourierdlem103  45224  fourierdlem104  45225  iccpartigtl  46390  fmtnoprmfac2lem1  46533  fmtno4prmfac  46539  lighneallem4a  46575  gboge9  46731  nnsum3primesle9  46761  bgoldbnnsum3prm  46771  bgoldbtbndlem3  46774  bgoldbtbndlem4  46775  bgoldbtbnd  46776  expnegico01  47287  fllog2  47342  dignn0ldlem  47376  dignnld  47377  digexp  47381  dignn0flhalf  47392