# Metamath Proof Explorer

## Theorem eluzp1m1

Description: Membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005)

Ref Expression
Assertion eluzp1m1 ${⊢}\left({M}\in ℤ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {N}-1\in {ℤ}_{\ge {M}}$

### Proof

Step Hyp Ref Expression
1 peano2zm ${⊢}{N}\in ℤ\to {N}-1\in ℤ$
2 1 ad2antrl ${⊢}\left({M}\in ℤ\wedge \left({N}\in ℤ\wedge {M}+1\le {N}\right)\right)\to {N}-1\in ℤ$
3 zre ${⊢}{M}\in ℤ\to {M}\in ℝ$
4 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
5 1re ${⊢}1\in ℝ$
6 leaddsub ${⊢}\left({M}\in ℝ\wedge 1\in ℝ\wedge {N}\in ℝ\right)\to \left({M}+1\le {N}↔{M}\le {N}-1\right)$
7 5 6 mp3an2 ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left({M}+1\le {N}↔{M}\le {N}-1\right)$
8 3 4 7 syl2an ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}+1\le {N}↔{M}\le {N}-1\right)$
9 8 biimpa ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {M}+1\le {N}\right)\to {M}\le {N}-1$
10 9 anasss ${⊢}\left({M}\in ℤ\wedge \left({N}\in ℤ\wedge {M}+1\le {N}\right)\right)\to {M}\le {N}-1$
11 2 10 jca ${⊢}\left({M}\in ℤ\wedge \left({N}\in ℤ\wedge {M}+1\le {N}\right)\right)\to \left({N}-1\in ℤ\wedge {M}\le {N}-1\right)$
12 11 ex ${⊢}{M}\in ℤ\to \left(\left({N}\in ℤ\wedge {M}+1\le {N}\right)\to \left({N}-1\in ℤ\wedge {M}\le {N}-1\right)\right)$
13 peano2z ${⊢}{M}\in ℤ\to {M}+1\in ℤ$
14 eluz1 ${⊢}{M}+1\in ℤ\to \left({N}\in {ℤ}_{\ge \left({M}+1\right)}↔\left({N}\in ℤ\wedge {M}+1\le {N}\right)\right)$
15 13 14 syl ${⊢}{M}\in ℤ\to \left({N}\in {ℤ}_{\ge \left({M}+1\right)}↔\left({N}\in ℤ\wedge {M}+1\le {N}\right)\right)$
16 eluz1 ${⊢}{M}\in ℤ\to \left({N}-1\in {ℤ}_{\ge {M}}↔\left({N}-1\in ℤ\wedge {M}\le {N}-1\right)\right)$
17 12 15 16 3imtr4d ${⊢}{M}\in ℤ\to \left({N}\in {ℤ}_{\ge \left({M}+1\right)}\to {N}-1\in {ℤ}_{\ge {M}}\right)$
18 17 imp ${⊢}\left({M}\in ℤ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {N}-1\in {ℤ}_{\ge {M}}$