Theorem sn-ltaddneg

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

	Ref	Expression
Assertion	sn-ltaddneg	|- ( ( A e. RR /\ B e. RR ) -> ( A < 0 <-> ( B + A ) < B ) )

Proof

Step	Hyp	Ref	Expression
1		0re	|- 0 e. RR
2		ltadd2	|- ( ( A e. RR /\ 0 e. RR /\ B e. RR ) -> ( A < 0 <-> ( B + A ) < ( B + 0 ) ) )
3	1 2	mp3an2	|- ( ( A e. RR /\ B e. RR ) -> ( A < 0 <-> ( B + A ) < ( B + 0 ) ) )
4		readdrid	|- ( B e. RR -> ( B + 0 ) = B )
5	4	adantl	|- ( ( A e. RR /\ B e. RR ) -> ( B + 0 ) = B )
6	5	breq2d	|- ( ( A e. RR /\ B e. RR ) -> ( ( B + A ) < ( B + 0 ) <-> ( B + A ) < B ) )
7	3 6	bitrd	|- ( ( A e. RR /\ B e. RR ) -> ( A < 0 <-> ( B + A ) < B ) )