Theorem eluz2 12799

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 12798	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1136	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12797	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 528	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 279	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1094	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 289	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 378	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2109   class class class wbr 5107  ‘cfv 6511   ≤ cle 11209  ℤcz 12529  ℤ_≥cuz 12793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-cnex 11124  ax-resscn 11125

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-neg 11408  df-z 12530  df-uz 12794

This theorem is referenced by:  eluzmn  12800  eluzuzle  12802  eluzelz  12803  eluzle  12806  uztrn  12811  eluzp1p1  12821  eluzadd  12822  eluzsub  12823  subeluzsub  12830  uzm1  12831  uznn0sub  12832  1eluzge0  12839  2eluzge1  12841  5eluz3  12842  uz3m2nn  12853  raluz2  12856  rexuz2  12858  peano2uz  12860  nn0pzuz  12864  uzind4  12865  uzinfi  12887  zsupss  12896  nn01to3  12900  nn0ge2m1nnALT  12901  elfzuzb  13479  uzsubsubfz  13507  ssfzunsn  13531  ige2m1fz  13578  fz0to4untppr  13591  fz0to5un2tp  13592  4fvwrd4  13609  elfzo2  13623  elfzouz2  13635  fzossrbm1  13649  fzossfzop1  13704  ssfzo12bi  13722  fzoopth  13723  elfzonelfzo  13730  elfzomelpfzo  13732  fzosplitprm1  13738  fzostep1  13744  fzind2  13746  flword2  13775  fldiv4p1lem1div2  13797  uzsup  13825  modaddmodup  13899  fzsdom2  14393  swrdsbslen  14629  swrdspsleq  14630  pfxtrcfv0  14659  pfxtrcfvl  14662  pfxccatin12lem2a  14692  cshwidxmod  14768  rexuzre  15319  limsupgre  15447  rlimclim1  15511  rlimclim  15512  climrlim2  15513  isercolllem1  15631  isercoll  15634  climcndslem1  15815  fallfacval4  16009  oddge22np1  16319  nn0o  16353  bitsmod  16406  smueqlem  16460  dvdsnprmd  16660  2mulprm  16663  oddprmgt2  16669  oddprmge3  16670  ge2nprmge4  16671  modprm0  16776  prm23ge5  16786  vdwlem9  16960  prmgaplem3  17024  prmgaplem5  17026  prmgaplem6  17027  prmgaplem7  17028  strleun  17127  setsstruct  17146  fislw  19555  efgsp1  19667  efgredleme  19673  lt6abl  19825  telgsumfzs  19919  ablfac1eu  20005  znidomb  21471  chfacfscmul0  22745  chfacfscmulfsupp  22746  chfacfpmmul0  22749  chfacfpmmulfsupp  22750  dvfsumlem1  25932  dvfsumlem3  25935  plyaddlem1  26118  coeidlem  26142  2logb9irr  26705  ppisval  27014  chtdif  27068  ppidif  27073  ppiublem1  27113  ppiub  27115  chtub  27123  lgsdilem2  27244  gausslemma2dlem2  27278  gausslemma2dlem4  27280  gausslemma2dlem5  27282  gausslemma2dlem6  27283  lgsquadlem1  27291  lgsquadlem3  27293  2lgslem1  27305  chebbnd1lem1  27380  chebbnd1lem2  27381  chebbnd1lem3  27382  dchrisumlem2  27401  dchrvmasumiflem1  27412  mulog2sumlem2  27446  logdivbnd  27467  pntlemg  27509  pntlemq  27512  pntlemf  27516  axlowdim  28888  pthdlem1  29696  crctcshwlkn0lem3  29742  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  crctcshwlkn0lem6  29745  wwlksm1edg  29811  wwlksnred  29822  clwlkclwwlklem2fv1  29924  clwlkclwwlklem2  29929  clwwisshclwwslem  29943  clwwlkinwwlk  29969  clwwlkf  29976  clwwlkext2edg  29985  wwlksubclwwlk  29987  frgrreggt1  30322  ssnnssfz  32710  ccatdmss  32871  chnub  32938  cycpmco2lem6  33088  ballotlemsdom  34503  ballotlemsel1i  34504  ballotlemfrceq  34520  signstfvc  34565  signstfveq0  34568  prodfzo03  34594  erdszelem8  35185  climuzcnv  35658  poimirlem6  37620  fdc  37739  sticksstones12  42146  eluzp1  42295  fimgmcyc  42522  eldioph2lem1  42748  hbt  43119  ssinc  45081  ssdec  45082  monoords  45295  fzdifsuc2  45308  eluzd  45405  fmul01lt1lem2  45583  sumnnodd  45628  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnmul  45941  dvnprodlem2  45945  itgspltprt  45977  stoweidlem11  46009  stoweidlem26  46024  wallispilem4  46066  fourierdlem12  46117  fourierdlem20  46125  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem54  46158  fourierdlem79  46183  fourierdlem102  46206  fourierdlem111  46215  fourierdlem114  46218  etransclem23  46255  etransclem48  46280  caratheodorylem1  46524  smfmullem4  46792  eluzge0nn0  47313  ssfz12  47315  elfzlble  47321  fzopredsuc  47324  ceilhalfelfzo1  47331  addmodne  47345  m1modnep2mod  47353  m1modmmod  47359  modm2nep1  47367  modp2nep1  47368  modm1nep2  47369  modm1nem2  47370  modm1p1ne  47371  iccpartipre  47422  iccpartiltu  47423  iccpartgt  47428  fmtnoge3  47531  odz2prm2pw  47564  fmtnoprmfac2lem1  47567  fmtno4prmfac  47573  31prm  47598  lighneallem4b  47610  341fppr2  47735  9fppr8  47738  fpprel2  47742  nfermltl8rev  47743  nfermltl2rev  47744  gbegt5  47762  gbowgt5  47763  sbgoldbm  47785  mogoldbb  47786  sbgoldbo  47788  nnsum3primesle9  47795  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  evengpop3  47799  evengpoap3  47800  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  bgoldbtbndlem3  47808  tgblthelfgott  47816  gpgusgralem  48047  gpgedgvtx1  48053  gpg5nbgrvtx13starlem2  48063  gpg3nbgrvtx0  48067  gpg3nbgrvtx0ALT  48068  gpg5nbgr3star  48072  gpg3kgrtriexlem3  48076  gpg3kgrtriexlem6  48079  cznnring  48250  ssnn0ssfz  48337  elfzolborelfzop1  48508  rege1logbzge0  48548  fllog2  48557  nnolog2flm1  48579  dignn0ldlem  48591