Metamath Proof Explorer

Theorem elfzd

Description: Membership in a finite set of sequential integers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses elfzd.1 ⊢ φ → M ∈ ℤ
elfzd.2 ⊢ φ → N ∈ ℤ
elfzd.3 ⊢ φ → K ∈ ℤ
elfzd.4 ⊢ φ → M ≤ K
elfzd.5 ⊢ φ → K ≤ N
Assertion elfzd ⊢ φ → K ∈ M … N

Proof

Step Hyp Ref Expression
1 elfzd.1 ⊢ φ → M ∈ ℤ
2 elfzd.2 ⊢ φ → N ∈ ℤ
3 elfzd.3 ⊢ φ → K ∈ ℤ
4 elfzd.4 ⊢ φ → M ≤ K
5 elfzd.5 ⊢ φ → K ≤ N
6 1 2 3 3jca ⊢ φ → M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ
7 6 4 5 jca32 ⊢ φ → M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N
8 elfz2 ⊢ K ∈ M … N ↔ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N
9 7 8 sylibr ⊢ φ → K ∈ M … N