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

Metamath Proof Explorer

Theorem renegid2

Description: Commuted version of renegid . (Contributed by SN, 4-May-2024)

Ref Expression
Assertion renegid2 ⊢ A ∈ ℝ → 0 - ℝ A + A = 0

Proof

Step Hyp Ref Expression
1 renegid ⊢ A ∈ ℝ → A + 0 - ℝ A = 0
2 1 oveq2d ⊢ A ∈ ℝ → 0 - ℝ A + A + 0 - ℝ A = 0 - ℝ A + 0
3 rernegcl ⊢ A ∈ ℝ → 0 - ℝ A ∈ ℝ
4 readdrid ⊢ 0 - ℝ A ∈ ℝ → 0 - ℝ A + 0 = 0 - ℝ A
5 3 4 syl ⊢ A ∈ ℝ → 0 - ℝ A + 0 = 0 - ℝ A
6 2 5 eqtrd ⊢ A ∈ ℝ → 0 - ℝ A + A + 0 - ℝ A = 0 - ℝ A
7 3 recnd ⊢ A ∈ ℝ → 0 - ℝ A ∈ ℂ
8 recn ⊢ A ∈ ℝ → A ∈ ℂ
9 7 8 7 addassd ⊢ A ∈ ℝ → 0 - ℝ A + A + 0 - ℝ A = 0 - ℝ A + A + 0 - ℝ A
10 readdlid ⊢ 0 - ℝ A ∈ ℝ → 0 + 0 - ℝ A = 0 - ℝ A
11 3 10 syl ⊢ A ∈ ℝ → 0 + 0 - ℝ A = 0 - ℝ A
12 6 9 11 3eqtr4d ⊢ A ∈ ℝ → 0 - ℝ A + A + 0 - ℝ A = 0 + 0 - ℝ A
13 id ⊢ A ∈ ℝ → A ∈ ℝ
14 3 13 readdcld ⊢ A ∈ ℝ → 0 - ℝ A + A ∈ ℝ
15 elre0re ⊢ A ∈ ℝ → 0 ∈ ℝ
16 readdcan2 ⊢ 0 - ℝ A + A ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 - ℝ A ∈ ℝ → 0 - ℝ A + A + 0 - ℝ A = 0 + 0 - ℝ A ↔ 0 - ℝ A + A = 0
17 14 15 3 16 syl3anc ⊢ A ∈ ℝ → 0 - ℝ A + A + 0 - ℝ A = 0 + 0 - ℝ A ↔ 0 - ℝ A + A = 0
18 12 17 mpbid ⊢ A ∈ ℝ → 0 - ℝ A + A = 0