Metamath Proof Explorer

Theorem eluzp1

Description: Membership in a successor upper set of integers. (Contributed by SN, 5-Jul-2025)

Ref Expression
Assertion eluzp1 ⊢ M ∈ ℤ → N ∈ ℤ ≥ M + 1 ↔ N ∈ ℤ ∧ M < N

Proof

Step Hyp Ref Expression
1 zltp1le ⊢ M ∈ ℤ ∧ N ∈ ℤ → M < N ↔ M + 1 ≤ N
2 1 pm5.32da ⊢ M ∈ ℤ → N ∈ ℤ ∧ M < N ↔ N ∈ ℤ ∧ M + 1 ≤ N
3 peano2z ⊢ M ∈ ℤ → M + 1 ∈ ℤ
4 3 3biant1d ⊢ M ∈ ℤ → N ∈ ℤ ∧ M + 1 ≤ N ↔ M + 1 ∈ ℤ ∧ N ∈ ℤ ∧ M + 1 ≤ N
5 eluz2 ⊢ N ∈ ℤ ≥ M + 1 ↔ M + 1 ∈ ℤ ∧ N ∈ ℤ ∧ M + 1 ≤ N
6 4 5 bitr4di ⊢ M ∈ ℤ → N ∈ ℤ ∧ M + 1 ≤ N ↔ N ∈ ℤ ≥ M + 1
7 2 6 bitr2d ⊢ M ∈ ℤ → N ∈ ℤ ≥ M + 1 ↔ N ∈ ℤ ∧ M < N