Theorem resubidaddlidlem

Description: Lemma for resubidaddlid . A special case of npncan . (Contributed by Steven Nguyen, 8-Jan-2023)

	Ref	Expression
Hypotheses	resubidaddridlem.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	resubidaddridlem.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	resubidaddridlem.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	resubidaddridlem.1	⊢ ( 𝜑 → ( 𝐴 −ℝ 𝐵 ) = ( 𝐵 −ℝ 𝐶 ) )
Assertion	resubidaddlidlem	⊢ ( 𝜑 → ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐵 −ℝ 𝐶 ) ) = ( 𝐴 −ℝ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		resubidaddridlem.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		resubidaddridlem.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		resubidaddridlem.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		resubidaddridlem.1	⊢ ( 𝜑 → ( 𝐴 −ℝ 𝐵 ) = ( 𝐵 −ℝ 𝐶 ) )
5		rersubcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 −ℝ 𝐵 ) ∈ ℝ )
6	1 2 5	syl2anc	⊢ ( 𝜑 → ( 𝐴 −ℝ 𝐵 ) ∈ ℝ )
7		rersubcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 −ℝ 𝐶 ) ∈ ℝ )
8	2 3 7	syl2anc	⊢ ( 𝜑 → ( 𝐵 −ℝ 𝐶 ) ∈ ℝ )
9	6 8	readdcld	⊢ ( 𝜑 → ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐵 −ℝ 𝐶 ) ) ∈ ℝ )
10	4	eqcomd	⊢ ( 𝜑 → ( 𝐵 −ℝ 𝐶 ) = ( 𝐴 −ℝ 𝐵 ) )
11	2 3 6	resubaddd	⊢ ( 𝜑 → ( ( 𝐵 −ℝ 𝐶 ) = ( 𝐴 −ℝ 𝐵 ) ↔ ( 𝐶 + ( 𝐴 −ℝ 𝐵 ) ) = 𝐵 ) )
12	10 11	mpbid	⊢ ( 𝜑 → ( 𝐶 + ( 𝐴 −ℝ 𝐵 ) ) = 𝐵 )
13	12	oveq1d	⊢ ( 𝜑 → ( ( 𝐶 + ( 𝐴 −ℝ 𝐵 ) ) + ( 𝐵 −ℝ 𝐶 ) ) = ( 𝐵 + ( 𝐵 −ℝ 𝐶 ) ) )
14	3	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
15	6	recnd	⊢ ( 𝜑 → ( 𝐴 −ℝ 𝐵 ) ∈ ℂ )
16	8	recnd	⊢ ( 𝜑 → ( 𝐵 −ℝ 𝐶 ) ∈ ℂ )
17	14 15 16	addassd	⊢ ( 𝜑 → ( ( 𝐶 + ( 𝐴 −ℝ 𝐵 ) ) + ( 𝐵 −ℝ 𝐶 ) ) = ( 𝐶 + ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐵 −ℝ 𝐶 ) ) ) )
18	1 2 8	resubaddd	⊢ ( 𝜑 → ( ( 𝐴 −ℝ 𝐵 ) = ( 𝐵 −ℝ 𝐶 ) ↔ ( 𝐵 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐴 ) )
19	4 18	mpbid	⊢ ( 𝜑 → ( 𝐵 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐴 )
20	13 17 19	3eqtr3d	⊢ ( 𝜑 → ( 𝐶 + ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐵 −ℝ 𝐶 ) ) ) = 𝐴 )
21	3 9 20	reladdrsub	⊢ ( 𝜑 → ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐵 −ℝ 𝐶 ) ) = ( 𝐴 −ℝ 𝐶 ) )