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