Metamath Proof Explorer

Theorem renegadd

Description: Relationship between real negation and addition. (Contributed by Steven Nguyen, 7-Jan-2023)

Ref Expression
Assertion renegadd ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 - ℝ A = B ↔ A + B = 0

Proof

Step Hyp Ref Expression
1 elre0re ⊢ A ∈ ℝ → 0 ∈ ℝ
2 resubval ⊢ 0 ∈ ℝ ∧ A ∈ ℝ → 0 - ℝ A = ι x ∈ ℝ | A + x = 0
3 1 2 mpancom ⊢ A ∈ ℝ → 0 - ℝ A = ι x ∈ ℝ | A + x = 0
4 3 eqeq1d ⊢ A ∈ ℝ → 0 - ℝ A = B ↔ ι x ∈ ℝ | A + x = 0 = B
5 4 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 - ℝ A = B ↔ ι x ∈ ℝ | A + x = 0 = B
6 renegeu ⊢ A ∈ ℝ → ∃! x ∈ ℝ A + x = 0
7 oveq2 ⊢ x = B → A + x = A + B
8 7 eqeq1d ⊢ x = B → A + x = 0 ↔ A + B = 0
9 8 riota2 ⊢ B ∈ ℝ ∧ ∃! x ∈ ℝ A + x = 0 → A + B = 0 ↔ ι x ∈ ℝ | A + x = 0 = B
10 6 9 sylan2 ⊢ B ∈ ℝ ∧ A ∈ ℝ → A + B = 0 ↔ ι x ∈ ℝ | A + x = 0 = B
11 10 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B = 0 ↔ ι x ∈ ℝ | A + x = 0 = B
12 5 11 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 - ℝ A = B ↔ A + B = 0