fzoaddel

Description: Translate membership in a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015)

		Ref	Expression
	Assertion	fzoaddel	$⊢ (A \in (B ..^C) \land D \in ℤ) \to A + D \in (B + D ..^C + D)$

Proof

Step	Hyp	Ref	Expression
1		elfzoel1	$⊢ A \in (B ..^C) \to B \in ℤ$
2	1	adantr	$⊢ (A \in (B ..^C) \land D \in ℤ) \to B \in ℤ$
3	2	zred	$⊢ (A \in (B ..^C) \land D \in ℤ) \to B \in ℝ$
4		elfzoelz	$⊢ A \in (B ..^C) \to A \in ℤ$
5	4	adantr	$⊢ (A \in (B ..^C) \land D \in ℤ) \to A \in ℤ$
6	5	zred	$⊢ (A \in (B ..^C) \land D \in ℤ) \to A \in ℝ$
7		simpr	$⊢ (A \in (B ..^C) \land D \in ℤ) \to D \in ℤ$
8	7	zred	$⊢ (A \in (B ..^C) \land D \in ℤ) \to D \in ℝ$
9		elfzole1	$⊢ A \in (B ..^C) \to B \leq A$
10	9	adantr	$⊢ (A \in (B ..^C) \land D \in ℤ) \to B \leq A$
11	3 6 8 10	leadd1dd	$⊢ (A \in (B ..^C) \land D \in ℤ) \to B + D \leq A + D$
12		elfzoel2	$⊢ A \in (B ..^C) \to C \in ℤ$
13	12	adantr	$⊢ (A \in (B ..^C) \land D \in ℤ) \to C \in ℤ$
14	13	zred	$⊢ (A \in (B ..^C) \land D \in ℤ) \to C \in ℝ$
15		elfzolt2	$⊢ A \in (B ..^C) \to A < C$
16	15	adantr	$⊢ (A \in (B ..^C) \land D \in ℤ) \to A < C$
17	6 14 8 16	ltadd1dd	$⊢ (A \in (B ..^C) \land D \in ℤ) \to A + D < C + D$
18		zaddcl	$⊢ (A \in ℤ \land D \in ℤ) \to A + D \in ℤ$
19	4 18	sylan	$⊢ (A \in (B ..^C) \land D \in ℤ) \to A + D \in ℤ$
20		zaddcl	$⊢ (B \in ℤ \land D \in ℤ) \to B + D \in ℤ$
21	1 20	sylan	$⊢ (A \in (B ..^C) \land D \in ℤ) \to B + D \in ℤ$
22		zaddcl	$⊢ (C \in ℤ \land D \in ℤ) \to C + D \in ℤ$
23	12 22	sylan	$⊢ (A \in (B ..^C) \land D \in ℤ) \to C + D \in ℤ$
24		elfzo	$⊢ (A + D \in ℤ \land B + D \in ℤ \land C + D \in ℤ) \to (A + D \in (B + D ..^C + D) \leftrightarrow (B + D \leq A + D \land A + D < C + D))$
25	19 21 23 24	syl3anc	$⊢ (A \in (B ..^C) \land D \in ℤ) \to (A + D \in (B + D ..^C + D) \leftrightarrow (B + D \leq A + D \land A + D < C + D))$
26	11 17 25	mpbir2and	$⊢ (A \in (B ..^C) \land D \in ℤ) \to A + D \in (B + D ..^C + D)$

Metamath Proof Explorer

Theorem fzoaddel

Proof