Theorem eluz2 12884

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 12883	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1137	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12882	. . . 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 2108   class class class wbr 5143  ‘cfv 6561   ≤ cle 11296  ℤcz 12613  ℤ_≥cuz 12878

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-cnex 11211  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-neg 11495  df-z 12614  df-uz 12879

This theorem is referenced by:  eluzmn  12885  eluzuzle  12887  eluzelz  12888  eluzle  12891  uztrn  12896  eluzp1p1  12906  eluzadd  12907  eluzsub  12908  subeluzsub  12915  uzm1  12916  uznn0sub  12917  5eluz3  12927  uz3m2nn  12933  1eluzge0  12934  2eluzge1  12936  raluz2  12939  rexuz2  12941  peano2uz  12943  nn0pzuz  12947  uzind4  12948  uzinfi  12970  zsupss  12979  nn01to3  12983  nn0ge2m1nnALT  12984  elfzuzb  13558  uzsubsubfz  13586  ssfzunsn  13610  ige2m1fz  13657  fz0to4untppr  13670  fz0to5un2tp  13671  4fvwrd4  13688  elfzo2  13702  elfzouz2  13714  fzossrbm1  13728  fzossfzop1  13782  ssfzo12bi  13800  fzoopth  13801  elfzonelfzo  13808  elfzomelpfzo  13810  fzosplitprm1  13816  fzostep1  13822  fzind2  13824  flword2  13853  fldiv4p1lem1div2  13875  uzsup  13903  modaddmodup  13975  fzsdom2  14467  swrdsbslen  14702  swrdspsleq  14703  pfxtrcfv0  14732  pfxtrcfvl  14735  pfxccatin12lem2a  14765  cshwidxmod  14841  rexuzre  15391  limsupgre  15517  rlimclim1  15581  rlimclim  15582  climrlim2  15583  isercolllem1  15701  isercoll  15704  climcndslem1  15885  fallfacval4  16079  oddge22np1  16386  nn0o  16420  bitsmod  16473  smueqlem  16527  dvdsnprmd  16727  2mulprm  16730  oddprmgt2  16736  oddprmge3  16737  ge2nprmge4  16738  modprm0  16843  prm23ge5  16853  vdwlem9  17027  prmgaplem3  17091  prmgaplem5  17093  prmgaplem6  17094  prmgaplem7  17095  strleun  17194  setsstruct  17213  fislw  19643  efgsp1  19755  efgredleme  19761  lt6abl  19913  telgsumfzs  20007  ablfac1eu  20093  znidomb  21580  chfacfscmul0  22864  chfacfscmulfsupp  22865  chfacfpmmul0  22868  chfacfpmmulfsupp  22869  dvfsumlem1  26066  dvfsumlem3  26069  plyaddlem1  26252  coeidlem  26276  2logb9irr  26838  ppisval  27147  chtdif  27201  ppidif  27206  ppiublem1  27246  ppiub  27248  chtub  27256  lgsdilem2  27377  gausslemma2dlem2  27411  gausslemma2dlem4  27413  gausslemma2dlem5  27415  gausslemma2dlem6  27416  lgsquadlem1  27424  lgsquadlem3  27426  2lgslem1  27438  chebbnd1lem1  27513  chebbnd1lem2  27514  chebbnd1lem3  27515  dchrisumlem2  27534  dchrvmasumiflem1  27545  mulog2sumlem2  27579  logdivbnd  27600  pntlemg  27642  pntlemq  27645  pntlemf  27649  axlowdim  28976  pthdlem1  29786  crctcshwlkn0lem3  29832  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  crctcshwlkn0lem6  29835  wwlksm1edg  29901  wwlksnred  29912  clwlkclwwlklem2fv1  30014  clwlkclwwlklem2  30019  clwwisshclwwslem  30033  clwwlkinwwlk  30059  clwwlkf  30066  clwwlkext2edg  30075  wwlksubclwwlk  30077  frgrreggt1  30412  ssnnssfz  32789  ccatdmss  32934  chnub  33002  cycpmco2lem6  33151  ballotlemsdom  34514  ballotlemsel1i  34515  ballotlemfrceq  34531  signstfvc  34589  signstfveq0  34592  prodfzo03  34618  erdszelem8  35203  climuzcnv  35676  poimirlem6  37633  fdc  37752  sticksstones12  42159  eluzp1  42341  fimgmcyc  42544  eldioph2lem1  42771  hbt  43142  ssinc  45092  ssdec  45093  monoords  45309  fzdifsuc2  45322  eluzd  45420  fmul01lt1lem2  45600  sumnnodd  45645  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnmul  45958  dvnprodlem2  45962  itgspltprt  45994  stoweidlem11  46026  stoweidlem26  46041  wallispilem4  46083  fourierdlem12  46134  fourierdlem20  46142  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem54  46175  fourierdlem79  46200  fourierdlem102  46223  fourierdlem111  46232  fourierdlem114  46235  etransclem23  46272  etransclem48  46297  caratheodorylem1  46541  smfmullem4  46809  eluzge0nn0  47324  ssfz12  47326  elfzlble  47332  fzopredsuc  47335  addmodne  47346  m1modnep2mod  47354  iccpartipre  47408  iccpartiltu  47409  iccpartgt  47414  fmtnoge3  47517  odz2prm2pw  47550  fmtnoprmfac2lem1  47553  fmtno4prmfac  47559  31prm  47584  lighneallem4b  47596  341fppr2  47721  9fppr8  47724  fpprel2  47728  nfermltl8rev  47729  nfermltl2rev  47730  gbegt5  47748  gbowgt5  47749  sbgoldbm  47771  mogoldbb  47772  sbgoldbo  47774  nnsum3primesle9  47781  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  evengpop3  47785  evengpoap3  47786  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  bgoldbtbndlem3  47794  tgblthelfgott  47802  gpgusgralem  48011  ceilhalfelfzo1  48016  gpgedgvtx1  48020  gpg5nbgrvtx13starlem2  48028  gpg3nbgrvtx0  48032  gpg3nbgrvtx0ALT  48033  gpg5nbgr3star  48037  gpg3kgrtriexlem3  48041  gpg3kgrtriexlem6  48044  cznnring  48178  ssnn0ssfz  48265  elfzolborelfzop1  48436  m1modmmod  48442  rege1logbzge0  48480  fllog2  48489  nnolog2flm1  48511  dignn0ldlem  48523