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

Theorem eluz2 11885
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 11884 . 2 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
2 simp1 1131 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁) → 𝑀 ∈ ℤ)
3 eluz1 11883 . . . 4 (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀𝑁)))
4 ibar 526 . . . 4 (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀𝑁))))
53, 4bitrd 268 . . 3 (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀𝑁))))
6 3anass 1081 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀𝑁)))
75, 6syl6bbr 278 . 2 (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁)))
81, 2, 7pm5.21nii 367 1 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  w3a 1072  wcel 2139   class class class wbr 4804  cfv 6049  cle 10267  cz 11569  cuz 11879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-cnex 10184  ax-resscn 10185
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-fv 6057  df-ov 6816  df-neg 10461  df-z 11570  df-uz 11880
This theorem is referenced by:  eluzmn  11886  eluzuzle  11888  eluzelz  11889  eluzle  11892  uztrn  11896  eluzp1p1  11905  subeluzsub  11910  uzm1  11911  uznn0sub  11912  uz3m2nn  11924  1eluzge0  11925  2eluzge1  11927  raluz2  11930  rexuz2  11932  peano2uz  11934  nn0pzuz  11938  uzind4  11939  uzinfi  11961  zsupss  11970  nn01to3  11974  nn0ge2m1nnALT  11975  elfzuzb  12529  uzsubsubfz  12556  ssfzunsnext  12579  ssfzunsn  12580  ige2m1fz  12623  4fvwrd4  12653  elfzo2  12667  elfzouz2  12678  fzossrbm1  12691  fzossfzop1  12740  ssfzo12bi  12757  elfzonelfzo  12764  elfzomelpfzo  12766  fzosplitprm1  12772  fzostep1  12778  fzind2  12780  flword2  12808  fldiv4p1lem1div2  12830  uzsup  12856  modaddmodup  12927  fzsdom2  13407  swrdtrcfv0  13642  swrdsbslen  13648  swrdspsleq  13649  swrdtrcfvl  13650  swrdccatin12lem2a  13685  cshwidxmod  13749  rexuzre  14291  limsupgre  14411  rlimclim1  14475  rlimclim  14476  climrlim2  14477  isercolllem1  14594  isercoll  14597  climcndslem1  14780  fallfacval4  14973  oddge22np1  15275  nn0o  15301  bitsmod  15360  smueqlem  15414  dvdsnprmd  15605  prmgt1  15611  oddprmgt2  15613  oddprmge3  15614  modprm0  15712  prm23ge5  15722  vdwlem9  15895  prmgaplem3  15959  prmgaplem5  15961  prmgaplem6  15962  prmgaplem7  15963  setsstruct  16100  strlemor1OLD  16171  strleun  16174  fislw  18240  efgsp1  18350  efgredleme  18356  lt6abl  18496  telgsumfzs  18586  ablfac1eu  18672  znidomb  20112  chfacfscmul0  20865  chfacfscmulfsupp  20866  chfacfpmmul0  20869  chfacfpmmulfsupp  20870  dvfsumlem1  23988  dvfsumlem3  23990  plyaddlem1  24168  coeidlem  24192  ppisval  25029  chtdif  25083  ppidif  25088  ppiublem1  25126  ppiub  25128  chtub  25136  lgsdilem2  25257  gausslemma2dlem2  25291  gausslemma2dlem4  25293  gausslemma2dlem5  25295  gausslemma2dlem6  25296  lgsquadlem1  25304  lgsquadlem3  25306  2lgslem1  25318  chebbnd1lem1  25357  chebbnd1lem2  25358  chebbnd1lem3  25359  dchrisumlem2  25378  dchrvmasumiflem1  25389  mulog2sumlem2  25423  logdivbnd  25444  pntlemg  25486  pntlemq  25489  pntlemf  25493  axlowdim  26040  pthdlem1  26872  crctcshwlkn0lem3  26915  crctcshwlkn0lem4  26916  crctcshwlkn0lem5  26917  crctcshwlkn0lem6  26918  wwlksm1edg  26990  wwlksnred  27010  clwlkclwwlklem2fv1  27118  clwlkclwwlklem2  27123  clwwisshclwwslem  27137  clwwlkinwwlk  27169  clwwlkf  27176  clwwlkext2edg  27186  wwlksubclwwlk  27189  clwlksfclwwlkOLD  27216  frgrreggt1  27561  ssnnssfz  29858  ballotlemsdom  30882  ballotlemsel1i  30883  ballotlemfrceq  30899  signstfvc  30960  signstfveq0  30963  prodfzo03  30990  erdszelem8  31487  climuzcnv  31872  poimirlem6  33728  fdc  33854  eldioph2lem1  37825  hbt  38202  ssinc  39763  ssdec  39764  monoords  40010  fzdifsuc2  40023  eluzd  40133  fmul01lt1lem2  40320  sumnnodd  40365  ioodvbdlimc1lem2  40650  ioodvbdlimc2lem  40652  dvnmul  40661  dvnprodlem2  40665  itgspltprt  40698  stoweidlem11  40731  stoweidlem26  40746  wallispilem4  40788  fourierdlem12  40839  fourierdlem20  40847  fourierdlem41  40868  fourierdlem48  40874  fourierdlem49  40875  fourierdlem50  40876  fourierdlem54  40880  fourierdlem79  40905  fourierdlem102  40928  fourierdlem111  40937  fourierdlem114  40940  etransclem23  40977  etransclem48  41002  caratheodorylem1  41246  smfmullem4  41507  eluzge0nn0  41832  ssfz12  41834  elfzlble  41840  fzopredsuc  41843  fzoopth  41847  iccpartipre  41867  iccpartiltu  41868  iccpartgt  41873  pfxtrcfv0  41912  pfxtrcfvl  41915  fmtnoge3  41952  odz2prm2pw  41985  fmtnoprmfac2lem1  41988  fmtno4prmfac  41994  31prm  42022  lighneallem4b  42036  gbegt5  42159  gbowgt5  42160  sbgoldbm  42182  mogoldbb  42183  sbgoldbo  42185  nnsum3primesle9  42192  nnsum4primesodd  42194  nnsum4primesoddALTV  42195  evengpop3  42196  evengpoap3  42197  nnsum4primeseven  42198  nnsum4primesevenALTV  42199  wtgoldbnnsum4prm  42200  bgoldbnnsum3prm  42202  bgoldbtbndlem3  42205  tgblthelfgott  42213  tgblthelfgottOLD  42219  cznnring  42466  ssnn0ssfz  42637  elfzolborelfzop1  42819  m1modmmod  42826  rege1logbzge0  42863  fllog2  42872  nnolog2flm1  42894  dignn0ldlem  42906
  Copyright terms: Public domain W3C validator