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

Metamath Proof Explorer

Theorem fzsubel

Description: Membership of a difference in a finite set of sequential integers. (Contributed by NM, 30-Jul-2005)

Ref Expression
Assertion fzsubel ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 − 𝐾 ) ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) ) )

Proof

Step Hyp Ref Expression
1 znegcl ⊢ ( 𝐾 ∈ ℤ → - 𝐾 ∈ ℤ )
2 fzaddel ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ - 𝐾 ∈ ℤ ) ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 + - 𝐾 ) ∈ ( ( 𝑀 + - 𝐾 ) ... ( 𝑁 + - 𝐾 ) ) ) )
3 1 2 sylanr2 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 + - 𝐾 ) ∈ ( ( 𝑀 + - 𝐾 ) ... ( 𝑁 + - 𝐾 ) ) ) )
4 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
5 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
6 4 5 anim12i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) )
7 zcn ⊢ ( 𝐽 ∈ ℤ → 𝐽 ∈ ℂ )
8 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
9 7 8 anim12i ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐽 ∈ ℂ ∧ 𝐾 ∈ ℂ ) )
10 negsub ⊢ ( ( 𝐽 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( 𝐽 + - 𝐾 ) = ( 𝐽 − 𝐾 ) )
11 10 adantl ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ∧ ( 𝐽 ∈ ℂ ∧ 𝐾 ∈ ℂ ) ) → ( 𝐽 + - 𝐾 ) = ( 𝐽 − 𝐾 ) )
12 negsub ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( 𝑀 + - 𝐾 ) = ( 𝑀 − 𝐾 ) )
13 negsub ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( 𝑁 + - 𝐾 ) = ( 𝑁 − 𝐾 ) )
14 12 13 oveqan12d ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝐾 ∈ ℂ ) ∧ ( 𝑁 ∈ ℂ ∧ 𝐾 ∈ ℂ ) ) → ( ( 𝑀 + - 𝐾 ) ... ( 𝑁 + - 𝐾 ) ) = ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) )
15 14 anandirs ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ∧ 𝐾 ∈ ℂ ) → ( ( 𝑀 + - 𝐾 ) ... ( 𝑁 + - 𝐾 ) ) = ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) )
16 15 adantrl ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ∧ ( 𝐽 ∈ ℂ ∧ 𝐾 ∈ ℂ ) ) → ( ( 𝑀 + - 𝐾 ) ... ( 𝑁 + - 𝐾 ) ) = ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) )
17 11 16 eleq12d ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ∧ ( 𝐽 ∈ ℂ ∧ 𝐾 ∈ ℂ ) ) → ( ( 𝐽 + - 𝐾 ) ∈ ( ( 𝑀 + - 𝐾 ) ... ( 𝑁 + - 𝐾 ) ) ↔ ( 𝐽 − 𝐾 ) ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) ) )
18 6 9 17 syl2an ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐽 + - 𝐾 ) ∈ ( ( 𝑀 + - 𝐾 ) ... ( 𝑁 + - 𝐾 ) ) ↔ ( 𝐽 − 𝐾 ) ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) ) )
19 3 18 bitrd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 − 𝐾 ) ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) ) )