Theorem renpncan3

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

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

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
2		rersubcl	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐶 −ℝ 𝐴 ) ∈ ℝ )
3	2	ancoms	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 −ℝ 𝐴 ) ∈ ℝ )
4	3	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 −ℝ 𝐴 ) ∈ ℝ )
5		simp2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
6		readdsub	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 −ℝ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + ( 𝐶 −ℝ 𝐴 ) ) −ℝ 𝐵 ) = ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐶 −ℝ 𝐴 ) ) )
7	1 4 5 6	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + ( 𝐶 −ℝ 𝐴 ) ) −ℝ 𝐵 ) = ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐶 −ℝ 𝐴 ) ) )
8		repncan3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + ( 𝐶 −ℝ 𝐴 ) ) = 𝐶 )
9	8	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + ( 𝐶 −ℝ 𝐴 ) ) = 𝐶 )
10	9	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + ( 𝐶 −ℝ 𝐴 ) ) −ℝ 𝐵 ) = ( 𝐶 −ℝ 𝐵 ) )
11	7 10	eqtr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐵 ) + ( 𝐶 −ℝ 𝐴 ) ) = ( 𝐶 −ℝ 𝐵 ) )