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

Metamath Proof Explorer

Theorem rennncan2

Description: Cancellation law for real subtraction. Compare nnncan2 . (Contributed by Steven Nguyen, 14-Jan-2023)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
2 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
3 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
4 rersubcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B -R C ) e. RR )
5 3 2 4 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B -R C ) e. RR )
6 resubsub4 
 |-  ( ( A e. RR /\ C e. RR /\ ( B -R C ) e. RR ) -> ( ( A -R C ) -R ( B -R C ) ) = ( A -R ( C + ( B -R C ) ) ) )
7 1 2 5 6 syl3anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A -R C ) -R ( B -R C ) ) = ( A -R ( C + ( B -R C ) ) ) )
8 repncan3 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C + ( B -R C ) ) = B )
9 2 3 8 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C + ( B -R C ) ) = B )
10 9 oveq2d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A -R ( C + ( B -R C ) ) ) = ( A -R B ) )
11 7 10 eqtrd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A -R C ) -R ( B -R C ) ) = ( A -R B ) )