Theorem eluzle 12832

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

Syntax hints:   → wi 4   ∈ wcel 2098   class class class wbr 5138  ‘cfv 6533   ≤ cle 11246  ℤcz 12555  ℤ_≥cuz 12819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-cnex 11162  ax-resscn 11163

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7404  df-neg 11444  df-z 12556  df-uz 12820

This theorem is referenced by:  uztrn  12837  uzneg  12839  uzss  12842  uz11  12844  eluzp1l  12846  eluzadd  12848  eluzsub  12849  subeluzsub  12856  uzm1  12857  uzin  12859  uzind4  12887  uzwo  12892  uzsupss  12921  elfz5  13490  elfzle1  13501  elfzle2  13502  elfzle3  13504  elfz1uz  13568  uzsplit  13570  uzdisj  13571  uznfz  13581  elfz2nn0  13589  uzsubfz0  13606  nn0disj  13614  fzouzdisj  13665  fzoun  13666  fldiv4lem1div2uz2  13798  m1modge3gt1  13880  expmulnbnd  14195  seqcoll  14422  swrdlen2  14607  swrdfv2  14608  rexuzre  15296  rlimclim1  15486  isercoll  15611  iseralt  15628  o1fsum  15756  mertenslem1  15827  fprodeq0  15916  efcllem  16018  rpnnen2lem9  16162  smuval2  16420  smupvallem  16421  isprm7  16642  hashdvds  16707  pcmpt2  16825  pcfaclem  16830  pcfac  16831  vdwlem6  16918  ramtlecl  16932  prmlem1  17040  prmlem2  17052  znfld  21423  lmnn  25113  mbflimsup  25517  mbfi1fseqlem6  25572  dvfsumge  25878  plyco0  26046  coeeulem  26078  radcnvlem2  26267  log2tlbnd  26793  lgamgulmlem4  26880  lgamcvg2  26903  chtub  27061  chpval2  27067  chpchtsum  27068  bcmax  27127  bpos1lem  27131  bpos1  27132  bposlem3  27135  bposlem4  27136  bposlem5  27137  bposlem6  27138  lgslem1  27146  lgsdirprm  27180  lgseisen  27228  dchrisumlema  27337  dchrisumlem2  27339  dchrisum0lem1  27365  axlowdimlem3  28671  axlowdimlem6  28674  axlowdimlem7  28675  axlowdimlem16  28684  axlowdimlem17  28685  dlwwlknondlwlknonf1olem1  30086  minvecolem3  30598  minvecolem4  30602  breprexplemc  34133  subfacval3  34669  climuzcnv  35145  knoppndvlem6  35883  poimirlem29  37007  fdc  37103  aks4d1lem1  41420  aks4d1p1  41434  aks4d1p2  41435  aks4d1p3  41436  aks4d1p5  41438  aks4d1p6  41439  aks4d1p7d1  41440  aks4d1p7  41441  aks4d1p8  41445  aks4d1p9  41446  jm2.24nn  42187  jm2.23  42224  expdiophlem1  42249  hashnzfz2  43569  bccbc  43593  binomcxplemnn0  43597  ssinc  44264  ssdec  44265  fzdifsuc2  44505  uzfissfz  44521  iuneqfzuzlem  44529  ssuzfz  44544  uzublem  44625  uzinico  44758  fmul01lt1lem1  44785  climsuselem1  44808  climsuse  44809  limsupubuzlem  44913  limsupequzlem  44923  limsupmnfuzlem  44927  limsupre3uzlem  44936  ioodvbdlimc1lem2  45133  ioodvbdlimc2lem  45135  iblspltprt  45174  itgspltprt  45180  stoweidlem11  45212  stirlinglem11  45285  fourierdlem79  45386  fourierdlem103  45410  fourierdlem104  45411  vonioolem1  45881  fmtnoprmfac1  46718  fmtnoprmfac2lem1  46719  lighneallem2  46759  lighneallem4a  46761  gboge9  46917  bgoldbnnsum3prm  46957  nnolog2flm1  47464