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 1154	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12882	. . . 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 5111  ‘cfv 6540   ≤ cle 11259  ℤcz 12606  ℤ_≥cuz 12878

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-cnex 11171  ax-resscn 11172

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7422  df-neg 11459  df-z 12607  df-uz 12879

This theorem is used by:  eluzmn  12885  eluzuzle  12887  eluzelz  12888  eluzle  12891  uztrn  12896  eluzp1p1  12906  eluzadd  12907  eluzsub  12908  subeluzsub  12911  uzm1  12912  uznn0sub  12913  1eluzge0  12920  2eluzge1  12922  5eluz3  12923  uz3m2nn  12934  raluz2  12937  rexuz2  12939  peano2uz  12941  nn0pzuz  12945  uzind4  12946  uzinfi  12968  zsupss  12977  nn01to3  12981  nn0ge2m1nnALT  12982  elfzuzb  13562  uzsubsubfz  13591  ssfzunsn  13615  ige2m1fz  13662  fz0to4untppr  13675  fz0to5un2tp  13676  4fvwrd4  13693  elfzo2  13707  elfzouz2  13720  fzossrbm1  13734  fzossfzop1  13789  ssfzo12bi  13807  fzoopth  13808  elfzonelfzo  13815  elfzomelpfzo  13818  fzosplitprm1  13824  fzostep1  13832  fzind2  13834  flword2  13864  fldiv4p1lem1div2  13886  uzsup  13914  modaddmodup  13988  fzsdom2  14483  ccatdmss  14637  swrdsbslen  14724  swrdspsleq  14725  pfxtrcfv0  14753  pfxtrcfvl  14756  pfxccatin12lem2a  14786  cshwidxmod  14864  rexuzre  15428  limsupgre  15556  rlimclim1  15620  rlimclim  15621  climrlim2  15622  isercolllem1  15740  isercoll  15743  climcndslem1  15926  fallfacval4  16119  oddge22np1  16429  nn0o  16463  bitsmod  16516  smueqlem  16570  dvdsnprmd  16770  2mulprm  16773  oddprmgt2  16780  oddprmge3  16781  ge2nprmge4  16782  modprm0  16887  prm23ge5  16897  vdwlem9  17071  prmgaplem3  17135  prmgaplem5  17137  prmgaplem6  17138  prmgaplem7  17139  strleun  17239  setsstruct  17258  chnub  18700  fislw  19739  efgsp1  19851  efgredleme  19857  lt6abl  20009  telgsumfzs  20103  ablfac1eu  20189  znidomb  21761  chfacfscmul0  23065  chfacfscmulfsupp  23066  chfacfpmmul0  23069  chfacfpmmulfsupp  23070  dvfsumlem1  26236  dvfsumlem3  26238  plyaddlem1  26421  coeidlem  26445  2logb9irr  27011  ppisval  27319  chtdif  27373  ppidif  27378  ppiublem1  27417  ppiub  27419  chtub  27427  lgsdilem2  27548  gausslemma2dlem2  27582  gausslemma2dlem4  27584  gausslemma2dlem5  27586  gausslemma2dlem6  27587  lgsquadlem1  27595  lgsquadlem3  27597  2lgslem1  27609  chebbnd1lem1  27684  chebbnd1lem2  27685  chebbnd1lem3  27686  dchrisumlem2  27705  dchrvmasumiflem1  27716  mulog2sumlem2  27750  logdivbnd  27771  pntlemg  27813  pntlemq  27816  pntlemf  27820  axlowdim  29366  pthdlem1  30179  crctcshwlkn0lem3  30228  crctcshwlkn0lem4  30229  crctcshwlkn0lem5  30230  crctcshwlkn0lem6  30231  wwlksm1edg  30297  wwlksnred  30308  clwlkclwwlklem2fv1  30413  clwlkclwwlklem2  30418  clwwisshclwwslem  30432  clwwlkinwwlk  30458  clwwlkf  30465  clwwlkext2edg  30474  wwlksubclwwlk  30476  frgrreggt1  30815  ssnnssfz  33202  cycpmco2lem6  33515  ballotlemsdom  34967  ballotlemsel1i  34968  ballotlemfrceq  34984  signstfvc  35026  signstfveq0  35029  prodfzo03  35055  erdszelem8  35727  climuzcnv  36200  poimirlem6  38334  fdc  38454  sticksstones12  42983  eluzp1  43126  fimgmcyc  43360  eldioph2lem1  43549  hbt  43915  ssinc  45863  ssdec  45864  monoords  46074  fzdifsuc2  46087  eluzd  46181  fmul01lt1lem2  46359  sumnnodd  46404  ioodvbdlimc1lem2  46704  ioodvbdlimc2lem  46706  dvnmul  46715  dvnprodlem2  46719  itgspltprt  46751  stoweidlem11  46783  stoweidlem26  46798  wallispilem4  46840  fourierdlem12  46891  fourierdlem20  46899  fourierdlem41  46920  fourierdlem50  46928  fourierdlem54  46932  fourierdlem79  46957  fourierdlem102  46980  fourierdlem111  46989  fourierdlem114  46992  etransclem23  47029  etransclem48  47054  caratheodorylem1  47298  smfmullem4  47566  eluzge0nn0  48107  ssfz12  48109  elfzlble  48115  fzopredsuc  48119  ceilhalfelfzo1  48129  addmodne  48145  m1modnep2mod  48153  m1modmmod  48159  modm2nep1  48167  modp2nep1  48168  modm1nep2  48169  modm1nem2  48170  modm1p1ne  48171  2timesltsqm1  48174  muldvdsfacgt  48181  muldvdsfacm1  48182  iccpartipre  48228  iccpartiltu  48229  iccpartgt  48234  fmtnoge3  48340  odz2prm2pw  48373  fmtnoprmfac2lem1  48376  fmtno4prmfac  48382  31prm  48407  lighneallem4b  48419  nprmdvdsfacm1lem2  48431  nprmdvdsfacm1lem3  48432  nprmdvdsfacm1lem4  48433  nprmdvdsfacm1  48434  ppivalnnnprmge6  48436  341fppr2  48557  9fppr8  48560  fpprel2  48564  nfermltl8rev  48565  nfermltl2rev  48566  gbegt5  48584  gbowgt5  48585  sbgoldbm  48607  mogoldbb  48608  sbgoldbo  48610  nnsum3primesle9  48617  nnsum4primesodd  48619  nnsum4primesoddALTV  48620  evengpop3  48621  evengpoap3  48622  nnsum4primeseven  48623  nnsum4primesevenALTV  48624  wtgoldbnnsum4prm  48625  bgoldbnnsum3prm  48627  bgoldbtbndlem3  48630  tgblthelfgott  48638  gpgusgralem  48879  gpgedgvtx1  48885  gpg5nbgrvtx13starlem2  48895  gpg3nbgrvtx0  48899  gpg3nbgrvtx0ALT  48900  gpg5nbgr3star  48904  gpg3kgrtriexlem3  48908  gpg3kgrtriexlem6  48911  gpg5edgnedg  48953  cznnring  49084  ssnn0ssfz  49186  elfzolborelfzop1  49356  rege1logbzge0  49396  fllog2  49405  nnolog2flm1  49427  dignn0ldlem  49439