Metamath Proof Explorer


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+A<A

Proof

Step Hyp Ref Expression
1 rpre A+A
2 1 renegcld A+A
3 0red A+0
4 rpgt0 A+0<A
5 1 lt0neg2d A+0<AA<0
6 4 5 mpbid A+A<0
7 2 3 1 6 4 lttrd A+A<A