Theorem absdifle

Description: The absolute value of a difference and 'less than or equal to' relation. (Contributed by Paul Chapman, 18-Sep-2007)

	Ref	Expression
Assertion	absdifle	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( abs ` ( A - B ) ) <_ C <-> ( ( B - C ) <_ A /\ A <_ ( B + C ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		resubcl	|- ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )
2		absle	|- ( ( ( A - B ) e. RR /\ C e. RR ) -> ( ( abs ` ( A - B ) ) <_ C <-> ( -u C <_ ( A - B ) /\ ( A - B ) <_ C ) ) )
3	1 2	stoic3	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( abs ` ( A - B ) ) <_ C <-> ( -u C <_ ( A - B ) /\ ( A - B ) <_ C ) ) )
4		renegcl	|- ( C e. RR -> -u C e. RR )
5		leaddsub2	|- ( ( B e. RR /\ -u C e. RR /\ A e. RR ) -> ( ( B + -u C ) <_ A <-> -u C <_ ( A - B ) ) )
6	4 5	syl3an2	|- ( ( B e. RR /\ C e. RR /\ A e. RR ) -> ( ( B + -u C ) <_ A <-> -u C <_ ( A - B ) ) )
7	6	3comr	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( B + -u C ) <_ A <-> -u C <_ ( A - B ) ) )
8		recn	|- ( B e. RR -> B e. CC )
9		recn	|- ( C e. RR -> C e. CC )
10		negsub	|- ( ( B e. CC /\ C e. CC ) -> ( B + -u C ) = ( B - C ) )
11	8 9 10	syl2an	|- ( ( B e. RR /\ C e. RR ) -> ( B + -u C ) = ( B - C ) )
12	11	3adant1	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B + -u C ) = ( B - C ) )
13	12	breq1d	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( B + -u C ) <_ A <-> ( B - C ) <_ A ) )
14	7 13	bitr3d	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( -u C <_ ( A - B ) <-> ( B - C ) <_ A ) )
15		lesubadd2	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - B ) <_ C <-> A <_ ( B + C ) ) )
16	14 15	anbi12d	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( -u C <_ ( A - B ) /\ ( A - B ) <_ C ) <-> ( ( B - C ) <_ A /\ A <_ ( B + C ) ) ) )
17	3 16	bitrd	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( abs ` ( A - B ) ) <_ C <-> ( ( B - C ) <_ A /\ A <_ ( B + C ) ) ) )