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	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑍 ∈ ℤ ) → ( 𝑁 + 𝑍 ) ∈ ( ℤ≥ ‘ 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑍 ∈ ℤ ) → 𝑍 ∈ ℤ )
2		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
3		zaddcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑍 ∈ ℤ ) → ( 𝑁 + 𝑍 ) ∈ ℤ )
4	2 3	sylan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑍 ∈ ℤ ) → ( 𝑁 + 𝑍 ) ∈ ℤ )
5		zre	⊢ ( 𝑍 ∈ ℤ → 𝑍 ∈ ℝ )
6		nn0addge2	⊢ ( ( 𝑍 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → 𝑍 ≤ ( 𝑁 + 𝑍 ) )
7	5 6	sylan	⊢ ( ( 𝑍 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑍 ≤ ( 𝑁 + 𝑍 ) )
8	7	ancoms	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑍 ∈ ℤ ) → 𝑍 ≤ ( 𝑁 + 𝑍 ) )
9		eluz2	⊢ ( ( 𝑁 + 𝑍 ) ∈ ( ℤ≥ ‘ 𝑍 ) ↔ ( 𝑍 ∈ ℤ ∧ ( 𝑁 + 𝑍 ) ∈ ℤ ∧ 𝑍 ≤ ( 𝑁 + 𝑍 ) ) )
10	1 4 8 9	syl3anbrc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑍 ∈ ℤ ) → ( 𝑁 + 𝑍 ) ∈ ( ℤ≥ ‘ 𝑍 ) )