Metamath Proof Explorer


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 syl5bb
 |-  ( B e. ZZ -> ( A e. ( ZZ \ ( ZZ>= ` ( B + 1 ) ) ) <-> ( A e. ZZ /\ A <_ B ) ) )