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