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 )