fzaddel

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

		Ref	Expression
	Assertion	fzaddel	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to (J \in (M \dots N) \leftrightarrow J + K \in (M + K \dots N + K))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (J \in ℤ \land K \in ℤ) \to J \in ℤ$
2		zaddcl	$⊢ (J \in ℤ \land K \in ℤ) \to J + K \in ℤ$
3	1 2	2thd	$⊢ (J \in ℤ \land K \in ℤ) \to (J \in ℤ \leftrightarrow J + K \in ℤ)$
4	3	adantl	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to (J \in ℤ \leftrightarrow J + K \in ℤ)$
5		zre	$⊢ M \in ℤ \to M \in ℝ$
6		zre	$⊢ J \in ℤ \to J \in ℝ$
7		zre	$⊢ K \in ℤ \to K \in ℝ$
8		leadd1	$⊢ (M \in ℝ \land J \in ℝ \land K \in ℝ) \to (M \leq J \leftrightarrow M + K \leq J + K)$
9	5 6 7 8	syl3an	$⊢ (M \in ℤ \land J \in ℤ \land K \in ℤ) \to (M \leq J \leftrightarrow M + K \leq J + K)$
10	9	3expb	$⊢ (M \in ℤ \land (J \in ℤ \land K \in ℤ)) \to (M \leq J \leftrightarrow M + K \leq J + K)$
11	10	adantlr	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to (M \leq J \leftrightarrow M + K \leq J + K)$
12		zre	$⊢ N \in ℤ \to N \in ℝ$
13		leadd1	$⊢ (J \in ℝ \land N \in ℝ \land K \in ℝ) \to (J \leq N \leftrightarrow J + K \leq N + K)$
14	6 12 7 13	syl3an	$⊢ (J \in ℤ \land N \in ℤ \land K \in ℤ) \to (J \leq N \leftrightarrow J + K \leq N + K)$
15	14	3com12	$⊢ (N \in ℤ \land J \in ℤ \land K \in ℤ) \to (J \leq N \leftrightarrow J + K \leq N + K)$
16	15	3expb	$⊢ (N \in ℤ \land (J \in ℤ \land K \in ℤ)) \to (J \leq N \leftrightarrow J + K \leq N + K)$
17	16	adantll	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to (J \leq N \leftrightarrow J + K \leq N + K)$
18	4 11 17	3anbi123d	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to ((J \in ℤ \land M \leq J \land J \leq N) \leftrightarrow (J + K \in ℤ \land M + K \leq J + K \land J + K \leq N + K))$
19		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (J \in (M \dots N) \leftrightarrow (J \in ℤ \land M \leq J \land J \leq N))$
20	19	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to (J \in (M \dots N) \leftrightarrow (J \in ℤ \land M \leq J \land J \leq N))$
21		zaddcl	$⊢ (M \in ℤ \land K \in ℤ) \to M + K \in ℤ$
22		zaddcl	$⊢ (N \in ℤ \land K \in ℤ) \to N + K \in ℤ$
23		elfz1	$⊢ (M + K \in ℤ \land N + K \in ℤ) \to (J + K \in (M + K \dots N + K) \leftrightarrow (J + K \in ℤ \land M + K \leq J + K \land J + K \leq N + K))$
24	21 22 23	syl2an	$⊢ ((M \in ℤ \land K \in ℤ) \land (N \in ℤ \land K \in ℤ)) \to (J + K \in (M + K \dots N + K) \leftrightarrow (J + K \in ℤ \land M + K \leq J + K \land J + K \leq N + K))$
25	24	anandirs	$⊢ ((M \in ℤ \land N \in ℤ) \land K \in ℤ) \to (J + K \in (M + K \dots N + K) \leftrightarrow (J + K \in ℤ \land M + K \leq J + K \land J + K \leq N + K))$
26	25	adantrl	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to (J + K \in (M + K \dots N + K) \leftrightarrow (J + K \in ℤ \land M + K \leq J + K \land J + K \leq N + K))$
27	18 20 26	3bitr4d	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to (J \in (M \dots N) \leftrightarrow J + K \in (M + K \dots N + K))$

Metamath Proof Explorer

Theorem fzaddel

Proof