Theorem eluz2 12828

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

Step	Hyp	Ref	Expression
1		eluzel2 12827	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1137	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12826	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 530	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 279	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1096	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 289	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 380	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   ∈ wcel 2107   class class class wbr 5149  ‘cfv 6544   ≤ cle 11249  ℤcz 12558  ℤ_≥cuz 12822

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 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-cnex 11166  ax-resscn 11167

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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7412  df-neg 11447  df-z 12559  df-uz 12823

This theorem is referenced by:  eluzmn  12829  eluzuzle  12831  eluzelz  12832  eluzle  12835  uztrn  12840  eluzp1p1  12850  eluzadd  12851  eluzsub  12852  subeluzsub  12859  uzm1  12860  uznn0sub  12861  uz3m2nn  12875  1eluzge0  12876  2eluzge1  12878  raluz2  12881  rexuz2  12883  peano2uz  12885  nn0pzuz  12889  uzind4  12890  uzinfi  12912  zsupss  12921  nn01to3  12925  nn0ge2m1nnALT  12926  elfzuzb  13495  uzsubsubfz  13523  ssfzunsn  13547  ige2m1fz  13591  4fvwrd4  13621  elfzo2  13635  elfzouz2  13647  fzossrbm1  13661  fzossfzop1  13710  ssfzo12bi  13727  elfzonelfzo  13734  elfzomelpfzo  13736  fzosplitprm1  13742  fzostep1  13748  fzind2  13750  flword2  13778  fldiv4p1lem1div2  13800  uzsup  13828  modaddmodup  13899  fzsdom2  14388  swrdsbslen  14614  swrdspsleq  14615  pfxtrcfv0  14644  pfxtrcfvl  14647  pfxccatin12lem2a  14677  cshwidxmod  14753  rexuzre  15299  limsupgre  15425  rlimclim1  15489  rlimclim  15490  climrlim2  15491  isercolllem1  15611  isercoll  15614  climcndslem1  15795  fallfacval4  15987  oddge22np1  16292  nn0o  16326  bitsmod  16377  smueqlem  16431  dvdsnprmd  16627  2mulprm  16630  oddprmgt2  16636  oddprmge3  16637  ge2nprmge4  16638  modprm0  16738  prm23ge5  16748  vdwlem9  16922  prmgaplem3  16986  prmgaplem5  16988  prmgaplem6  16989  prmgaplem7  16990  strleun  17090  setsstruct  17109  fislw  19493  efgsp1  19605  efgredleme  19611  lt6abl  19763  telgsumfzs  19857  ablfac1eu  19943  znidomb  21117  chfacfscmul0  22360  chfacfscmulfsupp  22361  chfacfpmmul0  22364  chfacfpmmulfsupp  22365  dvfsumlem1  25543  dvfsumlem3  25545  plyaddlem1  25727  coeidlem  25751  2logb9irr  26300  ppisval  26608  chtdif  26662  ppidif  26667  ppiublem1  26705  ppiub  26707  chtub  26715  lgsdilem2  26836  gausslemma2dlem2  26870  gausslemma2dlem4  26872  gausslemma2dlem5  26874  gausslemma2dlem6  26875  lgsquadlem1  26883  lgsquadlem3  26885  2lgslem1  26897  chebbnd1lem1  26972  chebbnd1lem2  26973  chebbnd1lem3  26974  dchrisumlem2  26993  dchrvmasumiflem1  27004  mulog2sumlem2  27038  logdivbnd  27059  pntlemg  27101  pntlemq  27104  pntlemf  27108  axlowdim  28219  pthdlem1  29023  crctcshwlkn0lem3  29066  crctcshwlkn0lem4  29067  crctcshwlkn0lem5  29068  crctcshwlkn0lem6  29069  wwlksm1edg  29135  wwlksnred  29146  clwlkclwwlklem2fv1  29248  clwlkclwwlklem2  29253  clwwisshclwwslem  29267  clwwlkinwwlk  29293  clwwlkf  29300  clwwlkext2edg  29309  wwlksubclwwlk  29311  frgrreggt1  29646  ssnnssfz  31998  cycpmco2lem6  32290  ballotlemsdom  33510  ballotlemsel1i  33511  ballotlemfrceq  33527  signstfvc  33585  signstfveq0  33588  prodfzo03  33615  erdszelem8  34189  climuzcnv  34656  poimirlem6  36494  fdc  36613  sticksstones12  40974  eldioph2lem1  41498  hbt  41872  ssinc  43776  ssdec  43777  monoords  44007  fzdifsuc2  44020  eluzd  44119  fmul01lt1lem2  44301  sumnnodd  44346  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnmul  44659  dvnprodlem2  44663  itgspltprt  44695  stoweidlem11  44727  stoweidlem26  44742  wallispilem4  44784  fourierdlem12  44835  fourierdlem20  44843  fourierdlem41  44864  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  fourierdlem54  44876  fourierdlem79  44901  fourierdlem102  44924  fourierdlem111  44933  fourierdlem114  44936  etransclem23  44973  etransclem48  44998  caratheodorylem1  45242  smfmullem4  45510  eluzge0nn0  46020  ssfz12  46022  elfzlble  46028  fzopredsuc  46031  fzoopth  46035  iccpartipre  46089  iccpartiltu  46090  iccpartgt  46095  fmtnoge3  46198  odz2prm2pw  46231  fmtnoprmfac2lem1  46234  fmtno4prmfac  46240  31prm  46265  lighneallem4b  46277  341fppr2  46402  9fppr8  46405  fpprel2  46409  nfermltl8rev  46410  nfermltl2rev  46411  gbegt5  46429  gbowgt5  46430  sbgoldbm  46452  mogoldbb  46453  sbgoldbo  46455  nnsum3primesle9  46462  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  evengpop3  46466  evengpoap3  46467  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  wtgoldbnnsum4prm  46470  bgoldbnnsum3prm  46472  bgoldbtbndlem3  46475  tgblthelfgott  46483  cznnring  46854  ssnn0ssfz  47025  elfzolborelfzop1  47200  m1modmmod  47207  rege1logbzge0  47245  fllog2  47254  nnolog2flm1  47276  dignn0ldlem  47288