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

Metamath Proof Explorer

Theorem renpncan3

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

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
2 rersubcl 
 |-  ( ( C e. RR /\ A e. RR ) -> ( C -R A ) e. RR )
3 2 ancoms 
 |-  ( ( A e. RR /\ C e. RR ) -> ( C -R A ) e. RR )
4 3 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C -R A ) e. RR )
5 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
6 readdsub 
 |-  ( ( A e. RR /\ ( C -R A ) e. RR /\ B e. RR ) -> ( ( A + ( C -R A ) ) -R B ) = ( ( A -R B ) + ( C -R A ) ) )
7 1 4 5 6 syl3anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + ( C -R A ) ) -R B ) = ( ( A -R B ) + ( C -R A ) ) )
8 repncan3 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A + ( C -R A ) ) = C )
9 8 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A + ( C -R A ) ) = C )
10 9 oveq1d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + ( C -R A ) ) -R B ) = ( C -R B ) )
11 7 10 eqtr3d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A -R B ) + ( C -R A ) ) = ( C -R B ) )