Metamath Proof Explorer


Theorem elfzolt3b

Description: Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion elfzolt3b KM..^NMM..^N

Proof

Step Hyp Ref Expression
1 elfzoel1 KM..^NM
2 elfzoel2 KM..^NN
3 elfzolt3 KM..^NM<N
4 fzolb MM..^NMNM<N
5 1 2 3 4 syl3anbrc KM..^NMM..^N