Theorem eluzp1

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

	Ref	Expression
Assertion	eluzp1	⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ) )

Proof

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