Theorem sublt0d

Description: When a subtraction gives a negative result. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	sublt0d.1	|- ( ph -> A e. RR )
	sublt0d.2	|- ( ph -> B e. RR )
Assertion	sublt0d	|- ( ph -> ( ( A - B ) < 0 <-> A < B ) )

Proof

Step	Hyp	Ref	Expression
1		sublt0d.1	|- ( ph -> A e. RR )
2		sublt0d.2	|- ( ph -> B e. RR )
3		0red	|- ( ph -> 0 e. RR )
4	1 2 3	ltsubaddd	|- ( ph -> ( ( A - B ) < 0 <-> A < ( 0 + B ) ) )
5	2	recnd	|- ( ph -> B e. CC )
6	5	addid2d	|- ( ph -> ( 0 + B ) = B )
7	6	breq2d	|- ( ph -> ( A < ( 0 + B ) <-> A < B ) )
8	4 7	bitrd	|- ( ph -> ( ( A - B ) < 0 <-> A < B ) )