Metamath Proof Explorer

Theorem zpnn0elfzo1

Description: Membership of an integer increased by a nonnegative integer in a half- open integer range. (Contributed by Alexander van der Vekens, 22-Sep-2018)

		Ref	Expression
	Assertion	zpnn0elfzo1	$⊢ (Z \in ℤ \land N \in ℕ_{0}) \to Z + N \in (Z ..^Z + N + 1)$

Proof

Step	Hyp	Ref	Expression
1		zpnn0elfzo	$⊢ (Z \in ℤ \land N \in ℕ_{0}) \to Z + N \in (Z ..^Z + N + 1)$
2		zcn	$⊢ Z \in ℤ \to Z \in ℂ$
3	2	adantr	$⊢ (Z \in ℤ \land N \in ℕ_{0}) \to Z \in ℂ$
4		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
5	4	adantl	$⊢ (Z \in ℤ \land N \in ℕ_{0}) \to N \in ℂ$
6		1cnd	$⊢ (Z \in ℤ \land N \in ℕ_{0}) \to 1 \in ℂ$
7	3 5 6	addassd	$⊢ (Z \in ℤ \land N \in ℕ_{0}) \to Z + N + 1 = Z + N + 1$
8	7	oveq2d	$⊢ (Z \in ℤ \land N \in ℕ_{0}) \to (Z ..^Z + N + 1) = (Z ..^Z + N + 1)$
9	1 8	eleqtrd	$⊢ (Z \in ℤ \land N \in ℕ_{0}) \to Z + N \in (Z ..^Z + N + 1)$