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

Theorem eluz 11095
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 11086 . 2  |-  ( M  e.  ZZ  ->  ( N  e.  ( ZZ>= `  M )  <->  ( N  e.  ZZ  /\  M  <_  N ) ) )
21baibd 907 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 367    e. wcel 1823   class class class wbr 4439   ` cfv 5570    <_ cle 9618   ZZcz 10860   ZZ>=cuz 11082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676  ax-cnex 9537  ax-resscn 9538
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-iota 5534  df-fun 5572  df-fv 5578  df-ov 6273  df-neg 9799  df-z 10861  df-uz 11083
This theorem is referenced by:  uzneg  11100  uztric  11103  uzwo3  11178  fzn  11705  fzsplit2  11713  fznn  11751  uzsplit  11754  elfz2nn0  11773  fzouzsplit  11837  faclbnd  12350  bcval5  12378  fz1isolem  12494  seqcoll  12496  rexuzre  13267  caurcvg  13581  caucvg  13583  summolem2a  13619  fsum0diaglem  13673  climcnds  13745  mertenslem1  13775  ntrivcvgmullem  13792  prodmolem2a  13823  ruclem10  14056  eulerthlem2  14396  pcpremul  14451  pcdvdsb  14476  pcadd  14492  pcfac  14502  pcbc  14503  prmunb  14516  prmreclem5  14522  vdwnnlem3  14599  lt6abl  17096  ovolunlem1a  22073  mbflimsup  22239  plyco0  22755  plyeq0lem  22773  aannenlem1  22890  aaliou3lem2  22905  aaliou3lem8  22907  chtublem  23684  bcmax  23751  bpos1lem  23755  bposlem1  23757  axlowdimlem16  24462  extwwlkfablem2  25280  fzsplit3  27833  ballotlem2  28691  ballotlemimin  28708  elfzm12  29305  mblfinlem2  30292  incsequz  30481  incsequz2  30482  nacsfix  30884  ellz1  30939  eluzrabdioph  30979  monotuz  31116  expdiophlem1  31202  nznngen  31462  fzisoeu  31739  fmul01  31813  climsuselem1  31852  climsuse  31853  iblspltprt  32011  itgspltprt  32017  wallispilem5  32090  stirlinglem8  32102  dirkertrigeqlem1  32119  fourierdlem12  32140  ssfz12  32704
  Copyright terms: Public domain W3C validator