Theorem eluzelre 13000

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ‘cfv 6555  ℝcr 11223  ℤ_≥cuz 12989

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-cnex 11280  ax-resscn 11281

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-fv 6563  df-ov 7443  df-neg 11568  df-z 12718  df-uz 12990

This theorem is used by:  eluzelcn  13001  eluzadd  13018  eluzsub  13019  uzm1  13023  ge2halflem1  13261  nnge2recico01  13662  uzsplit  13754  fzneuz  13766  fzouzsplit  13853  fzouzdisj  13854  fzoun  13855  eluzgtdifelfzo  13886  elfzonelfzo  13928  fldiv4lem1div2uz2  14000  mulp1mod1  14078  m1modge3gt1  14085  om2uzlt2i  14118  bernneq3  14399  hashfzp1  14600  seqcoll  14633  seqcoll2  14634  rexuzre  15546  rlimclim1  15738  climrlim2  15740  modm1div  16460  isprm5  16909  isprm7  16910  ncoprmlnprm  16930  dfphi2  16977  pclem  17042  pcmpt  17096  pockthg  17110  prmlem1  17311  prmlem2  17324  mtest  26758  rtprmirr  27115  logbleb  27138  logbgcd1irr  27149  isppw  27468  chtdif  27512  chtub  27566  fsumvma2  27568  chpval2  27572  bpos1lem  27636  bpos1  27637  gausslemma2dlem4  27723  chebbnd1lem1  27823  dchrisumlem2  27844  axlowdimlem16  29562  axlowdimlem17  29563  crctcshwlkn0lem5  30430  fzspl  33448  supfz  36671  nn0prpwlem  37287  rmspecsqrtnq  44104  rmspecnonsq  44105  rmspecfund  44107  rmspecpos  44114  rmxypos  44145  ltrmynn0  44146  ltrmxnn0  44147  jm2.24nn  44157  jm2.17a  44158  jm2.17b  44159  jm2.17c  44160  jm3.1lem1  44215  jm3.1lem2  44216  climsuselem1  46822  climsuse  46823  limsupequzlem  46935  limsupmnfuzlem  46939  ioodvbdlimc1lem2  47145  ioodvbdlimc2lem  47147  itgspltprt  47192  stoweidlem14  47227  wallispilem3  47280  stirlinglem11  47297  fourierdlem103  47422  fourierdlem104  47423  nnmul2  48603  2ltceilhalf  48605  ceilhalfgt1  48606  2tceilhalfelfzo1  48609  ceilhalfnn  48613  2timesltsqm1  48652  iccpartigtl  48708  fmtnoprmfac2lem1  48854  fmtno4prmfac  48860  lighneallem4a  48896  gboge9  49065  nnsum3primesle9  49095  bgoldbnnsum3prm  49105  bgoldbtbndlem3  49108  bgoldbtbndlem4  49109  bgoldbtbnd  49110  gpgusgralem  49357  gpgprismgrusgra  49359  gpg3nbgrvtx0ALT  49378  gpgprismgr4cycllem3  49398  expnegico01  49833  fllog2  49883  dignn0ldlem  49917  dignnld  49918  digexp  49922  dignn0flhalf  49933