Theorem pn0sr

Description: A signed real plus its negative is zero. (Contributed by NM, 14-May-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	pn0sr	⊢ ( 𝐴 ∈ R → ( 𝐴 +R ( 𝐴 ·R -1R ) ) = 0R )

Proof

Step	Hyp	Ref	Expression
1		1idsr	⊢ ( 𝐴 ∈ R → ( 𝐴 ·R 1R ) = 𝐴 )
2	1	oveq1d	⊢ ( 𝐴 ∈ R → ( ( 𝐴 ·R 1R ) +R ( 𝐴 ·R -1R ) ) = ( 𝐴 +R ( 𝐴 ·R -1R ) ) )
3		distrsr	⊢ ( 𝐴 ·R ( -1R +R 1R ) ) = ( ( 𝐴 ·R -1R ) +R ( 𝐴 ·R 1R ) )
4		m1p1sr	⊢ ( -1R +R 1R ) = 0R
5	4	oveq2i	⊢ ( 𝐴 ·R ( -1R +R 1R ) ) = ( 𝐴 ·R 0R )
6		addcomsr	⊢ ( ( 𝐴 ·R -1R ) +R ( 𝐴 ·R 1R ) ) = ( ( 𝐴 ·R 1R ) +R ( 𝐴 ·R -1R ) )
7	3 5 6	3eqtr3i	⊢ ( 𝐴 ·R 0R ) = ( ( 𝐴 ·R 1R ) +R ( 𝐴 ·R -1R ) )
8		00sr	⊢ ( 𝐴 ∈ R → ( 𝐴 ·R 0R ) = 0R )
9	7 8	eqtr3id	⊢ ( 𝐴 ∈ R → ( ( 𝐴 ·R 1R ) +R ( 𝐴 ·R -1R ) ) = 0R )
10	2 9	eqtr3d	⊢ ( 𝐴 ∈ R → ( 𝐴 +R ( 𝐴 ·R -1R ) ) = 0R )