MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eluzle Structured version   Visualization version   GIF version

Theorem eluzle 11892
Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.)
Assertion
Ref Expression
eluzle (𝑁 ∈ (ℤ𝑀) → 𝑀𝑁)

Proof of Theorem eluzle
StepHypRef Expression
1 eluz2 11885 . 2 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
21simp3bi 1142 1 (𝑁 ∈ (ℤ𝑀) → 𝑀𝑁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139   class class class wbr 4804  cfv 6049  cle 10267  cz 11569  cuz 11879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-cnex 10184  ax-resscn 10185
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-fv 6057  df-ov 6816  df-neg 10461  df-z 11570  df-uz 11880
This theorem is referenced by:  uztrn  11896  uzneg  11898  uzss  11900  uz11  11902  eluzp1l  11904  subeluzsub  11910  uzm1  11911  uzin  11913  uzind4  11939  uzwo  11944  uzsupss  11973  zgt1rpn0n1  12064  elfz5  12527  elfzle1  12537  elfzle2  12538  elfzle3  12540  elfz1uz  12603  uzsplit  12605  uzdisj  12606  uznfz  12616  elfz2nn0  12624  uzsubfz0  12641  nn0disj  12649  fzouzdisj  12698  fzoun  12699  fldiv4lem1div2uz2  12831  m1modge3gt1  12911  expmulnbnd  13190  seqcoll  13440  swrdlen2  13645  swrdfv2  13646  rexuzre  14291  rlimclim1  14475  isercoll  14597  iseralt  14614  o1fsum  14744  mertenslem1  14815  fprodeq0  14904  efcllem  15007  rpnnen2lem9  15150  smuval2  15406  smupvallem  15407  isprm7  15622  hashdvds  15682  pcmpt2  15799  pcfaclem  15804  pcfac  15805  vdwlem6  15892  ramtlecl  15906  prmlem1  16016  prmlem2  16029  znfld  20111  lmnn  23261  mbflimsup  23632  mbfi1fseqlem6  23686  dvfsumge  23984  plyco0  24147  coeeulem  24179  radcnvlem2  24367  log2tlbnd  24871  lgamgulmlem4  24957  lgamcvg2  24980  chtub  25136  chpval2  25142  chpchtsum  25143  bcmax  25202  bpos1lem  25206  bpos1  25207  bposlem3  25210  bposlem4  25211  bposlem5  25212  bposlem6  25213  lgslem1  25221  lgsdirprm  25255  lgseisen  25303  m1lgs  25312  dchrisumlema  25376  dchrisumlem2  25378  dchrisum0lem1  25404  axlowdimlem3  26023  axlowdimlem6  26026  axlowdimlem7  26027  axlowdimlem16  26036  axlowdimlem17  26037  dlwwlknonclwlknonf1olem1  27524  minvecolem3  28041  minvecolem4  28045  breprexplemc  31019  subfacval3  31478  climuzcnv  31872  knoppndvlem6  32814  poimirlem29  33751  fdc  33854  jm2.24nn  38028  jm2.23  38065  expdiophlem1  38090  hashnzfz2  39022  bccbc  39046  binomcxplemnn0  39050  ssinc  39763  ssdec  39764  fzdifsuc2  40023  uzfissfz  40040  iuneqfzuzlem  40048  ssuzfz  40063  uzublem  40155  uzinico  40290  fmul01lt1lem1  40319  climsuselem1  40342  climsuse  40343  limsupubuzlem  40447  limsupequzlem  40457  limsupmnfuzlem  40461  limsupre3uzlem  40470  ioodvbdlimc1lem2  40650  ioodvbdlimc2lem  40652  iblspltprt  40692  itgspltprt  40698  stoweidlem11  40731  stirlinglem11  40804  fourierdlem79  40905  fourierdlem103  40929  fourierdlem104  40930  vonioolem1  41400  fmtnoprmfac1  41987  fmtnoprmfac2lem1  41988  lighneallem2  42033  lighneallem4a  42035  gboge9  42162  bgoldbnnsum3prm  42202  nnolog2flm1  42894
  Copyright terms: Public domain W3C validator