Metamath Proof Explorer

Theorem elfzo

Description: Membership in a half-open finite set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion elfzo ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∈ M ..^ N ↔ M ≤ K ∧ K < N

Proof

Step Hyp Ref Expression
1 peano2zm ⊢ N ∈ ℤ → N − 1 ∈ ℤ
2 elfz ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N − 1 ∈ ℤ → K ∈ M … N − 1 ↔ M ≤ K ∧ K ≤ N − 1
3 1 2 syl3an3 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∈ M … N − 1 ↔ M ≤ K ∧ K ≤ N − 1
4 fzoval ⊢ N ∈ ℤ → M ..^ N = M … N − 1
5 4 eleq2d ⊢ N ∈ ℤ → K ∈ M ..^ N ↔ K ∈ M … N − 1
6 5 3ad2ant3 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∈ M ..^ N ↔ K ∈ M … N − 1
7 zltlem1 ⊢ K ∈ ℤ ∧ N ∈ ℤ → K < N ↔ K ≤ N − 1
8 7 3adant2 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K < N ↔ K ≤ N − 1
9 8 anbi2d ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → M ≤ K ∧ K < N ↔ M ≤ K ∧ K ≤ N − 1
10 3 6 9 3bitr4d ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∈ M ..^ N ↔ M ≤ K ∧ K < N