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