Theorem eluzelre 12776

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6502  ℝcr 11039  ℤ_≥cuz 12765

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pr 5381  ax-cnex 11096  ax-resscn 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-fv 6510  df-ov 7373  df-neg 11381  df-z 12503  df-uz 12766

This theorem is referenced by:  eluzelcn  12777  eluzadd  12794  eluzsub  12795  uzm1  12799  ge2halflem1  13036  uzsplit  13526  fzneuz  13538  fzouzsplit  13624  fzouzdisj  13625  fzoun  13626  eluzgtdifelfzo  13657  elfzonelfzo  13699  fldiv4lem1div2uz2  13770  mulp1mod1  13848  m1modge3gt1  13855  om2uzlt2i  13888  bernneq3  14168  hashfzp1  14368  seqcoll  14401  seqcoll2  14402  rexuzre  15290  rlimclim1  15482  climrlim2  15484  modm1div  16205  isprm5  16648  isprm7  16649  ncoprmlnprm  16669  dfphi2  16715  pclem  16780  pcmpt  16834  pockthg  16848  prmlem1  17049  prmlem2  17061  mtest  26386  rtprmirr  26743  logbleb  26766  logbgcd1irr  26777  isppw  27097  chtdif  27141  chtub  27196  fsumvma2  27198  chpval2  27202  bpos1lem  27266  bpos1  27267  gausslemma2dlem4  27353  chebbnd1lem1  27453  dchrisumlem2  27474  axlowdimlem16  29048  axlowdimlem17  29049  crctcshwlkn0lem5  29905  fzspl  32886  supfz  35951  nn0prpwlem  36544  rmspecsqrtnq  43292  rmspecnonsq  43293  rmspecfund  43295  rmspecpos  43302  rmxypos  43333  ltrmynn0  43334  ltrmxnn0  43335  jm2.24nn  43345  jm2.17a  43346  jm2.17b  43347  jm2.17c  43348  jm3.1lem1  43403  jm3.1lem2  43404  climsuselem1  45996  climsuse  45997  limsupequzlem  46109  limsupmnfuzlem  46113  ioodvbdlimc1lem2  46319  ioodvbdlimc2lem  46321  itgspltprt  46366  stoweidlem14  46401  wallispilem3  46454  stirlinglem11  46471  fourierdlem103  46596  fourierdlem104  46597  2ltceilhalf  47717  ceilhalfgt1  47718  2tceilhalfelfzo1  47721  ceilhalfnn  47725  iccpartigtl  47812  fmtnoprmfac2lem1  47955  fmtno4prmfac  47961  lighneallem4a  47997  gboge9  48153  nnsum3primesle9  48183  bgoldbnnsum3prm  48193  bgoldbtbndlem3  48196  bgoldbtbndlem4  48197  bgoldbtbnd  48198  gpgusgralem  48445  gpgprismgrusgra  48447  gpg3nbgrvtx0ALT  48466  gpgprismgr4cycllem3  48486  expnegico01  48907  fllog2  48957  dignn0ldlem  48991  dignnld  48992  digexp  48996  dignn0flhalf  49007