Theorem eluzelre 12298

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

Syntax hints:   → wi 4   ∈ wcel 2111  ‘cfv 6339  ℝcr 10579  ℤ_≥cuz 12287

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pr 5301  ax-cnex 10636  ax-resscn 10637

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5036  df-opab 5098  df-mpt 5116  df-id 5433  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-fv 6347  df-ov 7158  df-neg 10916  df-z 12026  df-uz 12288

This theorem is referenced by:  eluzelcn  12299  uzm1  12321  uzsplit  13033  fzneuz  13042  fzouzsplit  13126  fzouzdisj  13127  fzoun  13128  eluzgtdifelfzo  13153  elfzonelfzo  13193  fldiv4lem1div2uz2  13260  mulp1mod1  13334  m1modge3gt1  13340  om2uzlt2i  13373  bernneq3  13647  hashfzp1  13847  seqcoll  13879  seqcoll2  13880  rexuzre  14765  rlimclim1  14955  climrlim2  14957  modm1div  15672  isprm5  16108  isprm7  16109  ncoprmlnprm  16128  dfphi2  16171  pclem  16235  pcmpt  16288  pockthg  16302  prmlem1  16504  prmlem2  16516  mtest  25103  logbleb  25473  logbgcd1irr  25484  isppw  25803  chtdif  25847  chtub  25900  fsumvma2  25902  chpval2  25906  bpos1lem  25970  bpos1  25971  gausslemma2dlem4  26057  chebbnd1lem1  26157  dchrisumlem2  26178  axlowdimlem16  26855  axlowdimlem17  26856  crctcshwlkn0lem5  27704  fzspl  30639  supfz  33213  nn0prpwlem  34086  rtprmirr  39872  rmspecsqrtnq  40248  rmspecnonsq  40249  rmspecfund  40251  rmspecpos  40258  rmxypos  40289  ltrmynn0  40290  ltrmxnn0  40291  jm2.24nn  40301  jm2.17a  40302  jm2.17b  40303  jm2.17c  40304  jm3.1lem1  40359  jm3.1lem2  40360  climsuselem1  42643  climsuse  42644  limsupequzlem  42758  limsupmnfuzlem  42762  ioodvbdlimc1lem2  42968  ioodvbdlimc2lem  42970  itgspltprt  43015  stoweidlem14  43050  wallispilem3  43103  stirlinglem11  43120  fourierdlem103  43245  fourierdlem104  43246  iccpartigtl  44336  fmtnoprmfac2lem1  44479  fmtno4prmfac  44485  lighneallem4a  44521  gboge9  44677  nnsum3primesle9  44707  bgoldbnnsum3prm  44717  bgoldbtbndlem3  44720  bgoldbtbndlem4  44721  bgoldbtbnd  44722  expnegico01  45320  fllog2  45375  dignn0ldlem  45409  dignnld  45410  digexp  45414  dignn0flhalf  45425