Theorem eluzelre 12686

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

Syntax hints:   → wi 4   ∈ wcel 2105  ‘cfv 6473  ℝcr 10963  ℤ_≥cuz 12675

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pr 5369  ax-cnex 11020  ax-resscn 11021

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-br 5090  df-opab 5152  df-mpt 5173  df-id 5512  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-fv 6481  df-ov 7332  df-neg 11301  df-z 12413  df-uz 12676

This theorem is referenced by:  eluzelcn  12687  uzm1  12709  uzsplit  13421  fzneuz  13430  fzouzsplit  13515  fzouzdisj  13516  fzoun  13517  eluzgtdifelfzo  13542  elfzonelfzo  13582  fldiv4lem1div2uz2  13649  mulp1mod1  13725  m1modge3gt1  13731  om2uzlt2i  13764  bernneq3  14039  hashfzp1  14238  seqcoll  14270  seqcoll2  14271  rexuzre  15155  rlimclim1  15345  climrlim2  15347  modm1div  16066  isprm5  16501  isprm7  16502  ncoprmlnprm  16521  dfphi2  16564  pclem  16628  pcmpt  16682  pockthg  16696  prmlem1  16898  prmlem2  16910  mtest  25661  logbleb  26031  logbgcd1irr  26042  isppw  26361  chtdif  26405  chtub  26458  fsumvma2  26460  chpval2  26464  bpos1lem  26528  bpos1  26529  gausslemma2dlem4  26615  chebbnd1lem1  26715  dchrisumlem2  26736  axlowdimlem16  27555  axlowdimlem17  27556  crctcshwlkn0lem5  28408  fzspl  31339  supfz  33928  nn0prpwlem  34602  rtprmirr  40597  rmspecsqrtnq  40978  rmspecnonsq  40979  rmspecfund  40981  rmspecpos  40989  rmxypos  41020  ltrmynn0  41021  ltrmxnn0  41022  jm2.24nn  41032  jm2.17a  41033  jm2.17b  41034  jm2.17c  41035  jm3.1lem1  41090  jm3.1lem2  41091  climsuselem1  43473  climsuse  43474  limsupequzlem  43588  limsupmnfuzlem  43592  ioodvbdlimc1lem2  43798  ioodvbdlimc2lem  43800  itgspltprt  43845  stoweidlem14  43880  wallispilem3  43933  stirlinglem11  43950  fourierdlem103  44075  fourierdlem104  44076  iccpartigtl  45215  fmtnoprmfac2lem1  45358  fmtno4prmfac  45364  lighneallem4a  45400  gboge9  45556  nnsum3primesle9  45586  bgoldbnnsum3prm  45596  bgoldbtbndlem3  45599  bgoldbtbndlem4  45600  bgoldbtbnd  45601  expnegico01  46199  fllog2  46254  dignn0ldlem  46288  dignnld  46289  digexp  46293  dignn0flhalf  46304