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

Theorem eluzle 11528
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 11521 . 2 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
21simp3bi 1070 1 (𝑁 ∈ (ℤ𝑀) → 𝑀𝑁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1975   class class class wbr 4573  cfv 5786  cle 9927  cz 11206  cuz 11515
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-cnex 9844  ax-resscn 9845
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-sbc 3398  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-opab 4634  df-mpt 4635  df-id 4939  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-fv 5794  df-ov 6526  df-neg 10116  df-z 11207  df-uz 11516
This theorem is referenced by:  uztrn  11532  uzneg  11534  uzss  11536  uz11  11538  eluzp1l  11540  uzm1  11546  uzin  11548  uzind4  11574  uzwo  11579  uzsupss  11608  zgt1rpn0n1  11699  elfz5  12156  elfzle1  12166  elfzle2  12167  elfzle3  12169  ssfzunsn  12208  uzsplit  12232  uzdisj  12233  uznfz  12243  elfz2nn0  12251  uzsubfz0  12267  nn0disj  12275  fzouzdisj  12324  fldiv4lem1div2uz2  12450  m1modge3gt1  12530  expmulnbnd  12809  seqcoll  13053  swrdlen2  13239  swrdfv2  13240  rexuzre  13882  rlimclim1  14066  isercoll  14188  iseralt  14205  o1fsum  14328  mertenslem1  14397  fprodeq0  14486  efcllem  14589  rpnnen2lem9  14732  smuval2  14984  smupvallem  14985  isprm7  15200  hashdvds  15260  pcmpt2  15377  pcfaclem  15382  pcfac  15383  vdwlem6  15470  ramtlecl  15484  prmlem1  15594  prmlem2  15607  znfld  19669  lmnn  22783  mbflimsup  23152  mbfi1fseqlem6  23206  dvfsumge  23502  plyco0  23665  coeeulem  23697  radcnvlem2  23885  log2tlbnd  24385  lgamgulmlem4  24471  lgamcvg2  24494  chtub  24650  chpval2  24656  chpchtsum  24657  bcmax  24716  bpos1lem  24720  bpos1  24721  bposlem3  24724  bposlem4  24725  bposlem5  24726  bposlem6  24727  lgslem1  24735  lgsdirprm  24769  lgseisen  24817  m1lgs  24826  dchrisumlema  24890  dchrisumlem2  24892  dchrisum0lem1  24918  axlowdimlem3  25538  axlowdimlem6  25541  axlowdimlem7  25542  axlowdimlem16  25551  axlowdimlem17  25552  constr3trllem3  25942  minvecolem3  26918  minvecolem4  26922  subfacval3  30227  climuzcnv  30621  knoppndvlem6  31480  poimirlem29  32407  fdc  32510  jm2.24nn  36343  jm2.23  36380  expdiophlem1  36405  hashnzfz2  37341  bccbc  37365  binomcxplemnn0  37369  ssinc  38091  ssdec  38092  fzdifsuc2  38266  uzfissfz  38283  iuneqfzuzlem  38291  ssuzfz  38306  fmul01lt1lem1  38451  climsuselem1  38474  climsuse  38475  ioodvbdlimc1lem2  38622  ioodvbdlimc2lem  38624  iblspltprt  38665  itgspltprt  38671  stoweidlem11  38704  stirlinglem11  38777  fourierdlem79  38878  fourierdlem103  38902  fourierdlem104  38903  vonioolem1  39371  fmtnoprmfac1  39816  fmtnoprmfac2lem1  39817  lighneallem2  39862  lighneallem4a  39864  gboage9  39987  bgoldbnnsum3prm  40021  nnolog2flm1  42180
  Copyright terms: Public domain W3C validator