Theorem eluzle 12330

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5027  ‘cfv 6333   ≤ cle 10747  ℤcz 12055  ℤ_≥cuz 12317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pr 5293  ax-cnex 10664  ax-resscn 10665

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3399  df-sbc 3680  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-br 5028  df-opab 5090  df-mpt 5108  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-fv 6341  df-ov 7167  df-neg 10944  df-z 12056  df-uz 12318

This theorem is referenced by:  uztrn  12335  uzneg  12337  uzss  12340  uz11  12342  eluzp1l  12344  subeluzsub  12350  uzm1  12351  uzin  12353  uzind4  12381  uzwo  12386  uzsupss  12415  elfz5  12983  elfzle1  12994  elfzle2  12995  elfzle3  12997  elfz1uz  13061  uzsplit  13063  uzdisj  13064  uznfz  13074  elfz2nn0  13082  uzsubfz0  13099  nn0disj  13107  fzouzdisj  13157  fzoun  13158  fldiv4lem1div2uz2  13290  m1modge3gt1  13370  expmulnbnd  13681  seqcoll  13909  swrdlen2  14104  swrdfv2  14105  rexuzre  14795  rlimclim1  14985  isercoll  15110  iseralt  15127  o1fsum  15254  mertenslem1  15325  fprodeq0  15414  efcllem  15516  rpnnen2lem9  15660  smuval2  15918  smupvallem  15919  isprm7  16142  hashdvds  16205  pcmpt2  16322  pcfaclem  16327  pcfac  16328  vdwlem6  16415  ramtlecl  16429  prmlem1  16537  prmlem2  16549  znfld  20372  lmnn  24008  mbflimsup  24411  mbfi1fseqlem6  24465  dvfsumge  24766  plyco0  24933  coeeulem  24965  radcnvlem2  25153  log2tlbnd  25675  lgamgulmlem4  25761  lgamcvg2  25784  chtub  25940  chpval2  25946  chpchtsum  25947  bcmax  26006  bpos1lem  26010  bpos1  26011  bposlem3  26014  bposlem4  26015  bposlem5  26016  bposlem6  26017  lgslem1  26025  lgsdirprm  26059  lgseisen  26107  dchrisumlema  26216  dchrisumlem2  26218  dchrisum0lem1  26244  axlowdimlem3  26882  axlowdimlem6  26885  axlowdimlem7  26886  axlowdimlem16  26895  axlowdimlem17  26896  dlwwlknondlwlknonf1olem1  28293  minvecolem3  28803  minvecolem4  28807  breprexplemc  32174  subfacval3  32714  climuzcnv  33192  knoppndvlem6  34327  poimirlem29  35418  fdc  35515  aks4d1p1  39692  jm2.24nn  40337  jm2.23  40374  expdiophlem1  40399  hashnzfz2  41461  bccbc  41485  binomcxplemnn0  41489  ssinc  42159  ssdec  42160  fzdifsuc2  42371  uzfissfz  42387  iuneqfzuzlem  42395  ssuzfz  42410  uzublem  42492  uzinico  42622  fmul01lt1lem1  42651  climsuselem1  42674  climsuse  42675  limsupubuzlem  42779  limsupequzlem  42789  limsupmnfuzlem  42793  limsupre3uzlem  42802  ioodvbdlimc1lem2  42999  ioodvbdlimc2lem  43001  iblspltprt  43040  itgspltprt  43046  stoweidlem11  43078  stirlinglem11  43151  fourierdlem79  43252  fourierdlem103  43276  fourierdlem104  43277  vonioolem1  43744  fmtnoprmfac1  44535  fmtnoprmfac2lem1  44536  lighneallem2  44576  lighneallem4a  44578  gboge9  44734  bgoldbnnsum3prm  44774  nnolog2flm1  45454