Theorem eluz2 11929

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 11928	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1159	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 11927	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 520	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 270	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1109	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	syl6bbr 280	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 369	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ↔ wb 197   ∧ wa 384   ∧ w3a 1100   ∈ wcel 2157   class class class wbr 4855  ‘cfv 6110   ≤ cle 10369  ℤcz 11662  ℤ_≥cuz 11923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-cnex 10286  ax-resscn 10287

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-sbc 3645  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-opab 4918  df-mpt 4935  df-id 5232  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-iota 6073  df-fun 6112  df-fn 6113  df-f 6114  df-fv 6118  df-ov 6886  df-neg 10563  df-z 11663  df-uz 11924

This theorem is referenced by:  eluzmn  11930  eluzuzle  11932  eluzelz  11933  eluzle  11936  uztrn  11940  eluzp1p1  11949  subeluzsub  11954  uzm1  11955  uznn0sub  11956  uz3m2nn  11968  1eluzge0  11969  2eluzge1  11971  raluz2  11974  rexuz2  11976  peano2uz  11978  nn0pzuz  11982  uzind4  11983  uzinfi  12006  zsupss  12015  nn01to3  12019  nn0ge2m1nnALT  12020  elfzuzb  12578  uzsubsubfz  12605  ssfzunsnext  12628  ssfzunsn  12629  ige2m1fz  12672  4fvwrd4  12702  elfzo2  12716  elfzouz2  12727  fzossrbm1  12740  fzossfzop1  12789  ssfzo12bi  12806  elfzonelfzo  12813  elfzomelpfzo  12815  fzosplitprm1  12821  fzostep1  12827  fzind2  12829  flword2  12857  fldiv4p1lem1div2  12879  uzsup  12905  modaddmodup  12976  fzsdom2  13451  swrdtrcfv0  13685  swrdsbslen  13691  swrdspsleq  13692  swrdtrcfvl  13693  swrdccatin12lem2a  13728  cshwidxmod  13792  rexuzre  14334  limsupgre  14454  rlimclim1  14518  rlimclim  14519  climrlim2  14520  isercolllem1  14637  isercoll  14640  climcndslem1  14822  fallfacval4  15013  oddge22np1  15312  nn0o  15338  bitsmod  15396  smueqlem  15450  dvdsnprmd  15640  prmgt1  15646  oddprmgt2  15648  oddprmge3  15649  modprm0  15746  prm23ge5  15756  vdwlem9  15929  prmgaplem3  15993  prmgaplem5  15995  prmgaplem6  15996  prmgaplem7  15997  setsstruct  16128  strlemor1OLD  16199  strleun  16202  fislw  18260  efgsp1  18370  efgredleme  18376  lt6abl  18516  telgsumfzs  18607  ablfac1eu  18693  znidomb  20136  chfacfscmul0  20896  chfacfscmulfsupp  20897  chfacfpmmul0  20900  chfacfpmmulfsupp  20901  dvfsumlem1  24025  dvfsumlem3  24027  plyaddlem1  24205  coeidlem  24229  ppisval  25066  chtdif  25120  ppidif  25125  ppiublem1  25163  ppiub  25165  chtub  25173  lgsdilem2  25294  gausslemma2dlem2  25328  gausslemma2dlem4  25330  gausslemma2dlem5  25332  gausslemma2dlem6  25333  lgsquadlem1  25341  lgsquadlem3  25343  2lgslem1  25355  chebbnd1lem1  25394  chebbnd1lem2  25395  chebbnd1lem3  25396  dchrisumlem2  25415  dchrvmasumiflem1  25426  mulog2sumlem2  25460  logdivbnd  25481  pntlemg  25523  pntlemq  25526  pntlemf  25530  axlowdim  26077  pthdlem1  26912  crctcshwlkn0lem3  26955  crctcshwlkn0lem4  26956  crctcshwlkn0lem5  26957  crctcshwlkn0lem6  26958  wwlksm1edg  27030  wwlksnred  27051  clwlkclwwlklem2fv1  27160  clwlkclwwlklem2  27165  clwwisshclwwslem  27179  clwwlkinwwlk  27211  clwwlkf  27218  clwwlkext2edg  27228  wwlksubclwwlk  27231  clwlksfclwwlkOLD  27258  frgrreggt1  27603  ssnnssfz  29898  ballotlemsdom  30920  ballotlemsel1i  30921  ballotlemfrceq  30937  signstfvc  30998  signstfveq0  31001  prodfzo03  31028  erdszelem8  31524  climuzcnv  31908  poimirlem6  33746  fdc  33870  eldioph2lem1  37842  hbt  38218  ssinc  39774  ssdec  39775  monoords  40009  fzdifsuc2  40022  eluzd  40131  fmul01lt1lem2  40314  sumnnodd  40359  ioodvbdlimc1lem2  40644  ioodvbdlimc2lem  40646  dvnmul  40655  dvnprodlem2  40659  itgspltprt  40691  stoweidlem11  40724  stoweidlem26  40739  wallispilem4  40781  fourierdlem12  40832  fourierdlem20  40840  fourierdlem41  40861  fourierdlem48  40867  fourierdlem49  40868  fourierdlem50  40869  fourierdlem54  40873  fourierdlem79  40898  fourierdlem102  40921  fourierdlem111  40930  fourierdlem114  40933  etransclem23  40970  etransclem48  40995  caratheodorylem1  41239  smfmullem4  41500  eluzge0nn0  41914  ssfz12  41916  elfzlble  41922  fzopredsuc  41925  fzoopth  41929  iccpartipre  41949  iccpartiltu  41950  iccpartgt  41955  pfxtrcfv0  41994  pfxtrcfvl  41997  fmtnoge3  42034  odz2prm2pw  42067  fmtnoprmfac2lem1  42070  fmtno4prmfac  42076  31prm  42104  lighneallem4b  42118  gbegt5  42241  gbowgt5  42242  sbgoldbm  42264  mogoldbb  42265  sbgoldbo  42267  nnsum3primesle9  42274  nnsum4primesodd  42276  nnsum4primesoddALTV  42277  evengpop3  42278  evengpoap3  42279  nnsum4primeseven  42280  nnsum4primesevenALTV  42281  wtgoldbnnsum4prm  42282  bgoldbnnsum3prm  42284  bgoldbtbndlem3  42287  tgblthelfgott  42295  cznnring  42541  ssnn0ssfz  42712  elfzolborelfzop1  42894  m1modmmod  42901  rege1logbzge0  42938  fllog2  42947  nnolog2flm1  42969  dignn0ldlem  42981