Metamath Proof Explorer

Theorem reltsubadd2

Description: 'Less than' relationship between addition and subtraction. Compare ltsubadd2 . (Contributed by SN, 13-Feb-2024)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
2 readdcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B + C ) e. RR )
3 2 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B + C ) e. RR )
4 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
5 reltsub1 
 |-  ( ( A e. RR /\ ( B + C ) e. RR /\ B e. RR ) -> ( A < ( B + C ) <-> ( A -R B ) < ( ( B + C ) -R B ) ) )
6 1 3 4 5 syl3anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < ( B + C ) <-> ( A -R B ) < ( ( B + C ) -R B ) ) )
7 repncan2 
 |-  ( ( B e. RR /\ C e. RR ) -> ( ( B + C ) -R B ) = C )
8 7 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( B + C ) -R B ) = C )
9 8 breq2d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A -R B ) < ( ( B + C ) -R B ) <-> ( A -R B ) < C ) )
10 6 9 bitr2d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A -R B ) < C <-> A < ( B + C ) ) )