Metamath Proof Explorer

Theorem resubcan2

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

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

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A -R C ) = ( B -R C ) ) -> ( A -R C ) = ( B -R C ) )
2 simpl1 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A -R C ) = ( B -R C ) ) -> A e. RR )
3 simpl3 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A -R C ) = ( B -R C ) ) -> C e. RR )
4 simpl2 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A -R C ) = ( B -R C ) ) -> B e. RR )
5 rersubcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B -R C ) e. RR )
6 4 3 5 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A -R C ) = ( B -R C ) ) -> ( B -R C ) e. RR )
7 2 3 6 resubaddd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A -R C ) = ( B -R C ) ) -> ( ( A -R C ) = ( B -R C ) <-> ( C + ( B -R C ) ) = A ) )
8 1 7 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A -R C ) = ( B -R C ) ) -> ( C + ( B -R C ) ) = A )
9 repncan3 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C + ( B -R C ) ) = B )
10 3 4 9 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A -R C ) = ( B -R C ) ) -> ( C + ( B -R C ) ) = B )
11 8 10 eqtr3d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A -R C ) = ( B -R C ) ) -> A = B )
12 11 ex 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A -R C ) = ( B -R C ) -> A = B ) )
13 oveq1 
 |-  ( A = B -> ( A -R C ) = ( B -R C ) )
14 12 13 impbid1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A -R C ) = ( B -R C ) <-> A = B ) )