Theorem negelrpd

Description: The negation of a negative number is in the positive real numbers. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	negelrpd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	negelrpd.2	⊢ ( 𝜑 → 𝐴 < 0 )
Assertion	negelrpd	⊢ ( 𝜑 → - 𝐴 ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		negelrpd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		negelrpd.2	⊢ ( 𝜑 → 𝐴 < 0 )
3		negelrp	⊢ ( 𝐴 ∈ ℝ → ( - 𝐴 ∈ ℝ+ ↔ 𝐴 < 0 ) )
4	1 3	syl	⊢ ( 𝜑 → ( - 𝐴 ∈ ℝ+ ↔ 𝐴 < 0 ) )
5	2 4	mpbird	⊢ ( 𝜑 → - 𝐴 ∈ ℝ+ )