Step |
Hyp |
Ref |
Expression |
1 |
|
zre |
|- ( A e. ZZ -> A e. RR ) |
2 |
|
zre |
|- ( B e. ZZ -> B e. RR ) |
3 |
|
peano2re |
|- ( A e. RR -> ( A + 1 ) e. RR ) |
4 |
|
ltlen |
|- ( ( ( A + 1 ) e. RR /\ B e. RR ) -> ( ( A + 1 ) < B <-> ( ( A + 1 ) <_ B /\ B =/= ( A + 1 ) ) ) ) |
5 |
3 4
|
sylan |
|- ( ( A e. RR /\ B e. RR ) -> ( ( A + 1 ) < B <-> ( ( A + 1 ) <_ B /\ B =/= ( A + 1 ) ) ) ) |
6 |
1 2 5
|
syl2an |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A + 1 ) < B <-> ( ( A + 1 ) <_ B /\ B =/= ( A + 1 ) ) ) ) |
7 |
|
zltp1le |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A < B <-> ( A + 1 ) <_ B ) ) |
8 |
7
|
anbi1d |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A < B /\ B =/= ( A + 1 ) ) <-> ( ( A + 1 ) <_ B /\ B =/= ( A + 1 ) ) ) ) |
9 |
6 8
|
bitr4d |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A + 1 ) < B <-> ( A < B /\ B =/= ( A + 1 ) ) ) ) |