fzo0addelr

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

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

Step	Hyp	Ref	Expression
1		fzo0addel	$⊢ (A \in (0 ..^C) \land D \in ℤ) \to A + D \in (D ..^C + D)$
2		zcn	$⊢ D \in ℤ \to D \in ℂ$
3		elfzoel2	$⊢ A \in (0 ..^C) \to C \in ℤ$
4	3	zcnd	$⊢ A \in (0 ..^C) \to C \in ℂ$
5		addcom	$⊢ (D \in ℂ \land C \in ℂ) \to D + C = C + D$
6	2 4 5	syl2anr	$⊢ (A \in (0 ..^C) \land D \in ℤ) \to D + C = C + D$
7	6	oveq2d	$⊢ (A \in (0 ..^C) \land D \in ℤ) \to (D ..^D + C) = (D ..^C + D)$
8	1 7	eleqtrrd	$⊢ (A \in (0 ..^C) \land D \in ℤ) \to A + D \in (D ..^D + C)$

Metamath Proof Explorer