This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) ) )