MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eluz Structured version   Unicode version

Theorem eluz 11084
Description: Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005.)
Assertion
Ref Expression
eluz  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  M )  <->  M  <_  N ) )

Proof of Theorem eluz
StepHypRef Expression
1 eluz1 11075 . 2  |-  ( M  e.  ZZ  ->  ( N  e.  ( ZZ>= `  M )  <->  ( N  e.  ZZ  /\  M  <_  N ) ) )
21baibd 902 1  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  M )  <->  M  <_  N ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    e. wcel 1762   class class class wbr 4440   ` cfv 5579    <_ cle 9618   ZZcz 10853   ZZ>=cuz 11071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679  ax-cnex 9537  ax-resscn 9538
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-iota 5542  df-fun 5581  df-fv 5587  df-ov 6278  df-neg 9797  df-z 10854  df-uz 11072
This theorem is referenced by:  uzneg  11089  uztric  11092  uzwo3  11166  fzn  11691  fzsplit2  11699  fznn  11736  uzsplit  11739  elfz2nn0  11757  fzouzsplit  11817  faclbnd  12323  bcval5  12351  fz1isolem  12463  seqcoll  12465  rexuzre  13134  caurcvg  13448  caucvg  13450  summolem2a  13486  fsum0diaglem  13540  climcnds  13615  mertenslem1  13645  ruclem10  13822  isprm3  14074  eulerthlem2  14160  pcpremul  14215  pcdvdsb  14240  pcadd  14256  pcfac  14266  pcbc  14267  prmunb  14280  prmreclem5  14286  vdwnnlem3  14363  lt6abl  16681  ovolunlem1a  21635  mbflimsup  21801  plyco0  22317  plyeq0lem  22335  aannenlem1  22451  aaliou3lem2  22466  aaliou3lem8  22468  chtublem  23207  bcmax  23274  bpos1lem  23278  bposlem1  23280  axlowdimlem16  23929  axlowdimlem17  23930  axlowdim  23933  fzsplit3  27117  ballotlem2  27917  ballotlemfc0  27921  ballotlemfcc  27922  ballotlemimin  27934  elfzm12  28366  ntrivcvgmullem  28462  prodmolem2a  28493  mblfinlem2  29480  incsequz  29695  incsequz2  29696  nacsfix  30099  ellz1  30155  eluzrabdioph  30194  monotuz  30332  expdiophlem1  30420  fzisoeu  30896  fmul01  30949  climsuselem1  30968  climsuse  30969  iblspltprt  31110  itgspltprt  31116  wallispilem5  31188  stirlinglem8  31200  dirkertrigeqlem1  31217  fourierdlem12  31238  ssfz12  31618  extwwlkfablem2  31797
  Copyright terms: Public domain W3C validator