Theorem eluzelre 12852

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

Syntax hints:   → wi 4   ∈ wcel 2144  ‘cfv 6523  ℝcr 11074  ℤ_≥cuz 12841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pr 5392  ax-cnex 11131  ax-resscn 11132

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-fv 6531  df-ov 7401  df-neg 11419  df-z 12571  df-uz 12842

This theorem is referenced by:  eluzelcn  12853  eluzadd  12870  eluzsub  12871  uzm1  12875  ge2halflem1  13112  nnge2recico01  13513  uzsplit  13603  fzneuz  13615  fzouzsplit  13702  fzouzdisj  13703  fzoun  13704  eluzgtdifelfzo  13735  elfzonelfzo  13777  fldiv4lem1div2uz2  13848  mulp1mod1  13926  m1modge3gt1  13933  om2uzlt2i  13966  bernneq3  14246  hashfzp1  14446  seqcoll  14479  seqcoll2  14480  rexuzre  15382  rlimclim1  15574  climrlim2  15576  modm1div  16300  isprm5  16744  isprm7  16745  ncoprmlnprm  16765  dfphi2  16811  pclem  16876  pcmpt  16930  pockthg  16944  prmlem1  17145  prmlem2  17158  mtest  26469  rtprmirr  26827  logbleb  26850  logbgcd1irr  26861  isppw  27180  chtdif  27224  chtub  27278  fsumvma2  27280  chpval2  27284  bpos1lem  27348  bpos1  27349  gausslemma2dlem4  27435  chebbnd1lem1  27535  dchrisumlem2  27556  axlowdimlem16  29160  axlowdimlem17  29161  crctcshwlkn0lem5  30016  fzspl  32993  supfz  36084  nn0prpwlem  36687  rmspecsqrtnq  43488  rmspecnonsq  43489  rmspecfund  43491  rmspecpos  43498  rmxypos  43529  ltrmynn0  43530  ltrmxnn0  43531  jm2.24nn  43541  jm2.17a  43542  jm2.17b  43543  jm2.17c  43544  jm3.1lem1  43599  jm3.1lem2  43600  climsuselem1  46188  climsuse  46189  limsupequzlem  46301  limsupmnfuzlem  46305  ioodvbdlimc1lem2  46511  ioodvbdlimc2lem  46513  itgspltprt  46558  stoweidlem14  46593  wallispilem3  46646  stirlinglem11  46663  fourierdlem103  46788  fourierdlem104  46789  nnmul2  47929  2ltceilhalf  47931  ceilhalfgt1  47932  2tceilhalfelfzo1  47935  ceilhalfnn  47939  2timesltsqm1  47978  iccpartigtl  48034  fmtnoprmfac2lem1  48180  fmtno4prmfac  48186  lighneallem4a  48222  gboge9  48391  nnsum3primesle9  48421  bgoldbnnsum3prm  48431  bgoldbtbndlem3  48434  bgoldbtbndlem4  48435  bgoldbtbnd  48436  gpgusgralem  48683  gpgprismgrusgra  48685  gpg3nbgrvtx0ALT  48704  gpgprismgr4cycllem3  48724  expnegico01  49145  fllog2  49195  dignn0ldlem  49229  dignnld  49230  digexp  49234  dignn0flhalf  49245