Theorem eluz2 9739

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

Syntax hints:   ∧ wa 104   ↔ wb 105   ∧ w3a 1002   ∈ wcel 2200   class class class wbr 4083  ‘cfv 5318   ≤ cle 8193  ℤcz 9457  ℤ_≥cuz 9733

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-cnex 8101  ax-resscn 8102

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-opab 4146  df-mpt 4147  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-rn 4730  df-res 4731  df-ima 4732  df-iota 5278  df-fun 5320  df-fn 5321  df-f 5322  df-fv 5326  df-ov 6010  df-neg 8331  df-z 9458  df-uz 9734

This theorem is referenced by:  eluzmn  9740  eluzuzle  9742  eluzelz  9743  eluzle  9746  uztrn  9751  eluzp1p1  9760  uznn0sub  9766  uz3m2nn  9780  1eluzge0  9781  2eluzge1  9783  raluz2  9786  rexuz2  9788  peano2uz  9790  nn0pzuz  9794  uzind4  9795  nn0ge2m1nnALT  9825  elfzuzb  10227  uzsubsubfz  10255  ige2m1fz  10318  4fvwrd4  10348  elfzo2  10358  elfzouz2  10370  fzossrbm1  10383  fzossfzop1  10430  ssfzo12bi  10443  elfzonelfzo  10448  elfzomelpfzo  10449  fzosplitprm1  10452  fzostep1  10455  fzind2  10457  suprzubdc  10468  zsupssdc  10470  flqword2  10521  fldiv4p1lem1div2  10537  uzennn  10670  xnn0nnen  10671  seq3split  10722  iseqf1olemqk  10741  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  bcval5  10997  seq3coll  11077  swrdsbslen  11213  swrdspsleq  11214  pfxtrcfv0  11241  pfxtrcfvl  11244  pfxccatin12lem2a  11274  seq3shft  11364  resqrexlemoverl  11547  resqrexlemga  11549  fsum3cvg3  11922  fisumrev2  11972  isumshft  12016  cvgratnnlemseq  12052  cvgratnnlemabsle  12053  cvgratnnlemsumlt  12054  cvgratz  12058  oddge22np1  12407  nn0o  12433  bitsmod  12482  uzwodc  12573  dvdsnprmd  12662  prmgt1  12669  oddprmgt2  12671  oddprmge3  12672  prm23ge5  12802  nninfdclemcl  13034  nninfdclemp1  13036  nninfdclemlt  13037  strleund  13151  strleun  13152  gsumfzz  13543  gsumfzcl  13547  gsumfzreidx  13889  gsumfzsubmcl  13890  gsumfzmptfidmadd  13891  gsumfzmhm  13895  gsumfzfsum  14567  znidomb  14637  plyaddlem1  15436  2logb9irr  15660  2logb9irrap  15666  lgsdilem2  15730  gausslemma2dlem2  15756  gausslemma2dlem4  15758  gausslemma2dlem5  15760  gausslemma2dlem6  15761  lgsquadlem1  15771  lgsquadlem3  15773  2lgslem1  15785