Theorem nn0sub2

Description: Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005)

	Ref	Expression
Assertion	nn0sub2	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( 𝑁 − 𝑀 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		nn0sub	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ0 ) )
2	1	biimp3a	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( 𝑁 − 𝑀 ) ∈ ℕ0 )