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

Theorem eluz2 12238
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 12237 . 2 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
2 simp1 1128 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁) → 𝑀 ∈ ℤ)
3 eluz1 12236 . . . 4 (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀𝑁)))
4 ibar 529 . . . 4 (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀𝑁))))
53, 4bitrd 280 . . 3 (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀𝑁))))
6 3anass 1087 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀𝑁)))
75, 6syl6bbr 290 . 2 (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁)))
81, 2, 7pm5.21nii 380 1 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  w3a 1079  wcel 2105   class class class wbr 5058  cfv 6349  cle 10665  cz 11970  cuz 12232
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-cnex 10582  ax-resscn 10583
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-fv 6357  df-ov 7148  df-neg 10862  df-z 11971  df-uz 12233
This theorem is referenced by:  eluzmn  12239  eluzuzle  12241  eluzelz  12242  eluzle  12245  uztrn  12250  eluzp1p1  12259  subeluzsub  12264  uzm1  12265  uznn0sub  12266  uz3m2nn  12280  1eluzge0  12281  2eluzge1  12283  raluz2  12286  rexuz2  12288  peano2uz  12290  nn0pzuz  12294  uzind4  12295  uzinfi  12317  zsupss  12326  nn01to3  12330  nn0ge2m1nnALT  12331  elfzuzb  12892  uzsubsubfz  12919  ssfzunsnext  12942  ssfzunsn  12943  ige2m1fz  12987  4fvwrd4  13017  elfzo2  13031  elfzouz2  13042  fzossrbm1  13056  fzossfzop1  13105  ssfzo12bi  13122  elfzonelfzo  13129  elfzomelpfzo  13131  fzosplitprm1  13137  fzostep1  13143  fzind2  13145  flword2  13173  fldiv4p1lem1div2  13195  uzsup  13221  modaddmodup  13292  fzsdom2  13779  swrdsbslen  14016  swrdspsleq  14017  pfxtrcfv0  14046  pfxtrcfvl  14049  pfxccatin12lem2a  14079  cshwidxmod  14155  rexuzre  14702  limsupgre  14828  rlimclim1  14892  rlimclim  14893  climrlim2  14894  isercolllem1  15011  isercoll  15014  climcndslem1  15194  fallfacval4  15387  oddge22np1  15688  nn0o  15724  bitsmod  15775  smueqlem  15829  dvdsnprmd  16024  2mulprm  16027  oddprmgt2  16033  oddprmge3  16034  ge2nprmge4  16035  modprm0  16132  prm23ge5  16142  vdwlem9  16315  prmgaplem3  16379  prmgaplem5  16381  prmgaplem6  16382  prmgaplem7  16383  setsstruct  16513  strleun  16581  fislw  18681  efgsp1  18794  efgredleme  18800  lt6abl  18946  telgsumfzs  19040  ablfac1eu  19126  znidomb  20638  chfacfscmul0  21396  chfacfscmulfsupp  21397  chfacfpmmul0  21400  chfacfpmmulfsupp  21401  dvfsumlem1  24552  dvfsumlem3  24554  plyaddlem1  24732  coeidlem  24756  2logb9irr  25300  ppisval  25609  chtdif  25663  ppidif  25668  ppiublem1  25706  ppiub  25708  chtub  25716  lgsdilem2  25837  gausslemma2dlem2  25871  gausslemma2dlem4  25873  gausslemma2dlem5  25875  gausslemma2dlem6  25876  lgsquadlem1  25884  lgsquadlem3  25886  2lgslem1  25898  chebbnd1lem1  25973  chebbnd1lem2  25974  chebbnd1lem3  25975  dchrisumlem2  25994  dchrvmasumiflem1  26005  mulog2sumlem2  26039  logdivbnd  26060  pntlemg  26102  pntlemq  26105  pntlemf  26109  axlowdim  26675  pthdlem1  27475  crctcshwlkn0lem3  27518  crctcshwlkn0lem4  27519  crctcshwlkn0lem5  27520  crctcshwlkn0lem6  27521  wwlksm1edg  27587  wwlksnred  27598  clwlkclwwlklem2fv1  27701  clwlkclwwlklem2  27706  clwwisshclwwslem  27720  clwwlkinwwlk  27746  clwwlkf  27754  clwwlkext2edg  27763  wwlksubclwwlk  27765  frgrreggt1  28100  ssnnssfz  30437  cycpmco2lem6  30701  ballotlemsdom  31669  ballotlemsel1i  31670  ballotlemfrceq  31686  signstfvc  31744  signstfveq0  31747  prodfzo03  31774  erdszelem8  32343  climuzcnv  32812  poimirlem6  34780  fdc  34903  eldioph2lem1  39237  hbt  39610  ssinc  41233  ssdec  41234  monoords  41444  fzdifsuc2  41457  eluzd  41562  fmul01lt1lem2  41746  sumnnodd  41791  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvnmul  42108  dvnprodlem2  42112  itgspltprt  42144  stoweidlem11  42177  stoweidlem26  42192  wallispilem4  42234  fourierdlem12  42285  fourierdlem20  42293  fourierdlem41  42314  fourierdlem48  42320  fourierdlem49  42321  fourierdlem50  42322  fourierdlem54  42326  fourierdlem79  42351  fourierdlem102  42374  fourierdlem111  42383  fourierdlem114  42386  etransclem23  42423  etransclem48  42448  caratheodorylem1  42689  smfmullem4  42950  eluzge0nn0  43393  ssfz12  43395  elfzlble  43401  fzopredsuc  43404  fzoopth  43408  iccpartipre  43428  iccpartiltu  43429  iccpartgt  43434  fmtnoge3  43539  odz2prm2pw  43572  fmtnoprmfac2lem1  43575  fmtno4prmfac  43581  31prm  43607  lighneallem4b  43621  341fppr2  43746  9fppr8  43749  fpprel2  43753  nfermltl8rev  43754  nfermltl2rev  43755  gbegt5  43773  gbowgt5  43774  sbgoldbm  43796  mogoldbb  43797  sbgoldbo  43799  nnsum3primesle9  43806  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  evengpop3  43810  evengpoap3  43811  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  wtgoldbnnsum4prm  43814  bgoldbnnsum3prm  43816  bgoldbtbndlem3  43819  tgblthelfgott  43827  cznnring  44125  ssnn0ssfz  44295  elfzolborelfzop1  44472  m1modmmod  44479  rege1logbzge0  44517  fllog2  44526  nnolog2flm1  44548  dignn0ldlem  44560
  Copyright terms: Public domain W3C validator