Theorem eluzelre 12782

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6499  ℝcr 11045  ℤ_≥cuz 12771

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-cnex 11102  ax-resscn 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507  df-ov 7372  df-neg 11386  df-z 12508  df-uz 12772

This theorem is referenced by:  eluzelcn  12783  eluzadd  12800  eluzsub  12801  uzm1  12809  ge2halflem1  13046  uzsplit  13535  fzneuz  13547  fzouzsplit  13633  fzouzdisj  13634  fzoun  13635  eluzgtdifelfzo  13666  elfzonelfzo  13708  fldiv4lem1div2uz2  13776  mulp1mod1  13854  m1modge3gt1  13861  om2uzlt2i  13894  bernneq3  14174  hashfzp1  14374  seqcoll  14407  seqcoll2  14408  rexuzre  15296  rlimclim1  15488  climrlim2  15490  modm1div  16211  isprm5  16654  isprm7  16655  ncoprmlnprm  16675  dfphi2  16721  pclem  16786  pcmpt  16840  pockthg  16854  prmlem1  17055  prmlem2  17067  mtest  26347  rtprmirr  26704  logbleb  26727  logbgcd1irr  26738  isppw  27058  chtdif  27102  chtub  27157  fsumvma2  27159  chpval2  27163  bpos1lem  27227  bpos1  27228  gausslemma2dlem4  27314  chebbnd1lem1  27414  dchrisumlem2  27435  axlowdimlem16  28938  axlowdimlem17  28939  crctcshwlkn0lem5  29795  fzspl  32763  supfz  35710  nn0prpwlem  36304  rmspecsqrtnq  42888  rmspecnonsq  42889  rmspecfund  42891  rmspecpos  42899  rmxypos  42930  ltrmynn0  42931  ltrmxnn0  42932  jm2.24nn  42942  jm2.17a  42943  jm2.17b  42944  jm2.17c  42945  jm3.1lem1  43000  jm3.1lem2  43001  climsuselem1  45599  climsuse  45600  limsupequzlem  45714  limsupmnfuzlem  45718  ioodvbdlimc1lem2  45924  ioodvbdlimc2lem  45926  itgspltprt  45971  stoweidlem14  46006  wallispilem3  46059  stirlinglem11  46076  fourierdlem103  46201  fourierdlem104  46202  2ltceilhalf  47323  ceilhalfgt1  47324  2tceilhalfelfzo1  47327  ceilhalfnn  47331  iccpartigtl  47418  fmtnoprmfac2lem1  47561  fmtno4prmfac  47567  lighneallem4a  47603  gboge9  47759  nnsum3primesle9  47789  bgoldbnnsum3prm  47799  bgoldbtbndlem3  47802  bgoldbtbndlem4  47803  bgoldbtbnd  47804  gpgusgralem  48041  gpgprismgrusgra  48043  gpg3nbgrvtx0ALT  48062  gpgprismgr4cycllem3  48081  expnegico01  48501  fllog2  48551  dignn0ldlem  48585  dignnld  48586  digexp  48590  dignn0flhalf  48601