Theorem eluzle 12889

Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.)

Assertion

Ref	Expression
eluzle	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁)

Proof of Theorem eluzle

Step	Hyp	Ref	Expression
1		eluz2 12882	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
2	1	simp3bi 1146	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁)

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5148  ‘cfv 6563   ≤ cle 11294  ℤcz 12611  ℤ_≥cuz 12876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-cnex 11209  ax-resscn 11210

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fv 6571  df-ov 7434  df-neg 11493  df-z 12612  df-uz 12877

This theorem is referenced by:  uztrn  12894  uzneg  12896  uzss  12899  uz11  12901  eluzp1l  12903  eluzadd  12905  eluzsub  12906  subeluzsub  12913  uzm1  12914  uzin  12916  uzind4  12946  uzwo  12951  uzsupss  12980  ge2halflem1  13148  elfz5  13553  elfzle1  13564  elfzle2  13565  elfzle3  13567  elfz1uz  13631  uzsplit  13633  uzdisj  13634  uznfz  13647  elfz2nn0  13655  uzsubfz0  13673  nn0disj  13681  fzouzdisj  13732  fzoun  13733  fldiv4lem1div2uz2  13873  m1modge3gt1  13956  expmulnbnd  14271  seqcoll  14500  swrdlen2  14695  swrdfv2  14696  rexuzre  15388  rlimclim1  15578  isercoll  15701  iseralt  15718  o1fsum  15846  mertenslem1  15917  fprodeq0  16008  efcllem  16110  rpnnen2lem9  16255  smuval2  16516  smupvallem  16517  isprm7  16742  hashdvds  16809  pcmpt2  16927  pcfaclem  16932  pcfac  16933  vdwlem6  17020  ramtlecl  17034  prmlem1  17142  prmlem2  17154  znfld  21597  lmnn  25311  mbflimsup  25715  mbfi1fseqlem6  25770  dvfsumge  26077  plyco0  26246  coeeulem  26278  radcnvlem2  26472  log2tlbnd  27003  lgamgulmlem4  27090  lgamcvg2  27113  chtub  27271  chpval2  27277  chpchtsum  27278  bcmax  27337  bpos1lem  27341  bpos1  27342  bposlem3  27345  bposlem4  27346  bposlem5  27347  bposlem6  27348  lgslem1  27356  lgsdirprm  27390  lgseisen  27438  dchrisumlema  27547  dchrisumlem2  27549  dchrisum0lem1  27575  axlowdimlem3  28974  axlowdimlem6  28977  axlowdimlem7  28978  axlowdimlem16  28987  axlowdimlem17  28988  dlwwlknondlwlknonf1olem1  30393  minvecolem3  30905  minvecolem4  30909  breprexplemc  34626  subfacval3  35174  climuzcnv  35656  knoppndvlem6  36500  poimirlem29  37636  fdc  37732  aks4d1lem1  42044  aks4d1p1  42058  aks4d1p2  42059  aks4d1p3  42060  aks4d1p5  42062  aks4d1p6  42063  aks4d1p7d1  42064  aks4d1p7  42065  aks4d1p8  42069  aks4d1p9  42070  aks6d1c7lem1  42162  aks6d1c7lem2  42163  aks6d1c7  42166  aks5lem6  42174  aks5lem8  42183  jm2.24nn  42948  jm2.23  42985  expdiophlem1  43010  hashnzfz2  44317  bccbc  44341  binomcxplemnn0  44345  ssinc  45027  ssdec  45028  fzdifsuc2  45261  uzfissfz  45276  iuneqfzuzlem  45284  ssuzfz  45299  uzublem  45380  uzinico  45513  fmul01lt1lem1  45540  climsuselem1  45563  climsuse  45564  limsupubuzlem  45668  limsupequzlem  45678  limsupmnfuzlem  45682  limsupre3uzlem  45691  ioodvbdlimc1lem2  45888  ioodvbdlimc2lem  45890  iblspltprt  45929  itgspltprt  45935  stoweidlem11  45967  stirlinglem11  46040  fourierdlem79  46141  fourierdlem103  46165  fourierdlem104  46166  vonioolem1  46636  fmtnoprmfac1  47490  fmtnoprmfac2lem1  47491  lighneallem2  47531  lighneallem4a  47533  gboge9  47689  bgoldbnnsum3prm  47729  2ltceilhalf  47950  nnolog2flm1  48440