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 ⊢ K ∈ M ..^ N → M ∈ M ..^ N

Proof

Step Hyp Ref Expression
1 elfzoel1 ⊢ K ∈ M ..^ N → M ∈ ℤ
2 elfzoel2 ⊢ K ∈ M ..^ N → N ∈ ℤ
3 elfzolt3 ⊢ K ∈ M ..^ N → M < N
4 fzolb ⊢ M ∈ M ..^ N ↔ M ∈ ℤ ∧ N ∈ ℤ ∧ M < N
5 1 2 3 4 syl3anbrc ⊢ K ∈ M ..^ N → M ∈ M ..^ N