Theorem 0mnnnnn0

Description: The result of subtracting a positive integer from 0 is not a nonnegative integer. (Contributed by Alexander van der Vekens, 19-Mar-2018)

	Ref	Expression
Assertion	0mnnnnn0	|- ( N e. NN -> ( 0 - N ) e/ NN0 )

Proof

Step	Hyp	Ref	Expression
1		0re	|- 0 e. RR
2		nnel	|- ( -. ( 0 - N ) e/ NN0 <-> ( 0 - N ) e. NN0 )
3		df-neg	|- -u N = ( 0 - N )
4	3	eqcomi	|- ( 0 - N ) = -u N
5	4	eleq1i	|- ( ( 0 - N ) e. NN0 <-> -u N e. NN0 )
6		nn0ge0	|- ( -u N e. NN0 -> 0 <_ -u N )
7		nnre	|- ( N e. NN -> N e. RR )
8	7	le0neg1d	|- ( N e. NN -> ( N <_ 0 <-> 0 <_ -u N ) )
9		nngt0	|- ( N e. NN -> 0 < N )
10		0red	|- ( N e. NN -> 0 e. RR )
11	10 7	ltnled	|- ( N e. NN -> ( 0 < N <-> -. N <_ 0 ) )
12		pm2.21	|- ( -. N <_ 0 -> ( N <_ 0 -> -. 0 e. RR ) )
13	11 12	syl6bi	|- ( N e. NN -> ( 0 < N -> ( N <_ 0 -> -. 0 e. RR ) ) )
14	9 13	mpd	|- ( N e. NN -> ( N <_ 0 -> -. 0 e. RR ) )
15	8 14	sylbird	|- ( N e. NN -> ( 0 <_ -u N -> -. 0 e. RR ) )
16	6 15	syl5	|- ( N e. NN -> ( -u N e. NN0 -> -. 0 e. RR ) )
17	5 16	syl5bi	|- ( N e. NN -> ( ( 0 - N ) e. NN0 -> -. 0 e. RR ) )
18	2 17	syl5bi	|- ( N e. NN -> ( -. ( 0 - N ) e/ NN0 -> -. 0 e. RR ) )
19	1 18	mt4i	|- ( N e. NN -> ( 0 - N ) e/ NN0 )