Metamath Proof Explorer

Theorem reltsub1

Description: Subtraction from both sides of 'less than'. Compare ltsub1 . (Contributed by SN, 13-Feb-2024)

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

Proof

Step Hyp Ref Expression
1 rersubcl 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A -R C ) e. RR )
2 1 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A -R C ) e. RR )
3 rersubcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B -R C ) e. RR )
4 3 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B -R C ) e. RR )
5 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
6 2 4 5 ltadd2d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A -R C ) < ( B -R C ) <-> ( C + ( A -R C ) ) < ( C + ( B -R C ) ) ) )
7 repncan3 
 |-  ( ( C e. RR /\ A e. RR ) -> ( C + ( A -R C ) ) = A )
8 7 ancoms 
 |-  ( ( A e. RR /\ C e. RR ) -> ( C + ( A -R C ) ) = A )
9 8 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C + ( A -R C ) ) = A )
10 repncan3 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C + ( B -R C ) ) = B )
11 10 ancoms 
 |-  ( ( B e. RR /\ C e. RR ) -> ( C + ( B -R C ) ) = B )
12 11 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C + ( B -R C ) ) = B )
13 9 12 breq12d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C + ( A -R C ) ) < ( C + ( B -R C ) ) <-> A < B ) )
14 6 13 bitr2d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B <-> ( A -R C ) < ( B -R C ) ) )