fzo0addel

Description: Translate membership in a 0-based half-open integer range. (Contributed by AV, 30-Apr-2020)

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

Step	Hyp	Ref	Expression
1		fzoaddel	$⊢ (A \in (0 ..^C) \land D \in ℤ) \to A + D \in (0 + D ..^C + D)$
2		zcn	$⊢ D \in ℤ \to D \in ℂ$
3		addlid	$⊢ D \in ℂ \to 0 + D = D$
4	3	eqcomd	$⊢ D \in ℂ \to D = 0 + D$
5	2 4	syl	$⊢ D \in ℤ \to D = 0 + D$
6	5	adantl	$⊢ (A \in (0 ..^C) \land D \in ℤ) \to D = 0 + D$
7	6	oveq1d	$⊢ (A \in (0 ..^C) \land D \in ℤ) \to (D ..^C + D) = (0 + D ..^C + D)$
8	1 7	eleqtrrd	$⊢ (A \in (0 ..^C) \land D \in ℤ) \to A + D \in (D ..^C + D)$

Metamath Proof Explorer