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 ( 𝐴 ∈ ℝ → ( ( 0 −ℝ 𝐴 ) + 𝐴 ) = 0 )

Proof

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