Theorem eluzelre 12746

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6482  ℝcr 11008  ℤ_≥cuz 12735

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 5235  ax-nul 5245  ax-pr 5371  ax-cnex 11065  ax-resscn 11066

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-fv 6490  df-ov 7352  df-neg 11350  df-z 12472  df-uz 12736

This theorem is referenced by:  eluzelcn  12747  eluzadd  12764  eluzsub  12765  uzm1  12773  ge2halflem1  13010  uzsplit  13499  fzneuz  13511  fzouzsplit  13597  fzouzdisj  13598  fzoun  13599  eluzgtdifelfzo  13630  elfzonelfzo  13672  fldiv4lem1div2uz2  13740  mulp1mod1  13818  m1modge3gt1  13825  om2uzlt2i  13858  bernneq3  14138  hashfzp1  14338  seqcoll  14371  seqcoll2  14372  rexuzre  15260  rlimclim1  15452  climrlim2  15454  modm1div  16175  isprm5  16618  isprm7  16619  ncoprmlnprm  16639  dfphi2  16685  pclem  16750  pcmpt  16804  pockthg  16818  prmlem1  17019  prmlem2  17031  mtest  26311  rtprmirr  26668  logbleb  26691  logbgcd1irr  26702  isppw  27022  chtdif  27066  chtub  27121  fsumvma2  27123  chpval2  27127  bpos1lem  27191  bpos1  27192  gausslemma2dlem4  27278  chebbnd1lem1  27378  dchrisumlem2  27399  axlowdimlem16  28906  axlowdimlem17  28907  crctcshwlkn0lem5  29763  fzspl  32741  supfz  35722  nn0prpwlem  36316  rmspecsqrtnq  42899  rmspecnonsq  42900  rmspecfund  42902  rmspecpos  42909  rmxypos  42940  ltrmynn0  42941  ltrmxnn0  42942  jm2.24nn  42952  jm2.17a  42953  jm2.17b  42954  jm2.17c  42955  jm3.1lem1  43010  jm3.1lem2  43011  climsuselem1  45608  climsuse  45609  limsupequzlem  45723  limsupmnfuzlem  45727  ioodvbdlimc1lem2  45933  ioodvbdlimc2lem  45935  itgspltprt  45980  stoweidlem14  46015  wallispilem3  46068  stirlinglem11  46085  fourierdlem103  46210  fourierdlem104  46211  2ltceilhalf  47332  ceilhalfgt1  47333  2tceilhalfelfzo1  47336  ceilhalfnn  47340  iccpartigtl  47427  fmtnoprmfac2lem1  47570  fmtno4prmfac  47576  lighneallem4a  47612  gboge9  47768  nnsum3primesle9  47798  bgoldbnnsum3prm  47808  bgoldbtbndlem3  47811  bgoldbtbndlem4  47812  bgoldbtbnd  47813  gpgusgralem  48060  gpgprismgrusgra  48062  gpg3nbgrvtx0ALT  48081  gpgprismgr4cycllem3  48101  expnegico01  48523  fllog2  48573  dignn0ldlem  48607  dignnld  48608  digexp  48612  dignn0flhalf  48623