Theorem eluz2 12881

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 12880	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1135	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12879	. . . 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 2105   class class class wbr 5147  ‘cfv 6562   ≤ cle 11293  ℤcz 12610  ℤ_≥cuz 12875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-cnex 11208  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433  df-neg 11492  df-z 12611  df-uz 12876

This theorem is referenced by:  eluzmn  12882  eluzuzle  12884  eluzelz  12885  eluzle  12888  uztrn  12893  eluzp1p1  12903  eluzadd  12904  eluzsub  12905  subeluzsub  12912  uzm1  12913  uznn0sub  12914  5eluz3  12924  uz3m2nn  12930  1eluzge0  12931  2eluzge1  12933  raluz2  12936  rexuz2  12938  peano2uz  12940  nn0pzuz  12944  uzind4  12945  uzinfi  12967  zsupss  12976  nn01to3  12980  nn0ge2m1nnALT  12981  elfzuzb  13554  uzsubsubfz  13582  ssfzunsn  13606  ige2m1fz  13653  fz0to4untppr  13666  fz0to5un2tp  13667  4fvwrd4  13684  elfzo2  13698  elfzouz2  13710  fzossrbm1  13724  fzossfzop1  13778  ssfzo12bi  13796  fzoopth  13797  elfzonelfzo  13804  elfzomelpfzo  13806  fzosplitprm1  13812  fzostep1  13818  fzind2  13820  flword2  13849  fldiv4p1lem1div2  13871  uzsup  13899  modaddmodup  13971  fzsdom2  14463  swrdsbslen  14698  swrdspsleq  14699  pfxtrcfv0  14728  pfxtrcfvl  14731  pfxccatin12lem2a  14761  cshwidxmod  14837  rexuzre  15387  limsupgre  15513  rlimclim1  15577  rlimclim  15578  climrlim2  15579  isercolllem1  15697  isercoll  15700  climcndslem1  15881  fallfacval4  16075  oddge22np1  16382  nn0o  16416  bitsmod  16469  smueqlem  16523  dvdsnprmd  16723  2mulprm  16726  oddprmgt2  16732  oddprmge3  16733  ge2nprmge4  16734  modprm0  16838  prm23ge5  16848  vdwlem9  17022  prmgaplem3  17086  prmgaplem5  17088  prmgaplem6  17089  prmgaplem7  17090  strleun  17190  setsstruct  17209  fislw  19657  efgsp1  19769  efgredleme  19775  lt6abl  19927  telgsumfzs  20021  ablfac1eu  20107  znidomb  21597  chfacfscmul0  22879  chfacfscmulfsupp  22880  chfacfpmmul0  22883  chfacfpmmulfsupp  22884  dvfsumlem1  26080  dvfsumlem3  26083  plyaddlem1  26266  coeidlem  26290  2logb9irr  26852  ppisval  27161  chtdif  27215  ppidif  27220  ppiublem1  27260  ppiub  27262  chtub  27270  lgsdilem2  27391  gausslemma2dlem2  27425  gausslemma2dlem4  27427  gausslemma2dlem5  27429  gausslemma2dlem6  27430  lgsquadlem1  27438  lgsquadlem3  27440  2lgslem1  27452  chebbnd1lem1  27527  chebbnd1lem2  27528  chebbnd1lem3  27529  dchrisumlem2  27548  dchrvmasumiflem1  27559  mulog2sumlem2  27593  logdivbnd  27614  pntlemg  27656  pntlemq  27659  pntlemf  27663  axlowdim  28990  pthdlem1  29798  crctcshwlkn0lem3  29841  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  crctcshwlkn0lem6  29844  wwlksm1edg  29910  wwlksnred  29921  clwlkclwwlklem2fv1  30023  clwlkclwwlklem2  30028  clwwisshclwwslem  30042  clwwlkinwwlk  30068  clwwlkf  30075  clwwlkext2edg  30084  wwlksubclwwlk  30086  frgrreggt1  30421  ssnnssfz  32795  ccatdmss  32918  chnub  32985  cycpmco2lem6  33133  ballotlemsdom  34492  ballotlemsel1i  34493  ballotlemfrceq  34509  signstfvc  34567  signstfveq0  34570  prodfzo03  34596  erdszelem8  35182  climuzcnv  35655  poimirlem6  37612  fdc  37731  sticksstones12  42139  eluzp1  42319  fimgmcyc  42520  eldioph2lem1  42747  hbt  43118  ssinc  45026  ssdec  45027  monoords  45247  fzdifsuc2  45260  eluzd  45358  fmul01lt1lem2  45540  sumnnodd  45585  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnmul  45898  dvnprodlem2  45902  itgspltprt  45934  stoweidlem11  45966  stoweidlem26  45981  wallispilem4  46023  fourierdlem12  46074  fourierdlem20  46082  fourierdlem41  46103  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem54  46115  fourierdlem79  46140  fourierdlem102  46163  fourierdlem111  46172  fourierdlem114  46175  etransclem23  46212  etransclem48  46237  caratheodorylem1  46481  smfmullem4  46749  eluzge0nn0  47261  ssfz12  47263  elfzlble  47269  fzopredsuc  47272  addmodne  47283  m1modnep2mod  47291  iccpartipre  47345  iccpartiltu  47346  iccpartgt  47351  fmtnoge3  47454  odz2prm2pw  47487  fmtnoprmfac2lem1  47490  fmtno4prmfac  47496  31prm  47521  lighneallem4b  47533  341fppr2  47658  9fppr8  47661  fpprel2  47665  nfermltl8rev  47666  nfermltl2rev  47667  gbegt5  47685  gbowgt5  47686  sbgoldbm  47708  mogoldbb  47709  sbgoldbo  47711  nnsum3primesle9  47718  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  evengpop3  47722  evengpoap3  47723  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  bgoldbtbndlem3  47731  tgblthelfgott  47739  gpgusgralem  47945  ceilhalfelfzo1  47950  gpgedgvtx1  47954  gpg5nbgrvtx13starlem2  47962  gpg3nbgrvtx0  47966  gpg3nbgrvtx0ALT  47967  gpg5nbgr3star  47971  cznnring  48105  ssnn0ssfz  48193  elfzolborelfzop1  48364  m1modmmod  48370  rege1logbzge0  48408  fllog2  48417  nnolog2flm1  48439  dignn0ldlem  48451