Theorem abssubge0

Description: Absolute value of a nonnegative difference. (Contributed by NM, 14-Feb-2008)

	Ref	Expression
Assertion	abssubge0	|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( abs ` ( B - A ) ) = ( B - A ) )

Proof

Step	Hyp	Ref	Expression
1		resubcl	|- ( ( B e. RR /\ A e. RR ) -> ( B - A ) e. RR )
2	1	3adant3	|- ( ( B e. RR /\ A e. RR /\ A <_ B ) -> ( B - A ) e. RR )
3		subge0	|- ( ( B e. RR /\ A e. RR ) -> ( 0 <_ ( B - A ) <-> A <_ B ) )
4	3	biimp3ar	|- ( ( B e. RR /\ A e. RR /\ A <_ B ) -> 0 <_ ( B - A ) )
5		absid	|- ( ( ( B - A ) e. RR /\ 0 <_ ( B - A ) ) -> ( abs ` ( B - A ) ) = ( B - A ) )
6	2 4 5	syl2anc	|- ( ( B e. RR /\ A e. RR /\ A <_ B ) -> ( abs ` ( B - A ) ) = ( B - A ) )
7	6	3com12	|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( abs ` ( B - A ) ) = ( B - A ) )