Theorem eluz2 12785

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 12784	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1142	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12783	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 533	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 280	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1100	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 290	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 379	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   ∈ wcel 2119   class class class wbr 5072  ‘cfv 6485   ≤ cle 11171  ℤcz 12515  ℤ_≥cuz 12779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493  df-ov 7359  df-neg 11371  df-z 12516  df-uz 12780

This theorem is referenced by:  eluzmn  12786  eluzuzle  12788  eluzelz  12789  eluzle  12792  uztrn  12797  eluzp1p1  12807  eluzadd  12808  eluzsub  12809  subeluzsub  12812  uzm1  12813  uznn0sub  12814  1eluzge0  12821  2eluzge1  12823  5eluz3  12824  uz3m2nn  12835  raluz2  12838  rexuz2  12840  peano2uz  12842  nn0pzuz  12846  uzind4  12847  uzinfi  12869  zsupss  12878  nn01to3  12882  nn0ge2m1nnALT  12883  elfzuzb  13463  uzsubsubfz  13491  ssfzunsn  13515  ige2m1fz  13562  fz0to4untppr  13575  fz0to5un2tp  13576  4fvwrd4  13593  elfzo2  13607  elfzouz2  13620  fzossrbm1  13634  fzossfzop1  13689  ssfzo12bi  13707  fzoopth  13708  elfzonelfzo  13715  elfzomelpfzo  13718  fzosplitprm1  13724  fzostep1  13732  fzind2  13734  flword2  13763  fldiv4p1lem1div2  13785  uzsup  13813  modaddmodup  13887  fzsdom2  14381  ccatdmss  14535  swrdsbslen  14618  swrdspsleq  14619  pfxtrcfv0  14647  pfxtrcfvl  14650  pfxccatin12lem2a  14680  cshwidxmod  14756  rexuzre  15306  limsupgre  15434  rlimclim1  15498  rlimclim  15499  climrlim2  15500  isercolllem1  15618  isercoll  15621  climcndslem1  15805  fallfacval4  15999  oddge22np1  16309  nn0o  16343  bitsmod  16396  smueqlem  16450  dvdsnprmd  16650  2mulprm  16653  oddprmgt2  16660  oddprmge3  16661  ge2nprmge4  16662  modprm0  16767  prm23ge5  16777  vdwlem9  16951  prmgaplem3  17015  prmgaplem5  17017  prmgaplem6  17018  prmgaplem7  17019  strleun  17118  setsstruct  17137  chnub  18579  fislw  19591  efgsp1  19703  efgredleme  19709  lt6abl  19861  telgsumfzs  19955  ablfac1eu  20041  znidomb  21536  chfacfscmul0  22841  chfacfscmulfsupp  22842  chfacfpmmul0  22845  chfacfpmmulfsupp  22846  dvfsumlem1  26011  dvfsumlem3  26013  plyaddlem1  26196  coeidlem  26220  2logb9irr  26777  ppisval  27085  chtdif  27139  ppidif  27144  ppiublem1  27183  ppiub  27185  chtub  27193  lgsdilem2  27314  gausslemma2dlem2  27348  gausslemma2dlem4  27350  gausslemma2dlem5  27352  gausslemma2dlem6  27353  lgsquadlem1  27361  lgsquadlem3  27363  2lgslem1  27375  chebbnd1lem1  27450  chebbnd1lem2  27451  chebbnd1lem3  27452  dchrisumlem2  27471  dchrvmasumiflem1  27482  mulog2sumlem2  27516  logdivbnd  27537  pntlemg  27579  pntlemq  27582  pntlemf  27586  axlowdim  29048  pthdlem1  29852  crctcshwlkn0lem3  29898  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  crctcshwlkn0lem6  29901  wwlksm1edg  29967  wwlksnred  29978  clwlkclwwlklem2fv1  30083  clwlkclwwlklem2  30088  clwwisshclwwslem  30102  clwwlkinwwlk  30128  clwwlkf  30135  clwwlkext2edg  30144  wwlksubclwwlk  30146  frgrreggt1  30481  ssnnssfz  32879  cycpmco2lem6  33212  ballotlemsdom  34696  ballotlemsel1i  34697  ballotlemfrceq  34713  signstfvc  34758  signstfveq0  34761  prodfzo03  34787  erdszelem8  35426  climuzcnv  35899  poimirlem6  37993  fdc  38112  sticksstones12  42643  eluzp1  42784  fimgmcyc  43020  eldioph2lem1  43209  hbt  43575  ssinc  45534  ssdec  45535  monoords  45745  fzdifsuc2  45758  eluzd  45852  fmul01lt1lem2  46030  sumnnodd  46075  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnmul  46386  dvnprodlem2  46390  itgspltprt  46422  stoweidlem11  46454  stoweidlem26  46469  wallispilem4  46511  fourierdlem12  46562  fourierdlem20  46570  fourierdlem41  46591  fourierdlem48  46597  fourierdlem49  46598  fourierdlem50  46599  fourierdlem54  46603  fourierdlem79  46628  fourierdlem102  46651  fourierdlem111  46660  fourierdlem114  46663  etransclem23  46700  etransclem48  46725  caratheodorylem1  46969  smfmullem4  47237  eluzge0nn0  47775  ssfz12  47777  elfzlble  47783  fzopredsuc  47787  ceilhalfelfzo1  47797  addmodne  47813  m1modnep2mod  47821  m1modmmod  47827  modm2nep1  47835  modp2nep1  47836  modm1nep2  47837  modm1nem2  47838  modm1p1ne  47839  2timesltsqm1  47842  muldvdsfacgt  47849  muldvdsfacm1  47850  iccpartipre  47896  iccpartiltu  47897  iccpartgt  47902  fmtnoge3  48008  odz2prm2pw  48041  fmtnoprmfac2lem1  48044  fmtno4prmfac  48050  31prm  48075  lighneallem4b  48087  nprmdvdsfacm1lem2  48099  nprmdvdsfacm1lem3  48100  nprmdvdsfacm1lem4  48101  nprmdvdsfacm1  48102  ppivalnnnprmge6  48104  341fppr2  48225  9fppr8  48228  fpprel2  48232  nfermltl8rev  48233  nfermltl2rev  48234  gbegt5  48252  gbowgt5  48253  sbgoldbm  48275  mogoldbb  48276  sbgoldbo  48278  nnsum3primesle9  48285  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  evengpop3  48289  evengpoap3  48290  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  bgoldbtbndlem3  48298  tgblthelfgott  48306  gpgusgralem  48547  gpgedgvtx1  48553  gpg5nbgrvtx13starlem2  48563  gpg3nbgrvtx0  48567  gpg3nbgrvtx0ALT  48568  gpg5nbgr3star  48572  gpg3kgrtriexlem3  48576  gpg3kgrtriexlem6  48579  gpg5edgnedg  48621  cznnring  48753  ssnn0ssfz  48840  elfzolborelfzop1  49010  rege1logbzge0  49050  fllog2  49059  nnolog2flm1  49081  dignn0ldlem  49093