Theorem eluzelre 12811

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6514  ℝcr 11074  ℤ_≥cuz 12800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-cnex 11131  ax-resscn 11132

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522  df-ov 7393  df-neg 11415  df-z 12537  df-uz 12801

This theorem is referenced by:  eluzelcn  12812  eluzadd  12829  eluzsub  12830  uzm1  12838  ge2halflem1  13075  uzsplit  13564  fzneuz  13576  fzouzsplit  13662  fzouzdisj  13663  fzoun  13664  eluzgtdifelfzo  13695  elfzonelfzo  13737  fldiv4lem1div2uz2  13805  mulp1mod1  13883  m1modge3gt1  13890  om2uzlt2i  13923  bernneq3  14203  hashfzp1  14403  seqcoll  14436  seqcoll2  14437  rexuzre  15326  rlimclim1  15518  climrlim2  15520  modm1div  16241  isprm5  16684  isprm7  16685  ncoprmlnprm  16705  dfphi2  16751  pclem  16816  pcmpt  16870  pockthg  16884  prmlem1  17085  prmlem2  17097  mtest  26320  rtprmirr  26677  logbleb  26700  logbgcd1irr  26711  isppw  27031  chtdif  27075  chtub  27130  fsumvma2  27132  chpval2  27136  bpos1lem  27200  bpos1  27201  gausslemma2dlem4  27287  chebbnd1lem1  27387  dchrisumlem2  27408  axlowdimlem16  28891  axlowdimlem17  28892  crctcshwlkn0lem5  29751  fzspl  32719  supfz  35723  nn0prpwlem  36317  rmspecsqrtnq  42901  rmspecnonsq  42902  rmspecfund  42904  rmspecpos  42912  rmxypos  42943  ltrmynn0  42944  ltrmxnn0  42945  jm2.24nn  42955  jm2.17a  42956  jm2.17b  42957  jm2.17c  42958  jm3.1lem1  43013  jm3.1lem2  43014  climsuselem1  45612  climsuse  45613  limsupequzlem  45727  limsupmnfuzlem  45731  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  itgspltprt  45984  stoweidlem14  46019  wallispilem3  46072  stirlinglem11  46089  fourierdlem103  46214  fourierdlem104  46215  2ltceilhalf  47333  ceilhalfgt1  47334  2tceilhalfelfzo1  47337  ceilhalfnn  47341  iccpartigtl  47428  fmtnoprmfac2lem1  47571  fmtno4prmfac  47577  lighneallem4a  47613  gboge9  47769  nnsum3primesle9  47799  bgoldbnnsum3prm  47809  bgoldbtbndlem3  47812  bgoldbtbndlem4  47813  bgoldbtbnd  47814  gpgusgralem  48051  gpgprismgrusgra  48053  gpg3nbgrvtx0ALT  48072  gpgprismgr4cycllem3  48091  expnegico01  48511  fllog2  48561  dignn0ldlem  48595  dignnld  48596  digexp  48600  dignn0flhalf  48611