Metamath Proof Explorer

Theorem fzosubel3

Description: Membership in a translated half-open integer range when the original range is zero-based. (Contributed by Stefan O'Rear, 15-Aug-2015)

		Ref	Expression
	Assertion	fzosubel3	$⊢ (A \in (B ..^B + D) \land D \in ℤ) \to A - B \in (0 ..^D)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in (B ..^B + D) \land D \in ℤ) \to A \in (B ..^B + D)$
2		elfzoel1	$⊢ A \in (B ..^B + D) \to B \in ℤ$
3	2	adantr	$⊢ (A \in (B ..^B + D) \land D \in ℤ) \to B \in ℤ$
4	3	zcnd	$⊢ (A \in (B ..^B + D) \land D \in ℤ) \to B \in ℂ$
5	4	addridd	$⊢ (A \in (B ..^B + D) \land D \in ℤ) \to B + 0 = B$
6	5	oveq1d	$⊢ (A \in (B ..^B + D) \land D \in ℤ) \to (B + 0 ..^B + D) = (B ..^B + D)$
7	1 6	eleqtrrd	$⊢ (A \in (B ..^B + D) \land D \in ℤ) \to A \in (B + 0 ..^B + D)$
8		0zd	$⊢ (A \in (B ..^B + D) \land D \in ℤ) \to 0 \in ℤ$
9		simpr	$⊢ (A \in (B ..^B + D) \land D \in ℤ) \to D \in ℤ$
10		fzosubel2	$⊢ (A \in (B + 0 ..^B + D) \land (B \in ℤ \land 0 \in ℤ \land D \in ℤ)) \to A - B \in (0 ..^D)$
11	7 3 8 9 10	syl13anc	$⊢ (A \in (B ..^B + D) \land D \in ℤ) \to A - B \in (0 ..^D)$