Theorem eluzelre 12908

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6568  ℝcr 11177  ℤ_≥cuz 12897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-cnex 11234  ax-resscn 11235

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5701  df-rel 5702  df-cnv 5703  df-co 5704  df-dm 5705  df-rn 5706  df-res 5707  df-ima 5708  df-iota 6520  df-fun 6570  df-fn 6571  df-f 6572  df-fv 6576  df-ov 7446  df-neg 11517  df-z 12634  df-uz 12898

This theorem is referenced by:  eluzelcn  12909  eluzadd  12926  eluzsub  12927  uzm1  12935  uzsplit  13650  fzneuz  13659  fzouzsplit  13745  fzouzdisj  13746  fzoun  13747  eluzgtdifelfzo  13772  elfzonelfzo  13813  fldiv4lem1div2uz2  13881  mulp1mod1  13957  m1modge3gt1  13963  om2uzlt2i  13996  bernneq3  14274  hashfzp1  14474  seqcoll  14507  seqcoll2  14508  rexuzre  15395  rlimclim1  15585  climrlim2  15587  modm1div  16308  isprm5  16748  isprm7  16749  ncoprmlnprm  16769  dfphi2  16815  pclem  16879  pcmpt  16933  pockthg  16947  prmlem1  17149  prmlem2  17161  mtest  26457  rtprmirr  26813  logbleb  26836  logbgcd1irr  26847  isppw  27167  chtdif  27211  chtub  27266  fsumvma2  27268  chpval2  27272  bpos1lem  27336  bpos1  27337  gausslemma2dlem4  27423  chebbnd1lem1  27523  dchrisumlem2  27544  axlowdimlem16  28982  axlowdimlem17  28983  crctcshwlkn0lem5  29839  fzspl  32787  supfz  35683  nn0prpwlem  36280  rmspecsqrtnq  42854  rmspecnonsq  42855  rmspecfund  42857  rmspecpos  42865  rmxypos  42896  ltrmynn0  42897  ltrmxnn0  42898  jm2.24nn  42908  jm2.17a  42909  jm2.17b  42910  jm2.17c  42911  jm3.1lem1  42966  jm3.1lem2  42967  climsuselem1  45517  climsuse  45518  limsupequzlem  45632  limsupmnfuzlem  45636  ioodvbdlimc1lem2  45842  ioodvbdlimc2lem  45844  itgspltprt  45889  stoweidlem14  45924  wallispilem3  45977  stirlinglem11  45994  fourierdlem103  46119  fourierdlem104  46120  iccpartigtl  47286  fmtnoprmfac2lem1  47429  fmtno4prmfac  47435  lighneallem4a  47471  gboge9  47627  nnsum3primesle9  47657  bgoldbnnsum3prm  47667  bgoldbtbndlem3  47670  bgoldbtbndlem4  47671  bgoldbtbnd  47672  expnegico01  48236  fllog2  48291  dignn0ldlem  48325  dignnld  48326  digexp  48330  dignn0flhalf  48341