Theorem subne0nn

Description: A nonnegative difference is positive if the two numbers are not equal. (Contributed by Thierry Arnoux, 17-Dec-2023)

	Ref	Expression
Hypotheses	subne0nn.1	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
	subne0nn.2	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
	subne0nn.3	⊢ ( 𝜑 → ( 𝑀 − 𝑁 ) ∈ ℕ0 )
	subne0nn.4	⊢ ( 𝜑 → 𝑀 ≠ 𝑁 )
Assertion	subne0nn	⊢ ( 𝜑 → ( 𝑀 − 𝑁 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		subne0nn.1	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
2		subne0nn.2	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
3		subne0nn.3	⊢ ( 𝜑 → ( 𝑀 − 𝑁 ) ∈ ℕ0 )
4		subne0nn.4	⊢ ( 𝜑 → 𝑀 ≠ 𝑁 )
5	1 2 4	subne0d	⊢ ( 𝜑 → ( 𝑀 − 𝑁 ) ≠ 0 )
6		elnnne0	⊢ ( ( 𝑀 − 𝑁 ) ∈ ℕ ↔ ( ( 𝑀 − 𝑁 ) ∈ ℕ0 ∧ ( 𝑀 − 𝑁 ) ≠ 0 ) )
7	3 5 6	sylanbrc	⊢ ( 𝜑 → ( 𝑀 − 𝑁 ) ∈ ℕ )