Theorem sn-ltaddpos

Description: ltaddpos without ax-mulcom . (Contributed by SN, 13-Feb-2024)

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

Proof

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