Metamath Proof Explorer

Theorem fzrev2i

Description: Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005)

Ref Expression
Assertion fzrev2i ⊢ J ∈ ℤ ∧ K ∈ M … N → J − K ∈ J − N … J − M

Proof

Step Hyp Ref Expression
1 simpr ⊢ J ∈ ℤ ∧ K ∈ M … N → K ∈ M … N
2 elfzel1 ⊢ K ∈ M … N → M ∈ ℤ
3 2 adantl ⊢ J ∈ ℤ ∧ K ∈ M … N → M ∈ ℤ
4 elfzel2 ⊢ K ∈ M … N → N ∈ ℤ
5 4 adantl ⊢ J ∈ ℤ ∧ K ∈ M … N → N ∈ ℤ
6 simpl ⊢ J ∈ ℤ ∧ K ∈ M … N → J ∈ ℤ
7 elfzelz ⊢ K ∈ M … N → K ∈ ℤ
8 7 adantl ⊢ J ∈ ℤ ∧ K ∈ M … N → K ∈ ℤ
9 fzrev2 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ J ∈ ℤ ∧ K ∈ ℤ → K ∈ M … N ↔ J − K ∈ J − N … J − M
10 3 5 6 8 9 syl22anc ⊢ J ∈ ℤ ∧ K ∈ M … N → K ∈ M … N ↔ J − K ∈ J − N … J − M
11 1 10 mpbid ⊢ J ∈ ℤ ∧ K ∈ M … N → J − K ∈ J − N … J − M