fzadd2

Description: Membership of a sum in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010)

		Ref	Expression
	Assertion	fzadd2	$⊢ ((M \in ℤ \land N \in ℤ) \land (O \in ℤ \land P \in ℤ)) \to ((J \in (M \dots N) \land K \in (O \dots P)) \to J + K \in (M + O \dots N + P))$

Proof

Step	Hyp	Ref	Expression
1		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (J \in (M \dots N) \leftrightarrow (J \in ℤ \land M \leq J \land J \leq N))$
2		elfz1	$⊢ (O \in ℤ \land P \in ℤ) \to (K \in (O \dots P) \leftrightarrow (K \in ℤ \land O \leq K \land K \leq P))$
3	1 2	bi2anan9	$⊢ ((M \in ℤ \land N \in ℤ) \land (O \in ℤ \land P \in ℤ)) \to ((J \in (M \dots N) \land K \in (O \dots P)) \leftrightarrow ((J \in ℤ \land M \leq J \land J \leq N) \land (K \in ℤ \land O \leq K \land K \leq P)))$
4		an6	$⊢ ((J \in ℤ \land M \leq J \land J \leq N) \land (K \in ℤ \land O \leq K \land K \leq P)) \leftrightarrow ((J \in ℤ \land K \in ℤ) \land (M \leq J \land O \leq K) \land (J \leq N \land K \leq P))$
5		zre	$⊢ M \in ℤ \to M \in ℝ$
6		zre	$⊢ O \in ℤ \to O \in ℝ$
7	5 6	anim12i	$⊢ (M \in ℤ \land O \in ℤ) \to (M \in ℝ \land O \in ℝ)$
8		zre	$⊢ J \in ℤ \to J \in ℝ$
9		zre	$⊢ K \in ℤ \to K \in ℝ$
10	8 9	anim12i	$⊢ (J \in ℤ \land K \in ℤ) \to (J \in ℝ \land K \in ℝ)$
11		le2add	$⊢ ((M \in ℝ \land O \in ℝ) \land (J \in ℝ \land K \in ℝ)) \to ((M \leq J \land O \leq K) \to M + O \leq J + K)$
12	7 10 11	syl2an	$⊢ ((M \in ℤ \land O \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to ((M \leq J \land O \leq K) \to M + O \leq J + K)$
13	12	impr	$⊢ ((M \in ℤ \land O \in ℤ) \land ((J \in ℤ \land K \in ℤ) \land (M \leq J \land O \leq K))) \to M + O \leq J + K$
14	13	3adantr3	$⊢ ((M \in ℤ \land O \in ℤ) \land ((J \in ℤ \land K \in ℤ) \land (M \leq J \land O \leq K) \land (J \leq N \land K \leq P))) \to M + O \leq J + K$
15	14	adantlr	$⊢ (((M \in ℤ \land O \in ℤ) \land (N \in ℤ \land P \in ℤ)) \land ((J \in ℤ \land K \in ℤ) \land (M \leq J \land O \leq K) \land (J \leq N \land K \leq P))) \to M + O \leq J + K$
16		zre	$⊢ N \in ℤ \to N \in ℝ$
17		zre	$⊢ P \in ℤ \to P \in ℝ$
18	16 17	anim12i	$⊢ (N \in ℤ \land P \in ℤ) \to (N \in ℝ \land P \in ℝ)$
19		le2add	$⊢ ((J \in ℝ \land K \in ℝ) \land (N \in ℝ \land P \in ℝ)) \to ((J \leq N \land K \leq P) \to J + K \leq N + P)$
20	10 18 19	syl2anr	$⊢ ((N \in ℤ \land P \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to ((J \leq N \land K \leq P) \to J + K \leq N + P)$
21	20	impr	$⊢ ((N \in ℤ \land P \in ℤ) \land ((J \in ℤ \land K \in ℤ) \land (J \leq N \land K \leq P))) \to J + K \leq N + P$
22	21	3adantr2	$⊢ ((N \in ℤ \land P \in ℤ) \land ((J \in ℤ \land K \in ℤ) \land (M \leq J \land O \leq K) \land (J \leq N \land K \leq P))) \to J + K \leq N + P$
23	22	adantll	$⊢ (((M \in ℤ \land O \in ℤ) \land (N \in ℤ \land P \in ℤ)) \land ((J \in ℤ \land K \in ℤ) \land (M \leq J \land O \leq K) \land (J \leq N \land K \leq P))) \to J + K \leq N + P$
24		zaddcl	$⊢ (J \in ℤ \land K \in ℤ) \to J + K \in ℤ$
25		zaddcl	$⊢ (M \in ℤ \land O \in ℤ) \to M + O \in ℤ$
26		zaddcl	$⊢ (N \in ℤ \land P \in ℤ) \to N + P \in ℤ$
27		elfz	$⊢ (J + K \in ℤ \land M + O \in ℤ \land N + P \in ℤ) \to (J + K \in (M + O \dots N + P) \leftrightarrow (M + O \leq J + K \land J + K \leq N + P))$
28	24 25 26 27	syl3an	$⊢ ((J \in ℤ \land K \in ℤ) \land (M \in ℤ \land O \in ℤ) \land (N \in ℤ \land P \in ℤ)) \to (J + K \in (M + O \dots N + P) \leftrightarrow (M + O \leq J + K \land J + K \leq N + P))$
29	28	3expb	$⊢ ((J \in ℤ \land K \in ℤ) \land ((M \in ℤ \land O \in ℤ) \land (N \in ℤ \land P \in ℤ))) \to (J + K \in (M + O \dots N + P) \leftrightarrow (M + O \leq J + K \land J + K \leq N + P))$
30	29	ancoms	$⊢ (((M \in ℤ \land O \in ℤ) \land (N \in ℤ \land P \in ℤ)) \land (J \in ℤ \land K \in ℤ)) \to (J + K \in (M + O \dots N + P) \leftrightarrow (M + O \leq J + K \land J + K \leq N + P))$
31	30	3ad2antr1	$⊢ (((M \in ℤ \land O \in ℤ) \land (N \in ℤ \land P \in ℤ)) \land ((J \in ℤ \land K \in ℤ) \land (M \leq J \land O \leq K) \land (J \leq N \land K \leq P))) \to (J + K \in (M + O \dots N + P) \leftrightarrow (M + O \leq J + K \land J + K \leq N + P))$
32	15 23 31	mpbir2and	$⊢ (((M \in ℤ \land O \in ℤ) \land (N \in ℤ \land P \in ℤ)) \land ((J \in ℤ \land K \in ℤ) \land (M \leq J \land O \leq K) \land (J \leq N \land K \leq P))) \to J + K \in (M + O \dots N + P)$
33	32	ex	$⊢ ((M \in ℤ \land O \in ℤ) \land (N \in ℤ \land P \in ℤ)) \to (((J \in ℤ \land K \in ℤ) \land (M \leq J \land O \leq K) \land (J \leq N \land K \leq P)) \to J + K \in (M + O \dots N + P))$
34	33	an4s	$⊢ ((M \in ℤ \land N \in ℤ) \land (O \in ℤ \land P \in ℤ)) \to (((J \in ℤ \land K \in ℤ) \land (M \leq J \land O \leq K) \land (J \leq N \land K \leq P)) \to J + K \in (M + O \dots N + P))$
35	4 34	biimtrid	$⊢ ((M \in ℤ \land N \in ℤ) \land (O \in ℤ \land P \in ℤ)) \to (((J \in ℤ \land M \leq J \land J \leq N) \land (K \in ℤ \land O \leq K \land K \leq P)) \to J + K \in (M + O \dots N + P))$
36	3 35	sylbid	$⊢ ((M \in ℤ \land N \in ℤ) \land (O \in ℤ \land P \in ℤ)) \to ((J \in (M \dots N) \land K \in (O \dots P)) \to J + K \in (M + O \dots N + P))$

Metamath Proof Explorer

Theorem fzadd2

Proof