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