Theorem eluzle 12776

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  ‘cfv 6500   ≤ cle 11179  ℤcz 12500  ℤ_≥cuz 12763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-cnex 11094  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-neg 11379  df-z 12501  df-uz 12764

This theorem is referenced by:  uztrn  12781  uzneg  12783  uzss  12786  uz11  12788  eluzp1l  12790  eluzadd  12792  eluzsub  12793  subeluzsub  12796  uzm1  12797  uzin  12799  uzind4  12831  uzwo  12836  uzsupss  12865  ge2halflem1  13034  elfz5  13444  elfzle1  13455  elfzle2  13456  elfzle3  13458  elfz1uz  13522  uzsplit  13524  uzdisj  13525  uznfz  13538  elfz2nn0  13546  uzsubfz0  13564  nn0disj  13572  fzouzdisj  13623  fzoun  13624  fldiv4lem1div2uz2  13768  m1modge3gt1  13853  expmulnbnd  14170  seqcoll  14399  swrdlen2  14596  swrdfv2  14597  rexuzre  15288  rlimclim1  15480  isercoll  15603  iseralt  15620  o1fsum  15748  mertenslem1  15819  fprodeq0  15910  efcllem  16012  rpnnen2lem9  16159  smuval2  16421  smupvallem  16422  isprm7  16647  hashdvds  16714  pcmpt2  16833  pcfaclem  16838  pcfac  16839  vdwlem6  16926  ramtlecl  16940  prmlem1  17047  prmlem2  17059  znfld  21527  lmnn  25231  mbflimsup  25635  mbfi1fseqlem6  25689  dvfsumge  25996  plyco0  26165  coeeulem  26197  radcnvlem2  26391  log2tlbnd  26923  lgamgulmlem4  27010  lgamcvg2  27033  chtub  27191  chpval2  27197  chpchtsum  27198  bcmax  27257  bpos1lem  27261  bpos1  27262  bposlem3  27265  bposlem4  27266  bposlem5  27267  bposlem6  27268  lgslem1  27276  lgsdirprm  27310  lgseisen  27358  dchrisumlema  27467  dchrisumlem2  27469  dchrisum0lem1  27495  axlowdimlem3  29029  axlowdimlem6  29032  axlowdimlem7  29033  axlowdimlem16  29042  axlowdimlem17  29043  dlwwlknondlwlknonf1olem1  30451  minvecolem3  30964  minvecolem4  30968  breprexplemc  34810  subfacval3  35405  climuzcnv  35887  knoppndvlem6  36739  poimirlem29  37900  fdc  37996  aks4d1lem1  42432  aks4d1p1  42446  aks4d1p2  42447  aks4d1p3  42448  aks4d1p5  42450  aks4d1p6  42451  aks4d1p7d1  42452  aks4d1p7  42453  aks4d1p8  42457  aks4d1p9  42458  aks6d1c7lem1  42550  aks6d1c7lem2  42551  aks6d1c7  42554  aks5lem6  42562  aks5lem8  42571  jm2.24nn  43316  jm2.23  43353  expdiophlem1  43378  hashnzfz2  44677  bccbc  44701  binomcxplemnn0  44705  ssinc  45446  ssdec  45447  fzdifsuc2  45672  uzfissfz  45685  iuneqfzuzlem  45693  ssuzfz  45708  uzublem  45788  uzinico  45919  fmul01lt1lem1  45944  climsuselem1  45967  climsuse  45968  limsupubuzlem  46070  limsupequzlem  46080  limsupmnfuzlem  46084  limsupre3uzlem  46093  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  iblspltprt  46331  itgspltprt  46337  stoweidlem11  46369  stirlinglem11  46442  fourierdlem79  46543  fourierdlem103  46567  fourierdlem104  46568  vonioolem1  47038  2ltceilhalf  47688  ceilhalfnn  47696  fmtnoprmfac1  47925  fmtnoprmfac2lem1  47926  lighneallem2  47966  lighneallem4a  47968  gboge9  48124  bgoldbnnsum3prm  48164  nnolog2flm1  48950