Theorem eluzelre 12931

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6528  ℝcr 11156  ℤ_≥cuz 12920

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-cnex 11213  ax-resscn 11214

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-fv 6536  df-ov 7412  df-neg 11501  df-z 12649  df-uz 12921

This theorem is used by:  eluzelcn  12932  eluzadd  12949  eluzsub  12950  uzm1  12954  ge2halflem1  13192  nnge2recico01  13593  uzsplit  13684  fzneuz  13696  fzouzsplit  13783  fzouzdisj  13784  fzoun  13785  eluzgtdifelfzo  13816  elfzonelfzo  13858  fldiv4lem1div2uz2  13930  mulp1mod1  14008  m1modge3gt1  14015  om2uzlt2i  14048  bernneq3  14328  hashfzp1  14529  seqcoll  14562  seqcoll2  14563  rexuzre  15473  rlimclim1  15665  climrlim2  15667  modm1div  16387  isprm5  16831  isprm7  16832  ncoprmlnprm  16852  dfphi2  16898  pclem  16963  pcmpt  17017  pockthg  17031  prmlem1  17232  prmlem2  17245  mtest  26680  rtprmirr  27037  logbleb  27060  logbgcd1irr  27071  isppw  27390  chtdif  27434  chtub  27488  fsumvma2  27490  chpval2  27494  bpos1lem  27558  bpos1  27559  gausslemma2dlem4  27645  chebbnd1lem1  27745  dchrisumlem2  27766  axlowdimlem16  29454  axlowdimlem17  29455  crctcshwlkn0lem5  30322  fzspl  33300  supfz  36409  nn0prpwlem  37026  rmspecsqrtnq  43845  rmspecnonsq  43846  rmspecfund  43848  rmspecpos  43855  rmxypos  43886  ltrmynn0  43887  ltrmxnn0  43888  jm2.24nn  43898  jm2.17a  43899  jm2.17b  43900  jm2.17c  43901  jm3.1lem1  43956  jm3.1lem2  43957  climsuselem1  46535  climsuse  46536  limsupequzlem  46648  limsupmnfuzlem  46652  ioodvbdlimc1lem2  46858  ioodvbdlimc2lem  46860  itgspltprt  46905  stoweidlem14  46940  wallispilem3  46993  stirlinglem11  47010  fourierdlem103  47135  fourierdlem104  47136  nnmul2  48316  2ltceilhalf  48318  ceilhalfgt1  48319  2tceilhalfelfzo1  48322  ceilhalfnn  48326  2timesltsqm1  48365  iccpartigtl  48421  fmtnoprmfac2lem1  48567  fmtno4prmfac  48573  lighneallem4a  48609  gboge9  48778  nnsum3primesle9  48808  bgoldbnnsum3prm  48818  bgoldbtbndlem3  48821  bgoldbtbndlem4  48822  bgoldbtbnd  48823  gpgusgralem  49070  gpgprismgrusgra  49072  gpg3nbgrvtx0ALT  49091  gpgprismgr4cycllem3  49111  expnegico01  49546  fllog2  49596  dignn0ldlem  49630  dignnld  49631  digexp  49635  dignn0flhalf  49646