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

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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ0 ) )

Proof

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