Theorem eluzle 12524

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5070  ‘cfv 6418   ≤ cle 10941  ℤcz 12249  ℤ_≥cuz 12511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-cnex 10858  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-ov 7258  df-neg 11138  df-z 12250  df-uz 12512

This theorem is referenced by:  uztrn  12529  uzneg  12531  uzss  12534  uz11  12536  eluzp1l  12538  subeluzsub  12544  uzm1  12545  uzin  12547  uzind4  12575  uzwo  12580  uzsupss  12609  elfz5  13177  elfzle1  13188  elfzle2  13189  elfzle3  13191  elfz1uz  13255  uzsplit  13257  uzdisj  13258  uznfz  13268  elfz2nn0  13276  uzsubfz0  13293  nn0disj  13301  fzouzdisj  13351  fzoun  13352  fldiv4lem1div2uz2  13484  m1modge3gt1  13566  expmulnbnd  13878  seqcoll  14106  swrdlen2  14301  swrdfv2  14302  rexuzre  14992  rlimclim1  15182  isercoll  15307  iseralt  15324  o1fsum  15453  mertenslem1  15524  fprodeq0  15613  efcllem  15715  rpnnen2lem9  15859  smuval2  16117  smupvallem  16118  isprm7  16341  hashdvds  16404  pcmpt2  16522  pcfaclem  16527  pcfac  16528  vdwlem6  16615  ramtlecl  16629  prmlem1  16737  prmlem2  16749  znfld  20680  lmnn  24332  mbflimsup  24735  mbfi1fseqlem6  24790  dvfsumge  25091  plyco0  25258  coeeulem  25290  radcnvlem2  25478  log2tlbnd  26000  lgamgulmlem4  26086  lgamcvg2  26109  chtub  26265  chpval2  26271  chpchtsum  26272  bcmax  26331  bpos1lem  26335  bpos1  26336  bposlem3  26339  bposlem4  26340  bposlem5  26341  bposlem6  26342  lgslem1  26350  lgsdirprm  26384  lgseisen  26432  dchrisumlema  26541  dchrisumlem2  26543  dchrisum0lem1  26569  axlowdimlem3  27215  axlowdimlem6  27218  axlowdimlem7  27219  axlowdimlem16  27228  axlowdimlem17  27229  dlwwlknondlwlknonf1olem1  28629  minvecolem3  29139  minvecolem4  29143  breprexplemc  32512  subfacval3  33051  climuzcnv  33529  knoppndvlem6  34624  poimirlem29  35733  fdc  35830  aks4d1lem1  39998  aks4d1p1  40012  aks4d1p2  40013  aks4d1p3  40014  aks4d1p5  40016  aks4d1p6  40017  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8  40023  aks4d1p9  40024  jm2.24nn  40697  jm2.23  40734  expdiophlem1  40759  hashnzfz2  41828  bccbc  41852  binomcxplemnn0  41856  ssinc  42526  ssdec  42527  fzdifsuc2  42739  uzfissfz  42755  iuneqfzuzlem  42763  ssuzfz  42778  uzublem  42860  uzinico  42988  fmul01lt1lem1  43015  climsuselem1  43038  climsuse  43039  limsupubuzlem  43143  limsupequzlem  43153  limsupmnfuzlem  43157  limsupre3uzlem  43166  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  iblspltprt  43404  itgspltprt  43410  stoweidlem11  43442  stirlinglem11  43515  fourierdlem79  43616  fourierdlem103  43640  fourierdlem104  43641  vonioolem1  44108  fmtnoprmfac1  44905  fmtnoprmfac2lem1  44906  lighneallem2  44946  lighneallem4a  44948  gboge9  45104  bgoldbnnsum3prm  45144  nnolog2flm1  45824