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	|- ( ph -> M e. CC )
	subne0nn.2	|- ( ph -> N e. CC )
	subne0nn.3	|- ( ph -> ( M - N ) e. NN0 )
	subne0nn.4	|- ( ph -> M =/= N )
Assertion	subne0nn	|- ( ph -> ( M - N ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		subne0nn.1	|- ( ph -> M e. CC )
2		subne0nn.2	|- ( ph -> N e. CC )
3		subne0nn.3	|- ( ph -> ( M - N ) e. NN0 )
4		subne0nn.4	|- ( ph -> M =/= N )
5	1 2 4	subne0d	|- ( ph -> ( M - N ) =/= 0 )
6		elnnne0	|- ( ( M - N ) e. NN <-> ( ( M - N ) e. NN0 /\ ( M - N ) =/= 0 ) )
7	3 5 6	sylanbrc	|- ( ph -> ( M - N ) e. NN )