Theorem eluzle 12870

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

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5109  ‘cfv 6536   ≤ cle 11239  ℤcz 12586  ℤ_≥cuz 12857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-cnex 11151  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-neg 11439  df-z 12587  df-uz 12858

This theorem is referenced by:  uztrn  12875  uzneg  12877  uzss  12880  uz11  12882  eluzp1l  12884  eluzadd  12886  eluzsub  12887  subeluzsub  12890  uzm1  12891  uzin  12893  uzind4  12925  uzwo  12930  uzsupss  12959  ge2halflem1  13128  elfz5  13539  elfzle1  13550  elfzle2  13551  elfzle3  13553  elfz1uz  13618  uzsplit  13620  uzdisj  13621  uznfz  13634  elfz2nn0  13642  uzsubfz0  13660  nn0disj  13668  fzouzdisj  13720  fzoun  13721  fldiv4lem1div2uz2  13865  m1modge3gt1  13950  expmulnbnd  14267  seqcoll  14497  swrdlen2  14694  swrdfv2  14695  rexuzre  15400  rlimclim1  15592  isercoll  15715  iseralt  15732  o1fsum  15861  mertenslem1  15934  fprodeq0  16025  efcllem  16126  rpnnen2lem9  16273  smuval2  16535  smupvallem  16536  isprm7  16762  hashdvds  16829  pcmpt2  16948  pcfaclem  16953  pcfac  16954  vdwlem6  17041  ramtlecl  17055  prmlem1  17162  prmlem2  17175  znfld  21710  lmnn  25422  mbflimsup  25825  mbfi1fseqlem6  25879  dvfsumge  26181  plyco0  26349  coeeulem  26381  radcnvlem2  26577  log2tlbnd  27110  lgamgulmlem4  27196  lgamcvg2  27219  chtub  27376  chpval2  27382  chpchtsum  27383  bcmax  27442  bpos1lem  27446  bpos1  27447  bposlem3  27450  bposlem4  27451  bposlem5  27452  bposlem6  27453  lgslem1  27461  lgsdirprm  27495  lgseisen  27543  dchrisumlema  27652  dchrisumlem2  27654  dchrisum0lem1  27680  axlowdimlem3  29294  axlowdimlem6  29297  axlowdimlem7  29298  axlowdimlem16  29307  axlowdimlem17  29308  dlwwlknondlwlknonf1olem1  30715  minvecolem3  31228  minvecolem4  31232  breprexplemc  35019  subfacval3  35681  climuzcnv  36163  knoppndvlem6  37106  poimirlem29  38300  fdc  38396  aks4d1lem1  42829  aks4d1p1  42843  aks4d1p2  42844  aks4d1p3  42845  aks4d1p5  42847  aks4d1p6  42848  aks4d1p7d1  42849  aks4d1p7  42850  aks4d1p8  42854  aks4d1p9  42855  aks6d1c7lem1  42947  aks6d1c7lem2  42948  aks6d1c7  42951  aks5lem6  42959  aks5lem8  42968  jm2.24nn  43686  jm2.23  43723  expdiophlem1  43748  hashnzfz2  45031  bccbc  45055  binomcxplemnn0  45059  ssinc  45805  ssdec  45806  fzdifsuc2  46029  uzfissfz  46042  iuneqfzuzlem  46050  ssuzfz  46065  uzublem  46144  uzinico  46275  fmul01lt1lem1  46300  climsuselem1  46323  climsuse  46324  limsupubuzlem  46426  limsupequzlem  46436  limsupmnfuzlem  46440  limsupre3uzlem  46449  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  iblspltprt  46687  itgspltprt  46693  stoweidlem11  46725  stirlinglem11  46798  fourierdlem79  46899  fourierdlem103  46923  fourierdlem104  46924  vonioolem1  47394  nnmul2  48067  2ltceilhalf  48069  ceilhalfnn  48077  2timesltsq  48115  2timesltsqm1  48116  fmtnoprmfac1  48317  fmtnoprmfac2lem1  48318  lighneallem2  48358  lighneallem4a  48360  gboge9  48529  bgoldbnnsum3prm  48569  nnolog2flm1  49370