Theorem eluzelre 12764

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6491  ℝcr 11027  ℤ_≥cuz 12753

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 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pr 5376  ax-cnex 11084  ax-resscn 11085

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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-fv 6499  df-ov 7361  df-neg 11369  df-z 12491  df-uz 12754

This theorem is referenced by:  eluzelcn  12765  eluzadd  12782  eluzsub  12783  uzm1  12787  ge2halflem1  13024  uzsplit  13514  fzneuz  13526  fzouzsplit  13612  fzouzdisj  13613  fzoun  13614  eluzgtdifelfzo  13645  elfzonelfzo  13687  fldiv4lem1div2uz2  13758  mulp1mod1  13836  m1modge3gt1  13843  om2uzlt2i  13876  bernneq3  14156  hashfzp1  14356  seqcoll  14389  seqcoll2  14390  rexuzre  15278  rlimclim1  15470  climrlim2  15472  modm1div  16193  isprm5  16636  isprm7  16637  ncoprmlnprm  16657  dfphi2  16703  pclem  16768  pcmpt  16822  pockthg  16836  prmlem1  17037  prmlem2  17049  mtest  26371  rtprmirr  26728  logbleb  26751  logbgcd1irr  26762  isppw  27082  chtdif  27126  chtub  27181  fsumvma2  27183  chpval2  27187  bpos1lem  27251  bpos1  27252  gausslemma2dlem4  27338  chebbnd1lem1  27438  dchrisumlem2  27459  axlowdimlem16  29011  axlowdimlem17  29012  crctcshwlkn0lem5  29868  fzspl  32848  supfz  35902  nn0prpwlem  36495  rmspecsqrtnq  43185  rmspecnonsq  43186  rmspecfund  43188  rmspecpos  43195  rmxypos  43226  ltrmynn0  43227  ltrmxnn0  43228  jm2.24nn  43238  jm2.17a  43239  jm2.17b  43240  jm2.17c  43241  jm3.1lem1  43296  jm3.1lem2  43297  climsuselem1  45890  climsuse  45891  limsupequzlem  46003  limsupmnfuzlem  46007  ioodvbdlimc1lem2  46213  ioodvbdlimc2lem  46215  itgspltprt  46260  stoweidlem14  46295  wallispilem3  46348  stirlinglem11  46365  fourierdlem103  46490  fourierdlem104  46491  2ltceilhalf  47611  ceilhalfgt1  47612  2tceilhalfelfzo1  47615  ceilhalfnn  47619  iccpartigtl  47706  fmtnoprmfac2lem1  47849  fmtno4prmfac  47855  lighneallem4a  47891  gboge9  48047  nnsum3primesle9  48077  bgoldbnnsum3prm  48087  bgoldbtbndlem3  48090  bgoldbtbndlem4  48091  bgoldbtbnd  48092  gpgusgralem  48339  gpgprismgrusgra  48341  gpg3nbgrvtx0ALT  48360  gpgprismgr4cycllem3  48380  expnegico01  48801  fllog2  48851  dignn0ldlem  48885  dignnld  48886  digexp  48890  dignn0flhalf  48901