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

Theorem eluz 10975
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 10966 . 2  |-  ( M  e.  ZZ  ->  ( N  e.  ( ZZ>= `  M )  <->  ( N  e.  ZZ  /\  M  <_  N ) ) )
21baibd 900 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 1758   class class class wbr 4390   ` cfv 5516    <_ cle 9520   ZZcz 10747   ZZ>=cuz 10962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pr 4629  ax-cnex 9439  ax-resscn 9440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-iota 5479  df-fun 5518  df-fv 5524  df-ov 6193  df-neg 9699  df-z 10748  df-uz 10963
This theorem is referenced by:  uzneg  10980  uztric  10983  uzwo3  11049  fzn  11567  fzsplit2  11575  elfz2nn0  11581  fznn  11627  uzsplit  11631  fzouzsplit  11685  faclbnd  12167  bcval5  12195  fz1isolem  12316  seqcoll  12318  rexuzre  12942  caurcvg  13256  caucvg  13258  summolem2a  13294  fsum0diaglem  13345  climcnds  13416  mertenslem1  13446  ruclem10  13623  isprm3  13874  eulerthlem2  13959  pcpremul  14012  pcdvdsb  14037  pcadd  14053  pcfac  14063  pcbc  14064  prmunb  14077  prmreclem5  14083  vdwnnlem3  14160  lt6abl  16475  ovolunlem1a  21095  mbflimsup  21260  plyco0  21776  plyeq0lem  21794  aannenlem1  21910  aaliou3lem2  21925  aaliou3lem8  21927  chtublem  22666  bcmax  22733  bpos1lem  22737  bposlem1  22739  axlowdimlem16  23338  axlowdimlem17  23339  axlowdim  23342  fzsplit3  26212  ballotlem2  27005  ballotlemfc0  27009  ballotlemfcc  27010  ballotlemimin  27022  elfzm12  27454  ntrivcvgmullem  27550  prodmolem2a  27581  mblfinlem2  28567  incsequz  28782  incsequz2  28783  nacsfix  29186  ellz1  29243  eluzrabdioph  29282  monotuz  29420  expdiophlem1  29508  fmul01  29899  climsuselem1  29918  climsuse  29919  wallispilem5  30002  stirlinglem8  30014  ssfz12  30335  extwwlkfablem2  30809
  Copyright terms: Public domain W3C validator