Metamath Proof Explorer

Theorem nn0pzuz

Description: The sum of a nonnegative integer and an integer is an integer greater than or equal to that integer. (Contributed by Alexander van der Vekens, 3-Oct-2018)

		Ref	Expression
	Assertion	nn0pzuz	$⊢ (N \in ℕ_{0} \land Z \in ℤ) \to N + Z \in ℤ_{\geq Z}$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (N \in ℕ_{0} \land Z \in ℤ) \to Z \in ℤ$
2		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
3		zaddcl	$⊢ (N \in ℤ \land Z \in ℤ) \to N + Z \in ℤ$
4	2 3	sylan	$⊢ (N \in ℕ_{0} \land Z \in ℤ) \to N + Z \in ℤ$
5		zre	$⊢ Z \in ℤ \to Z \in ℝ$
6		nn0addge2	$⊢ (Z \in ℝ \land N \in ℕ_{0}) \to Z \leq N + Z$
7	5 6	sylan	$⊢ (Z \in ℤ \land N \in ℕ_{0}) \to Z \leq N + Z$
8	7	ancoms	$⊢ (N \in ℕ_{0} \land Z \in ℤ) \to Z \leq N + Z$
9		eluz2	$⊢ N + Z \in ℤ_{\geq Z} \leftrightarrow (Z \in ℤ \land N + Z \in ℤ \land Z \leq N + Z)$
10	1 4 8 9	syl3anbrc	$⊢ (N \in ℕ_{0} \land Z \in ℤ) \to N + Z \in ℤ_{\geq Z}$