Theorem eluzle 12801

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5085  ‘cfv 6498   ≤ cle 11180  ℤcz 12524  ℤ_≥cuz 12788

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-ov 7370  df-neg 11380  df-z 12525  df-uz 12789

This theorem is referenced by:  uztrn  12806  uzneg  12808  uzss  12811  uz11  12813  eluzp1l  12815  eluzadd  12817  eluzsub  12818  subeluzsub  12821  uzm1  12822  uzin  12824  uzind4  12856  uzwo  12861  uzsupss  12890  ge2halflem1  13059  elfz5  13470  elfzle1  13481  elfzle2  13482  elfzle3  13484  elfz1uz  13548  uzsplit  13550  uzdisj  13551  uznfz  13564  elfz2nn0  13572  uzsubfz0  13590  nn0disj  13598  fzouzdisj  13650  fzoun  13651  fldiv4lem1div2uz2  13795  m1modge3gt1  13880  expmulnbnd  14197  seqcoll  14426  swrdlen2  14623  swrdfv2  14624  rexuzre  15315  rlimclim1  15507  isercoll  15630  iseralt  15647  o1fsum  15776  mertenslem1  15849  fprodeq0  15940  efcllem  16042  rpnnen2lem9  16189  smuval2  16451  smupvallem  16452  isprm7  16678  hashdvds  16745  pcmpt2  16864  pcfaclem  16869  pcfac  16870  vdwlem6  16957  ramtlecl  16971  prmlem1  17078  prmlem2  17090  znfld  21540  lmnn  25230  mbflimsup  25633  mbfi1fseqlem6  25687  dvfsumge  25989  plyco0  26157  coeeulem  26189  radcnvlem2  26379  log2tlbnd  26909  lgamgulmlem4  26995  lgamcvg2  27018  chtub  27175  chpval2  27181  chpchtsum  27182  bcmax  27241  bpos1lem  27245  bpos1  27246  bposlem3  27249  bposlem4  27250  bposlem5  27251  bposlem6  27252  lgslem1  27260  lgsdirprm  27294  lgseisen  27342  dchrisumlema  27451  dchrisumlem2  27453  dchrisum0lem1  27479  axlowdimlem3  29013  axlowdimlem6  29016  axlowdimlem7  29017  axlowdimlem16  29026  axlowdimlem17  29027  dlwwlknondlwlknonf1olem1  30434  minvecolem3  30947  minvecolem4  30951  breprexplemc  34776  subfacval3  35371  climuzcnv  35853  knoppndvlem6  36777  poimirlem29  37970  fdc  38066  aks4d1lem1  42501  aks4d1p1  42515  aks4d1p2  42516  aks4d1p3  42517  aks4d1p5  42519  aks4d1p6  42520  aks4d1p7d1  42521  aks4d1p7  42522  aks4d1p8  42526  aks4d1p9  42527  aks6d1c7lem1  42619  aks6d1c7lem2  42620  aks6d1c7  42623  aks5lem6  42631  aks5lem8  42640  jm2.24nn  43387  jm2.23  43424  expdiophlem1  43449  hashnzfz2  44748  bccbc  44772  binomcxplemnn0  44776  ssinc  45517  ssdec  45518  fzdifsuc2  45743  uzfissfz  45756  iuneqfzuzlem  45764  ssuzfz  45779  uzublem  45858  uzinico  45989  fmul01lt1lem1  46014  climsuselem1  46037  climsuse  46038  limsupubuzlem  46140  limsupequzlem  46150  limsupmnfuzlem  46154  limsupre3uzlem  46163  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  iblspltprt  46401  itgspltprt  46407  stoweidlem11  46439  stirlinglem11  46512  fourierdlem79  46613  fourierdlem103  46637  fourierdlem104  46638  vonioolem1  47108  nnmul2  47778  2ltceilhalf  47780  ceilhalfnn  47788  2timesltsq  47826  2timesltsqm1  47827  fmtnoprmfac1  48028  fmtnoprmfac2lem1  48029  lighneallem2  48069  lighneallem4a  48071  gboge9  48240  bgoldbnnsum3prm  48280  nnolog2flm1  49066