This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zpnn0elfzo

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	zpnn0elfzo	$⊢ (Z \in ℤ \land N \in ℕ_{0}) \to Z + N \in (Z ..^Z + N + 1)$

Proof

Step	Hyp	Ref	Expression
1		uzid	$⊢ Z \in ℤ \to Z \in ℤ_{\geq Z}$
2	1	anim1i	$⊢ (Z \in ℤ \land N \in ℕ_{0}) \to (Z \in ℤ_{\geq Z} \land N \in ℕ_{0})$
3		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
4		zaddcl	$⊢ (Z \in ℤ \land N \in ℤ) \to Z + N \in ℤ$
5	3 4	sylan2	$⊢ (Z \in ℤ \land N \in ℕ_{0}) \to Z + N \in ℤ$
6		elfzomin	$⊢ Z + N \in ℤ \to Z + N \in (Z + N ..^Z + N + 1)$
7	5 6	syl	$⊢ (Z \in ℤ \land N \in ℕ_{0}) \to Z + N \in (Z + N ..^Z + N + 1)$
8		uzaddcl	$⊢ (Z \in ℤ_{\geq Z} \land N \in ℕ_{0}) \to Z + N \in ℤ_{\geq Z}$
9		fzoss1	$⊢ Z + N \in ℤ_{\geq Z} \to (Z + N ..^Z + N + 1) \subseteq (Z ..^Z + N + 1)$
10	8 9	syl	$⊢ (Z \in ℤ_{\geq Z} \land N \in ℕ_{0}) \to (Z + N ..^Z + N + 1) \subseteq (Z ..^Z + N + 1)$
11	10	sselda	$⊢ ((Z \in ℤ_{\geq Z} \land N \in ℕ_{0}) \land Z + N \in (Z + N ..^Z + N + 1)) \to Z + N \in (Z ..^Z + N + 1)$
12	2 7 11	syl2anc	$⊢ (Z \in ℤ \land N \in ℕ_{0}) \to Z + N \in (Z ..^Z + N + 1)$