Metamath Proof Explorer

Theorem ltaddsublt

Description: Addition and subtraction on one side of 'less than'. (Contributed by AV, 24-Nov-2018)

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

Proof

Step Hyp Ref Expression
1 ltadd2 
 |-  ( ( B e. RR /\ C e. RR /\ A e. RR ) -> ( B < C <-> ( A + B ) < ( A + C ) ) )
2 1 3comr 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B < C <-> ( A + B ) < ( A + C ) ) )
3 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
4 3 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A + B ) e. RR )
5 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
6 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
7 4 5 6 ltsubaddd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( ( A + B ) - C ) < A <-> ( A + B ) < ( A + C ) ) )
8 2 7 bitr4d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B < C <-> ( ( A + B ) - C ) < A ) )