Metamath Proof Explorer

Theorem fzolb2

Description: The left endpoint of a half-open integer interval is in the set iff the two arguments are integers with M < N . This provides an alternative notation for the "strict upper integer" predicate by analogy to the "weak upper integer" predicate M e. ( ZZ>=N ) . (Contributed by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion fzolb2 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∈ M ..^ N ↔ M < N

Proof

Step Hyp Ref Expression
1 fzolb ⊢ M ∈ M ..^ N ↔ M ∈ ℤ ∧ N ∈ ℤ ∧ M < N
2 df-3an ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M < N ↔ M ∈ ℤ ∧ N ∈ ℤ ∧ M < N
3 1 2 bitri ⊢ M ∈ M ..^ N ↔ M ∈ ℤ ∧ N ∈ ℤ ∧ M < N
4 3 baib ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∈ M ..^ N ↔ M < N