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\in \mathbb{N}\to \left(0-N\right)\notin {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2		nnel	$$⊢\neg \left(0-N\right)\notin {\mathbb{N}}_0\leftrightarrow 0-N\in {\mathbb{N}}_0$$
3		df-neg	$$⊢-N=0-N$$
4	3	eqcomi	$$⊢0-N=-N$$
5	4	eleq1i	$$⊢0-N\in {\mathbb{N}}_0\leftrightarrow -N\in {\mathbb{N}}_0$$
6		nn0ge0	$$⊢-N\in {\mathbb{N}}_0\to 0\le -N$$
7		nnre	$$⊢N\in \mathbb{N}\to N\in ℝ$$
8	7	le0neg1d	$$⊢N\in \mathbb{N}\to \left(N\le 0\leftrightarrow 0\le -N\right)$$
9		nngt0	$$⊢N\in \mathbb{N}\to 0<N$$
10		0red	$$⊢N\in \mathbb{N}\to 0\in ℝ$$
11	10 7	ltnled	$$⊢N\in \mathbb{N}\to \left(0<N\leftrightarrow \neg N\le 0\right)$$
12		pm2.21	$$⊢\neg N\le 0\to \left(N\le 0\to \neg 0\in ℝ\right)$$
13	11 12	biimtrdi	$$⊢N\in \mathbb{N}\to \left(0<N\to \left(N\le 0\to \neg 0\in ℝ\right)\right)$$
14	9 13	mpd	$$⊢N\in \mathbb{N}\to \left(N\le 0\to \neg 0\in ℝ\right)$$
15	8 14	sylbird	$$⊢N\in \mathbb{N}\to \left(0\le -N\to \neg 0\in ℝ\right)$$
16	6 15	syl5	$$⊢N\in \mathbb{N}\to \left(-N\in {\mathbb{N}}_0\to \neg 0\in ℝ\right)$$
17	5 16	biimtrid	$$⊢N\in \mathbb{N}\to \left(0-N\in {\mathbb{N}}_0\to \neg 0\in ℝ\right)$$
18	2 17	biimtrid	$$⊢N\in \mathbb{N}\to \left(\neg \left(0-N\right)\notin {\mathbb{N}}_0\to \neg 0\in ℝ\right)$$
19	1 18	mt4i	$$⊢N\in \mathbb{N}\to \left(0-N\right)\notin {\mathbb{N}}_0$$