Theorem resubcan2

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

	Ref	Expression
Assertion	resubcan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) )
2		simpl1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → 𝐴 ∈ ℝ )
3		simpl3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → 𝐶 ∈ ℝ )
4		simpl2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → 𝐵 ∈ ℝ )
5		rersubcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 −ℝ 𝐶 ) ∈ ℝ )
6	4 3 5	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → ( 𝐵 −ℝ 𝐶 ) ∈ ℝ )
7	2 3 6	resubaddd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → ( ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ↔ ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐴 ) )
8	1 7	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐴 )
9		repncan3	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐵 )
10	3 4 9	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐵 )
11	8 10	eqtr3d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ) → 𝐴 = 𝐵 )
12	11	ex	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) → 𝐴 = 𝐵 ) )
13		oveq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) )
14	12 13	impbid1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) ↔ 𝐴 = 𝐵 ) )