Theorem eluzelre 12104

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

Syntax hints:   → wi 4   ∈ wcel 2081  ‘cfv 6225  ℝcr 10382  ℤ_≥cuz 12093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-cnex 10439  ax-resscn 10440

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-fv 6233  df-ov 7019  df-neg 10720  df-z 11830  df-uz 12094

This theorem is referenced by:  eluzelcn  12105  uzm1  12125  uzsplit  12829  fzneuz  12838  fzouzsplit  12922  fzouzdisj  12923  fzoun  12924  eluzgtdifelfzo  12949  elfzonelfzo  12989  fldiv4lem1div2uz2  13056  mulp1mod1  13130  m1modge3gt1  13136  om2uzlt2i  13169  bernneq3  13442  hashfzp1  13640  seqcoll  13670  seqcoll2  13671  rexuzre  14546  rlimclim1  14736  climrlim2  14738  modm1div  15452  isprm5  15880  isprm7  15881  ncoprmlnprm  15897  dfphi2  15940  pclem  16004  pcmpt  16057  pockthg  16071  prmlem1  16270  prmlem2  16282  mtest  24675  logbleb  25042  logbgcd1irr  25053  isppw  25373  chtdif  25417  chtub  25470  fsumvma2  25472  chpval2  25476  bpos1lem  25540  bpos1  25541  gausslemma2dlem4  25627  chebbnd1lem1  25727  dchrisumlem2  25748  axlowdimlem16  26426  axlowdimlem17  26427  crctcshwlkn0lem5  27279  fzspl  30199  supfz  32569  nn0prpwlem  33280  rtprmirr  38735  rmspecsqrtnq  39007  rmspecnonsq  39008  rmspecfund  39010  rmspecpos  39017  rmxypos  39048  ltrmynn0  39049  ltrmxnn0  39050  jm2.24nn  39060  jm2.17a  39061  jm2.17b  39062  jm2.17c  39063  jm3.1lem1  39118  jm3.1lem2  39119  climsuselem1  41449  climsuse  41450  limsupequzlem  41564  limsupmnfuzlem  41568  ioodvbdlimc1lem2  41778  ioodvbdlimc2lem  41780  itgspltprt  41825  stoweidlem14  41861  wallispilem3  41914  stirlinglem11  41931  fourierdlem103  42056  fourierdlem104  42057  iccpartigtl  43085  fmtnoprmfac2lem1  43230  fmtno4prmfac  43236  lighneallem4a  43275  gboge9  43431  nnsum3primesle9  43461  bgoldbnnsum3prm  43471  bgoldbtbndlem3  43474  bgoldbtbndlem4  43475  bgoldbtbnd  43476  expnegico01  44074  fllog2  44129  dignn0ldlem  44163  dignnld  44164  digexp  44168  dignn0flhalf  44179