Theorem eluzle 12795

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  ‘cfv 6493   ≤ cle 11174  ℤcz 12518  ℤ_≥cuz 12782

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 5232  ax-nul 5242  ax-pr 5371  ax-cnex 11088  ax-resscn 11089

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7364  df-neg 11374  df-z 12519  df-uz 12783

This theorem is referenced by:  uztrn  12800  uzneg  12802  uzss  12805  uz11  12807  eluzp1l  12809  eluzadd  12811  eluzsub  12812  subeluzsub  12815  uzm1  12816  uzin  12818  uzind4  12850  uzwo  12855  uzsupss  12884  ge2halflem1  13053  elfz5  13464  elfzle1  13475  elfzle2  13476  elfzle3  13478  elfz1uz  13542  uzsplit  13544  uzdisj  13545  uznfz  13558  elfz2nn0  13566  uzsubfz0  13584  nn0disj  13592  fzouzdisj  13644  fzoun  13645  fldiv4lem1div2uz2  13789  m1modge3gt1  13874  expmulnbnd  14191  seqcoll  14420  swrdlen2  14617  swrdfv2  14618  rexuzre  15309  rlimclim1  15501  isercoll  15624  iseralt  15641  o1fsum  15770  mertenslem1  15843  fprodeq0  15934  efcllem  16036  rpnnen2lem9  16183  smuval2  16445  smupvallem  16446  isprm7  16672  hashdvds  16739  pcmpt2  16858  pcfaclem  16863  pcfac  16864  vdwlem6  16951  ramtlecl  16965  prmlem1  17072  prmlem2  17084  znfld  21553  lmnn  25243  mbflimsup  25646  mbfi1fseqlem6  25700  dvfsumge  26002  plyco0  26170  coeeulem  26202  radcnvlem2  26395  log2tlbnd  26925  lgamgulmlem4  27012  lgamcvg2  27035  chtub  27192  chpval2  27198  chpchtsum  27199  bcmax  27258  bpos1lem  27262  bpos1  27263  bposlem3  27266  bposlem4  27267  bposlem5  27268  bposlem6  27269  lgslem1  27277  lgsdirprm  27311  lgseisen  27359  dchrisumlema  27468  dchrisumlem2  27470  dchrisum0lem1  27496  axlowdimlem3  29030  axlowdimlem6  29033  axlowdimlem7  29034  axlowdimlem16  29043  axlowdimlem17  29044  dlwwlknondlwlknonf1olem1  30452  minvecolem3  30965  minvecolem4  30969  breprexplemc  34795  subfacval3  35390  climuzcnv  35872  knoppndvlem6  36796  poimirlem29  37987  fdc  38083  aks4d1lem1  42518  aks4d1p1  42532  aks4d1p2  42533  aks4d1p3  42534  aks4d1p5  42536  aks4d1p6  42537  aks4d1p7d1  42538  aks4d1p7  42539  aks4d1p8  42543  aks4d1p9  42544  aks6d1c7lem1  42636  aks6d1c7lem2  42637  aks6d1c7  42640  aks5lem6  42648  aks5lem8  42657  jm2.24nn  43408  jm2.23  43445  expdiophlem1  43470  hashnzfz2  44769  bccbc  44793  binomcxplemnn0  44797  ssinc  45538  ssdec  45539  fzdifsuc2  45764  uzfissfz  45777  iuneqfzuzlem  45785  ssuzfz  45800  uzublem  45879  uzinico  46010  fmul01lt1lem1  46035  climsuselem1  46058  climsuse  46059  limsupubuzlem  46161  limsupequzlem  46171  limsupmnfuzlem  46175  limsupre3uzlem  46184  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  iblspltprt  46422  itgspltprt  46428  stoweidlem11  46460  stirlinglem11  46533  fourierdlem79  46634  fourierdlem103  46658  fourierdlem104  46659  vonioolem1  47129  nnmul2  47793  2ltceilhalf  47795  ceilhalfnn  47803  2timesltsq  47841  2timesltsqm1  47842  fmtnoprmfac1  48043  fmtnoprmfac2lem1  48044  lighneallem2  48084  lighneallem4a  48086  gboge9  48255  bgoldbnnsum3prm  48295  nnolog2flm1  49081