Metamath Proof Explorer


Theorem sn-ltaddneg

Description: ltaddneg without ax-mulcom . (Contributed by SN, 25-Jan-2025)

Ref Expression
Assertion sn-ltaddneg A B A < 0 B + A < B

Proof

Step Hyp Ref Expression
1 0re 0
2 ltadd2 A 0 B A < 0 B + A < B + 0
3 1 2 mp3an2 A B A < 0 B + A < B + 0
4 readdrid B B + 0 = B
5 4 adantl A B B + 0 = B
6 5 breq2d A B B + A < B + 0 B + A < B
7 3 6 bitrd A B A < 0 B + A < B