Metamath Proof Explorer


Theorem elfzouz

Description: Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion elfzouz KM..^NKM

Proof

Step Hyp Ref Expression
1 elfzo2 KM..^NKMNK<N
2 1 simp1bi KM..^NKM