Theorem eluz2 12794

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114   class class class wbr 5085  ‘cfv 6498   ≤ cle 11180  ℤcz 12524  ℤ_≥cuz 12788

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-cnex 11094  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-ov 7370  df-neg 11380  df-z 12525  df-uz 12789

This theorem is referenced by:  eluzmn  12795  eluzuzle  12797  eluzelz  12798  eluzle  12801  uztrn  12806  eluzp1p1  12816  eluzadd  12817  eluzsub  12818  subeluzsub  12821  uzm1  12822  uznn0sub  12823  1eluzge0  12830  2eluzge1  12832  5eluz3  12833  uz3m2nn  12844  raluz2  12847  rexuz2  12849  peano2uz  12851  nn0pzuz  12855  uzind4  12856  uzinfi  12878  zsupss  12887  nn01to3  12891  nn0ge2m1nnALT  12892  elfzuzb  13472  uzsubsubfz  13500  ssfzunsn  13524  ige2m1fz  13571  fz0to4untppr  13584  fz0to5un2tp  13585  4fvwrd4  13602  elfzo2  13616  elfzouz2  13629  fzossrbm1  13643  fzossfzop1  13698  ssfzo12bi  13716  fzoopth  13717  elfzonelfzo  13724  elfzomelpfzo  13727  fzosplitprm1  13733  fzostep1  13741  fzind2  13743  flword2  13772  fldiv4p1lem1div2  13794  uzsup  13822  modaddmodup  13896  fzsdom2  14390  ccatdmss  14544  swrdsbslen  14627  swrdspsleq  14628  pfxtrcfv0  14656  pfxtrcfvl  14659  pfxccatin12lem2a  14689  cshwidxmod  14765  rexuzre  15315  limsupgre  15443  rlimclim1  15507  rlimclim  15508  climrlim2  15509  isercolllem1  15627  isercoll  15630  climcndslem1  15814  fallfacval4  16008  oddge22np1  16318  nn0o  16352  bitsmod  16405  smueqlem  16459  dvdsnprmd  16659  2mulprm  16662  oddprmgt2  16669  oddprmge3  16670  ge2nprmge4  16671  modprm0  16776  prm23ge5  16786  vdwlem9  16960  prmgaplem3  17024  prmgaplem5  17026  prmgaplem6  17027  prmgaplem7  17028  strleun  17127  setsstruct  17146  chnub  18588  fislw  19600  efgsp1  19712  efgredleme  19718  lt6abl  19870  telgsumfzs  19964  ablfac1eu  20050  znidomb  21541  chfacfscmul0  22823  chfacfscmulfsupp  22824  chfacfpmmul0  22827  chfacfpmmulfsupp  22828  dvfsumlem1  25993  dvfsumlem3  25995  plyaddlem1  26178  coeidlem  26202  2logb9irr  26759  ppisval  27067  chtdif  27121  ppidif  27126  ppiublem1  27165  ppiub  27167  chtub  27175  lgsdilem2  27296  gausslemma2dlem2  27330  gausslemma2dlem4  27332  gausslemma2dlem5  27334  gausslemma2dlem6  27335  lgsquadlem1  27343  lgsquadlem3  27345  2lgslem1  27357  chebbnd1lem1  27432  chebbnd1lem2  27433  chebbnd1lem3  27434  dchrisumlem2  27453  dchrvmasumiflem1  27464  mulog2sumlem2  27498  logdivbnd  27519  pntlemg  27561  pntlemq  27564  pntlemf  27568  axlowdim  29030  pthdlem1  29834  crctcshwlkn0lem3  29880  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  crctcshwlkn0lem6  29883  wwlksm1edg  29949  wwlksnred  29960  clwlkclwwlklem2fv1  30065  clwlkclwwlklem2  30070  clwwisshclwwslem  30084  clwwlkinwwlk  30110  clwwlkf  30117  clwwlkext2edg  30126  wwlksubclwwlk  30128  frgrreggt1  30463  ssnnssfz  32860  cycpmco2lem6  33192  ballotlemsdom  34656  ballotlemsel1i  34657  ballotlemfrceq  34673  signstfvc  34718  signstfveq0  34721  prodfzo03  34747  erdszelem8  35380  climuzcnv  35853  poimirlem6  37947  fdc  38066  sticksstones12  42597  eluzp1  42739  fimgmcyc  42979  eldioph2lem1  43192  hbt  43558  ssinc  45517  ssdec  45518  monoords  45730  fzdifsuc2  45743  eluzd  45837  fmul01lt1lem2  46015  sumnnodd  46060  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnmul  46371  dvnprodlem2  46375  itgspltprt  46407  stoweidlem11  46439  stoweidlem26  46454  wallispilem4  46496  fourierdlem12  46547  fourierdlem20  46555  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem54  46588  fourierdlem79  46613  fourierdlem102  46636  fourierdlem111  46645  fourierdlem114  46648  etransclem23  46685  etransclem48  46710  caratheodorylem1  46954  smfmullem4  47222  eluzge0nn0  47760  ssfz12  47762  elfzlble  47768  fzopredsuc  47772  ceilhalfelfzo1  47782  addmodne  47798  m1modnep2mod  47806  m1modmmod  47812  modm2nep1  47820  modp2nep1  47821  modm1nep2  47822  modm1nem2  47823  modm1p1ne  47824  2timesltsqm1  47827  muldvdsfacgt  47834  muldvdsfacm1  47835  iccpartipre  47881  iccpartiltu  47882  iccpartgt  47887  fmtnoge3  47993  odz2prm2pw  48026  fmtnoprmfac2lem1  48029  fmtno4prmfac  48035  31prm  48060  lighneallem4b  48072  nprmdvdsfacm1lem2  48084  nprmdvdsfacm1lem3  48085  nprmdvdsfacm1lem4  48086  nprmdvdsfacm1  48087  ppivalnnnprmge6  48089  341fppr2  48210  9fppr8  48213  fpprel2  48217  nfermltl8rev  48218  nfermltl2rev  48219  gbegt5  48237  gbowgt5  48238  sbgoldbm  48260  mogoldbb  48261  sbgoldbo  48263  nnsum3primesle9  48270  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  evengpop3  48274  evengpoap3  48275  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  bgoldbtbndlem3  48283  tgblthelfgott  48291  gpgusgralem  48532  gpgedgvtx1  48538  gpg5nbgrvtx13starlem2  48548  gpg3nbgrvtx0  48552  gpg3nbgrvtx0ALT  48553  gpg5nbgr3star  48557  gpg3kgrtriexlem3  48561  gpg3kgrtriexlem6  48564  gpg5edgnedg  48606  cznnring  48738  ssnn0ssfz  48825  elfzolborelfzop1  48995  rege1logbzge0  49035  fllog2  49044  nnolog2flm1  49066  dignn0ldlem  49078