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

Theorem eluz2 10879
Description: Membership in an upper set of 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 10878 . 2  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
2 simp1 988 . 2  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N )  ->  M  e.  ZZ )
3 eluz1 10877 . . . 4  |-  ( M  e.  ZZ  ->  ( N  e.  ( ZZ>= `  M )  <->  ( N  e.  ZZ  /\  M  <_  N ) ) )
4 ibar 504 . . . 4  |-  ( M  e.  ZZ  ->  (
( N  e.  ZZ  /\  M  <_  N )  <->  ( M  e.  ZZ  /\  ( N  e.  ZZ  /\  M  <_  N )
) ) )
53, 4bitrd 253 . . 3  |-  ( M  e.  ZZ  ->  ( N  e.  ( ZZ>= `  M )  <->  ( M  e.  ZZ  /\  ( N  e.  ZZ  /\  M  <_  N ) ) ) )
6 3anass 969 . . 3  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N )  <->  ( M  e.  ZZ  /\  ( N  e.  ZZ  /\  M  <_  N ) ) )
75, 6syl6bbr 263 . 2  |-  ( M  e.  ZZ  ->  ( N  e.  ( ZZ>= `  M )  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) ) )
81, 2, 7pm5.21nii 353 1  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    /\ w3a 965    e. wcel 1756   class class class wbr 4304   ` cfv 5430    <_ cle 9431   ZZcz 10658   ZZ>=cuz 10873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-cnex 9350  ax-resscn 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-sbc 3199  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-opab 4363  df-mpt 4364  df-id 4648  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5393  df-fun 5432  df-fn 5433  df-f 5434  df-fv 5438  df-ov 6106  df-neg 9610  df-z 10659  df-uz 10874
This theorem is referenced by:  uzletr  10881  eluzelz  10882  eluzle  10885  uztrn  10889  eluzp1p1  10898  uzm1  10903  uznn0sub  10904  1eluzge0  10911  2eluzge0  10912  2eluzge1  10913  raluz2  10916  rexuz2  10918  peano2uz  10920  uzind4  10924  zsupss  10956  elfzuzb  11459  uzsubsubfz  11483  elfzelfzadd  11520  4fvwrd4  11545  elfzo2  11568  elfzouz2  11578  fzossrbm1  11590  fzossfzop1  11622  ssfzo12bi  11634  elfzonelfzo  11639  elfzomelpfzo  11641  fzostep1  11647  fzind2  11649  flword2  11673  uzsup  11714  modaddmodup  11774  fzsdom2  12201  ccatval1  12288  swrdtrcfv0  12350  swrdtrcfvl  12356  swrdccatin12lem2a  12388  cshwidxmod  12452  rexuzre  12852  limsupgre  12971  rlimclim1  13035  rlimclim  13036  climrlim2  13037  isercolllem1  13154  isercoll  13157  climcndslem1  13324  bitsmod  13644  smueqlem  13698  prmgt1  13794  modprm0  13885  vdwlem9  14062  strlemor1  14277  strleun  14280  fislw  16136  efgsp1  16246  efgredleme  16252  lt6abl  16383  ablfac1eu  16586  znidomb  18006  dvfsumlem1  21510  dvfsumlem3  21512  plyaddlem1  21693  coeidlem  21717  ppisval  22453  chtdif  22508  ppidif  22513  ppiublem1  22553  ppiub  22555  chtub  22563  lgsdilem2  22682  lgsquadlem1  22705  lgsquadlem3  22707  chebbnd1lem1  22730  chebbnd1lem2  22731  chebbnd1lem3  22732  dchrisumlem2  22751  dchrvmasumiflem1  22762  mulog2sumlem2  22796  logdivbnd  22817  pntlemg  22859  pntlemq  22862  pntlemf  22866  axlowdim  23219  4cycl4v4e  23564  4cycl4dv4e  23566  eupath2lem3  23612  ssnnssfz  26088  ballotlemsdom  26906  ballotlemsel1i  26907  ballotlemfrceq  26923  eluzmn  26947  signstfvc  26987  signstfveq0  26990  erdszelem8  27098  climuzcnv  27328  fallfacval4  27558  fdc  28653  eldioph2lem1  29110  hbt  29498  fmul01lt1lem2  29778  stoweidlem11  29818  stoweidlem26  29833  wallispilem4  29875  nn0ge2m1nn  30196  nn01to3  30199  eluzge0nn0  30201  uzuzle  30202  uz3m2nn  30207  nn0pzuz  30208  ssfz12  30209  ige2m1fz  30218  elfzlble  30220  el2fzo  30224  fzoopth  30225  elfzom1elfzo  30229  fzosplitprm1  30236  prmn2uzge3  30261  wwlknred  30367  wwlkm1edg  30379  clwlkisclwwlklem2fv1  30456  clwlkisclwwlklem1  30461  clwwlkf  30468  clwwlkext2edg  30476  wwlksubclwwlk  30478  clwwisshclwwlem  30482  usg2cwwkdifex  30507  clwlkfclwwlk  30529  extwwlkfablem2  30683  numclwwlkovf2ex  30691  numclwlk1lem2f1  30699  frgrareggt1  30721  frgrareg  30722  frgraregord013  30723  ssnn0ssfz  30753  telescfzgsum  30822
  Copyright terms: Public domain W3C validator