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

Metamath Proof Explorer

Theorem resubsub4

Description: Law for double subtraction. Compare subsub4 . (Contributed by Steven Nguyen, 14-Jan-2023)

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

Proof

Step Hyp Ref Expression
1 readdcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B + C ) e. RR )
2 1 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B + C ) e. RR )
3 rersubcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A -R B ) e. RR )
4 3 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A -R B ) e. RR )
5 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
6 rersubcl 
 |-  ( ( ( A -R B ) e. RR /\ C e. RR ) -> ( ( A -R B ) -R C ) e. RR )
7 4 5 6 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A -R B ) -R C ) e. RR )
8 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
9 8 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. CC )
10 5 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. CC )
11 7 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A -R B ) -R C ) e. CC )
12 9 10 11 addassd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( B + C ) + ( ( A -R B ) -R C ) ) = ( B + ( C + ( ( A -R B ) -R C ) ) ) )
13 repncan3 
 |-  ( ( C e. RR /\ ( A -R B ) e. RR ) -> ( C + ( ( A -R B ) -R C ) ) = ( A -R B ) )
14 5 4 13 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C + ( ( A -R B ) -R C ) ) = ( A -R B ) )
15 14 oveq2d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B + ( C + ( ( A -R B ) -R C ) ) ) = ( B + ( A -R B ) ) )
16 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
17 repncan3 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B + ( A -R B ) ) = A )
18 8 16 17 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B + ( A -R B ) ) = A )
19 12 15 18 3eqtrd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( B + C ) + ( ( A -R B ) -R C ) ) = A )
20 2 7 19 reladdrsub 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A -R B ) -R C ) = ( A -R ( B + C ) ) )