Theorem eluzelre 12593

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

Syntax hints:   → wi 4   ∈ wcel 2106  ‘cfv 6433  ℝcr 10870  ℤ_≥cuz 12582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-cnex 10927  ax-resscn 10928

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-fv 6441  df-ov 7278  df-neg 11208  df-z 12320  df-uz 12583

This theorem is referenced by:  eluzelcn  12594  uzm1  12616  uzsplit  13328  fzneuz  13337  fzouzsplit  13422  fzouzdisj  13423  fzoun  13424  eluzgtdifelfzo  13449  elfzonelfzo  13489  fldiv4lem1div2uz2  13556  mulp1mod1  13632  m1modge3gt1  13638  om2uzlt2i  13671  bernneq3  13946  hashfzp1  14146  seqcoll  14178  seqcoll2  14179  rexuzre  15064  rlimclim1  15254  climrlim2  15256  modm1div  15975  isprm5  16412  isprm7  16413  ncoprmlnprm  16432  dfphi2  16475  pclem  16539  pcmpt  16593  pockthg  16607  prmlem1  16809  prmlem2  16821  mtest  25563  logbleb  25933  logbgcd1irr  25944  isppw  26263  chtdif  26307  chtub  26360  fsumvma2  26362  chpval2  26366  bpos1lem  26430  bpos1  26431  gausslemma2dlem4  26517  chebbnd1lem1  26617  dchrisumlem2  26638  axlowdimlem16  27325  axlowdimlem17  27326  crctcshwlkn0lem5  28179  fzspl  31111  supfz  33694  nn0prpwlem  34511  rtprmirr  40347  rmspecsqrtnq  40728  rmspecnonsq  40729  rmspecfund  40731  rmspecpos  40738  rmxypos  40769  ltrmynn0  40770  ltrmxnn0  40771  jm2.24nn  40781  jm2.17a  40782  jm2.17b  40783  jm2.17c  40784  jm3.1lem1  40839  jm3.1lem2  40840  climsuselem1  43148  climsuse  43149  limsupequzlem  43263  limsupmnfuzlem  43267  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  itgspltprt  43520  stoweidlem14  43555  wallispilem3  43608  stirlinglem11  43625  fourierdlem103  43750  fourierdlem104  43751  iccpartigtl  44875  fmtnoprmfac2lem1  45018  fmtno4prmfac  45024  lighneallem4a  45060  gboge9  45216  nnsum3primesle9  45246  bgoldbnnsum3prm  45256  bgoldbtbndlem3  45259  bgoldbtbndlem4  45260  bgoldbtbnd  45261  expnegico01  45859  fllog2  45914  dignn0ldlem  45948  dignnld  45949  digexp  45953  dignn0flhalf  45964