Theorem eluzelre 12886

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

Syntax hints:   → wi 4   ∈ wcel 2105  ‘cfv 6562  ℝcr 11151  ℤ_≥cuz 12875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-cnex 11208  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433  df-neg 11492  df-z 12611  df-uz 12876

This theorem is referenced by:  eluzelcn  12887  eluzadd  12904  eluzsub  12905  uzm1  12913  ge2halflem1  13147  uzsplit  13632  fzneuz  13644  fzouzsplit  13730  fzouzdisj  13731  fzoun  13732  eluzgtdifelfzo  13762  elfzonelfzo  13804  fldiv4lem1div2uz2  13872  mulp1mod1  13948  m1modge3gt1  13955  om2uzlt2i  13988  bernneq3  14266  hashfzp1  14466  seqcoll  14499  seqcoll2  14500  rexuzre  15387  rlimclim1  15577  climrlim2  15579  modm1div  16298  isprm5  16740  isprm7  16741  ncoprmlnprm  16761  dfphi2  16807  pclem  16871  pcmpt  16925  pockthg  16939  prmlem1  17141  prmlem2  17153  mtest  26461  rtprmirr  26817  logbleb  26840  logbgcd1irr  26851  isppw  27171  chtdif  27215  chtub  27270  fsumvma2  27272  chpval2  27276  bpos1lem  27340  bpos1  27341  gausslemma2dlem4  27427  chebbnd1lem1  27527  dchrisumlem2  27548  axlowdimlem16  28986  axlowdimlem17  28987  crctcshwlkn0lem5  29843  fzspl  32797  supfz  35708  nn0prpwlem  36304  rmspecsqrtnq  42893  rmspecnonsq  42894  rmspecfund  42896  rmspecpos  42904  rmxypos  42935  ltrmynn0  42936  ltrmxnn0  42937  jm2.24nn  42947  jm2.17a  42948  jm2.17b  42949  jm2.17c  42950  jm3.1lem1  43005  jm3.1lem2  43006  climsuselem1  45562  climsuse  45563  limsupequzlem  45677  limsupmnfuzlem  45681  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  itgspltprt  45934  stoweidlem14  45969  wallispilem3  46022  stirlinglem11  46039  fourierdlem103  46164  fourierdlem104  46165  iccpartigtl  47347  fmtnoprmfac2lem1  47490  fmtno4prmfac  47496  lighneallem4a  47532  gboge9  47688  nnsum3primesle9  47718  bgoldbnnsum3prm  47728  bgoldbtbndlem3  47731  bgoldbtbndlem4  47732  bgoldbtbnd  47733  gpgusgralem  47945  2ltceilhalf  47949  2tceilhalfelfzo1  47952  gpg3nbgrvtx0ALT  47967  expnegico01  48363  fllog2  48417  dignn0ldlem  48451  dignnld  48452  digexp  48456  dignn0flhalf  48467