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

Metamath Proof Explorer

Theorem resubadd

Description: Relation between real subtraction and addition. Based on subadd . (Contributed by Steven Nguyen, 7-Jan-2023)

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

Proof

Step Hyp Ref Expression
1 resubval ⊢ A ∈ ℝ ∧ B ∈ ℝ → A - ℝ B = ι x ∈ ℝ | B + x = A
2 1 eqeq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A - ℝ B = C ↔ ι x ∈ ℝ | B + x = A = C
3 2 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ B = C ↔ ι x ∈ ℝ | B + x = A = C
4 resubeu ⊢ B ∈ ℝ ∧ A ∈ ℝ → ∃! x ∈ ℝ B + x = A
5 oveq2 ⊢ x = C → B + x = B + C
6 5 eqeq1d ⊢ x = C → B + x = A ↔ B + C = A
7 6 riota2 ⊢ C ∈ ℝ ∧ ∃! x ∈ ℝ B + x = A → B + C = A ↔ ι x ∈ ℝ | B + x = A = C
8 4 7 sylan2 ⊢ C ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ → B + C = A ↔ ι x ∈ ℝ | B + x = A = C
9 8 3impb ⊢ C ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ → B + C = A ↔ ι x ∈ ℝ | B + x = A = C
10 9 3com13 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + C = A ↔ ι x ∈ ℝ | B + x = A = C
11 3 10 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ B = C ↔ B + C = A