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

Theorem eluz2 12241
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 12240 . 2 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
2 simp1 1133 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁) → 𝑀 ∈ ℤ)
3 eluz1 12239 . . . 4 (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀𝑁)))
4 ibar 532 . . . 4 (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀𝑁))))
53, 4bitrd 282 . . 3 (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀𝑁))))
6 3anass 1092 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀𝑁)))
75, 6syl6bbr 292 . 2 (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁)))
81, 2, 7pm5.21nii 383 1 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  w3a 1084  wcel 2112   class class class wbr 5033  cfv 6328  cle 10669  cz 11973  cuz 12235
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-cnex 10586  ax-resscn 10587
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-fv 6336  df-ov 7142  df-neg 10866  df-z 11974  df-uz 12236
This theorem is referenced by:  eluzmn  12242  eluzuzle  12244  eluzelz  12245  eluzle  12248  uztrn  12253  eluzp1p1  12262  subeluzsub  12267  uzm1  12268  uznn0sub  12269  uz3m2nn  12283  1eluzge0  12284  2eluzge1  12286  raluz2  12289  rexuz2  12291  peano2uz  12293  nn0pzuz  12297  uzind4  12298  uzinfi  12320  zsupss  12329  nn01to3  12333  nn0ge2m1nnALT  12334  elfzuzb  12900  uzsubsubfz  12928  ssfzunsnext  12951  ssfzunsn  12952  ige2m1fz  12996  4fvwrd4  13026  elfzo2  13040  elfzouz2  13051  fzossrbm1  13065  fzossfzop1  13114  ssfzo12bi  13131  elfzonelfzo  13138  elfzomelpfzo  13140  fzosplitprm1  13146  fzostep1  13152  fzind2  13154  flword2  13182  fldiv4p1lem1div2  13204  uzsup  13230  modaddmodup  13301  fzsdom2  13789  swrdsbslen  14021  swrdspsleq  14022  pfxtrcfv0  14051  pfxtrcfvl  14054  pfxccatin12lem2a  14084  cshwidxmod  14160  rexuzre  14708  limsupgre  14834  rlimclim1  14898  rlimclim  14899  climrlim2  14900  isercolllem1  15017  isercoll  15020  climcndslem1  15200  fallfacval4  15393  oddge22np1  15694  nn0o  15728  bitsmod  15779  smueqlem  15833  dvdsnprmd  16028  2mulprm  16031  oddprmgt2  16037  oddprmge3  16038  ge2nprmge4  16039  modprm0  16136  prm23ge5  16146  vdwlem9  16319  prmgaplem3  16383  prmgaplem5  16385  prmgaplem6  16386  prmgaplem7  16387  setsstruct  16519  strleun  16587  fislw  18746  efgsp1  18859  efgredleme  18865  lt6abl  19012  telgsumfzs  19106  ablfac1eu  19192  znidomb  20257  chfacfscmul0  21467  chfacfscmulfsupp  21468  chfacfpmmul0  21471  chfacfpmmulfsupp  21472  dvfsumlem1  24633  dvfsumlem3  24635  plyaddlem1  24814  coeidlem  24838  2logb9irr  25385  ppisval  25693  chtdif  25747  ppidif  25752  ppiublem1  25790  ppiub  25792  chtub  25800  lgsdilem2  25921  gausslemma2dlem2  25955  gausslemma2dlem4  25957  gausslemma2dlem5  25959  gausslemma2dlem6  25960  lgsquadlem1  25968  lgsquadlem3  25970  2lgslem1  25982  chebbnd1lem1  26057  chebbnd1lem2  26058  chebbnd1lem3  26059  dchrisumlem2  26078  dchrvmasumiflem1  26089  mulog2sumlem2  26123  logdivbnd  26144  pntlemg  26186  pntlemq  26189  pntlemf  26193  axlowdim  26759  pthdlem1  27559  crctcshwlkn0lem3  27602  crctcshwlkn0lem4  27603  crctcshwlkn0lem5  27604  crctcshwlkn0lem6  27605  wwlksm1edg  27671  wwlksnred  27682  clwlkclwwlklem2fv1  27784  clwlkclwwlklem2  27789  clwwisshclwwslem  27803  clwwlkinwwlk  27829  clwwlkf  27836  clwwlkext2edg  27845  wwlksubclwwlk  27847  frgrreggt1  28182  ssnnssfz  30540  cycpmco2lem6  30827  ballotlemsdom  31883  ballotlemsel1i  31884  ballotlemfrceq  31900  signstfvc  31958  signstfveq0  31961  prodfzo03  31988  erdszelem8  32559  climuzcnv  33028  poimirlem6  35062  fdc  35182  eldioph2lem1  39694  hbt  40067  ssinc  41716  ssdec  41717  monoords  41922  fzdifsuc2  41935  eluzd  42039  fmul01lt1lem2  42220  sumnnodd  42265  ioodvbdlimc1lem2  42567  ioodvbdlimc2lem  42569  dvnmul  42578  dvnprodlem2  42582  itgspltprt  42614  stoweidlem11  42646  stoweidlem26  42661  wallispilem4  42703  fourierdlem12  42754  fourierdlem20  42762  fourierdlem41  42783  fourierdlem48  42789  fourierdlem49  42790  fourierdlem50  42791  fourierdlem54  42795  fourierdlem79  42820  fourierdlem102  42843  fourierdlem111  42852  fourierdlem114  42855  etransclem23  42892  etransclem48  42917  caratheodorylem1  43158  smfmullem4  43419  eluzge0nn0  43862  ssfz12  43864  elfzlble  43870  fzopredsuc  43873  fzoopth  43877  iccpartipre  43931  iccpartiltu  43932  iccpartgt  43937  fmtnoge3  44040  odz2prm2pw  44073  fmtnoprmfac2lem1  44076  fmtno4prmfac  44082  31prm  44107  lighneallem4b  44120  341fppr2  44245  9fppr8  44248  fpprel2  44252  nfermltl8rev  44253  nfermltl2rev  44254  gbegt5  44272  gbowgt5  44273  sbgoldbm  44295  mogoldbb  44296  sbgoldbo  44298  nnsum3primesle9  44305  nnsum4primesodd  44307  nnsum4primesoddALTV  44308  evengpop3  44309  evengpoap3  44310  nnsum4primeseven  44311  nnsum4primesevenALTV  44312  wtgoldbnnsum4prm  44313  bgoldbnnsum3prm  44315  bgoldbtbndlem3  44318  tgblthelfgott  44326  cznnring  44573  ssnn0ssfz  44744  elfzolborelfzop1  44921  m1modmmod  44928  rege1logbzge0  44966  fllog2  44975  nnolog2flm1  44997  dignn0ldlem  45009
  Copyright terms: Public domain W3C validator