Theorem lesub2

Description: Subtraction of both sides of 'less than or equal to'. (Contributed by NM, 29-Sep-2005) (Revised by Mario Carneiro, 27-May-2016)

	Ref	Expression
Assertion	lesub2	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <_ B <-> ( C - B ) <_ ( C - A ) ) )

Proof

Step	Hyp	Ref	Expression
1		leadd2	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <_ B <-> ( C + A ) <_ ( C + B ) ) )
2		simp3	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
3		simp1	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
4	2 3	readdcld	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C + A ) e. RR )
5		simp2	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
6		lesubadd	|- ( ( ( C + A ) e. RR /\ B e. RR /\ C e. RR ) -> ( ( ( C + A ) - B ) <_ C <-> ( C + A ) <_ ( C + B ) ) )
7	4 5 2 6	syl3anc	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( ( C + A ) - B ) <_ C <-> ( C + A ) <_ ( C + B ) ) )
8	2	recnd	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. CC )
9	3	recnd	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. CC )
10	5	recnd	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. CC )
11	8 9 10	addsubd	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C + A ) - B ) = ( ( C - B ) + A ) )
12	11	breq1d	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( ( C + A ) - B ) <_ C <-> ( ( C - B ) + A ) <_ C ) )
13	1 7 12	3bitr2d	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <_ B <-> ( ( C - B ) + A ) <_ C ) )
14	2 5	resubcld	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C - B ) e. RR )
15		leaddsub	|- ( ( ( C - B ) e. RR /\ A e. RR /\ C e. RR ) -> ( ( ( C - B ) + A ) <_ C <-> ( C - B ) <_ ( C - A ) ) )
16	14 3 2 15	syl3anc	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( ( C - B ) + A ) <_ C <-> ( C - B ) <_ ( C - A ) ) )
17	13 16	bitrd	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <_ B <-> ( C - B ) <_ ( C - A ) ) )