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 e. RR+ -> -u A < A )

Proof

Step	Hyp	Ref	Expression
1		rpre	|- ( A e. RR+ -> A e. RR )
2	1	renegcld	|- ( A e. RR+ -> -u A e. RR )
3		0red	|- ( A e. RR+ -> 0 e. RR )
4		rpgt0	|- ( A e. RR+ -> 0 < A )
5	1	lt0neg2d	|- ( A e. RR+ -> ( 0 < A <-> -u A < 0 ) )
6	4 5	mpbid	|- ( A e. RR+ -> -u A < 0 )
7	2 3 1 6 4	lttrd	|- ( A e. RR+ -> -u A < A )