Theorem eluzelre 12901

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6537  ℝcr 11126  ℤ_≥cuz 12890

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-cnex 11183  ax-resscn 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7419  df-neg 11471  df-z 12619  df-uz 12891

This theorem is used by:  eluzelcn  12902  eluzadd  12919  eluzsub  12920  uzm1  12924  ge2halflem1  13161  nnge2recico01  13562  uzsplit  13653  fzneuz  13665  fzouzsplit  13752  fzouzdisj  13753  fzoun  13754  eluzgtdifelfzo  13785  elfzonelfzo  13827  fldiv4lem1div2uz2  13899  mulp1mod1  13977  m1modge3gt1  13984  om2uzlt2i  14017  bernneq3  14297  hashfzp1  14498  seqcoll  14531  seqcoll2  14532  rexuzre  15442  rlimclim1  15634  climrlim2  15636  modm1div  16358  isprm5  16802  isprm7  16803  ncoprmlnprm  16823  dfphi2  16869  pclem  16934  pcmpt  16988  pockthg  17002  prmlem1  17203  prmlem2  17216  mtest  26637  rtprmirr  26995  logbleb  27018  logbgcd1irr  27029  isppw  27348  chtdif  27392  chtub  27446  fsumvma2  27448  chpval2  27452  bpos1lem  27516  bpos1  27517  gausslemma2dlem4  27603  chebbnd1lem1  27703  dchrisumlem2  27724  axlowdimlem16  29400  axlowdimlem17  29401  crctcshwlkn0lem5  30268  fzspl  33247  supfz  36295  nn0prpwlem  36928  rmspecsqrtnq  43734  rmspecnonsq  43735  rmspecfund  43737  rmspecpos  43744  rmxypos  43775  ltrmynn0  43776  ltrmxnn0  43777  jm2.24nn  43787  jm2.17a  43788  jm2.17b  43789  jm2.17c  43790  jm3.1lem1  43845  jm3.1lem2  43846  climsuselem1  46424  climsuse  46425  limsupequzlem  46537  limsupmnfuzlem  46541  ioodvbdlimc1lem2  46747  ioodvbdlimc2lem  46749  itgspltprt  46794  stoweidlem14  46829  wallispilem3  46882  stirlinglem11  46899  fourierdlem103  47024  fourierdlem104  47025  nnmul2  48205  2ltceilhalf  48207  ceilhalfgt1  48208  2tceilhalfelfzo1  48211  ceilhalfnn  48215  2timesltsqm1  48254  iccpartigtl  48310  fmtnoprmfac2lem1  48456  fmtno4prmfac  48462  lighneallem4a  48498  gboge9  48667  nnsum3primesle9  48697  bgoldbnnsum3prm  48707  bgoldbtbndlem3  48710  bgoldbtbndlem4  48711  bgoldbtbnd  48712  gpgusgralem  48959  gpgprismgrusgra  48961  gpg3nbgrvtx0ALT  48980  gpgprismgr4cycllem3  49000  expnegico01  49435  fllog2  49485  dignn0ldlem  49519  dignnld  49520  digexp  49524  dignn0flhalf  49535