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	$$⊢A\in {ℝ}^{+}\to -A<A$$

Proof

Step	Hyp	Ref	Expression
1		rpre	$$⊢A\in {ℝ}^{+}\to A\in ℝ$$
2	1	renegcld	$$⊢A\in {ℝ}^{+}\to -A\in ℝ$$
3		0red	$$⊢A\in {ℝ}^{+}\to 0\in ℝ$$
4		rpgt0	$$⊢A\in {ℝ}^{+}\to 0<A$$
5	1	lt0neg2d	$$⊢A\in {ℝ}^{+}\to \left(0<A\leftrightarrow -A<0\right)$$
6	4 5	mpbid	$$⊢A\in {ℝ}^{+}\to -A<0$$
7	2 3 1 6 4	lttrd	$$⊢A\in {ℝ}^{+}\to -A<A$$