Theorem eluz2 12981

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 12980	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1154	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12979	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 538	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 282	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1111	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 292	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 381	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2146   class class class wbr 5105  ‘cfv 6546   ≤ cle 11354  ℤcz 12703  ℤ_≥cuz 12975

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pr 5394  ax-cnex 11266  ax-resscn 11267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-fv 6554  df-ov 7430  df-neg 11554  df-z 12704  df-uz 12976

This theorem is used by:  eluzmn  12982  eluzuzle  12984  eluzelz  12985  eluzle  12988  uztrn  12993  eluzp1p1  13003  eluzadd  13004  eluzsub  13005  subeluzsub  13008  uzm1  13009  uznn0sub  13010  1eluzge0  13017  2eluzge1  13019  5eluz3  13020  uz3m2nn  13031  raluz2  13034  rexuz2  13036  peano2uz  13038  nn0pzuz  13042  uzind4  13043  uzinfi  13065  zsupss  13074  nn01to3  13078  nn0ge2m1nnALT  13079  elfzuzb  13660  uzsubsubfz  13690  ssfzunsn  13714  ige2m1fz  13761  fz0to4untppr  13774  fz0to5un2tp  13775  4fvwrd4  13792  elfzo2  13806  elfzouz2  13819  fzossrbm1  13833  fzossfzop1  13888  ssfzo12bi  13906  fzoopth  13907  elfzonelfzo  13914  elfzomelpfzo  13917  fzosplitprm1  13923  fzostep1  13931  fzind2  13933  flword2  13963  fldiv4p1lem1div2  13985  uzsup  14013  modaddmodup  14087  fzsdom2  14583  ccatdmss  14737  swrdsbslen  14825  swrdspsleq  14826  pfxtrcfv0  14854  pfxtrcfvl  14857  pfxccatin12lem2a  14887  cshwidxmod  14965  rexuzre  15532  limsupgre  15660  rlimclim1  15724  rlimclim  15725  climrlim2  15726  isercolllem1  15844  isercoll  15847  climcndslem1  16030  fallfacval4  16221  oddge22np1  16531  nn0o  16565  bitsmod  16618  smueqlem  16672  dvdsnprmd  16877  2mulprm  16880  oddprmgt2  16887  oddprmge3  16888  ge2nprmge4  16889  modprm0  16995  prm23ge5  17005  vdwlem9  17179  prmgaplem3  17243  prmgaplem5  17245  prmgaplem6  17246  prmgaplem7  17247  strleun  17347  setsstruct  17366  chnub  18808  fislw  19851  efgsp1  19963  efgredleme  19969  lt6abl  20121  telgsumfzs  20215  ablfac1eu  20301  znidomb  21879  chfacfscmul0  23188  chfacfscmulfsupp  23189  chfacfpmmul0  23192  chfacfpmmulfsupp  23193  dvfsumlem1  26358  dvfsumlem3  26360  plyaddlem1  26544  coeidlem  26568  2logb9irr  27135  ppisval  27443  chtdif  27497  ppidif  27502  ppiublem1  27541  ppiub  27543  chtub  27551  lgsdilem2  27672  gausslemma2dlem2  27706  gausslemma2dlem4  27708  gausslemma2dlem5  27710  gausslemma2dlem6  27711  lgsquadlem1  27719  lgsquadlem3  27721  2lgslem1  27733  chebbnd1lem1  27808  chebbnd1lem2  27809  chebbnd1lem3  27810  dchrisumlem2  27829  dchrvmasumiflem1  27840  mulog2sumlem2  27874  logdivbnd  27895  pntlemg  27937  pntlemq  27940  pntlemf  27944  fltoprmlem2  28006  axlowdim  29551  pthdlem1  30364  crctcshwlkn0lem3  30413  crctcshwlkn0lem4  30414  crctcshwlkn0lem5  30415  crctcshwlkn0lem6  30416  wwlksm1edg  30482  wwlksnred  30493  clwlkclwwlklem2fv1  30598  clwlkclwwlklem2  30603  clwwisshclwwslem  30617  clwwlkinwwlk  30643  clwwlkf  30650  clwwlkext2edg  30659  wwlksubclwwlk  30661  frgrreggt1  31006  ssnnssfz  33432  cycpmco2lem6  33745  ballotlemsdom  35197  ballotlemsel1i  35198  ballotlemfrceq  35214  signstfvc  35256  signstfveq0  35259  prodfzo03  35285  erdszelem8  36084  climuzcnv  36557  poimirlem6  38684  fdc  38819  sticksstones12  43348  eluzp1  43504  fimgmcyc  43738  eldioph2lem1  43911  hbt  44272  ssinc  46241  ssdec  46242  monoords  46452  fzdifsuc2  46465  eluzd  46558  fmul01lt1lem2  46736  sumnnodd  46781  ioodvbdlimc1lem2  47081  ioodvbdlimc2lem  47083  dvnmul  47092  dvnprodlem2  47096  itgspltprt  47128  stoweidlem11  47160  stoweidlem26  47175  wallispilem4  47217  fourierdlem12  47268  fourierdlem20  47276  fourierdlem41  47297  fourierdlem50  47305  fourierdlem54  47309  fourierdlem79  47334  fourierdlem102  47357  fourierdlem111  47366  fourierdlem114  47369  etransclem23  47406  etransclem48  47431  caratheodorylem1  47675  smfmullem4  47943  eluzge0nn0  48521  ssfz12  48523  elfzlble  48529  fzopredsuc  48533  ceilhalfelfzo1  48543  addmodne  48559  m1modnep2mod  48567  m1modmmod  48573  modm2nep1  48581  modp2nep1  48582  modm1nep2  48583  modm1nem2  48584  modm1p1ne  48585  2timesltsqm1  48588  muldvdsfacgt  48595  muldvdsfacm1  48596  iccpartipre  48642  iccpartiltu  48643  iccpartgt  48648  fmtnoge3  48754  odz2prm2pw  48787  fmtnoprmfac2lem1  48790  fmtno4prmfac  48796  31prm  48821  lighneallem4b  48833  nprmdvdsfacm1lem2  48845  nprmdvdsfacm1lem3  48846  nprmdvdsfacm1lem4  48847  nprmdvdsfacm1  48848  ppivalnnnprmge6  48850  341fppr2  48971  9fppr8  48974  fpprel2  48978  nfermltl8rev  48979  nfermltl2rev  48980  gbegt5  48998  gbowgt5  48999  sbgoldbm  49021  mogoldbb  49022  sbgoldbo  49024  nnsum3primesle9  49031  nnsum4primesodd  49033  nnsum4primesoddALTV  49034  evengpop3  49035  evengpoap3  49036  nnsum4primeseven  49037  nnsum4primesevenALTV  49038  wtgoldbnnsum4prm  49039  bgoldbnnsum3prm  49041  bgoldbtbndlem3  49044  tgblthelfgott  49052  gpgusgralem  49293  gpgedgvtx1  49299  gpg5nbgrvtx13starlem2  49309  gpg3nbgrvtx0  49313  gpg3nbgrvtx0ALT  49314  gpg5nbgr3star  49318  gpg3kgrtriexlem3  49322  gpg3kgrtriexlem6  49325  gpg5edgnedg  49367  cznnring  49498  ssnn0ssfz  49600  elfzolborelfzop1  49770  rege1logbzge0  49810  fllog2  49819  nnolog2flm1  49841  dignn0ldlem  49853