Theorem eluzelre 12522

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6418  ℝcr 10801  ℤ_≥cuz 12511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-cnex 10858  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-ov 7258  df-neg 11138  df-z 12250  df-uz 12512

This theorem is referenced by:  eluzelcn  12523  uzm1  12545  uzsplit  13257  fzneuz  13266  fzouzsplit  13350  fzouzdisj  13351  fzoun  13352  eluzgtdifelfzo  13377  elfzonelfzo  13417  fldiv4lem1div2uz2  13484  mulp1mod1  13560  m1modge3gt1  13566  om2uzlt2i  13599  bernneq3  13874  hashfzp1  14074  seqcoll  14106  seqcoll2  14107  rexuzre  14992  rlimclim1  15182  climrlim2  15184  modm1div  15903  isprm5  16340  isprm7  16341  ncoprmlnprm  16360  dfphi2  16403  pclem  16467  pcmpt  16521  pockthg  16535  prmlem1  16737  prmlem2  16749  mtest  25468  logbleb  25838  logbgcd1irr  25849  isppw  26168  chtdif  26212  chtub  26265  fsumvma2  26267  chpval2  26271  bpos1lem  26335  bpos1  26336  gausslemma2dlem4  26422  chebbnd1lem1  26522  dchrisumlem2  26543  axlowdimlem16  27228  axlowdimlem17  27229  crctcshwlkn0lem5  28080  fzspl  31013  supfz  33600  nn0prpwlem  34438  rtprmirr  40268  rmspecsqrtnq  40644  rmspecnonsq  40645  rmspecfund  40647  rmspecpos  40654  rmxypos  40685  ltrmynn0  40686  ltrmxnn0  40687  jm2.24nn  40697  jm2.17a  40698  jm2.17b  40699  jm2.17c  40700  jm3.1lem1  40755  jm3.1lem2  40756  climsuselem1  43038  climsuse  43039  limsupequzlem  43153  limsupmnfuzlem  43157  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  itgspltprt  43410  stoweidlem14  43445  wallispilem3  43498  stirlinglem11  43515  fourierdlem103  43640  fourierdlem104  43641  iccpartigtl  44763  fmtnoprmfac2lem1  44906  fmtno4prmfac  44912  lighneallem4a  44948  gboge9  45104  nnsum3primesle9  45134  bgoldbnnsum3prm  45144  bgoldbtbndlem3  45147  bgoldbtbndlem4  45148  bgoldbtbnd  45149  expnegico01  45747  fllog2  45802  dignn0ldlem  45836  dignnld  45837  digexp  45841  dignn0flhalf  45852