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

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