Theorem nnneneg

Description: No positive integer is equal to its negation. (Contributed by AV, 20-Jun-2023)

	Ref	Expression
Assertion	nnneneg	$$⊢A\in \mathbb{N}\to A\ne -A$$

Proof

Step	Hyp	Ref	Expression
1		nnne0	$$⊢A\in \mathbb{N}\to A\ne 0$$
2	1	neneqd	$$⊢A\in \mathbb{N}\to \neg A=0$$
3		nncn	$$⊢A\in \mathbb{N}\to A\in ℂ$$
4	3	eqnegd	$$⊢A\in \mathbb{N}\to \left(A=-A\leftrightarrow A=0\right)$$
5	2 4	mtbird	$$⊢A\in \mathbb{N}\to \neg A=-A$$
6	5	neqned	$$⊢A\in \mathbb{N}\to A\ne -A$$