Metamath Proof Explorer

Theorem reppncan

Description: Cancellation law for mixed addition and real subtraction. Compare ppncan . (Contributed by SN, 3-Sep-2023)

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

Proof

Step Hyp Ref Expression
1 repnpcan 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) -R ( A + C ) ) = ( B -R C ) )
2 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
3 2 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A + B ) e. RR )
4 readdcl 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A + C ) e. RR )
5 4 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A + C ) e. RR )
6 rersubcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B -R C ) e. RR )
7 6 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B -R C ) e. RR )
8 3 5 7 resubaddd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( ( A + B ) -R ( A + C ) ) = ( B -R C ) <-> ( ( A + C ) + ( B -R C ) ) = ( A + B ) ) )
9 1 8 mpbid 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + C ) + ( B -R C ) ) = ( A + B ) )