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