Theorem nnneneg

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

	Ref	Expression
Assertion	nnneneg	⊢ ( 𝐴 ∈ ℕ → 𝐴 ≠ - 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nnne0	⊢ ( 𝐴 ∈ ℕ → 𝐴 ≠ 0 )
2	1	neneqd	⊢ ( 𝐴 ∈ ℕ → ¬ 𝐴 = 0 )
3		nncn	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
4	3	eqnegd	⊢ ( 𝐴 ∈ ℕ → ( 𝐴 = - 𝐴 ↔ 𝐴 = 0 ) )
5	2 4	mtbird	⊢ ( 𝐴 ∈ ℕ → ¬ 𝐴 = - 𝐴 )
6	5	neqned	⊢ ( 𝐴 ∈ ℕ → 𝐴 ≠ - 𝐴 )