Metamath Proof Explorer

Theorem fzosubel2

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

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

Proof

Step	Hyp	Ref	Expression
1		fzosubel	$⊢ (A \in (B + C ..^B + D) \land B \in ℤ) \to A - B \in (B + C - B ..^B + D - B)$
2	1	3ad2antr1	$⊢ (A \in (B + C ..^B + D) \land (B \in ℤ \land C \in ℤ \land D \in ℤ)) \to A - B \in (B + C - B ..^B + D - B)$
3		zcn	$⊢ B \in ℤ \to B \in ℂ$
4		zcn	$⊢ C \in ℤ \to C \in ℂ$
5		zcn	$⊢ D \in ℤ \to D \in ℂ$
6		pncan2	$⊢ (B \in ℂ \land C \in ℂ) \to B + C - B = C$
7	6	3adant3	$⊢ (B \in ℂ \land C \in ℂ \land D \in ℂ) \to B + C - B = C$
8		pncan2	$⊢ (B \in ℂ \land D \in ℂ) \to B + D - B = D$
9	8	3adant2	$⊢ (B \in ℂ \land C \in ℂ \land D \in ℂ) \to B + D - B = D$
10	7 9	oveq12d	$⊢ (B \in ℂ \land C \in ℂ \land D \in ℂ) \to (B + C - B ..^B + D - B) = (C ..^D)$
11	3 4 5 10	syl3an	$⊢ (B \in ℤ \land C \in ℤ \land D \in ℤ) \to (B + C - B ..^B + D - B) = (C ..^D)$
12	11	adantl	$⊢ (A \in (B + C ..^B + D) \land (B \in ℤ \land C \in ℤ \land D \in ℤ)) \to (B + C - B ..^B + D - B) = (C ..^D)$
13	2 12	eleqtrd	$⊢ (A \in (B + C ..^B + D) \land (B \in ℤ \land C \in ℤ \land D \in ℤ)) \to A - B \in (C ..^D)$