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 +_{𝑹} (A \cdot_{𝑹} {-1}_{𝑹}) = 0_{𝑹}$

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

Metamath Proof Explorer