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

Theorem eluz2 11731
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 11730 . 2 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
2 simp1 1081 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁) → 𝑀 ∈ ℤ)
3 eluz1 11729 . . . 4 (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀𝑁)))
4 ibar 524 . . . 4 (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀𝑁))))
53, 4bitrd 268 . . 3 (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀𝑁))))
6 3anass 1059 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀𝑁)))
75, 6syl6bbr 278 . 2 (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁)))
81, 2, 7pm5.21nii 367 1 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  w3a 1054  wcel 2030   class class class wbr 4685  cfv 5926  cle 10113  cz 11415  cuz 11725
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-cnex 10030  ax-resscn 10031
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934  df-ov 6693  df-neg 10307  df-z 11416  df-uz 11726
This theorem is referenced by:  eluzmn  11732  eluzuzle  11734  eluzelz  11735  eluzle  11738  uztrn  11742  eluzp1p1  11751  uzm1  11756  uznn0sub  11757  uz3m2nn  11769  1eluzge0  11770  2eluzge1  11772  raluz2  11775  rexuz2  11777  peano2uz  11779  nn0pzuz  11783  uzind4  11784  uzinfi  11806  zsupss  11815  nn01to3  11819  nn0ge2m1nnALT  11820  elfzuzb  12374  uzsubsubfz  12401  ssfzunsnext  12424  ssfzunsn  12425  ige2m1fz  12468  4fvwrd4  12498  elfzo2  12512  elfzouz2  12523  fzossrbm1  12536  fzossfzop1  12585  ssfzo12bi  12603  elfzonelfzo  12610  elfzomelpfzo  12612  fzosplitprm1  12618  fzostep1  12624  fzind2  12626  flword2  12654  fldiv4p1lem1div2  12676  uzsup  12702  modaddmodup  12773  fzsdom2  13253  swrdtrcfv0  13488  swrdsbslen  13494  swrdspsleq  13495  swrdtrcfvl  13496  swrdccatin12lem2a  13531  cshwidxmod  13595  rexuzre  14136  limsupgre  14256  rlimclim1  14320  rlimclim  14321  climrlim2  14322  isercolllem1  14439  isercoll  14442  climcndslem1  14625  fallfacval4  14818  oddge22np1  15120  nn0o  15146  bitsmod  15205  smueqlem  15259  dvdsnprmd  15450  prmgt1  15456  oddprmgt2  15458  oddprmge3  15459  modprm0  15557  prm23ge5  15567  vdwlem9  15740  prmgaplem3  15804  prmgaplem5  15806  prmgaplem6  15807  prmgaplem7  15808  setsstruct  15945  strlemor1OLD  16016  strleun  16019  fislw  18086  efgsp1  18196  efgredleme  18202  lt6abl  18342  telgsumfzs  18432  ablfac1eu  18518  znidomb  19958  chfacfscmul0  20711  chfacfscmulfsupp  20712  chfacfpmmul0  20715  chfacfpmmulfsupp  20716  dvfsumlem1  23834  dvfsumlem3  23836  plyaddlem1  24014  coeidlem  24038  ppisval  24875  chtdif  24929  ppidif  24934  ppiublem1  24972  ppiub  24974  chtub  24982  lgsdilem2  25103  gausslemma2dlem2  25137  gausslemma2dlem4  25139  gausslemma2dlem5  25141  gausslemma2dlem6  25142  lgsquadlem1  25150  lgsquadlem3  25152  2lgslem1  25164  chebbnd1lem1  25203  chebbnd1lem2  25204  chebbnd1lem3  25205  dchrisumlem2  25224  dchrvmasumiflem1  25235  mulog2sumlem2  25269  logdivbnd  25290  pntlemg  25332  pntlemq  25335  pntlemf  25339  axlowdim  25886  pthdlem1  26718  crctcshwlkn0lem3  26760  crctcshwlkn0lem4  26761  crctcshwlkn0lem5  26762  crctcshwlkn0lem6  26763  wwlksm1edg  26835  wwlksnred  26855  clwlkclwwlklem2fv1  26961  clwlkclwwlklem2  26966  clwwisshclwwslem  26971  clwwlkinwwlk  27003  clwwlkf  27010  clwwlkext2edg  27020  wwlksubclwwlk  27023  clwlksfclwwlk  27049  frgrreggt1  27380  ssnnssfz  29677  ballotlemsdom  30701  ballotlemsel1i  30702  ballotlemfrceq  30718  signstfvc  30779  signstfveq0  30782  prodfzo03  30809  erdszelem8  31306  climuzcnv  31691  poimirlem6  33545  fdc  33671  eldioph2lem1  37640  hbt  38017  ssinc  39578  ssdec  39579  monoords  39825  fzdifsuc2  39838  eluzd  39948  fmul01lt1lem2  40135  sumnnodd  40180  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnmul  40476  dvnprodlem2  40480  itgspltprt  40513  stoweidlem11  40546  stoweidlem26  40561  wallispilem4  40603  fourierdlem12  40654  fourierdlem20  40662  fourierdlem41  40683  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem54  40695  fourierdlem79  40720  fourierdlem102  40743  fourierdlem111  40752  fourierdlem114  40755  etransclem23  40792  etransclem48  40817  caratheodorylem1  41061  smfmullem4  41322  eluzge0nn0  41647  ssfz12  41649  elfzlble  41655  fzopredsuc  41658  fzoopth  41662  iccpartipre  41682  iccpartiltu  41683  iccpartgt  41688  pfxtrcfv0  41727  pfxtrcfvl  41730  fmtnoge3  41767  odz2prm2pw  41800  fmtnoprmfac2lem1  41803  fmtno4prmfac  41809  31prm  41837  lighneallem4b  41851  gbegt5  41974  gbowgt5  41975  sbgoldbm  41997  mogoldbb  41998  sbgoldbo  42000  nnsum3primesle9  42007  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  evengpop3  42011  evengpoap3  42012  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  bgoldbtbndlem3  42020  tgblthelfgott  42028  tgblthelfgottOLD  42034  cznnring  42281  ssnn0ssfz  42452  elfzolborelfzop1  42634  m1modmmod  42641  rege1logbzge0  42678  fllog2  42687  nnolog2flm1  42709  dignn0ldlem  42721
  Copyright terms: Public domain W3C validator