# Metamath Proof Explorer

## Theorem eluz2

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 M e. ZZ . (Contributed by NM, 5-Sep-2005) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion eluz2 ${⊢}{N}\in {ℤ}_{\ge {M}}↔\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}\le {N}\right)$

### Proof

Step Hyp Ref Expression
1 eluzel2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
2 simp1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}\le {N}\right)\to {M}\in ℤ$
3 eluz1 ${⊢}{M}\in ℤ\to \left({N}\in {ℤ}_{\ge {M}}↔\left({N}\in ℤ\wedge {M}\le {N}\right)\right)$
4 ibar ${⊢}{M}\in ℤ\to \left(\left({N}\in ℤ\wedge {M}\le {N}\right)↔\left({M}\in ℤ\wedge \left({N}\in ℤ\wedge {M}\le {N}\right)\right)\right)$
5 3 4 bitrd ${⊢}{M}\in ℤ\to \left({N}\in {ℤ}_{\ge {M}}↔\left({M}\in ℤ\wedge \left({N}\in ℤ\wedge {M}\le {N}\right)\right)\right)$
6 3anass ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}\le {N}\right)↔\left({M}\in ℤ\wedge \left({N}\in ℤ\wedge {M}\le {N}\right)\right)$
7 5 6 syl6bbr ${⊢}{M}\in ℤ\to \left({N}\in {ℤ}_{\ge {M}}↔\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}\le {N}\right)\right)$
8 1 2 7 pm5.21nii ${⊢}{N}\in {ℤ}_{\ge {M}}↔\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}\le {N}\right)$