Theorem neglt

Description: The negative of a positive number is less than the number itself. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	neglt	⊢ ( 𝐴 ∈ ℝ+ → - 𝐴 < 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		rpre	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
2	1	renegcld	⊢ ( 𝐴 ∈ ℝ+ → - 𝐴 ∈ ℝ )
3		0red	⊢ ( 𝐴 ∈ ℝ+ → 0 ∈ ℝ )
4		rpgt0	⊢ ( 𝐴 ∈ ℝ+ → 0 < 𝐴 )
5	1	lt0neg2d	⊢ ( 𝐴 ∈ ℝ+ → ( 0 < 𝐴 ↔ - 𝐴 < 0 ) )
6	4 5	mpbid	⊢ ( 𝐴 ∈ ℝ+ → - 𝐴 < 0 )
7	2 3 1 6 4	lttrd	⊢ ( 𝐴 ∈ ℝ+ → - 𝐴 < 𝐴 )