This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )