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

Theorem eluz2 11116
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 . (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
Assertion
Ref Expression
eluz2

Proof of Theorem eluz2
StepHypRef Expression
1 eluzel2 11115 . 2
2 simp1 996 . 2
3 eluz1 11114 . . . 4
4 ibar 504 . . . 4
53, 4bitrd 253 . . 3
6 3anass 977 . . 3
75, 6syl6bbr 263 . 2
81, 2, 7pm5.21nii 353 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  /\w3a 973  e.wcel 1818   class class class wbr 4452  `cfv 5593   cle 9650   cz 10889   cuz 11110
This theorem is referenced by:  eluzuzle  11118  eluzelz  11119  eluzle  11122  uztrn  11126  eluzp1p1  11135  uzm1  11140  uznn0sub  11141  uz3m2nn  11152  1eluzge0  11153  2eluzge0OLD  11155  2eluzge1  11156  raluz2  11159  rexuz2  11161  peano2uz  11163  nn0pzuz  11167  uzind4  11168  zsupss  11200  nn01to3  11204  nn0ge2m1nnALT  11205  elfzuzb  11711  uzsubsubfz  11736  ige2m1fz  11797  elfz0addOLD  11805  4fvwrd4  11822  elfzo2  11832  elfzouz2  11842  fzossrbm1  11854  fzossfzop1  11893  ssfzo12bi  11907  elfzonelfzo  11912  elfzomelpfzo  11914  fzosplitprm1  11919  fzostep1  11922  fzind2  11924  flword2  11949  uzsup  11990  modaddmodup  12050  fzsdom2  12486  ccatval1  12595  swrdtrcfv0  12669  swrdtrcfvl  12675  swrdccatin12lem2a  12710  cshwidxmod  12774  rexuzre  13185  limsupgre  13304  rlimclim1  13368  rlimclim  13369  climrlim2  13370  isercolllem1  13487  isercoll  13490  climcndslem1  13661  bitsmod  14086  smueqlem  14140  prmgt1  14236  prmn2uzge3  14237  modprm0  14330  vdwlem9  14507  strlemor1  14724  strleun  14727  fislw  16645  efgsp1  16755  efgredleme  16761  lt6abl  16897  telgsumfzs  17018  ablfac1eu  17124  znidomb  18600  chfacfscmul0  19359  chfacfscmulfsupp  19360  chfacfpmmul0  19363  chfacfpmmulfsupp  19364  dvfsumlem1  22427  dvfsumlem3  22429  plyaddlem1  22610  coeidlem  22634  ppisval  23377  chtdif  23432  ppidif  23437  ppiublem1  23477  ppiub  23479  chtub  23487  lgsdilem2  23606  lgsquadlem1  23629  lgsquadlem3  23631  chebbnd1lem1  23654  chebbnd1lem2  23655  chebbnd1lem3  23656  dchrisumlem2  23675  dchrvmasumiflem1  23686  mulog2sumlem2  23720  logdivbnd  23741  pntlemg  23783  pntlemq  23786  pntlemf  23790  axlowdim  24264  4cycl4v4e  24666  4cycl4dv4e  24668  wwlknred  24723  wwlkm1edg  24735  clwlkisclwwlklem2fv1  24782  clwlkisclwwlklem1  24787  clwwlkf  24794  clwwlkext2edg  24802  wwlksubclwwlk  24804  clwwisshclwwlem  24806  usg2cwwkdifex  24821  clwlkfclwwlk  24844  eupath2lem3  24979  extwwlkfablem2  25078  numclwwlkovf2ex  25086  numclwlk1lem2f1  25094  frgrareggt1  25116  frgrareg  25117  frgraregord013  25118  ssnnssfz  27597  ballotlemsdom  28450  ballotlemsel1i  28451  ballotlemfrceq  28467  eluzmn  28491  signstfvc  28531  signstfveq0  28534  erdszelem8  28642  climuzcnv  29037  fallfacval4  29165  fdc  30238  eldioph2lem1  30693  hbt  31079  monoords  31496  fzdifsuc2  31512  fmul01lt1lem2  31579  sumnnodd  31636  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnmul  31740  dvnprodlem2  31744  itgspltprt  31778  stoweidlem11  31793  stoweidlem26  31808  wallispilem4  31850  fourierdlem12  31901  fourierdlem20  31909  fourierdlem41  31930  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem54  31943  fourierdlem79  31968  fourierdlem102  31991  fourierdlem111  32000  fourierdlem114  32003  etransclem23  32040  etransclem48  32065  eluzge0nn0  32329  ssfz12  32330  elfzlble  32336  el2fzo  32339  fzoopth  32340  cznnring  32764  ssnn0ssfz  32938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-cnex 9569  ax-resscn 9570
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-fv 5601  df-ov 6299  df-neg 9831  df-z 10890  df-uz 11111
  Copyright terms: Public domain W3C validator