Theorem eluzelre 12804

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6511  ℝcr 11067  ℤ_≥cuz 12793

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-cnex 11124  ax-resscn 11125

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-neg 11408  df-z 12530  df-uz 12794

This theorem is referenced by:  eluzelcn  12805  eluzadd  12822  eluzsub  12823  uzm1  12831  ge2halflem1  13068  uzsplit  13557  fzneuz  13569  fzouzsplit  13655  fzouzdisj  13656  fzoun  13657  eluzgtdifelfzo  13688  elfzonelfzo  13730  fldiv4lem1div2uz2  13798  mulp1mod1  13876  m1modge3gt1  13883  om2uzlt2i  13916  bernneq3  14196  hashfzp1  14396  seqcoll  14429  seqcoll2  14430  rexuzre  15319  rlimclim1  15511  climrlim2  15513  modm1div  16234  isprm5  16677  isprm7  16678  ncoprmlnprm  16698  dfphi2  16744  pclem  16809  pcmpt  16863  pockthg  16877  prmlem1  17078  prmlem2  17090  mtest  26313  rtprmirr  26670  logbleb  26693  logbgcd1irr  26704  isppw  27024  chtdif  27068  chtub  27123  fsumvma2  27125  chpval2  27129  bpos1lem  27193  bpos1  27194  gausslemma2dlem4  27280  chebbnd1lem1  27380  dchrisumlem2  27401  axlowdimlem16  28884  axlowdimlem17  28885  crctcshwlkn0lem5  29744  fzspl  32712  supfz  35716  nn0prpwlem  36310  rmspecsqrtnq  42894  rmspecnonsq  42895  rmspecfund  42897  rmspecpos  42905  rmxypos  42936  ltrmynn0  42937  ltrmxnn0  42938  jm2.24nn  42948  jm2.17a  42949  jm2.17b  42950  jm2.17c  42951  jm3.1lem1  43006  jm3.1lem2  43007  climsuselem1  45605  climsuse  45606  limsupequzlem  45720  limsupmnfuzlem  45724  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  itgspltprt  45977  stoweidlem14  46012  wallispilem3  46065  stirlinglem11  46082  fourierdlem103  46207  fourierdlem104  46208  2ltceilhalf  47329  ceilhalfgt1  47330  2tceilhalfelfzo1  47333  ceilhalfnn  47337  iccpartigtl  47424  fmtnoprmfac2lem1  47567  fmtno4prmfac  47573  lighneallem4a  47609  gboge9  47765  nnsum3primesle9  47795  bgoldbnnsum3prm  47805  bgoldbtbndlem3  47808  bgoldbtbndlem4  47809  bgoldbtbnd  47810  gpgusgralem  48047  gpgprismgrusgra  48049  gpg3nbgrvtx0ALT  48068  gpgprismgr4cycllem3  48087  expnegico01  48507  fllog2  48557  dignn0ldlem  48591  dignnld  48592  digexp  48596  dignn0flhalf  48607