Theorem reposdif

Description: Comparison of two numbers whose difference is positive. Compare posdif . (Contributed by SN, 13-Feb-2024)

	Ref	Expression
Assertion	reposdif	|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> 0 < ( B -R A ) ) )

Proof

Step	Hyp	Ref	Expression
1		reltsub1	|- ( ( A e. RR /\ B e. RR /\ A e. RR ) -> ( A < B <-> ( A -R A ) < ( B -R A ) ) )
2	1	3anidm13	|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( A -R A ) < ( B -R A ) ) )
3		resubid	|- ( A e. RR -> ( A -R A ) = 0 )
4	3	adantr	|- ( ( A e. RR /\ B e. RR ) -> ( A -R A ) = 0 )
5	4	breq1d	|- ( ( A e. RR /\ B e. RR ) -> ( ( A -R A ) < ( B -R A ) <-> 0 < ( B -R A ) ) )
6	2 5	bitrd	|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> 0 < ( B -R A ) ) )