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

Theorem eluz1i 11101
Description: Membership in an upper set of integers. (Contributed by NM, 5-Sep-2005.)
Hypothesis
Ref Expression
eluz.1  |-  M  e.  ZZ
Assertion
Ref Expression
eluz1i  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( N  e.  ZZ  /\  M  <_  N ) )

Proof of Theorem eluz1i
StepHypRef Expression
1 eluz.1 . 2  |-  M  e.  ZZ
2 eluz1 11098 . 2  |-  ( M  e.  ZZ  ->  ( N  e.  ( ZZ>= `  M )  <->  ( N  e.  ZZ  /\  M  <_  N ) ) )
31, 2ax-mp 5 1  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( N  e.  ZZ  /\  M  <_  N ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    e. wcel 1767   class class class wbr 4453   ` cfv 5594    <_ cle 9641   ZZcz 10876   ZZ>=cuz 11094
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pr 4692  ax-cnex 9560  ax-resscn 9561
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-iota 5557  df-fun 5596  df-fv 5602  df-ov 6298  df-neg 9820  df-z 10877  df-uz 11095
This theorem is referenced by:  eluzaddi  11120  eluzsubi  11121  eluz2b1  11165  injresinj  11906  faclbnd4lem1  12351  climcndslem1  13641  ef01bndlem  13797  sin01bnd  13798  cos01bnd  13799  sin01gt0  13803  dvradcnv  22683  bposlem3  23427  bposlem4  23428  bposlem5  23429  bposlem9  23433  axlowdimlem16  24083  axlowdimlem17  24084  usgraexvlem  24218  rnlogblem  27840  ballotlem2  28252  ballotlemfc0  28256  ballotlemfcc  28257  nn0prpwlem  30067  jm2.20nn  30867  stoweidlem17  31640  wallispilem4  31691
  Copyright terms: Public domain W3C validator