Theorem eluzle 12762

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 12755	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
2	1	simp3bi 1147	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁)

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5096  ‘cfv 6490   ≤ cle 11165  ℤcz 12486  ℤ_≥cuz 12749

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-cnex 11080  ax-resscn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-ov 7359  df-neg 11365  df-z 12487  df-uz 12750

This theorem is referenced by:  uztrn  12767  uzneg  12769  uzss  12772  uz11  12774  eluzp1l  12776  eluzadd  12778  eluzsub  12779  subeluzsub  12782  uzm1  12783  uzin  12785  uzind4  12817  uzwo  12822  uzsupss  12851  ge2halflem1  13020  elfz5  13430  elfzle1  13441  elfzle2  13442  elfzle3  13444  elfz1uz  13508  uzsplit  13510  uzdisj  13511  uznfz  13524  elfz2nn0  13532  uzsubfz0  13550  nn0disj  13558  fzouzdisj  13609  fzoun  13610  fldiv4lem1div2uz2  13754  m1modge3gt1  13839  expmulnbnd  14156  seqcoll  14385  swrdlen2  14582  swrdfv2  14583  rexuzre  15274  rlimclim1  15466  isercoll  15589  iseralt  15606  o1fsum  15734  mertenslem1  15805  fprodeq0  15896  efcllem  15998  rpnnen2lem9  16145  smuval2  16407  smupvallem  16408  isprm7  16633  hashdvds  16700  pcmpt2  16819  pcfaclem  16824  pcfac  16825  vdwlem6  16912  ramtlecl  16926  prmlem1  17033  prmlem2  17045  znfld  21513  lmnn  25217  mbflimsup  25621  mbfi1fseqlem6  25675  dvfsumge  25982  plyco0  26151  coeeulem  26183  radcnvlem2  26377  log2tlbnd  26909  lgamgulmlem4  26996  lgamcvg2  27019  chtub  27177  chpval2  27183  chpchtsum  27184  bcmax  27243  bpos1lem  27247  bpos1  27248  bposlem3  27251  bposlem4  27252  bposlem5  27253  bposlem6  27254  lgslem1  27262  lgsdirprm  27296  lgseisen  27344  dchrisumlema  27453  dchrisumlem2  27455  dchrisum0lem1  27481  axlowdimlem3  28966  axlowdimlem6  28969  axlowdimlem7  28970  axlowdimlem16  28979  axlowdimlem17  28980  dlwwlknondlwlknonf1olem1  30388  minvecolem3  30900  minvecolem4  30904  breprexplemc  34738  subfacval3  35332  climuzcnv  35814  knoppndvlem6  36660  poimirlem29  37789  fdc  37885  aks4d1lem1  42255  aks4d1p1  42269  aks4d1p2  42270  aks4d1p3  42271  aks4d1p5  42273  aks4d1p6  42274  aks4d1p7d1  42275  aks4d1p7  42276  aks4d1p8  42280  aks4d1p9  42281  aks6d1c7lem1  42373  aks6d1c7lem2  42374  aks6d1c7  42377  aks5lem6  42385  aks5lem8  42394  jm2.24nn  43143  jm2.23  43180  expdiophlem1  43205  hashnzfz2  44504  bccbc  44528  binomcxplemnn0  44532  ssinc  45273  ssdec  45274  fzdifsuc2  45500  uzfissfz  45513  iuneqfzuzlem  45521  ssuzfz  45536  uzublem  45616  uzinico  45747  fmul01lt1lem1  45772  climsuselem1  45795  climsuse  45796  limsupubuzlem  45898  limsupequzlem  45908  limsupmnfuzlem  45912  limsupre3uzlem  45921  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  iblspltprt  46159  itgspltprt  46165  stoweidlem11  46197  stirlinglem11  46270  fourierdlem79  46371  fourierdlem103  46395  fourierdlem104  46396  vonioolem1  46866  2ltceilhalf  47516  ceilhalfnn  47524  fmtnoprmfac1  47753  fmtnoprmfac2lem1  47754  lighneallem2  47794  lighneallem4a  47796  gboge9  47952  bgoldbnnsum3prm  47992  nnolog2flm1  48778