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 ) ) )