Theorem eluzle 12841

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

Syntax hints:   → wi 4   ∈ wcel 2104   class class class wbr 5149  ‘cfv 6544   ≤ cle 11255  ℤcz 12564  ℤ_≥cuz 12828

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-cnex 11170  ax-resscn 11171

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7416  df-neg 11453  df-z 12565  df-uz 12829

This theorem is referenced by:  uztrn  12846  uzneg  12848  uzss  12851  uz11  12853  eluzp1l  12855  eluzadd  12857  eluzsub  12858  subeluzsub  12865  uzm1  12866  uzin  12868  uzind4  12896  uzwo  12901  uzsupss  12930  elfz5  13499  elfzle1  13510  elfzle2  13511  elfzle3  13513  elfz1uz  13577  uzsplit  13579  uzdisj  13580  uznfz  13590  elfz2nn0  13598  uzsubfz0  13615  nn0disj  13623  fzouzdisj  13674  fzoun  13675  fldiv4lem1div2uz2  13807  m1modge3gt1  13889  expmulnbnd  14204  seqcoll  14431  swrdlen2  14616  swrdfv2  14617  rexuzre  15305  rlimclim1  15495  isercoll  15620  iseralt  15637  o1fsum  15765  mertenslem1  15836  fprodeq0  15925  efcllem  16027  rpnnen2lem9  16171  smuval2  16429  smupvallem  16430  isprm7  16651  hashdvds  16714  pcmpt2  16832  pcfaclem  16837  pcfac  16838  vdwlem6  16925  ramtlecl  16939  prmlem1  17047  prmlem2  17059  znfld  21337  lmnn  25013  mbflimsup  25417  mbfi1fseqlem6  25472  dvfsumge  25773  plyco0  25940  coeeulem  25972  radcnvlem2  26160  log2tlbnd  26684  lgamgulmlem4  26770  lgamcvg2  26793  chtub  26949  chpval2  26955  chpchtsum  26956  bcmax  27015  bpos1lem  27019  bpos1  27020  bposlem3  27023  bposlem4  27024  bposlem5  27025  bposlem6  27026  lgslem1  27034  lgsdirprm  27068  lgseisen  27116  dchrisumlema  27225  dchrisumlem2  27227  dchrisum0lem1  27253  axlowdimlem3  28467  axlowdimlem6  28470  axlowdimlem7  28471  axlowdimlem16  28480  axlowdimlem17  28481  dlwwlknondlwlknonf1olem1  29882  minvecolem3  30394  minvecolem4  30398  breprexplemc  33940  subfacval3  34476  climuzcnv  34952  knoppndvlem6  35698  poimirlem29  36822  fdc  36918  aks4d1lem1  41235  aks4d1p1  41249  aks4d1p2  41250  aks4d1p3  41251  aks4d1p5  41253  aks4d1p6  41254  aks4d1p7d1  41255  aks4d1p7  41256  aks4d1p8  41260  aks4d1p9  41261  jm2.24nn  42002  jm2.23  42039  expdiophlem1  42064  hashnzfz2  43384  bccbc  43408  binomcxplemnn0  43412  ssinc  44079  ssdec  44080  fzdifsuc2  44320  uzfissfz  44336  iuneqfzuzlem  44344  ssuzfz  44359  uzublem  44440  uzinico  44573  fmul01lt1lem1  44600  climsuselem1  44623  climsuse  44624  limsupubuzlem  44728  limsupequzlem  44738  limsupmnfuzlem  44742  limsupre3uzlem  44751  ioodvbdlimc1lem2  44948  ioodvbdlimc2lem  44950  iblspltprt  44989  itgspltprt  44995  stoweidlem11  45027  stirlinglem11  45100  fourierdlem79  45201  fourierdlem103  45225  fourierdlem104  45226  vonioolem1  45696  fmtnoprmfac1  46533  fmtnoprmfac2lem1  46534  lighneallem2  46574  lighneallem4a  46576  gboge9  46732  bgoldbnnsum3prm  46772  nnolog2flm1  47365