Theorem eluzelre 12255

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6355  ℝcr 10536  ℤ_≥cuz 12244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-cnex 10593  ax-resscn 10594

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363  df-ov 7159  df-neg 10873  df-z 11983  df-uz 12245

This theorem is referenced by:  eluzelcn  12256  uzm1  12277  uzsplit  12980  fzneuz  12989  fzouzsplit  13073  fzouzdisj  13074  fzoun  13075  eluzgtdifelfzo  13100  elfzonelfzo  13140  fldiv4lem1div2uz2  13207  mulp1mod1  13281  m1modge3gt1  13287  om2uzlt2i  13320  bernneq3  13593  hashfzp1  13793  seqcoll  13823  seqcoll2  13824  rexuzre  14712  rlimclim1  14902  climrlim2  14904  modm1div  15619  isprm5  16051  isprm7  16052  ncoprmlnprm  16068  dfphi2  16111  pclem  16175  pcmpt  16228  pockthg  16242  prmlem1  16441  prmlem2  16453  mtest  24992  logbleb  25361  logbgcd1irr  25372  isppw  25691  chtdif  25735  chtub  25788  fsumvma2  25790  chpval2  25794  bpos1lem  25858  bpos1  25859  gausslemma2dlem4  25945  chebbnd1lem1  26045  dchrisumlem2  26066  axlowdimlem16  26743  axlowdimlem17  26744  crctcshwlkn0lem5  27592  fzspl  30513  supfz  32960  nn0prpwlem  33670  rtprmirr  39243  rmspecsqrtnq  39552  rmspecnonsq  39553  rmspecfund  39555  rmspecpos  39562  rmxypos  39593  ltrmynn0  39594  ltrmxnn0  39595  jm2.24nn  39605  jm2.17a  39606  jm2.17b  39607  jm2.17c  39608  jm3.1lem1  39663  jm3.1lem2  39664  climsuselem1  41937  climsuse  41938  limsupequzlem  42052  limsupmnfuzlem  42056  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  itgspltprt  42313  stoweidlem14  42348  wallispilem3  42401  stirlinglem11  42418  fourierdlem103  42543  fourierdlem104  42544  iccpartigtl  43632  fmtnoprmfac2lem1  43777  fmtno4prmfac  43783  lighneallem4a  43822  gboge9  43978  nnsum3primesle9  44008  bgoldbnnsum3prm  44018  bgoldbtbndlem3  44021  bgoldbtbndlem4  44022  bgoldbtbnd  44023  expnegico01  44622  fllog2  44677  dignn0ldlem  44711  dignnld  44712  digexp  44716  dignn0flhalf  44727