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	$$⊢A\in 𝑹\to A{+}_{𝑹}\left(A{\cdot }_{𝑹}{-1}_{𝑹}\right)=0_{𝑹}$$

Proof

Step	Hyp	Ref	Expression
1		1idsr	$$⊢A\in 𝑹\to A{\cdot }_{𝑹}{1}_{𝑹}=A$$
2	1	oveq1d	$$⊢A\in 𝑹\to \left(A{\cdot }_{𝑹}{1}_{𝑹}\right){+}_{𝑹}\left(A{\cdot }_{𝑹}{-1}_{𝑹}\right)=A{+}_{𝑹}\left(A{\cdot }_{𝑹}{-1}_{𝑹}\right)$$
3		distrsr	$$⊢A{\cdot }_{𝑹}\left({-1}_{𝑹}{+}_{𝑹}{1}_{𝑹}\right)=\left(A{\cdot }_{𝑹}{-1}_{𝑹}\right){+}_{𝑹}\left(A{\cdot }_{𝑹}{1}_{𝑹}\right)$$
4		m1p1sr	$$⊢{-1}_{𝑹}{+}_{𝑹}{1}_{𝑹}=0_{𝑹}$$
5	4	oveq2i	$$⊢A{\cdot }_{𝑹}\left({-1}_{𝑹}{+}_{𝑹}{1}_{𝑹}\right)=A{\cdot }_{𝑹}{0}_{𝑹}$$
6		addcomsr	$$⊢\left(A{\cdot }_{𝑹}{-1}_{𝑹}\right){+}_{𝑹}\left(A{\cdot }_{𝑹}{1}_{𝑹}\right)=\left(A{\cdot }_{𝑹}{1}_{𝑹}\right){+}_{𝑹}\left(A{\cdot }_{𝑹}{-1}_{𝑹}\right)$$
7	3 5 6	3eqtr3i	$$⊢A{\cdot }_{𝑹}{0}_{𝑹}=\left(A{\cdot }_{𝑹}{1}_{𝑹}\right){+}_{𝑹}\left(A{\cdot }_{𝑹}{-1}_{𝑹}\right)$$
8		00sr	$$⊢A\in 𝑹\to A{\cdot }_{𝑹}{0}_{𝑹}=0_{𝑹}$$
9	7 8	eqtr3id	$$⊢A\in 𝑹\to \left(A{\cdot }_{𝑹}{1}_{𝑹}\right){+}_{𝑹}\left(A{\cdot }_{𝑹}{-1}_{𝑹}\right)=0_{𝑹}$$
10	2 9	eqtr3d	$$⊢A\in 𝑹\to A{+}_{𝑹}\left(A{\cdot }_{𝑹}{-1}_{𝑹}\right)=0_{𝑹}$$