Theorem fzaddel

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

	Ref	Expression
Assertion	fzaddel	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝐽 ∈ ℤ )
2		zaddcl	⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐽 + 𝐾 ) ∈ ℤ )
3	1 2	2thd	⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐽 ∈ ℤ ↔ ( 𝐽 + 𝐾 ) ∈ ℤ ) )
4	3	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 ∈ ℤ ↔ ( 𝐽 + 𝐾 ) ∈ ℤ ) )
5		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
6		zre	⊢ ( 𝐽 ∈ ℤ → 𝐽 ∈ ℝ )
7		zre	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
8		leadd1	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑀 ≤ 𝐽 ↔ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ) )
9	5 6 7 8	syl3an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ≤ 𝐽 ↔ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ) )
10	9	3expb	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝑀 ≤ 𝐽 ↔ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ) )
11	10	adantlr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝑀 ≤ 𝐽 ↔ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ) )
12		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
13		leadd1	⊢ ( ( 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝐽 ≤ 𝑁 ↔ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
14	6 12 7 13	syl3an	⊢ ( ( 𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐽 ≤ 𝑁 ↔ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
15	14	3com12	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐽 ≤ 𝑁 ↔ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
16	15	3expb	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 ≤ 𝑁 ↔ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
17	16	adantll	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 ≤ 𝑁 ↔ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) )
18	4 11 17	3anbi123d	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐽 ∈ ℤ ∧ 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ↔ ( ( 𝐽 + 𝐾 ) ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ∧ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) ) )
19		elfz1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 ∈ ℤ ∧ 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ) )
20	19	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 ∈ ℤ ∧ 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ) )
21		zaddcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 + 𝐾 ) ∈ ℤ )
22		zaddcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 + 𝐾 ) ∈ ℤ )
23		elfz1	⊢ ( ( ( 𝑀 + 𝐾 ) ∈ ℤ ∧ ( 𝑁 + 𝐾 ) ∈ ℤ ) → ( ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↔ ( ( 𝐽 + 𝐾 ) ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ∧ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) ) )
24	21 22 23	syl2an	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↔ ( ( 𝐽 + 𝐾 ) ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ∧ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) ) )
25	24	anandirs	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↔ ( ( 𝐽 + 𝐾 ) ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ∧ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) ) )
26	25	adantrl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↔ ( ( 𝐽 + 𝐾 ) ∈ ℤ ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝐽 + 𝐾 ) ∧ ( 𝐽 + 𝐾 ) ≤ ( 𝑁 + 𝐾 ) ) ) )
27	18 20 26	3bitr4d	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) )