Theorem eluzle 12806

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5107  ‘cfv 6511   ≤ cle 11209  ℤcz 12529  ℤ_≥cuz 12793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-cnex 11124  ax-resscn 11125

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-neg 11408  df-z 12530  df-uz 12794

This theorem is referenced by:  uztrn  12811  uzneg  12813  uzss  12816  uz11  12818  eluzp1l  12820  eluzadd  12822  eluzsub  12823  subeluzsub  12830  uzm1  12831  uzin  12833  uzind4  12865  uzwo  12870  uzsupss  12899  ge2halflem1  13068  elfz5  13477  elfzle1  13488  elfzle2  13489  elfzle3  13491  elfz1uz  13555  uzsplit  13557  uzdisj  13558  uznfz  13571  elfz2nn0  13579  uzsubfz0  13597  nn0disj  13605  fzouzdisj  13656  fzoun  13657  fldiv4lem1div2uz2  13798  m1modge3gt1  13883  expmulnbnd  14200  seqcoll  14429  swrdlen2  14625  swrdfv2  14626  rexuzre  15319  rlimclim1  15511  isercoll  15634  iseralt  15651  o1fsum  15779  mertenslem1  15850  fprodeq0  15941  efcllem  16043  rpnnen2lem9  16190  smuval2  16452  smupvallem  16453  isprm7  16678  hashdvds  16745  pcmpt2  16864  pcfaclem  16869  pcfac  16870  vdwlem6  16957  ramtlecl  16971  prmlem1  17078  prmlem2  17090  znfld  21470  lmnn  25163  mbflimsup  25567  mbfi1fseqlem6  25621  dvfsumge  25928  plyco0  26097  coeeulem  26129  radcnvlem2  26323  log2tlbnd  26855  lgamgulmlem4  26942  lgamcvg2  26965  chtub  27123  chpval2  27129  chpchtsum  27130  bcmax  27189  bpos1lem  27193  bpos1  27194  bposlem3  27197  bposlem4  27198  bposlem5  27199  bposlem6  27200  lgslem1  27208  lgsdirprm  27242  lgseisen  27290  dchrisumlema  27399  dchrisumlem2  27401  dchrisum0lem1  27427  axlowdimlem3  28871  axlowdimlem6  28874  axlowdimlem7  28875  axlowdimlem16  28884  axlowdimlem17  28885  dlwwlknondlwlknonf1olem1  30293  minvecolem3  30805  minvecolem4  30809  breprexplemc  34623  subfacval3  35176  climuzcnv  35658  knoppndvlem6  36505  poimirlem29  37643  fdc  37739  aks4d1lem1  42050  aks4d1p1  42064  aks4d1p2  42065  aks4d1p3  42066  aks4d1p5  42068  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8  42075  aks4d1p9  42076  aks6d1c7lem1  42168  aks6d1c7lem2  42169  aks6d1c7  42172  aks5lem6  42180  aks5lem8  42189  jm2.24nn  42948  jm2.23  42985  expdiophlem1  43010  hashnzfz2  44310  bccbc  44334  binomcxplemnn0  44338  ssinc  45081  ssdec  45082  fzdifsuc2  45308  uzfissfz  45322  iuneqfzuzlem  45330  ssuzfz  45345  uzublem  45426  uzinico  45557  fmul01lt1lem1  45582  climsuselem1  45605  climsuse  45606  limsupubuzlem  45710  limsupequzlem  45720  limsupmnfuzlem  45724  limsupre3uzlem  45733  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  iblspltprt  45971  itgspltprt  45977  stoweidlem11  46009  stirlinglem11  46082  fourierdlem79  46183  fourierdlem103  46207  fourierdlem104  46208  vonioolem1  46678  2ltceilhalf  47329  ceilhalfnn  47337  fmtnoprmfac1  47566  fmtnoprmfac2lem1  47567  lighneallem2  47607  lighneallem4a  47609  gboge9  47765  bgoldbnnsum3prm  47805  nnolog2flm1  48579