Metamath Proof Explorer

Theorem elfzm11

Description: Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion elfzm11 ⊢ M ∈ ℤ ∧ N ∈ ℤ → K ∈ M … N − 1 ↔ K ∈ ℤ ∧ M ≤ K ∧ K < N

Proof

Step Hyp Ref Expression
1 peano2zm ⊢ N ∈ ℤ → N − 1 ∈ ℤ
2 elfz1 ⊢ M ∈ ℤ ∧ N − 1 ∈ ℤ → K ∈ M … N − 1 ↔ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N − 1
3 1 2 sylan2 ⊢ M ∈ ℤ ∧ N ∈ ℤ → K ∈ M … N − 1 ↔ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N − 1
4 zltlem1 ⊢ K ∈ ℤ ∧ N ∈ ℤ → K < N ↔ K ≤ N − 1
5 4 anbi2d ⊢ K ∈ ℤ ∧ N ∈ ℤ → M ≤ K ∧ K < N ↔ M ≤ K ∧ K ≤ N − 1
6 5 expcom ⊢ N ∈ ℤ → K ∈ ℤ → M ≤ K ∧ K < N ↔ M ≤ K ∧ K ≤ N − 1
7 6 pm5.32d ⊢ N ∈ ℤ → K ∈ ℤ ∧ M ≤ K ∧ K < N ↔ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N − 1
8 3anass ⊢ K ∈ ℤ ∧ M ≤ K ∧ K < N ↔ K ∈ ℤ ∧ M ≤ K ∧ K < N
9 3anass ⊢ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N − 1 ↔ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N − 1
10 7 8 9 3bitr4g ⊢ N ∈ ℤ → K ∈ ℤ ∧ M ≤ K ∧ K < N ↔ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N − 1
11 10 adantl ⊢ M ∈ ℤ ∧ N ∈ ℤ → K ∈ ℤ ∧ M ≤ K ∧ K < N ↔ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N − 1
12 3 11 bitr4d ⊢ M ∈ ℤ ∧ N ∈ ℤ → K ∈ M … N − 1 ↔ K ∈ ℤ ∧ M ≤ K ∧ K < N