Theorem eluzelre 12783

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

Syntax hints:   → wi 4   ∈ wcel 2106  ‘cfv 6501  ℝcr 11059  ℤ_≥cuz 12772

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-cnex 11116  ax-resscn 11117

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-fv 6509  df-ov 7365  df-neg 11397  df-z 12509  df-uz 12773

This theorem is referenced by:  eluzelcn  12784  eluzadd  12801  eluzsub  12802  uzm1  12810  uzsplit  13523  fzneuz  13532  fzouzsplit  13617  fzouzdisj  13618  fzoun  13619  eluzgtdifelfzo  13644  elfzonelfzo  13684  fldiv4lem1div2uz2  13751  mulp1mod1  13827  m1modge3gt1  13833  om2uzlt2i  13866  bernneq3  14144  hashfzp1  14341  seqcoll  14375  seqcoll2  14376  rexuzre  15249  rlimclim1  15439  climrlim2  15441  modm1div  16159  isprm5  16594  isprm7  16595  ncoprmlnprm  16614  dfphi2  16657  pclem  16721  pcmpt  16775  pockthg  16789  prmlem1  16991  prmlem2  17003  mtest  25800  logbleb  26170  logbgcd1irr  26181  isppw  26500  chtdif  26544  chtub  26597  fsumvma2  26599  chpval2  26603  bpos1lem  26667  bpos1  26668  gausslemma2dlem4  26754  chebbnd1lem1  26854  dchrisumlem2  26875  axlowdimlem16  27969  axlowdimlem17  27970  crctcshwlkn0lem5  28822  fzspl  31761  supfz  34387  nn0prpwlem  34870  rtprmirr  40891  rmspecsqrtnq  41287  rmspecnonsq  41288  rmspecfund  41290  rmspecpos  41298  rmxypos  41329  ltrmynn0  41330  ltrmxnn0  41331  jm2.24nn  41341  jm2.17a  41342  jm2.17b  41343  jm2.17c  41344  jm3.1lem1  41399  jm3.1lem2  41400  climsuselem1  43968  climsuse  43969  limsupequzlem  44083  limsupmnfuzlem  44087  ioodvbdlimc1lem2  44293  ioodvbdlimc2lem  44295  itgspltprt  44340  stoweidlem14  44375  wallispilem3  44428  stirlinglem11  44445  fourierdlem103  44570  fourierdlem104  44571  iccpartigtl  45735  fmtnoprmfac2lem1  45878  fmtno4prmfac  45884  lighneallem4a  45920  gboge9  46076  nnsum3primesle9  46106  bgoldbnnsum3prm  46116  bgoldbtbndlem3  46119  bgoldbtbndlem4  46120  bgoldbtbnd  46121  expnegico01  46719  fllog2  46774  dignn0ldlem  46808  dignnld  46809  digexp  46813  dignn0flhalf  46824