Metamath Proof Explorer

Theorem znn0sub

Description: The nonnegative difference of integers is a nonnegative integer. (Generalization of nn0sub .) (Contributed by NM, 14-Jul-2005)

Ref Expression
Assertion znn0sub ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ≤ N ↔ N − M ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 zre ⊢ N ∈ ℤ → N ∈ ℝ
2 zre ⊢ M ∈ ℤ → M ∈ ℝ
3 subge0 ⊢ N ∈ ℝ ∧ M ∈ ℝ → 0 ≤ N − M ↔ M ≤ N
4 1 2 3 syl2an ⊢ N ∈ ℤ ∧ M ∈ ℤ → 0 ≤ N − M ↔ M ≤ N
5 zsubcl ⊢ N ∈ ℤ ∧ M ∈ ℤ → N − M ∈ ℤ
6 5 biantrurd ⊢ N ∈ ℤ ∧ M ∈ ℤ → 0 ≤ N − M ↔ N − M ∈ ℤ ∧ 0 ≤ N − M
7 4 6 bitr3d ⊢ N ∈ ℤ ∧ M ∈ ℤ → M ≤ N ↔ N − M ∈ ℤ ∧ 0 ≤ N − M
8 7 ancoms ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ≤ N ↔ N − M ∈ ℤ ∧ 0 ≤ N − M
9 elnn0z ⊢ N − M ∈ ℕ 0 ↔ N − M ∈ ℤ ∧ 0 ≤ N − M
10 8 9 bitr4di ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ≤ N ↔ N − M ∈ ℕ 0