Theorem eluzelre 12766

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6493  ℝcr 11029  ℤ_≥cuz 12755

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378  ax-cnex 11086  ax-resscn 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7363  df-neg 11371  df-z 12493  df-uz 12756

This theorem is referenced by:  eluzelcn  12767  eluzadd  12784  eluzsub  12785  uzm1  12789  ge2halflem1  13026  uzsplit  13516  fzneuz  13528  fzouzsplit  13614  fzouzdisj  13615  fzoun  13616  eluzgtdifelfzo  13647  elfzonelfzo  13689  fldiv4lem1div2uz2  13760  mulp1mod1  13838  m1modge3gt1  13845  om2uzlt2i  13878  bernneq3  14158  hashfzp1  14358  seqcoll  14391  seqcoll2  14392  rexuzre  15280  rlimclim1  15472  climrlim2  15474  modm1div  16195  isprm5  16638  isprm7  16639  ncoprmlnprm  16659  dfphi2  16705  pclem  16770  pcmpt  16824  pockthg  16838  prmlem1  17039  prmlem2  17051  mtest  26373  rtprmirr  26730  logbleb  26753  logbgcd1irr  26764  isppw  27084  chtdif  27128  chtub  27183  fsumvma2  27185  chpval2  27189  bpos1lem  27253  bpos1  27254  gausslemma2dlem4  27340  chebbnd1lem1  27440  dchrisumlem2  27461  axlowdimlem16  29034  axlowdimlem17  29035  crctcshwlkn0lem5  29891  fzspl  32871  supfz  35925  nn0prpwlem  36518  rmspecsqrtnq  43215  rmspecnonsq  43216  rmspecfund  43218  rmspecpos  43225  rmxypos  43256  ltrmynn0  43257  ltrmxnn0  43258  jm2.24nn  43268  jm2.17a  43269  jm2.17b  43270  jm2.17c  43271  jm3.1lem1  43326  jm3.1lem2  43327  climsuselem1  45920  climsuse  45921  limsupequzlem  46033  limsupmnfuzlem  46037  ioodvbdlimc1lem2  46243  ioodvbdlimc2lem  46245  itgspltprt  46290  stoweidlem14  46325  wallispilem3  46378  stirlinglem11  46395  fourierdlem103  46520  fourierdlem104  46521  2ltceilhalf  47641  ceilhalfgt1  47642  2tceilhalfelfzo1  47645  ceilhalfnn  47649  iccpartigtl  47736  fmtnoprmfac2lem1  47879  fmtno4prmfac  47885  lighneallem4a  47921  gboge9  48077  nnsum3primesle9  48107  bgoldbnnsum3prm  48117  bgoldbtbndlem3  48120  bgoldbtbndlem4  48121  bgoldbtbnd  48122  gpgusgralem  48369  gpgprismgrusgra  48371  gpg3nbgrvtx0ALT  48390  gpgprismgr4cycllem3  48410  expnegico01  48831  fllog2  48881  dignn0ldlem  48915  dignnld  48916  digexp  48920  dignn0flhalf  48931