fzosubel

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

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

Step	Hyp	Ref	Expression
1		znegcl	$⊢ D \in ℤ \to - D \in ℤ$
2		fzoaddel	$⊢ (A \in (B ..^C) \land - D \in ℤ) \to A + (- D) \in (B + (- D) ..^C + (- D))$
3	1 2	sylan2	$⊢ (A \in (B ..^C) \land D \in ℤ) \to A + (- D) \in (B + (- D) ..^C + (- D))$
4		elfzoelz	$⊢ A \in (B ..^C) \to A \in ℤ$
5	4	adantr	$⊢ (A \in (B ..^C) \land D \in ℤ) \to A \in ℤ$
6	5	zcnd	$⊢ (A \in (B ..^C) \land D \in ℤ) \to A \in ℂ$
7		simpr	$⊢ (A \in (B ..^C) \land D \in ℤ) \to D \in ℤ$
8	7	zcnd	$⊢ (A \in (B ..^C) \land D \in ℤ) \to D \in ℂ$
9	6 8	negsubd	$⊢ (A \in (B ..^C) \land D \in ℤ) \to A + (- D) = A - D$
10		elfzoel1	$⊢ A \in (B ..^C) \to B \in ℤ$
11	10	adantr	$⊢ (A \in (B ..^C) \land D \in ℤ) \to B \in ℤ$
12	11	zcnd	$⊢ (A \in (B ..^C) \land D \in ℤ) \to B \in ℂ$
13	12 8	negsubd	$⊢ (A \in (B ..^C) \land D \in ℤ) \to B + (- D) = B - D$
14		elfzoel2	$⊢ A \in (B ..^C) \to C \in ℤ$
15	14	adantr	$⊢ (A \in (B ..^C) \land D \in ℤ) \to C \in ℤ$
16	15	zcnd	$⊢ (A \in (B ..^C) \land D \in ℤ) \to C \in ℂ$
17	16 8	negsubd	$⊢ (A \in (B ..^C) \land D \in ℤ) \to C + (- D) = C - D$
18	13 17	oveq12d	$⊢ (A \in (B ..^C) \land D \in ℤ) \to (B + (- D) ..^C + (- D)) = (B - D ..^C - D)$
19	3 9 18	3eltr3d	$⊢ (A \in (B ..^C) \land D \in ℤ) \to A - D \in (B - D ..^C - D)$

Metamath Proof Explorer