Theorem ellz1

Description: Membership in a lower set of integers. (Contributed by Stefan O'Rear, 9-Oct-2014)

	Ref	Expression
Assertion	ellz1	|- ( B e. ZZ -> ( A e. ( ZZ \ ( ZZ>= ` ( B + 1 ) ) ) <-> ( A e. ZZ /\ A <_ B ) ) )

Proof

Step	Hyp	Ref	Expression
1		eldif	|- ( A e. ( ZZ \ ( ZZ>= ` ( B + 1 ) ) ) <-> ( A e. ZZ /\ -. A e. ( ZZ>= ` ( B + 1 ) ) ) )
2		zltp1le	|- ( ( B e. ZZ /\ A e. ZZ ) -> ( B < A <-> ( B + 1 ) <_ A ) )
3	2	notbid	|- ( ( B e. ZZ /\ A e. ZZ ) -> ( -. B < A <-> -. ( B + 1 ) <_ A ) )
4		zre	|- ( A e. ZZ -> A e. RR )
5		zre	|- ( B e. ZZ -> B e. RR )
6		lenlt	|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
7	4 5 6	syl2anr	|- ( ( B e. ZZ /\ A e. ZZ ) -> ( A <_ B <-> -. B < A ) )
8		peano2z	|- ( B e. ZZ -> ( B + 1 ) e. ZZ )
9		eluz	|- ( ( ( B + 1 ) e. ZZ /\ A e. ZZ ) -> ( A e. ( ZZ>= ` ( B + 1 ) ) <-> ( B + 1 ) <_ A ) )
10	8 9	sylan	|- ( ( B e. ZZ /\ A e. ZZ ) -> ( A e. ( ZZ>= ` ( B + 1 ) ) <-> ( B + 1 ) <_ A ) )
11	10	notbid	|- ( ( B e. ZZ /\ A e. ZZ ) -> ( -. A e. ( ZZ>= ` ( B + 1 ) ) <-> -. ( B + 1 ) <_ A ) )
12	3 7 11	3bitr4rd	|- ( ( B e. ZZ /\ A e. ZZ ) -> ( -. A e. ( ZZ>= ` ( B + 1 ) ) <-> A <_ B ) )
13	12	pm5.32da	|- ( B e. ZZ -> ( ( A e. ZZ /\ -. A e. ( ZZ>= ` ( B + 1 ) ) ) <-> ( A e. ZZ /\ A <_ B ) ) )
14	1 13	bitrid	|- ( B e. ZZ -> ( A e. ( ZZ \ ( ZZ>= ` ( B + 1 ) ) ) <-> ( A e. ZZ /\ A <_ B ) ) )