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

Theorem eluz2 12776
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 12775 . 2 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
2 simp1 1137 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁) → 𝑀 ∈ ℤ)
3 eluz1 12774 . . . 4 (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀𝑁)))
4 ibar 530 . . . 4 (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀𝑁))))
53, 4bitrd 279 . . 3 (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀𝑁))))
6 3anass 1096 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀𝑁)))
75, 6bitr4di 289 . 2 (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁)))
81, 2, 7pm5.21nii 380 1 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  w3a 1088  wcel 2107   class class class wbr 5110  cfv 6501  cle 11197  cz 12506  cuz 12770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-cnex 11114  ax-resscn 11115
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-fv 6509  df-ov 7365  df-neg 11395  df-z 12507  df-uz 12771
This theorem is referenced by:  eluzmn  12777  eluzuzle  12779  eluzelz  12780  eluzle  12783  uztrn  12788  eluzp1p1  12798  eluzadd  12799  eluzsub  12800  subeluzsub  12807  uzm1  12808  uznn0sub  12809  uz3m2nn  12823  1eluzge0  12824  2eluzge1  12826  raluz2  12829  rexuz2  12831  peano2uz  12833  nn0pzuz  12837  uzind4  12838  uzinfi  12860  zsupss  12869  nn01to3  12873  nn0ge2m1nnALT  12874  elfzuzb  13442  uzsubsubfz  13470  ssfzunsn  13494  ige2m1fz  13538  4fvwrd4  13568  elfzo2  13582  elfzouz2  13594  fzossrbm1  13608  fzossfzop1  13657  ssfzo12bi  13674  elfzonelfzo  13681  elfzomelpfzo  13683  fzosplitprm1  13689  fzostep1  13695  fzind2  13697  flword2  13725  fldiv4p1lem1div2  13747  uzsup  13775  modaddmodup  13846  fzsdom2  14335  swrdsbslen  14559  swrdspsleq  14560  pfxtrcfv0  14589  pfxtrcfvl  14592  pfxccatin12lem2a  14622  cshwidxmod  14698  rexuzre  15244  limsupgre  15370  rlimclim1  15434  rlimclim  15435  climrlim2  15436  isercolllem1  15556  isercoll  15559  climcndslem1  15741  fallfacval4  15933  oddge22np1  16238  nn0o  16272  bitsmod  16323  smueqlem  16377  dvdsnprmd  16573  2mulprm  16576  oddprmgt2  16582  oddprmge3  16583  ge2nprmge4  16584  modprm0  16684  prm23ge5  16694  vdwlem9  16868  prmgaplem3  16932  prmgaplem5  16934  prmgaplem6  16935  prmgaplem7  16936  strleun  17036  setsstruct  17055  fislw  19414  efgsp1  19526  efgredleme  19532  lt6abl  19679  telgsumfzs  19773  ablfac1eu  19859  znidomb  20984  chfacfscmul0  22223  chfacfscmulfsupp  22224  chfacfpmmul0  22227  chfacfpmmulfsupp  22228  dvfsumlem1  25406  dvfsumlem3  25408  plyaddlem1  25590  coeidlem  25614  2logb9irr  26161  ppisval  26469  chtdif  26523  ppidif  26528  ppiublem1  26566  ppiub  26568  chtub  26576  lgsdilem2  26697  gausslemma2dlem2  26731  gausslemma2dlem4  26733  gausslemma2dlem5  26735  gausslemma2dlem6  26736  lgsquadlem1  26744  lgsquadlem3  26746  2lgslem1  26758  chebbnd1lem1  26833  chebbnd1lem2  26834  chebbnd1lem3  26835  dchrisumlem2  26854  dchrvmasumiflem1  26865  mulog2sumlem2  26899  logdivbnd  26920  pntlemg  26962  pntlemq  26965  pntlemf  26969  axlowdim  27952  pthdlem1  28756  crctcshwlkn0lem3  28799  crctcshwlkn0lem4  28800  crctcshwlkn0lem5  28801  crctcshwlkn0lem6  28802  wwlksm1edg  28868  wwlksnred  28879  clwlkclwwlklem2fv1  28981  clwlkclwwlklem2  28986  clwwisshclwwslem  29000  clwwlkinwwlk  29026  clwwlkf  29033  clwwlkext2edg  29042  wwlksubclwwlk  29044  frgrreggt1  29379  ssnnssfz  31732  cycpmco2lem6  32022  ballotlemsdom  33151  ballotlemsel1i  33152  ballotlemfrceq  33168  signstfvc  33226  signstfveq0  33229  prodfzo03  33256  erdszelem8  33832  climuzcnv  34299  poimirlem6  36113  fdc  36233  sticksstones12  40595  eldioph2lem1  41112  hbt  41486  ssinc  43371  ssdec  43372  monoords  43605  fzdifsuc2  43618  eluzd  43718  fmul01lt1lem2  43900  sumnnodd  43945  ioodvbdlimc1lem2  44247  ioodvbdlimc2lem  44249  dvnmul  44258  dvnprodlem2  44262  itgspltprt  44294  stoweidlem11  44326  stoweidlem26  44341  wallispilem4  44383  fourierdlem12  44434  fourierdlem20  44442  fourierdlem41  44463  fourierdlem48  44469  fourierdlem49  44470  fourierdlem50  44471  fourierdlem54  44475  fourierdlem79  44500  fourierdlem102  44523  fourierdlem111  44532  fourierdlem114  44535  etransclem23  44572  etransclem48  44597  caratheodorylem1  44841  smfmullem4  45109  eluzge0nn0  45618  ssfz12  45620  elfzlble  45626  fzopredsuc  45629  fzoopth  45633  iccpartipre  45687  iccpartiltu  45688  iccpartgt  45693  fmtnoge3  45796  odz2prm2pw  45829  fmtnoprmfac2lem1  45832  fmtno4prmfac  45838  31prm  45863  lighneallem4b  45875  341fppr2  46000  9fppr8  46003  fpprel2  46007  nfermltl8rev  46008  nfermltl2rev  46009  gbegt5  46027  gbowgt5  46028  sbgoldbm  46050  mogoldbb  46051  sbgoldbo  46053  nnsum3primesle9  46060  nnsum4primesodd  46062  nnsum4primesoddALTV  46063  evengpop3  46064  evengpoap3  46065  nnsum4primeseven  46066  nnsum4primesevenALTV  46067  wtgoldbnnsum4prm  46068  bgoldbnnsum3prm  46070  bgoldbtbndlem3  46073  tgblthelfgott  46081  cznnring  46328  ssnn0ssfz  46499  elfzolborelfzop1  46674  m1modmmod  46681  rege1logbzge0  46719  fllog2  46728  nnolog2flm1  46750  dignn0ldlem  46762
  Copyright terms: Public domain W3C validator