Theorem eluz2 9684

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

Syntax hints:   ∧ wa 104   ↔ wb 105   ∧ w3a 981   ∈ wcel 2177   class class class wbr 4054  ‘cfv 5285   ≤ cle 8138  ℤcz 9402  ℤ_≥cuz 9678

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4173  ax-pow 4229  ax-pr 4264  ax-cnex 8046  ax-resscn 8047

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-rab 2494  df-v 2775  df-sbc 3003  df-un 3174  df-in 3176  df-ss 3183  df-pw 3623  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3860  df-br 4055  df-opab 4117  df-mpt 4118  df-id 4353  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-iota 5246  df-fun 5287  df-fn 5288  df-f 5289  df-fv 5293  df-ov 5965  df-neg 8276  df-z 9403  df-uz 9679

This theorem is referenced by:  eluzuzle  9686  eluzelz  9687  eluzle  9690  uztrn  9695  eluzp1p1  9704  uznn0sub  9710  uz3m2nn  9724  1eluzge0  9725  2eluzge1  9727  raluz2  9730  rexuz2  9732  peano2uz  9734  nn0pzuz  9738  uzind4  9739  nn0ge2m1nnALT  9769  elfzuzb  10171  uzsubsubfz  10199  ige2m1fz  10262  4fvwrd4  10292  elfzo2  10302  elfzouz2  10314  fzossrbm1  10327  fzossfzop1  10373  ssfzo12bi  10386  elfzonelfzo  10391  elfzomelpfzo  10392  fzosplitprm1  10395  fzostep1  10398  fzind2  10400  suprzubdc  10411  zsupssdc  10413  flqword2  10464  fldiv4p1lem1div2  10480  uzennn  10613  xnn0nnen  10614  seq3split  10665  iseqf1olemqk  10684  seq3f1olemqsumkj  10688  seq3f1olemqsumk  10689  seq3f1olemqsum  10690  bcval5  10940  seq3coll  11019  swrdsbslen  11152  swrdspsleq  11153  pfxtrcfv0  11180  pfxtrcfvl  11183  seq3shft  11234  resqrexlemoverl  11417  resqrexlemga  11419  fsum3cvg3  11792  fisumrev2  11842  isumshft  11886  cvgratnnlemseq  11922  cvgratnnlemabsle  11923  cvgratnnlemsumlt  11924  cvgratz  11928  oddge22np1  12277  nn0o  12303  bitsmod  12352  uzwodc  12443  dvdsnprmd  12532  prmgt1  12539  oddprmgt2  12541  oddprmge3  12542  prm23ge5  12672  nninfdclemcl  12904  nninfdclemp1  12906  nninfdclemlt  12907  strleund  13020  strleun  13021  gsumfzz  13412  gsumfzcl  13416  gsumfzreidx  13758  gsumfzsubmcl  13759  gsumfzmptfidmadd  13760  gsumfzmhm  13764  gsumfzfsum  14435  znidomb  14505  plyaddlem1  15304  2logb9irr  15528  2logb9irrap  15534  lgsdilem2  15598  gausslemma2dlem2  15624  gausslemma2dlem4  15626  gausslemma2dlem5  15628  gausslemma2dlem6  15629  lgsquadlem1  15639  lgsquadlem3  15641  2lgslem1  15653