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 ) )