Theorem resubsub4

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

	Ref	Expression
Assertion	resubsub4	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐵 ) −ℝ 𝐶 ) = ( 𝐴 −ℝ ( 𝐵 + 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		readdcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
2	1	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
3		rersubcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 −ℝ 𝐵 ) ∈ ℝ )
4	3	3adant3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 −ℝ 𝐵 ) ∈ ℝ )
5		simp3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
6		rersubcl	⊢ ( ( ( 𝐴 −ℝ 𝐵 ) ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐵 ) −ℝ 𝐶 ) ∈ ℝ )
7	4 5 6	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐵 ) −ℝ 𝐶 ) ∈ ℝ )
8		simp2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
9	8	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
10	5	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
11	7	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐵 ) −ℝ 𝐶 ) ∈ ℂ )
12	9 10 11	addassd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 + 𝐶 ) + ( ( 𝐴 −ℝ 𝐵 ) −ℝ 𝐶 ) ) = ( 𝐵 + ( 𝐶 + ( ( 𝐴 −ℝ 𝐵 ) −ℝ 𝐶 ) ) ) )
13		repncan3	⊢ ( ( 𝐶 ∈ ℝ ∧ ( 𝐴 −ℝ 𝐵 ) ∈ ℝ ) → ( 𝐶 + ( ( 𝐴 −ℝ 𝐵 ) −ℝ 𝐶 ) ) = ( 𝐴 −ℝ 𝐵 ) )
14	5 4 13	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 + ( ( 𝐴 −ℝ 𝐵 ) −ℝ 𝐶 ) ) = ( 𝐴 −ℝ 𝐵 ) )
15	14	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + ( 𝐶 + ( ( 𝐴 −ℝ 𝐵 ) −ℝ 𝐶 ) ) ) = ( 𝐵 + ( 𝐴 −ℝ 𝐵 ) ) )
16		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
17		repncan3	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 + ( 𝐴 −ℝ 𝐵 ) ) = 𝐴 )
18	8 16 17	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + ( 𝐴 −ℝ 𝐵 ) ) = 𝐴 )
19	12 15 18	3eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 + 𝐶 ) + ( ( 𝐴 −ℝ 𝐵 ) −ℝ 𝐶 ) ) = 𝐴 )
20	2 7 19	reladdrsub	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐵 ) −ℝ 𝐶 ) = ( 𝐴 −ℝ ( 𝐵 + 𝐶 ) ) )