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 ⊢M∈ℤ∧N∈ℤ∧J∈ℤ∧K∈ℤ→J∈M…N↔J−K∈M−K…N−K

Proof

Step Hyp Ref Expression
1 znegcl ⊢K∈ℤ→−K∈ℤ
2 fzaddel ⊢M∈ℤ∧N∈ℤ∧J∈ℤ∧−K∈ℤ→J∈M…N↔J+−K∈M+−K…N+−K
3 1 2 sylanr2 ⊢M∈ℤ∧N∈ℤ∧J∈ℤ∧K∈ℤ→J∈M…N↔J+−K∈M+−K…N+−K
4 zcn ⊢M∈ℤ→M∈ℂ
5 zcn ⊢N∈ℤ→N∈ℂ
6 4 5 anim12i ⊢M∈ℤ∧N∈ℤ→M∈ℂ∧N∈ℂ
7 zcn ⊢J∈ℤ→J∈ℂ
8 zcn ⊢K∈ℤ→K∈ℂ
9 7 8 anim12i ⊢J∈ℤ∧K∈ℤ→J∈ℂ∧K∈ℂ
10 negsub ⊢J∈ℂ∧K∈ℂ→J+−K=J−K
11 10 adantl ⊢M∈ℂ∧N∈ℂ∧J∈ℂ∧K∈ℂ→J+−K=J−K
12 negsub ⊢M∈ℂ∧K∈ℂ→M+−K=M−K
13 negsub ⊢N∈ℂ∧K∈ℂ→N+−K=N−K
14 12 13 oveqan12d ⊢M∈ℂ∧K∈ℂ∧N∈ℂ∧K∈ℂ→M+−K…N+−K=M−K…N−K
15 14 anandirs ⊢M∈ℂ∧N∈ℂ∧K∈ℂ→M+−K…N+−K=M−K…N−K
16 15 adantrl ⊢M∈ℂ∧N∈ℂ∧J∈ℂ∧K∈ℂ→M+−K…N+−K=M−K…N−K
17 11 16 eleq12d ⊢M∈ℂ∧N∈ℂ∧J∈ℂ∧K∈ℂ→J+−K∈M+−K…N+−K↔J−K∈M−K…N−K
18 6 9 17 syl2an ⊢M∈ℤ∧N∈ℤ∧J∈ℤ∧K∈ℤ→J+−K∈M+−K…N+−K↔J−K∈M−K…N−K
19 3 18 bitrd ⊢M∈ℤ∧N∈ℤ∧J∈ℤ∧K∈ℤ→J∈M…N↔J−K∈M−K…N−K