Theorem eluz2 12845

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 12844	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1149	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 12843	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 536	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 281	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1106	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 291	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 380	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ↔ wb 208   ∧ wa 399   ∧ w3a 1098   ∈ wcel 2142   class class class wbr 5100  ‘cfv 6521   ≤ cle 11217  ℤcz 12568  ℤ_≥cuz 12839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-cnex 11129  ax-resscn 11130

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-fv 6529  df-ov 7399  df-neg 11417  df-z 12569  df-uz 12840

This theorem is referenced by:  eluzmn  12846  eluzuzle  12848  eluzelz  12849  eluzle  12852  uztrn  12857  eluzp1p1  12867  eluzadd  12868  eluzsub  12869  subeluzsub  12872  uzm1  12873  uznn0sub  12874  1eluzge0  12881  2eluzge1  12883  5eluz3  12884  uz3m2nn  12895  raluz2  12898  rexuz2  12900  peano2uz  12902  nn0pzuz  12906  uzind4  12907  uzinfi  12929  zsupss  12938  nn01to3  12942  nn0ge2m1nnALT  12943  elfzuzb  13523  uzsubsubfz  13551  ssfzunsn  13575  ige2m1fz  13622  fz0to4untppr  13635  fz0to5un2tp  13636  4fvwrd4  13653  elfzo2  13667  elfzouz2  13680  fzossrbm1  13694  fzossfzop1  13749  ssfzo12bi  13767  fzoopth  13768  elfzonelfzo  13775  elfzomelpfzo  13778  fzosplitprm1  13784  fzostep1  13792  fzind2  13794  flword2  13823  fldiv4p1lem1div2  13845  uzsup  13873  modaddmodup  13947  fzsdom2  14441  ccatdmss  14595  swrdsbslen  14678  swrdspsleq  14679  pfxtrcfv0  14707  pfxtrcfvl  14710  pfxccatin12lem2a  14740  cshwidxmod  14816  rexuzre  15380  limsupgre  15508  rlimclim1  15572  rlimclim  15573  climrlim2  15574  isercolllem1  15692  isercoll  15695  climcndslem1  15879  fallfacval4  16073  oddge22np1  16383  nn0o  16417  bitsmod  16470  smueqlem  16524  dvdsnprmd  16724  2mulprm  16727  oddprmgt2  16734  oddprmge3  16735  ge2nprmge4  16736  modprm0  16841  prm23ge5  16851  vdwlem9  17025  prmgaplem3  17089  prmgaplem5  17091  prmgaplem6  17092  prmgaplem7  17093  strleun  17193  setsstruct  17212  chnub  18654  fislw  19665  efgsp1  19777  efgredleme  19783  lt6abl  19935  telgsumfzs  20029  ablfac1eu  20115  znidomb  21613  chfacfscmul0  22918  chfacfscmulfsupp  22919  chfacfpmmul0  22922  chfacfpmmulfsupp  22923  dvfsumlem1  26088  dvfsumlem3  26090  plyaddlem1  26273  coeidlem  26297  2logb9irr  26860  ppisval  27168  chtdif  27222  ppidif  27227  ppiublem1  27266  ppiub  27268  chtub  27276  lgsdilem2  27397  gausslemma2dlem2  27431  gausslemma2dlem4  27433  gausslemma2dlem5  27435  gausslemma2dlem6  27436  lgsquadlem1  27444  lgsquadlem3  27446  2lgslem1  27458  chebbnd1lem1  27533  chebbnd1lem2  27534  chebbnd1lem3  27535  dchrisumlem2  27554  dchrvmasumiflem1  27565  mulog2sumlem2  27599  logdivbnd  27620  pntlemg  27662  pntlemq  27665  pntlemf  27669  axlowdim  29162  pthdlem1  29966  crctcshwlkn0lem3  30012  crctcshwlkn0lem4  30013  crctcshwlkn0lem5  30014  crctcshwlkn0lem6  30015  wwlksm1edg  30081  wwlksnred  30092  clwlkclwwlklem2fv1  30197  clwlkclwwlklem2  30202  clwwisshclwwslem  30216  clwwlkinwwlk  30242  clwwlkf  30249  clwwlkext2edg  30258  wwlksubclwwlk  30260  frgrreggt1  30595  ssnnssfz  32989  cycpmco2lem6  33311  ballotlemsdom  34809  ballotlemsel1i  34810  ballotlemfrceq  34826  signstfvc  34868  signstfveq0  34871  prodfzo03  34897  erdszelem8  35548  climuzcnv  36021  poimirlem6  38125  fdc  38244  sticksstones12  42775  eluzp1  42916  fimgmcyc  43152  eldioph2lem1  43341  hbt  43707  ssinc  45665  ssdec  45666  monoords  45876  fzdifsuc2  45889  eluzd  45983  fmul01lt1lem2  46161  sumnnodd  46206  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  dvnmul  46517  dvnprodlem2  46521  itgspltprt  46553  stoweidlem11  46585  stoweidlem26  46600  wallispilem4  46642  fourierdlem12  46693  fourierdlem20  46701  fourierdlem41  46722  fourierdlem50  46730  fourierdlem54  46734  fourierdlem79  46759  fourierdlem102  46782  fourierdlem111  46791  fourierdlem114  46794  etransclem23  46831  etransclem48  46856  caratheodorylem1  47100  smfmullem4  47368  eluzge0nn0  47906  ssfz12  47908  elfzlble  47914  fzopredsuc  47918  ceilhalfelfzo1  47928  addmodne  47944  m1modnep2mod  47952  m1modmmod  47958  modm2nep1  47966  modp2nep1  47967  modm1nep2  47968  modm1nem2  47969  modm1p1ne  47970  2timesltsqm1  47973  muldvdsfacgt  47980  muldvdsfacm1  47981  iccpartipre  48027  iccpartiltu  48028  iccpartgt  48033  fmtnoge3  48139  odz2prm2pw  48172  fmtnoprmfac2lem1  48175  fmtno4prmfac  48181  31prm  48206  lighneallem4b  48218  nprmdvdsfacm1lem2  48230  nprmdvdsfacm1lem3  48231  nprmdvdsfacm1lem4  48232  nprmdvdsfacm1  48233  ppivalnnnprmge6  48235  341fppr2  48356  9fppr8  48359  fpprel2  48363  nfermltl8rev  48364  nfermltl2rev  48365  gbegt5  48383  gbowgt5  48384  sbgoldbm  48406  mogoldbb  48407  sbgoldbo  48409  nnsum3primesle9  48416  nnsum4primesodd  48418  nnsum4primesoddALTV  48419  evengpop3  48420  evengpoap3  48421  nnsum4primeseven  48422  nnsum4primesevenALTV  48423  wtgoldbnnsum4prm  48424  bgoldbnnsum3prm  48426  bgoldbtbndlem3  48429  tgblthelfgott  48437  gpgusgralem  48678  gpgedgvtx1  48684  gpg5nbgrvtx13starlem2  48694  gpg3nbgrvtx0  48698  gpg3nbgrvtx0ALT  48699  gpg5nbgr3star  48703  gpg3kgrtriexlem3  48707  gpg3kgrtriexlem6  48710  gpg5edgnedg  48752  cznnring  48884  ssnn0ssfz  48971  elfzolborelfzop1  49141  rege1logbzge0  49181  fllog2  49190  nnolog2flm1  49212  dignn0ldlem  49224