Theorem eluzelre 12794

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

Syntax hints:   → wi 4   ∈ wcel 2121  ‘cfv 6489  ℝcr 11032  ℤ_≥cuz 12783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pr 5365  ax-cnex 11089  ax-resscn 11090

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-fv 6497  df-ov 7363  df-neg 11375  df-z 12520  df-uz 12784

This theorem is referenced by:  eluzelcn  12795  eluzadd  12812  eluzsub  12813  uzm1  12817  ge2halflem1  13054  nnge2recico01  13455  uzsplit  13545  fzneuz  13557  fzouzsplit  13644  fzouzdisj  13645  fzoun  13646  eluzgtdifelfzo  13677  elfzonelfzo  13719  fldiv4lem1div2uz2  13790  mulp1mod1  13868  m1modge3gt1  13875  om2uzlt2i  13908  bernneq3  14188  hashfzp1  14388  seqcoll  14421  seqcoll2  14422  rexuzre  15310  rlimclim1  15502  climrlim2  15504  modm1div  16228  isprm5  16672  isprm7  16673  ncoprmlnprm  16693  dfphi2  16739  pclem  16804  pcmpt  16858  pockthg  16872  prmlem1  17073  prmlem2  17085  mtest  26391  rtprmirr  26746  logbleb  26769  logbgcd1irr  26780  isppw  27099  chtdif  27143  chtub  27197  fsumvma2  27199  chpval2  27203  bpos1lem  27267  bpos1  27268  gausslemma2dlem4  27354  chebbnd1lem1  27454  dchrisumlem2  27475  axlowdimlem16  29048  axlowdimlem17  29049  crctcshwlkn0lem5  29904  fzspl  32885  supfz  35972  nn0prpwlem  36565  rmspecsqrtnq  43366  rmspecnonsq  43367  rmspecfund  43369  rmspecpos  43376  rmxypos  43407  ltrmynn0  43408  ltrmxnn0  43409  jm2.24nn  43419  jm2.17a  43420  jm2.17b  43421  jm2.17c  43422  jm3.1lem1  43477  jm3.1lem2  43478  climsuselem1  46066  climsuse  46067  limsupequzlem  46179  limsupmnfuzlem  46183  ioodvbdlimc1lem2  46389  ioodvbdlimc2lem  46391  itgspltprt  46436  stoweidlem14  46471  wallispilem3  46524  stirlinglem11  46541  fourierdlem103  46666  fourierdlem104  46667  nnmul2  47807  2ltceilhalf  47809  ceilhalfgt1  47810  2tceilhalfelfzo1  47813  ceilhalfnn  47817  2timesltsqm1  47856  iccpartigtl  47912  fmtnoprmfac2lem1  48058  fmtno4prmfac  48064  lighneallem4a  48100  gboge9  48269  nnsum3primesle9  48299  bgoldbnnsum3prm  48309  bgoldbtbndlem3  48312  bgoldbtbndlem4  48313  bgoldbtbnd  48314  gpgusgralem  48561  gpgprismgrusgra  48563  gpg3nbgrvtx0ALT  48582  gpgprismgr4cycllem3  48602  expnegico01  49023  fllog2  49073  dignn0ldlem  49107  dignnld  49108  digexp  49112  dignn0flhalf  49123