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

Theorem eluz2 10387
Description: Membership in a set of upper integers. We use the fact that a function's value (under our function value definition) is empty outside of its domain to show  M  e.  ZZ. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
Assertion
Ref Expression
eluz2  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) )

Proof of Theorem eluz2
StepHypRef Expression
1 eluzel2 10386 . 2  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
2 simp1 956 . 2  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N )  ->  M  e.  ZZ )
3 eluz1 10385 . . . 4  |-  ( M  e.  ZZ  ->  ( N  e.  ( ZZ>= `  M )  <->  ( N  e.  ZZ  /\  M  <_  N ) ) )
4 ibar 490 . . . 4  |-  ( M  e.  ZZ  ->  (
( N  e.  ZZ  /\  M  <_  N )  <->  ( M  e.  ZZ  /\  ( N  e.  ZZ  /\  M  <_  N )
) ) )
53, 4bitrd 244 . . 3  |-  ( M  e.  ZZ  ->  ( N  e.  ( ZZ>= `  M )  <->  ( M  e.  ZZ  /\  ( N  e.  ZZ  /\  M  <_  N ) ) ) )
6 3anass 939 . . 3  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N )  <->  ( M  e.  ZZ  /\  ( N  e.  ZZ  /\  M  <_  N ) ) )
75, 6syl6bbr 254 . 2  |-  ( M  e.  ZZ  ->  ( N  e.  ( ZZ>= `  M )  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) ) )
81, 2, 7pm5.21nii 342 1  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    /\ w3a 935    e. wcel 1715   class class class wbr 4125   ` cfv 5358    <_ cle 9015   ZZcz 10175   ZZ>=cuz 10381
This theorem is referenced by:  eluzelz  10389  eluzle  10391  uztrn  10395  eluzp1p1  10404  uzm1  10409  uznn0sub  10410  raluz2  10419  rexuz2  10421  peano2uz  10423  uzind4  10427  zsupss  10458  elfzuzb  10945  4fvwrd4  11011  elfzo2  11033  elfzouz2  11043  fzossrbm1  11054  fzostep1  11084  fzind2  11085  flword2  11107  uzsup  11131  fzsdom2  11580  ccatval1  11632  rexuzre  12043  limsupgre  12162  rlimclim1  12226  rlimclim  12227  climrlim2  12228  isercolllem1  12345  isercoll  12348  climcndslem1  12516  bitsmod  12835  smueqlem  12889  vdwlem9  13244  strlemor1  13443  strleun  13446  fislw  15146  efgsp1  15256  efgredleme  15262  lt6abl  15391  ablfac1eu  15518  znidomb  16732  dvfsumlem1  19588  dvfsumlem3  19590  plyaddlem1  19810  coeidlem  19834  ppisval  20564  chtdif  20619  ppidif  20624  ppiublem1  20664  ppiub  20666  chtub  20674  lgsdilem2  20793  lgsquadlem1  20816  lgsquadlem3  20818  chebbnd1lem1  20841  chebbnd1lem2  20842  chebbnd1lem3  20843  dchrisumlem2  20862  dchrvmasumiflem1  20873  mulog2sumlem2  20907  logdivbnd  20928  pntlemg  20970  pntlemq  20973  pntlemf  20977  eupath2lem3  21212  ssnnssfz  23670  ballotlemsdom  24338  ballotlemsel1i  24339  ballotlemfrceq  24355  erdszelem8  24453  climuzcnv  24676  rpdmgamma  24918  axlowdim  25416  fdc  26047  eldioph2lem1  26430  hbt  26925  fmul01lt1lem2  27306  stoweidlem11  27351  stoweidlem26  27366  wallispilem4  27408  4cycl4v4e  27801  4cycl4dv4e  27803
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316  ax-cnex 8940  ax-resscn 8941
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 936  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-rab 2637  df-v 2875  df-sbc 3078  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-pw 3716  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-opab 4180  df-mpt 4181  df-id 4412  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-iota 5322  df-fun 5360  df-fn 5361  df-f 5362  df-fv 5366  df-ov 5984  df-neg 9187  df-z 10176  df-uz 10382
  Copyright terms: Public domain W3C validator