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