This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resubcan2

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

Ref Expression
Assertion resubcan2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ C = B - ℝ C ↔ A = B

Proof

Step Hyp Ref Expression
1 simpr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A - ℝ C = B - ℝ C → A - ℝ C = B - ℝ C
2 simpl1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A - ℝ C = B - ℝ C → A ∈ ℝ
3 simpl3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A - ℝ C = B - ℝ C → C ∈ ℝ
4 simpl2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A - ℝ C = B - ℝ C → B ∈ ℝ
5 rersubcl ⊢ B ∈ ℝ ∧ C ∈ ℝ → B - ℝ C ∈ ℝ
6 4 3 5 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A - ℝ C = B - ℝ C → B - ℝ C ∈ ℝ
7 2 3 6 resubaddd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A - ℝ C = B - ℝ C → A - ℝ C = B - ℝ C ↔ C + B - ℝ C = A
8 1 7 mpbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A - ℝ C = B - ℝ C → C + B - ℝ C = A
9 repncan3 ⊢ C ∈ ℝ ∧ B ∈ ℝ → C + B - ℝ C = B
10 3 4 9 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A - ℝ C = B - ℝ C → C + B - ℝ C = B
11 8 10 eqtr3d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ A - ℝ C = B - ℝ C → A = B
12 11 ex ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ C = B - ℝ C → A = B
13 oveq1 ⊢ A = B → A - ℝ C = B - ℝ C
14 12 13 impbid1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ C = B - ℝ C ↔ A = B