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	$$⊢\phi \to M\in ℂ$$
	subne0nn.2	$$⊢\phi \to N\in ℂ$$
	subne0nn.3	$$⊢\phi \to M-N\in {\mathbb{N}}_0$$
	subne0nn.4	$$⊢\phi \to M\ne N$$
Assertion	subne0nn	$$⊢\phi \to M-N\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		subne0nn.1	$$⊢\phi \to M\in ℂ$$
2		subne0nn.2	$$⊢\phi \to N\in ℂ$$
3		subne0nn.3	$$⊢\phi \to M-N\in {\mathbb{N}}_0$$
4		subne0nn.4	$$⊢\phi \to M\ne N$$
5	1 2 4	subne0d	$$⊢\phi \to M-N\ne 0$$
6		elnnne0	$$⊢M-N\in \mathbb{N}\leftrightarrow \left(M-N\in {\mathbb{N}}_0\wedge M-N\ne 0\right)$$
7	3 5 6	sylanbrc	$$⊢\phi \to M-N\in \mathbb{N}$$