This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐽 − 𝐾 ) ∈ ( ( 𝐽 − 𝑁 ) ... ( 𝐽 − 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )
2 elfzel1 ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ∈ ℤ )
3 2 adantl ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ∈ ℤ )
4 elfzel2 ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ℤ )
5 4 adantl ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ℤ )
6 simpl ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐽 ∈ ℤ )
7 elfzelz ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ℤ )
8 7 adantl ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ℤ )
9 fzrev2 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 − 𝐾 ) ∈ ( ( 𝐽 − 𝑁 ) ... ( 𝐽 − 𝑀 ) ) ) )
10 3 5 6 8 9 syl22anc ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 − 𝐾 ) ∈ ( ( 𝐽 − 𝑁 ) ... ( 𝐽 − 𝑀 ) ) ) )
11 1 10 mpbid ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐽 − 𝐾 ) ∈ ( ( 𝐽 − 𝑁 ) ... ( 𝐽 − 𝑀 ) ) )