Theorem eluz2 9760

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 9759	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		simp1 1023	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ)
3		eluz1 9758	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
4		ibar 301	. . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
5	3, 4	bitrd 188	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))))
6		3anass 1008	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
7	5, 6	bitr4di 198	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
8	1, 2, 7	pm5.21nii 711	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))

Syntax hints:   ∧ wa 104   ↔ wb 105   ∧ w3a 1004   ∈ wcel 2202   class class class wbr 4088  ‘cfv 5326   ≤ cle 8214  ℤcz 9478  ℤ_≥cuz 9754

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-cnex 8122  ax-resscn 8123

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-mpt 4152  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-fv 5334  df-ov 6020  df-neg 8352  df-z 9479  df-uz 9755

This theorem is referenced by:  eluzmn  9761  eluzuzle  9763  eluzelz  9764  eluzle  9767  uztrn  9772  eluzp1p1  9781  uznn0sub  9787  5eluz3  9794  uz3m2nn  9806  1eluzge0  9807  2eluzge1  9809  raluz2  9812  rexuz2  9814  peano2uz  9816  nn0pzuz  9820  uzind4  9821  nn0ge2m1nnALT  9851  elfzuzb  10253  uzsubsubfz  10281  ige2m1fz  10344  4fvwrd4  10374  elfzo2  10384  elfzouz2  10396  fzossrbm1  10409  fzossfzop1  10456  ssfzo12bi  10469  elfzonelfzo  10474  elfzomelpfzo  10475  fzosplitprm1  10479  fzostep1  10482  fzind2  10484  suprzubdc  10495  zsupssdc  10497  flqword2  10548  fldiv4p1lem1div2  10564  uzennn  10697  xnn0nnen  10698  seq3split  10749  iseqf1olemqk  10768  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seq3f1olemqsum  10774  bcval5  11024  seq3coll  11105  swrdsbslen  11246  swrdspsleq  11247  pfxtrcfv0  11274  pfxtrcfvl  11277  pfxccatin12lem2a  11307  seq3shft  11398  resqrexlemoverl  11581  resqrexlemga  11583  fsum3cvg3  11956  fisumrev2  12006  isumshft  12050  cvgratnnlemseq  12086  cvgratnnlemabsle  12087  cvgratnnlemsumlt  12088  cvgratz  12092  oddge22np1  12441  nn0o  12467  bitsmod  12516  uzwodc  12607  dvdsnprmd  12696  prmgt1  12703  oddprmgt2  12705  oddprmge3  12706  prm23ge5  12836  nninfdclemcl  13068  nninfdclemp1  13070  nninfdclemlt  13071  strleund  13185  strleun  13186  gsumfzz  13577  gsumfzcl  13581  gsumfzreidx  13923  gsumfzsubmcl  13924  gsumfzmptfidmadd  13925  gsumfzmhm  13929  gsumfzfsum  14601  znidomb  14671  plyaddlem1  15470  2logb9irr  15694  2logb9irrap  15700  lgsdilem2  15764  gausslemma2dlem2  15790  gausslemma2dlem4  15792  gausslemma2dlem5  15794  gausslemma2dlem6  15795  lgsquadlem1  15805  lgsquadlem3  15807  2lgslem1  15819  clwwlkext2edg  16272  trlsegvdeglem6  16315  gsumgfsumlem  16683  gsumgfsum  16684