Theorem eluzelre 12877

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

Syntax hints:   → wi 4   ∈ wcel 2099  ‘cfv 6544  ℝcr 11146  ℤ_≥cuz 12866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5295  ax-nul 5302  ax-pr 5424  ax-cnex 11203  ax-resscn 11204

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ral 3052  df-rex 3061  df-rab 3421  df-v 3465  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4907  df-br 5145  df-opab 5207  df-mpt 5228  df-id 5571  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7417  df-neg 11486  df-z 12603  df-uz 12867

This theorem is referenced by:  eluzelcn  12878  eluzadd  12895  eluzsub  12896  uzm1  12904  uzsplit  13619  fzneuz  13628  fzouzsplit  13713  fzouzdisj  13714  fzoun  13715  eluzgtdifelfzo  13740  elfzonelfzo  13781  fldiv4lem1div2uz2  13848  mulp1mod1  13924  m1modge3gt1  13930  om2uzlt2i  13963  bernneq3  14241  hashfzp1  14441  seqcoll  14476  seqcoll2  14477  rexuzre  15350  rlimclim1  15540  climrlim2  15542  modm1div  16261  isprm5  16701  isprm7  16702  ncoprmlnprm  16723  dfphi2  16769  pclem  16833  pcmpt  16887  pockthg  16901  prmlem1  17103  prmlem2  17115  mtest  26428  rtprmirr  26783  logbleb  26806  logbgcd1irr  26817  isppw  27137  chtdif  27181  chtub  27236  fsumvma2  27238  chpval2  27242  bpos1lem  27306  bpos1  27307  gausslemma2dlem4  27393  chebbnd1lem1  27493  dchrisumlem2  27514  axlowdimlem16  28886  axlowdimlem17  28887  crctcshwlkn0lem5  29743  fzspl  32693  supfz  35562  nn0prpwlem  36045  rmspecsqrtnq  42598  rmspecnonsq  42599  rmspecfund  42601  rmspecpos  42609  rmxypos  42640  ltrmynn0  42641  ltrmxnn0  42642  jm2.24nn  42652  jm2.17a  42653  jm2.17b  42654  jm2.17c  42655  jm3.1lem1  42710  jm3.1lem2  42711  climsuselem1  45262  climsuse  45263  limsupequzlem  45377  limsupmnfuzlem  45381  ioodvbdlimc1lem2  45587  ioodvbdlimc2lem  45589  itgspltprt  45634  stoweidlem14  45669  wallispilem3  45722  stirlinglem11  45739  fourierdlem103  45864  fourierdlem104  45865  iccpartigtl  47029  fmtnoprmfac2lem1  47172  fmtno4prmfac  47178  lighneallem4a  47214  gboge9  47370  nnsum3primesle9  47400  bgoldbnnsum3prm  47410  bgoldbtbndlem3  47413  bgoldbtbndlem4  47414  bgoldbtbnd  47415  expnegico01  47935  fllog2  47990  dignn0ldlem  48024  dignnld  48025  digexp  48029  dignn0flhalf  48040