Theorem eluzp1

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

	Ref	Expression
Assertion	eluzp1	|- ( M e. ZZ -> ( N e. ( ZZ>= ` ( M + 1 ) ) <-> ( N e. ZZ /\ M < N ) ) )

Proof

Step	Hyp	Ref	Expression
1		zltp1le	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( M + 1 ) <_ N ) )
2	1	pm5.32da	|- ( M e. ZZ -> ( ( N e. ZZ /\ M < N ) <-> ( N e. ZZ /\ ( M + 1 ) <_ N ) ) )
3		peano2z	|- ( M e. ZZ -> ( M + 1 ) e. ZZ )
4	3	3biant1d	|- ( M e. ZZ -> ( ( N e. ZZ /\ ( M + 1 ) <_ N ) <-> ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ ( M + 1 ) <_ N ) ) )
5		eluz2	|- ( N e. ( ZZ>= ` ( M + 1 ) ) <-> ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ ( M + 1 ) <_ N ) )
6	4 5	bitr4di	|- ( M e. ZZ -> ( ( N e. ZZ /\ ( M + 1 ) <_ N ) <-> N e. ( ZZ>= ` ( M + 1 ) ) ) )
7	2 6	bitr2d	|- ( M e. ZZ -> ( N e. ( ZZ>= ` ( M + 1 ) ) <-> ( N e. ZZ /\ M < N ) ) )